English
There is a type-level equivalence between sections of a functor F : C ⥤ Type and morphisms from the constant functor on X to F, namely F.sections ≃ (const_C X ⟶ F), provided a chosen X with Unique X.
Русский
Существует тип-эквивалент между секциями функторa F : C ⥤ Type и морфизмами из константного функторa на X к F, то есть F.sections ≃ (const_C X ⟶ F), при заданном X с Unique X.
LaTeX
$$$$ F. ext{sections} \simeq (\mathrm{const}_C X \to F) $$$$
Lean4
/-- A type-level equivalence between sections of a functor and morphisms from a terminal functor
to it. We use the constant functor on a given singleton type here as a specific choice of terminal
functor. -/
@[simps apply_app]
def sectionsEquivHom (F : C ⥤ Type u₂) (X : Type u₂) [Unique X] : F.sections ≃ ((const _).obj X ⟶ F)
where
toFun
s :=
{ app j x := s.1 j
naturality _ _ _ := by ext x; simp }
invFun τ := ⟨fun j ↦ τ.app _ (default : X), fun φ ↦ (congr_fun (τ.naturality φ) _).symm⟩
right_inv
τ := by
ext _ (x : X)
rw [Unique.eq_default x]
