Library UniMath.CategoryTheory.Monoidal.Examples.SetWithSubset


Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Projection.

Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Functors.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.MonoidalSections.

Require Import UniMath.CategoryTheory.categories.HSET.All.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian.
Require Import UniMath.CategoryTheory.Monoidal.Examples.SetCartesianMonoidal.

Section SetWithSubset.

  Local Definition setsubtype (X : HSET) : UU := hsubtype (pr1 X).

  Definition SS_disp_cat_ob_mor : disp_cat_ob_mor hset_category.
  Show proof.
    use tpair.
    - exact (λ X, setsubtype X).
    - exact (λ _ _ U V f, hsubtype_preserving U V f).

  Definition SS_disp_cat_data : disp_cat_data hset_category.
  Show proof.
    exists SS_disp_cat_ob_mor.
    use tpair.
    - intro ; intro.
      apply id_hsubtype_preserving.
    - intros ? ? ? ? ? ? ? ? fsp gsp.
      apply (comp_hsubtype_preserving fsp gsp).

  Lemma SS_disp_cat_locally_prop : locally_propositional SS_disp_cat_data.
  Show proof.
    intro; intros; apply isaprop_hsubtype_preserving.

  Definition SS_disp_cat : disp_cat hset_category.
  Show proof.
    use make_disp_cat_locally_prop.
    - exact SS_disp_cat_data.
    - exact SS_disp_cat_locally_prop.

  Definition total_subset_section_data : section_disp_data SS_disp_cat.
  Show proof.
    exists (λ X, totalsubtype (pr1 X)).
    intro ; intros.
    apply total_hsubtype_preserving.

  Definition total_subset_section_axioms : section_disp_axioms total_subset_section_data.
  Show proof.
    use tpair.
    - intro ; repeat (apply funextsec ; intro) ; apply totalsubtype.
    - intro ; intros ; repeat (apply funextsec ; intro) ; apply totalsubtype.

  Definition total_subset_section : section_disp SS_disp_cat
    := total_subset_section_data ,, total_subset_section_axioms.

End SetWithSubset.

Section SetWithSubsetMonoidal.

  Definition SS_disp_cat_tensor_data
    : disp_bifunctor_data SET_cart_monoidal SS_disp_cat SS_disp_cat SS_disp_cat.
  Show proof.
    exists (λ _ _ U V, subtypesdirprod U V).
    split.
    - intros X Y1 Y2 g Ux U1 U2 gsp.
      intros xy2 xy1_prop.
      use (factor_through_squash _ _ xy1_prop).
      { apply subtypesdirprod. }
      intro xy1.
      split.
      + rewrite (! pr12 xy1).
        exact (pr122 xy1).
      + simpl in *.
        apply (gsp _).
        apply hinhpr.
        exists (pr21 xy1).
        split.
        * rewrite (! pr12 xy1).
          apply idpath.
        * exact (pr222 xy1).
    - intros X1 X2 Y f U1 U2 Uy fsp.
      intros x2y x1y_prop.
      use (factor_through_squash _ _ x1y_prop).
      { apply subtypesdirprod. }
      intro x1y.
      split.
      + simpl in *.
        apply (fsp _).
        apply hinhpr.
        exists (pr11 x1y).
        split.
        * rewrite (! pr12 x1y).
          apply idpath.
        * exact (pr122 x1y).
      + rewrite (! pr12 x1y).
        exact (pr222 x1y).

  Definition SS_disp_cat_tensor : disp_tensor SS_disp_cat SET_cart_monoidal.
  Show proof.
    use make_disp_bifunctor_locally_prop.
    - exact SS_disp_cat_locally_prop.
    - exact SS_disp_cat_tensor_data.

  Definition SS_disp_monoidal_data : disp_monoidal_data SS_disp_cat SET_cart_monoidal.
  Show proof.
    exists (SS_disp_cat_tensor).
    exists (totalsubtype (pr1 unitHSET)).
    repeat (use tpair).
    - intros X U x xinU_prop.
      use (factor_through_squash _ _ xinU_prop).
      { apply U. }
      intro xinU.
      rewrite (! pr12 xinU).
      exact (pr222 xinU).
    - intros X U x xinU_prop.
      exists tt.
      use (factor_through_squash _ _ xinU_prop).
      { apply U. }
      intro xinU.
      rewrite (! pr12 xinU).
      exact (pr22 xinU).
    - intros X U x xinU_prop.
      use (factor_through_squash _ _ xinU_prop).
      { apply U. }
      intro xinU.
      rewrite (! pr12 xinU).
      exact (pr122 xinU).
    - intros X U x xinU_prop.
      refine (_ ,, tt).
      use (factor_through_squash _ _ xinU_prop).
      { apply U. }
      intro xinU.
      rewrite (! pr12 xinU).
      exact (pr22 xinU).
    - intros X Y Z U V W xyz xyzinUVW_prop.
      use (factor_through_squash _ _ xyzinUVW_prop).
      {
        repeat (apply isapropdirprod).
        + apply U.
        + apply V.
        + apply W.
      }
      intro xyzinUVW.
      rewrite (! pr12 xyzinUVW).
      repeat split ; apply (pr22 xyzinUVW).
    - intros X Y Z U V W xyz xyzinUVW_prop.
      use (factor_through_squash _ _ xyzinUVW_prop).
      {
        repeat (apply isapropdirprod).
        + apply U.
        + apply V.
        + apply W.
      }
      intro xyzinUVW.
      rewrite (! pr12 xyzinUVW).
      repeat split ; apply (pr22 xyzinUVW).

  Definition SS_disp_monoidal : disp_monoidal SS_disp_cat SET_cart_monoidal.
  Show proof.
    apply make_disp_monoidal_locally_prop.
    - exact SS_disp_cat_locally_prop.
    - exact SS_disp_monoidal_data.

  Definition total_subset_section_monoidal_data
    : smonoidal_data SET_cart_monoidal SS_disp_monoidal total_subset_section.
  Show proof.
    use tpair.
    - exact (λ _ _ _ _, tt).
    - exact (λ _ _, tt).

  Definition total_subset_section_monoidal_ax
    : smonoidal_laxlaws _ _ total_subset_section_monoidal_data.
  Show proof.
    repeat split ; repeat (intro ; intros ; apply isaprop_hsubtype_preserving).

  Definition total_subset_section_monoidal_lax
    : smonoidal_lax SET_cart_monoidal SS_disp_monoidal total_subset_section
    := total_subset_section_monoidal_data,, total_subset_section_monoidal_ax.

  Definition total_subset_section_monoidal
    : smonoidal SET_cart_monoidal SS_disp_monoidal total_subset_section.
  Show proof.
    exists (total_subset_section_monoidal_lax).
    use tpair.
    - intros X Y.
      repeat (use tpair) ; repeat (apply isaprop_hsubtype_preserving).
      exists tt.
      exact tt.
    - repeat (use tpair) ; repeat (apply isaprop_hsubtype_preserving).
      exact (λ _ _, tt).

End SetWithSubsetMonoidal.