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.
Show 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).

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

Definition cartesian_cube_category : category.
Show proof.
  exists cartesian_cube_precategory.
  intros m n.
  apply funspace_isaset, isfinite_isaset.
  apply isfinitecoprod; apply isfinitestn.

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.
Show 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].

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

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.
Show 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).

The interval in cartesian cubical sets has decidable equality
The interval in cartesian cubical sets is tiny