Lemma subtype_equal_cond {X:UU} (S T : hsubtype X) : S ⊆ T ∧ T ⊆ S ⇔ S ≡ T. Proof. split. - intros c x. induction c as [st ts]. split. + intro s. exact (st x s). + intro t. exact (ts x t). - intro e. split. + intros x s. exact (pr1 (e x) s). + intros x t. exact (pr2 (e x) t). Defined.