Library UniMath.CategoryTheory.EnrichedCats.BenabouCosmos

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Core.PosetCat.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.Limits.Coends.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Require Import UniMath.CategoryTheory.Limits.Coequalizers.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.Products.
Require Import UniMath.CategoryTheory.Limits.Equalizers.
Require Import UniMath.CategoryTheory.Limits.Preservation.
Require Import UniMath.CategoryTheory.OppositeCategory.Core.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed.

Local Open Scope cat.
Local Open Scope moncat.

1. Benabou cosmos

Definition benabou_cosmos
  : UU
  := ∑ (V : sym_mon_closed_cat),
     (∏ (I : UU), Products I V)
     ×
     Equalizers V
     ×
     (∏ (I : UU), Coproducts I V)
     ×
     Coequalizers V.

2. Accessors

Coercion benabou_cosmos_to_sym_mon_closed_cat
         (V : benabou_cosmos)
  : sym_mon_closed_cat.
Show proof.
  exact (pr1 V).

Definition benabou_cosmos_products
           (V : benabou_cosmos)
           (I : UU)
  : Products I V
  := pr12 V I.

Definition benabou_cosmos_binproducts
           (V : benabou_cosmos)
  : BinProducts V.
Show proof.
  use BinProducts_from_Products.
  apply benabou_cosmos_products.

Definition benabou_cosmos_equalizers
           (V : benabou_cosmos)
  : Equalizers V
  := pr122 V.

Definition benabou_cosmos_coproducts
           (V : benabou_cosmos)
           (I : UU)
  : Coproducts I V
  := pr1 (pr222 V) I.

Definition benabou_cosmos_initial
           (V : benabou_cosmos)
  : Initial V
  := initial_from_empty_coproduct V (benabou_cosmos_coproducts V ∅ _).

Definition benabou_cosmos_coequalizers
           (V : benabou_cosmos)
  : Coequalizers V
  := pr2 (pr222 V).

Definition benabou_cosmos_coends
           (V : benabou_cosmos)
           {C : category}
           (F : category_binproduct (C^opp) C ⟶ V)
  : coend_colimit F.
Show proof.
  use construction_of_coends.
  - apply benabou_cosmos_coequalizers.
  - apply benabou_cosmos_coproducts.
  - apply benabou_cosmos_coproducts.

#[global] Opaque benabou_cosmos_initial.
#[global] Opaque benabou_cosmos_coends.
#[global] Opaque benabou_cosmos_binproducts.

Definition is_initial_tensor_initial_l
           {V : benabou_cosmos}
           (v : V)
  : isInitial V (v ⊗ benabou_cosmos_initial V).
Show proof.
  exact ((left_adjoint_preserves_initial
            _
            (sym_mon_closed_left_tensor_left_adjoint V v))
           _
           (pr2 (benabou_cosmos_initial V))).

Definition is_initial_tensor_initial_r
           {V : benabou_cosmos}
           (v : V)
  : isInitial V (benabou_cosmos_initial V ⊗ v).
Show proof.
  exact ((left_adjoint_preserves_initial
            _
            (sym_mon_closed_right_tensor_left_adjoint V v))
           _
           (pr2 (benabou_cosmos_initial V))).

Definition arrow_from_tensor_initial_l_benabou_cosmos
           {V : benabou_cosmos}
           (v w : V)
  : v ⊗ benabou_cosmos_initial V --> w.
Show proof.
  exact (InitialArrow
           (make_Initial
              _
              (is_initial_tensor_initial_l v))
           w).

Definition arrow_from_tensor_initial_r_benabou_cosmos
           {V : benabou_cosmos}
           (v w : V)
  : benabou_cosmos_initial V ⊗ v --> w.
Show proof.
  exact (InitialArrow
           (make_Initial
              _
              (is_initial_tensor_initial_r v))
           w).

Proposition arrow_from_tensor_initial_l_benabou_cosmos_eq
            {V : benabou_cosmos}
            {v w : V}
            (f g : v ⊗ benabou_cosmos_initial V --> w)
  : f = g.
Show proof.
  apply (@InitialArrowEq _ (make_Initial _ (is_initial_tensor_initial_l v))).

Proposition arrow_from_tensor_initial_r_benabou_cosmos_eq
            {V : benabou_cosmos}
            {v w : V}
            (f g : benabou_cosmos_initial V ⊗ v --> w)
  : f = g.
Show proof.
  apply (@InitialArrowEq _ (make_Initial _ (is_initial_tensor_initial_r v))).

Definition is_initial_tensor_initial_1
           {V : benabou_cosmos}
           (v₁ v₂ : V)
  : isInitial V (benabou_cosmos_initial V ⊗ v₁ ⊗ v₂).
Show proof.
  refine ((left_adjoint_preserves_initial
             _
             (sym_mon_closed_right_tensor_left_adjoint V _))
            _
            _).
  apply is_initial_tensor_initial_r.

Proposition arrow_from_tensor_initial_1_benabou_cosmos_eq
            {V : benabou_cosmos}
            {v₁ v₂ w : V}
            (f g : benabou_cosmos_initial V ⊗ v₁ ⊗ v₂ --> w)
  : f = g.
Show proof.
  apply (@InitialArrowEq _ (make_Initial _ (is_initial_tensor_initial_1 _ _))).

Definition is_initial_tensor_initial_2
           {V : benabou_cosmos}
           (v₁ v₂ : V)
  : isInitial V (v₁ ⊗ benabou_cosmos_initial V ⊗ v₂).
Show proof.
  refine ((left_adjoint_preserves_initial
             _
             (sym_mon_closed_right_tensor_left_adjoint V _))
            _
            _).
  apply is_initial_tensor_initial_l.

Proposition arrow_from_tensor_initial_2_benabou_cosmos_eq
            {V : benabou_cosmos}
            {v₁ v₂ w : V}
            (f g : v₁ ⊗ benabou_cosmos_initial V ⊗ v₂ --> w)
  : f = g.
Show proof.
  apply (@InitialArrowEq _ (make_Initial _ (is_initial_tensor_initial_2 _ _))).

Definition is_initial_tensor_initial_3
           {V : benabou_cosmos}
           (v₁ v₂ : V)
  : isInitial V (v₁ ⊗ (v₂ ⊗ benabou_cosmos_initial V)).
Show proof.
  refine ((left_adjoint_preserves_initial
             _
             (sym_mon_closed_left_tensor_left_adjoint V _))
            _
            _).
  apply is_initial_tensor_initial_l.

Proposition arrow_from_tensor_initial_3_benabou_cosmos_eq
            {V : benabou_cosmos}
            {v₁ v₂ w : V}
            (f g : v₁ ⊗ (v₂ ⊗ benabou_cosmos_initial V) --> w)
  : f = g.
Show proof.
  apply (@InitialArrowEq _ (make_Initial _ (is_initial_tensor_initial_3 _ _))).

Definition arrow_from_tensor_coproduct_benabou_cosmos
           {V : benabou_cosmos}
           {v w : V}
           {I : UU}
           {D : I → V}
           (fs : ∏ (i : I), v ⊗ D i --> w)
  : v ⊗ benabou_cosmos_coproducts V I D --> w.
Show proof.
  use (CoproductArrow
         _ _
         (make_Coproduct
            _ _ _ _ _
            (left_adjoint_preserves_coproduct
               _
               (sym_mon_closed_left_tensor_left_adjoint V v)
               I
               _ _ _
               (isCoproduct_Coproduct _ _ (benabou_cosmos_coproducts V I D))))).
  exact fs.

3. Quantales

Definition quantale_cosmos
  : UU
  := ∑ (V : benabou_cosmos)
       (HV : is_univalent V),
     is_poset_category (_ ,, HV).

Coercion quantale_cosmos_to_benabou_cosmos
         (V : quantale_cosmos)
  : benabou_cosmos.
Show proof.
  exact (pr1 V).

Proposition is_univalent_quantale_cosmos
            (V : quantale_cosmos)
  : is_univalent V.
Show proof.
  exact (pr12 V).

Definition univalent_category_of_quantale_cosmos
           (V : quantale_cosmos)
  : univalent_category.
Show proof.
  use make_univalent_category.
  - exact V.
  - exact (is_univalent_quantale_cosmos V).

Proposition is_poset_category_quantale_cosmos
            (V : quantale_cosmos)
  : is_poset_category (_ ,, is_univalent_quantale_cosmos V).
Show proof.
  exact (pr22 V).