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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Pushouts.