Definition isofnelondirprod {X Y : UU} {n m : nat} (sx : isofnel n X) (sy : isofnel m Y) : isofnel (n * m) (X × Y) := hinhfun2 nelstructondirprod sx sy.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.