proposition: Lemma isPullback_two_pullback (b' d' : C) (h' : C⟦d', b'⟧) (i : C⟦b', b⟧) (i' : C⟦d', d⟧) (Hinner : h · f = k · g) (Hinnerpb : isPullback Hinner) (Hleft : h' · i = i' · h) (Houterpb : isPullback (glueSquares Hinner Hleft )) : isPullback Hleft.
proof: Proof. apply make_isPullback. intros e x y Hxy. use tpair. - use tpair. use (PullbackArrow (make_Pullback _ Houterpb)). + apply x. + apply (y · k). + abstract (rewrite assoc; rewrite Hxy; repeat rewrite <- assoc; rewrite Hinner; apply idpath). + abstract ( split ; [ apply (PullbackArrow_PullbackPr1 (make_Pullback _ Houterpb)) | idtac ]; apply (MorphismsIntoPullbackEqual Hinnerpb); [rewrite <- assoc; match goal with |[ |- ?KK · ( _ · _ ) = _ ] => intermediate_path (KK · (h' · i)) end; [ apply maponpaths; apply (!Hleft) | rewrite assoc; assert (T:= PullbackArrow_PullbackPr1 (make_Pullback _ Houterpb)); cbn in T; rewrite T; apply Hxy ] | idtac ] ; assert (T:= PullbackArrow_PullbackPr2 (make_Pullback _ Houterpb)); cbn in T; rewrite <- assoc, T; apply idpath ). - abstract ( intro t; apply subtypePath; [ intro; apply isapropdirprod; apply C | simpl; apply PullbackArrowUnique; [ apply (pr1 (pr2 t)) | cbn; rewrite assoc; rewrite (pr2 (pr2 t)); apply idpath ]] ). 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