`{Funext} {A B} (f : A -> B) : IsEmbedding f <~> (forall x y, IsEquiv (@ap _ _ f x y)). Proof. exact (equiv_iff_hprop (@isequiv_ap_isembedding _ _ f) (@isembedding_isequiv_ap _ _ f)). Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.