Lemma PushoutEndo_is_identity {a b c : C} {f : C⟦a, b⟧} {g : C⟦a, c⟧} (Po : Pushout f g) (k : C⟦colim Po , colim Po⟧) (kH1 : PushoutIn1 Po · k = PushoutIn1 Po) (kH2 : PushoutIn2 Po · k = PushoutIn2 Po) : identity (colim Po) = k. Proof. apply colim_endo_is_identity. use three_rec_dep; cbn. - unfold colimIn. set (T := (coconeInCommutes (colimCocone Po) One Three tt)). use (pathscomp0 (! (maponpaths (λ h' : _, h' · k) T))). use (pathscomp0 _ (coconeInCommutes (colimCocone Po) One Three tt)). rewrite <- assoc. apply cancel_precomposition. apply kH2. - apply kH1. - apply kH2. 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.