Theorem transposhfpsqstr {X X' Y Z : UU} (f : X -> Y) (f' : X' -> Y) (g : Z -> X) (g' : Z -> X') (hf : hfsqstr f f' g g') : hfsqstr f' f g' g. Proof. intros. set (is := pr2 hf). set (h := pr1 hf). set (th := transposcommsqstr f f' g g' h). split with th. set (w1 := weqhfpcomm f f'). assert (h1 : ∏ z : Z, (w1 (commsqZtohfp f f' g g' h z)) = (commsqZtohfp f' f g' g th z)). intro. unfold commsqZtohfp. simpl. unfold fpmap. unfold totalfun. simpl. apply idpath. apply (isweqhomot _ _ h1). apply (twooutof3c _ _ is (pr2 w1)). Defined.