Definition commsqZtohfphomot {X X' Y Z : UU} (f : X -> Y) (f' : X' -> Y) (g : Z -> X) (g' : Z -> X') (h : commsqstr g' f' g f) : ∏ z : Z, (hfpg _ _ (commsqZtohfp _ _ _ _ h z)) = (g z) := λ z : _, idpath _.