Definition cartesian_cube_precategory_data : precategory_data. Proof. exists cartesian_cube_precategory_ob_mor. split. - intro n. exact (λ i : ⟦n⟧, inl i). - intros l m n f g i. induction (g i) as [j1 | j2]. + exact (f j1). + exact (inr j2). 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.