Lemma weqsubtypesdirprod {X Y : UU} (A : hsubtype X) (B : hsubtype Y) : subtypesdirprod A B ≃ A × B. Proof. intros. set (f := fromdsubtypesdirprodcarrier A B). set (g := tosubtypesdirprodcarrier A B). split with f. assert (egf : ∏ a : _, paths (g (f a)) a). { intro a. induction a as [ xy is ]. induction xy as [ x y ]. induction is as [ isx isy ]. apply idpath. } assert (efg : ∏ a : _, paths (f (g a)) a). { intro a. induction a as [ xis yis ]. induction xis as [ x isx ]. induction yis as [ y isy ]. apply idpath. } apply (isweq_iso _ _ egf efg). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.