Definition cartesian_cube_category : category. Proof. exists cartesian_cube_precategory. intros m n. apply funspace_isaset, isfinite_isaset. apply isfinitecoprod; apply isfinitestn. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.ExponentiationLeftAdjoint. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.Categories.HSET.Structures.