Definition carrier_subtype_weq_contained_subtype : hsubtype A ≃ contained_subtype A := weq_iso carrier_subtype_to_contained_subtype contained_subtype_to_carrier_subtype carrier_subtype_to_contained_subtype_to_carrier_subtype contained_subtype_to_carrier_subtype_to_contained_subtype.