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. 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.
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.