Lemma carrier_subtype_to_contained_subtype_to_carrier_subtype (B : hsubtype A) : contained_subtype_to_carrier_subtype (carrier_subtype_to_contained_subtype B) = B. Proof. apply funextfun. intro x. apply hPropUnivalence. - intro H. refine (transportf B _ (pr2 H)). now apply carrier_eq. - intro H. exists (pr2 x). refine (transportf B _ H). now apply carrier_eq. Qed.