{A B C : Type} `{IsHSet B} {f : A -> B} {g : B -> C} `{IsEmbedding (g o f)} : IsEmbedding f. Proof. rapply isembedding_isinj_hset. rapply (isinj_cancelL _ g). Defined.
Require Import Basics. Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.