Definition equiv_Pushout1 {a b c : C} (f : C⟦a, b⟧) (g : C⟦a, c⟧) : Limits.Pushouts.Pushout f g -> Pushout C f g. Proof. intros X. exact (make_Pushout C f g X (Limits.Pushouts.PushoutIn1 X) (Limits.Pushouts.PushoutIn2 X) (Limits.Pushouts.PushoutSqrCommutes X) (equiv_isPushout1 _ _ _ _ _ (Limits.Pushouts.isPushout_Pushout X))). Defined.
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.