proposition: Lemma equiv_path_pullback_rec_hset `{Funext} {A X Y Z : Type} `{IsHSet Z} (f : X -> Z) (g : Y -> Z) (phi psi : A -> Pullback f g) : ((pullback_pr1 o phi == pullback_pr1 o psi) * (pullback_pr2 o phi == pullback_pr2 o psi)) <~> (phi == psi).
proof: Proof. refine (_ oE equiv_prod_coind _ _). srapply equiv_functor_forall_id; intro a; cbn. apply equiv_path_pullback_hset. Defined.
imports: HoTT.Basics HoTT.Types HFiber PathAny Cubical.PathSquare Diagrams.CommutativeSquares