fact: Definition pullback_commsq {A B C} (f : B -> A) (g : C -> A) : f o pullback_pr1 == g o pullback_pr2 := (fun z => z.2.2).
imports: HoTT.Basics HoTT.Types HFiber PathAny Cubical.PathSquare Diagrams.CommutativeSquares