Lemma ishinhsubtypedirprod {X Y : UU} (A : hsubtype X) (B : hsubtype Y) (isa : ishinh A) (isb : ishinh B) : ishinh (subtypesdirprod A B). Proof. intros. apply (hinhfun (invweq (weqsubtypesdirprod A B))). apply hinhand. apply isa. apply isb. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.