{A B} n (f:A -> B) `{!forall x y, IsTruncMap n (@ap _ _ f x y)} : IsTruncMap n.+1 f. Proof. intro y; apply istrunc_S. intros [a p] [b q]; destruct q; exact (istrunc_equiv_istrunc _ (hfiber_ap p)). Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.