Library UniMath.CategoryTheory.categories.CartesianCubicalSets

****************************************************************************
We define the cartesian cubical sets and show that the interval satisfies axioms B1, B2 and B3 in:
A Survey of Constructive Presheaf Models of Univalence (2018), Thierry Coquand https://dl.acm.org/doi/abs/10.1145/3242953.3242962
Contents:
Written by: Elisabeth Bonnevier, 2019
The cartesian cube category.
Definition cartesian_cube_precategory_ob_mor : precategory_ob_mor :=
  make_precategory_ob_mor nat (λ m n : nat, n m ⨿ 2).

Definition cartesian_cube_precategory_data : precategory_data.
Proof.
   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.

Definition cartesian_cube_precategory : precategory.
Proof.
   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.

Definition cartesian_cube_category : category.
Proof.
   cartesian_cube_precategory.
  intros m n.
  apply funspace_isaset, isfinite_isaset.
  apply isfinitecoprod; apply isfinitestn.
Defined.

Binary products in the cartesian cube category. The product ⟦m⟧ × ⟦n⟧ is the sum ⟦m + n⟧.
Definition cartesian_cube_category_binproducts : BinProducts cartesian_cube_category.
Proof.
  intros m n.
  use make_BinProduct.
  - exact (m + n).
  - exact (λ i : m, inl (stn_left _ _ i)).
  - exact (λ i : n, inl (stn_right _ _ i)).
  - use make_isBinProduct.
    + intros l f g.
      use unique_exists.
      × intro i.
        induction (weqfromcoprodofstn_invmap _ _ i) as [x1 | x2];
          [exact (f x1) | exact (g x2)].
      × cbn.
        split; apply funextfun; intro i.
        -- assert (H : weqfromcoprodofstn_invmap _ _ (stn_left m n i) = inl i).
           { now rewrite <- weqfromcoprodofstn_eq1. }
           now rewrite H.
        -- assert (H : weqfromcoprodofstn_invmap _ _ (stn_right m n i) = inr i).
           { now rewrite <- weqfromcoprodofstn_eq1. }
           now rewrite H.
      × intro h.
        now apply isapropdirprod; apply homset_property.
      × intros h [H1 H2].
        apply funextfun; intros i.
        rewrite <- (maponpaths h (weqfromcoprodofstn_eq2 _ _ i)).
        induction (weqfromcoprodofstn_invmap _ _ i) as [x1 | x2];
          [now rewrite <- H1 | now rewrite <- H2].
Defined.

The empty set is terminal in the cartesian cube category.
Lemma empty_is_terminal_cartesian_cube_category : Terminal cartesian_cube_category.
Proof.
   0.
  intro n.
  apply iscontrfunfromempty2.
  use weqstn0toempty.
Defined.

Local Close Scope stn.

Local Open Scope cat.

Cartesian cubical sets
The interval in cartesian cubical sets has two distinct elements
Lemma interval_cartesian_cubical_sets_two_elements :
   n : cartesian_cube_category, f g : ((I : functor _ _) n : hSet), f != g.
Proof.
  intro n.
   (λ _ : stn 1, @inr (stn n) (stn 2) (make_stn 2 0 (idpath _))).
   (λ _ : 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.

The interval in cartesian cubical sets has decidable equality
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.

Definition cartesian_cubical_sets_exponentials : Exponentials (@BinProducts_PreShv cartesian_cube_category).
Proof.
  apply Exponentials_functor_HSET.
Defined.

Local Definition exp_I : cartesian_cubical_sets cartesian_cubical_sets :=
  pr1 (cartesian_cubical_sets_exponentials I).

The interval in cartesian cubical sets is tiny