proposition: Proposition isembedding_pi_psect {n : nat} {X Y : pType} (s : X ->* Y) (r : Y ->* X) (k : r o* s ==* pmap_idmap) : IsEmbedding (fmap (pPi n) s).
proof: Proof. apply isembedding_isinj_hset. rapply (isinj_section (r:=fmap (pPi n) r)). intro x. lhs_V rapply (fmap_comp (pPi n) s r x). lhs rapply (fmap2 (pPi n) k x). exact (fmap_id (pPi n) X x). Defined.
imports: Basics Types Pointed HSet Modalities.Modality Truncations.Core Truncations.SeparatedTrunc Algebra.AbGroups WildCat