punitIso — Mathlib

English

The identity functor on Type is isomorphic to the coyoneda functor at Opposite(PUnit).

Русский

Тождественный функтор на Type изоморфен функтору coyoneda на Opposite(PUnit).

LaTeX

$$$\mathrm{coyoneda}(\mathrm{op}(\mathrm{PUnit})) \cong \mathrm{Id}_{\mathrm{Type}}$$$

Lean4

/-- The identity functor on `Type` is isomorphic to the coyoneda functor coming from `PUnit`. -/
def punitIso : coyoneda.obj (Opposite.op PUnit) ≅ 𝟭 (Type v₁) :=
  NatIso.ofComponents fun X =>
    { hom := fun f => f ⟨⟩
      inv := fun x _ => x }

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