{A B C} (f : B -> A) (g : C -> A) (x y : Pullback f g) : { p : x.1 = y.1 & { q : x.2.1 = y.2.1 & PathSquare (ap f p) (ap g q) x.2.2 y.2.2 } } <~> (x = y). Proof. revert y; rapply equiv_path_from_contr. { exists idpath. exists idpath. cbn. apply sq_refl_v. } destruct x as [b [c p]]; unfold Pullback; cbn. contr_sigsig b (idpath b). contr_sigsig c (idpath c). cbn. rapply (contr_equiv' {p' : f b = g c & p = p'}). apply equiv_functor_sigma_id; intros p'. apply sq_1G. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.