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