Proposition el_pullback_set_pr2 {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) = x. Proof. pose (P := make_Pullback _ Hp). use (eqtohomot (PullbackArrow_PullbackPr2 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.