Definition identity_isPullback {C : category} {x y : C} {f g : x --> y} {ix : x --> x} {iy : y --> y} (p : f · iy = ix · g) (q₁ : f = g) (q₂ : ix = identity _) (q₃ : iy = identity _) : isPullback p. Proof. intros w h k r. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ; refine (!(id_right _) @ _) ; rewrite <- q₂ ; refine (pr22 φ₁ @ !(pr22 φ₂) @ _) ; rewrite q₂ ; apply id_right). - simple refine (k ,, _ ,, _). + abstract (rewrite q₁ ; rewrite <- r ; rewrite q₃ ; apply id_right). + abstract (cbn ; rewrite q₂ ; apply id_right). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Monics. Definition UnivProductFromPullback (c d a : C) (f : a --> c) (g : a --> d): exists (UnivProductFromPullback c d a f g). Definition BinProductsFromPullbacks : BinProducts C := BinProduct_Pullback.