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