fact: Definition equiv_istruncmap_ap `{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).
imports: Basics Types Diagrams.CommutativeSquares HSet