`{Funext} {A B} n (f:A -> B) : IsTruncMap n.+1 f <~> (forall x y, IsTruncMap n (@ap _ _ f x y)) := equiv_iff_hprop (@istruncmap_ap _ _ n f) (@istruncmap_from_ap _ _ n f). Global Instance isequiv_ap_isembedding {A B} (f : A -> B) `{!IsEmbedding f} : forall x y, IsEquiv (@ap _ _ f x y). Proof. intros x y. apply isequiv_contr_map,_. Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.