Theorem fibseqstrtohfsqstr {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (hf : fibseqstr f g z) : hfsqstr (λ t : unit, z) g (λ x : X, tt) f. Proof. intros. split with (pr1 hf). set (ff := ezweq f g z hf). set (ggff := commsqZtohfp (λ t : unit, z) g (λ x : X, tt) f (pr1 hf)). set (gg := weqhfibertohfp g z). apply (pr2 (weqcomp ff gg)). Defined.