Definition equiv_Pullback_1 {a b c : C} (f : C⟦b, a⟧) (g : C⟦c, a⟧) : Limits.Pullbacks.Pullback f g -> Pullback f g. Proof. intros X. exact (make_Pullback f g (Limits.Pullbacks.PullbackObject X) (Limits.Pullbacks.PullbackPr1 X) (Limits.Pullbacks.PullbackPr2 X) (Limits.Pullbacks.PullbackSqrCommutes X) (equiv_isPullback_1 _ _ _ _ _ (Limits.Pullbacks.isPullback_Pullback 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.