instHasPairwisePullbacksOfHasPullbacks

English

If HasPullbacks holds in the ambient category, then every presieve has pairwise pullbacks.

Русский

Если в исходной категории существуют pullbacks, то каждая предсистема имеет попарные pullbacks.

LaTeX

$$$\\forall R:\\mathrm{Presieve}(X),\\ if\\ HasPullbacks(C)\\ then\\ R.HasPairwisePullbacks$$$

Lean4

instance (R : Presieve X) [HasPullbacks C] : R.HasPairwisePullbacks :=
  ⟨fun _ _ ↦ inferInstance⟩

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