Definition cartesian_cube_precategory : precategory. Proof. exists cartesian_cube_precategory_data. use make_is_precategory_one_assoc. - intros m n f. apply funextfun; intro i. cbn. now induction (f i). - intros m n g. apply idpath. - intros k l m n f g h. apply funextfun; intro i. cbn. now induction (h i). 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.