hasPullbacks_of_hasWidePullbacks — Mathlib

English

If a category D has wide pullbacks, then it has binary pullbacks.

Русский

Если в категории D существуют широкие pullbacks, то существуют бинарные pullbacks.

LaTeX

$$$$ \text{HasWidePullbacks}(D) \Rightarrow \text{HasPullbacks}(D). $$$$

Lean4

/-- Having wide pullback at any universe level implies having binary pullbacks. -/
instance (priority := 100) hasPullbacks_of_hasWidePullbacks (D : Type u) [Category.{v} D] [HasWidePullbacks.{w} D] :
    HasPullbacks.{v, u} D :=
  hasWidePullbacks_shrink WalkingPair

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