Lemma interval_cartesian_cubical_sets_dec_eq : ∏ (n : cartesian_cube_category), isdeceq ((I : functor _ _) n : hSet). Proof. intro n. use isdeceqweqb. - exact (stn ((n+2) * 1)). - use weqcomp. + exact ((stn 1) → (stn (n+2))). + apply weqffun, weqfromcoprodofstn. + apply weqfromfunstntostn. - apply isdeceqstn. 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.