proposition: Lemma isBinProduct_Pullback (c d : C): isBinProduct C c d (PullbackObject (Pb _ _ _ (TerminalArrow T c) (TerminalArrow T d))) (PullbackPr1 _ ) (PullbackPr2 _ ).
proof: Proof. intros a f g. exists (UnivProductFromPullback c d a f g). intro t. abstract (apply proofirrelevancecontr, isPullback_Pullback, TerminalArrowEq). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Monics