Lemma carrier_subtype_contained_iff_contained_subtype_contained (B B' : hsubtype A) : B ⊆ B' ≃ carrier_subtype_weq_contained_subtype B ⊆ carrier_subtype_weq_contained_subtype B'. Proof. refine (weqiff _ (propproperty _) (propproperty _)). split. - intros H x Hx. pose (f := invmap (carrier_subtype_carrier_weq_contained_subtype_carrier B)). pose (g := subtype_inc H). pose (h := carrier_subtype_carrier_weq_contained_subtype_carrier B'). exact ((pr2 ∘ h ∘ g ∘ f)%functions (x ,, Hx)). - intros H x Hx. pose (f := carrier_subtype_carrier_weq_contained_subtype_carrier B). pose (g := subtype_inc H). pose (h := invmap (carrier_subtype_carrier_weq_contained_subtype_carrier B')). refine (transportf B' _ ((pr2 ∘ h ∘ g ∘ f)%functions (x ,, Hx))). now apply carrier_eq. Qed.