equivPullbackObj — Mathlib

English

For a pullback cone c with IsLimit hc, there is a natural equivalence between its cone point and the explicit pullback object Types.PullbackObj f g.

Русский

Для конуса предельного типа c с IsLimit hc существует естественное эквивалество между точкой конуса и явным объектом pullback в типах Types.PullbackObj f g.

LaTeX

$$$c.pt \\simeq Types.PullbackObj\ f\ g$ (via IsLimit.conePointUniqueUpToIso hc (Types.pullbackLimitCone f g).isLimit).toEquiv$$

Lean4

/-- A limit pullback cone in the category of types identifies to the explicit pullback. -/
noncomputable def equivPullbackObj : c.pt ≃ Types.PullbackObj f g :=
  (IsLimit.conePointUniqueUpToIso hc (Types.pullbackLimitCone f g).isLimit).toEquiv

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