{A B C} (f : B -> A) (g : C -> A) : Pullback f g <~> Pullback g f. Proof. refine (_ oE equiv_sigma_symm (fun b c => f b = g c)). apply equiv_functor_sigma_id; intros c. apply equiv_functor_sigma_id; intros b. apply equiv_path_inverse. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.