{n : nat} {X Y : pType} (s : X ->* Y) (r : Y ->* X) (k : r o* s ==* pmap_idmap) : IsEmbedding (fmap (pPi n) s). 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.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.