Definition el_pullback_set {X₁ X₂ Y₁ Y₂ : hSet} {f₁ : Y₁ → Y₂} {f₂ : X₂ → Y₂} {g₁ : X₁ → X₂} {g₂ : X₁ → Y₁} {p : (λ x, f₁(g₂ x)) = (λ x, f₂(g₁ x))} (Hp : isPullback (C := SET) p) (y : Y₁) (x : X₂) (q : f₁ y = f₂ x) : X₁. Proof. pose (P := make_Pullback _ Hp). simple refine (PullbackArrow P unitset _ _ _ tt). - exact (λ _, y). - exact (λ _, x). - abstract (use funextsec ; intro ; exact q). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.WeakEquivalences. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Equalizers. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Categories.HSET.Core.