instHasLimitObjFunctorConstTerminal

English

There is a limit for constant functors valued in the terminal object, under HasTerminal.

Русский

Существование предела для константных функторов в терминиальном объекте при условии HasTerminal.

LaTeX

$$$\\text{HasLimit}((\\mathrm{Functor.const}\\ J) (\\top_C))$$$

Lean4

instance {J : Type*} [Category J] {C : Type*} [Category C] [HasTerminal C] :
    HasLimit ((CategoryTheory.Functor.const J).obj (⊤_ C)) :=
  HasLimit.mk
    { cone :=
        { pt := ⊤_ C
          π := { app := fun _ => terminal.from _ } }
      isLimit := { lift := fun _ => terminal.from _ } }

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