proposition: Lemma PushoutArrowUnique' {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) (P : isPushout f g i1 i2 H) e (h : C⟦b, e⟧) (k : C⟦c, e⟧) (Hcomm : f · h = g · k) (w : C⟦d, e⟧) (H1 : i1 · w = h) (H2 : i2 · w = k) : w = (pr1 (pr1 (P e (PushoutCocone f g _ h k Hcomm)))).
proof: Proof. apply path_to_ctr. use three_rec_dep; try assumption; simpl. change (three_rec_dep (λ n, C⟦three_rec a b c n, d⟧) _ _ _ _) with (f · i1). change (three_rec_dep (λ n, C⟦three_rec a b c n, e⟧) _ _ _ _) with (f · h). now rewrite <- assoc, H1. 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