instHasTerminal — Mathlib

English

The equality of projections in a homDiagram holds compatibly with eqToHom under a given equality of limits.

Русский

Согласованность проекции в гом Diagram с eqToHom при заданном равенстве предела.

LaTeX

$$$$\\text{For } X,Y \\text{ in } \\lim( F\\!\\downarrow\\mathrm{Cat.objects} ),\\; \\pi_j(\\mathrm{homDiagram}\\,X,Y)\\big(\\mathrm{eqToHom}(h)\\big) = \\mathrm{eqToHom}(\\mathrm{congrArg}( \\pi_j(\\,F\\!\\downarrow\\mathrm{Cat.objects}\\,) )(h)).$$$$

Lean4

instance : HasTerminal Cat.{v, u} :=
  by
  have : IsDiscrete (ShrinkHoms.{u} PUnit.{u + 1}) :=
    { subsingleton _ _ := { allEq _ _ := eq_of_comp_right_eq (congrFun rfl) }
      eq_of_hom _ := rfl }
  exact IsTerminal.hasTerminal (X := Cat.of (ShrinkHoms PUnit)) isTerminalOfUniqueOfIsDiscrete

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