proposition: Lemma equiv_isPushout1 {a b c d : C} (f : C ⟦a, b⟧) (g : C ⟦a, c⟧) (i1 : C⟦b, d⟧) (i2 : C⟦c, d⟧) (H : f · i1 = g · i2) : Limits.Pushouts.isPushout f g i1 i2 H -> isPushout C f g i1 i2 H.
proof: Proof. intros X R cc. set (XR := Limits.Pushouts.make_Pushout f g d i1 i2 H X). use unique_exists. + use (Limits.Pushouts.PushoutArrow XR). - exact (coconeIn cc Two). - exact (coconeIn cc Three). - use (pathscomp0 ((coconeInCommutes cc One Two tt))). apply (!(coconeInCommutes cc One Three tt)). + use three_rec_dep; simpl. - change (three_rec_dep (λ n, C⟦three_rec a b c n, d⟧) _ _ _ _) with (f · i1). rewrite <- assoc, (Limits.Pushouts.PushoutArrow_PushoutIn1 XR). apply (coconeInCommutes cc One Two tt). - apply (Limits.Pushouts.PushoutArrow_PushoutIn1 XR). - apply (Limits.Pushouts.PushoutArrow_PushoutIn2 XR). + intros y; apply impred_isaprop; intros t; apply C. + intros y T. use Limits.Pushouts.PushoutArrowUnique. - apply (T Two). - apply (T Three). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Pushouts