proposition: Corollary isofhleveldirprod (n : nat) (X Y : UU) (is1 : isofhlevel n X) (is2 : isofhlevel n Y) : isofhlevel n (X × Y).
proof: Proof. intros. apply isofhleveltotal2. assumption. intro. assumption. Defined.
imports: UniMath.Foundations.PartA