Lemma interval_cartesian_cubical_sets_two_elements : ∏ n : cartesian_cube_category, ∑ f g : ((I : functor _ _) n : hSet), f != g. Proof. intro n. exists (λ _ : stn 1, @inr (stn n) (stn 2) (make_stn 2 0 (idpath _))). exists (λ _ : stn 1, @inr (stn n) (stn 2) (make_stn 2 1 (idpath _))). intro p. apply toforallpaths in p. set (e := p (make_stn 1 0 (idpath _))). apply ii2_injectivity in e. apply (maponpaths pr1) in e. apply (negpaths0sx 0 e). 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.