equivFunctorToCodiscrete — Mathlib

English

There is an equivalence between functions C → A and functors C ⥤ Codiscrete A.

Русский

Существует эквивалентность между функциями C → A и функторaми C ⥤ Codiscrete A.

LaTeX

$$$ (C \to A) \simeq (C \to \mathrm{Codiscrete} A) $$$

Lean4

/-- For a category `C` and type `A`, there is an equivalence between functions `objects.obj C ⟶ A`
and functors `C ⥤ Codiscrete A`. -/
def equivFunctorToCodiscrete {C : Type u} [Category.{v} C] {A : Type w} : (C → A) ≃ (C ⥤ Codiscrete A)
    where
  toFun := functor
  invFun := invFunctor

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