{A B C} `{IsHSet A} (f : B -> A) (g : C -> A) (x y : Pullback f g) : (x.1 = y.1) * (x.2.1 = y.2.1) <~> (x = y). Proof. refine (equiv_path_pullback f g x y oE _^-1%equiv). refine (_ oE equiv_sigma_prod (fun pq => PathSquare (ap f (fst pq)) (ap g (snd pq)) (x.2).2 (y.2).2)). rapply equiv_sigma_contr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.