fromChosenTerminalEquiv — Mathlib

English

There is an equivalence between functors from the chosen terminal category to C and objects of C.

Русский

Существует эквиваленция между функторaми из выбранной терминальной категории в C и объектами категории C.

LaTeX

$$$$\mathrm{Fun}(\mathrm{Cat.chosenTerminal}, C) \simeq C.$$$$

Lean4

/-- The type of functors out of the chosen terminal category is equivalent to the type of objects
in the target category. TODO: upgrade to an equivalence of categories. -/
def fromChosenTerminalEquiv {C : Type u} [Category.{v} C] : Cat.chosenTerminal ⥤ C ≃ C
    where
  toFun F := F.obj ⟨⟨()⟩⟩
  invFun := (Functor.const _).obj
  left_inv
    _ := by
    apply Functor.ext
    · rintro ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟨⟩⟩⟩⟩
      simp only [eqToHom_refl, Category.comp_id, Category.id_comp]
      exact (Functor.map_id _ _).symm
    · intro; rfl
  right_inv _ := rfl

Похожие утверждения