Proposition el_pullback_set_pr1 {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) : g₂ (el_pullback_set Hp y x q) = y. Proof. pose (P := make_Pullback _ Hp). use (eqtohomot (PullbackArrow_PullbackPr1 P _ _ _ _)). Qed.
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.