fact: Definition path_hfiber_uncurried {A B : Type} {f : A -> B} {y : B} {x1 x2 : hfiber f y} : { q : x1.1 = x2.1 & x1.2 = ap f q @ x2.2 } -> (x1 = x2) := equiv_path_hfiber x1 x2.
imports: Basics Types Diagrams.CommutativeSquares HSet