Library UniMath.Semantics.EnrichedEffectCalculus.EECModel

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.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed.
Require Import UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment.
Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor.
Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation.
Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentAdjunction.
Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched.
Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedTerminal.
Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedBinaryProducts.
Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedPowers.
Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedInitial.
Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedBinaryCoproducts.
Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers.

Local Open Scope cat.

1. Definition of models of the enriched calculus

1.1. Model of the enriched effect calculus

Definition eec_model
  : UU
  := ∑ (VC : category)
       (TV : Terminal VC)
       (VP : BinProducts VC)
       (expV : Exponentials VP)
       (V : sym_mon_closed_cat := sym_mon_closed_cartesian_cat VC VP TV expV)
       (C : category)
       (EC : enrichment C V ),
     (enriched_adjunction (self_enrichment V) EC )
     ×
     (terminal_enriched EC )
     ×
     (initial_enriched EC )
     ×
     (enrichment_power EC )
     ×
     (enrichment_copower EC )
     ×
     (enrichment_binary_prod EC )
     ×
     (enrichment_binary_coprod EC ).

1.2. Model of the enriched effect calculus with additives

Definition eec_plus_model
  : UU
  := ∑ (M : eec_model ),
     Initial (pr1 M)
     ×
     BinCoproducts (pr1 M).

Coercion eec_plus_model_to_eec_model
         (E : eec_plus_model)
  : eec_model
  := pr1 E.