{-# OPTIONS --type-in-type #-}

module Concurrent where

open import Base
open import Monoidal

module ≤-Reasoning {ℂ : MonoidalCategory} {X Y : MonoidalCategory.obj ℂ} where
  open MonoidalCategory ℂ

  eq2≤refl : {f g : MonoidalCategory.hom ℂ X Y} → f ≡ g → f ≤ g
  eq2≤refl {f} {g} refl = ≤refl {X} {Y} {g}

  infix   _≤∎
  infixr  _≤⟨⟩_ step-≤ step-≦
  infix   ≤begin_

  ≤begin_ : {x y : hom X Y} → x ≤ y → x ≤ y
  ≤begin_ x≤y = x≤y

  _≤⟨⟩_ : (x {y} : hom X Y) → x ≤ y → x ≤ y
  _ ≤⟨⟩ x≤y = x≤y

  step-≤ : (x {y z} : hom X Y) → y ≤ z → x ≤ y → x ≤ z
  step-≤ _ y≤z x≤y = ≤trans x≤y y≤z

  step-≦ : (x {y z} : hom X Y) → y ≤ z → x ≡ y → x ≤ z
  step-≦ x y≤z x≡y = ≤trans (eq2≤refl x≡y) y≤z

  _≤∎ : (x : hom X Y) → x ≤ x
  _≤∎ _ = ≤refl

  syntax step-≤ x y≤z x≤y = x ≤⟨ x≤y ⟩ y≤z
  syntax step-≦ x y≤z x≡y = x ≦⟨ x≡y ⟩ y≤z


record IsKLaxMonoidalFunctor {c : Set} {⊗₀ : c × c → c} {I₀ : ⊤ → c}
                             {𝕂 : ParamMonoidalLikeCategory c ⊗₀ I₀} {ℂ : ParamMonoidalCategory c ⊗₀ I₀}
                             (funcJ : ParamFunctor (ParamMonoidalCategory.P ℂ) (ParamMonoidalLikeCategory.P 𝕂) (λ C → C))
                             (funcK : Functor (ParamMonoidalLikeCategory.U 𝕂) (ParamMonoidalCategory.U ℂ)): Set where
  private
    module 𝕂 = ParamMonoidalLikeCategory 𝕂
    module ℂ = ParamMonoidalCategory ℂ
    open Functor funcK renaming (F₀ to K ; F₁ to K₁)
    module J = ParamFunctor funcJ
    J₁ = J.F₁
  field
    ϕ-at : (A B : c) → ℂ.hom (K A ℂ.⊗ K B) (K (A 𝕂.⊗ B)) 
    ϕ-naturality : {A B C D : c} {f1 : 𝕂.hom A B} {f2 : 𝕂.hom C D}
                      → ϕ-at A C ℂ.▷ K₁ (f1 𝕂.∥ f2) ≡ K₁ f1 ℂ.⊗₁ K₁ f2 ℂ.▷ ϕ-at B D
    ϕ⁰ : ℂ.hom ℂ.I (K 𝕂.I)
    laxAssoc : {X Y Z : c}
      → ϕ-at X Y ℂ.⊗₁ ℂ.id (K Z) ℂ.▷ ϕ-at (X 𝕂.⊗ Y) Z ℂ.▷ K₁ (J₁ (ℂ.α-at X Y Z))
        ≡ ℂ.α-at (K X) (K Y) (K Z) ℂ.▷ ℂ.id (K X) ℂ.⊗₁ ϕ-at Y Z ℂ.▷ ϕ-at X (Y 𝕂.⊗ Z)
    laxLunital : {X : c} → ℂ.λ-at (K X)
        ≡ ϕ⁰ ℂ.⊗₁ ℂ.id (K X) ℂ.▷ ϕ-at 𝕂.I X ℂ.▷ K₁ (J₁ (ℂ.λ-at X))
    laxRunital : {X : c} → K₁ (J₁ (ℂ.ρ-at X))
        ≡ ℂ.ρ-at (K X) ℂ.▷ ℂ.id (K X) ℂ.⊗₁ ϕ⁰ ℂ.▷ ϕ-at X 𝕂.I

    -- conditions on morphisms
    -- preserve⊗ is the exact same as ϕ-naturality!
    preserveI₁ :  ϕ⁰ ℂ.▷ K₁ 𝕂.jd ℂ.≤ ℂ.I₁ ℂ.▷ ϕ⁰
    preserve⊗₁ : {X Y U V : 𝕂.obj} {f : 𝕂.hom X Y} {g : 𝕂.hom U V}
                  → ϕ-at X U ℂ.▷ K₁ (f 𝕂.∥ g) ℂ.≤ K₁ f ℂ.⊗₁ K₁ g ℂ.▷ ϕ-at Y V 

-- since this 'template' is only made for J, we have it very specific on purpose
-- it's param since it needs to be identity on objects and then Monoidal to MonoidalLike
record IsJOplaxMonoidalFunctor {obj : Set} {_⊗₀_ : obj × obj → obj} {I₀ : ⊤ → obj}
       {ℂ : ParamMonoidalCategory obj _⊗₀_ I₀} {𝕂 : ParamMonoidalLikeCategory obj _⊗₀_ I₀}
       (funcJ : ParamFunctor (ParamMonoidalCategory.P ℂ) (ParamMonoidalLikeCategory.P 𝕂) (λ C → C)): Set where
  module ℂ = ParamMonoidalCategory ℂ
  module 𝕂 = ParamMonoidalLikeCategory 𝕂
  J : obj → obj
  J = λ C → C
  open ParamFunctor funcJ renaming (F₁ to J₁)
  _∥_ = 𝕂._∥_
  field
    ω-at : (A B : ℂ.obj) → 𝕂.hom (J (A ℂ.⊗ B)) (J A 𝕂.⊗ J B)
    ω-naturality : {A B C D : ℂ.obj} {f1 : ℂ.hom A B} {f2 : ℂ.hom C D}
                      → J₁ (f1 ℂ.⊗₁ f2) 𝕂.▷ ω-at B D 𝕂.≤ ω-at A C 𝕂.▷ J₁ f1 ∥ J₁ f2
    ω⁰ : 𝕂.hom (J ℂ.I) 𝕂.I
    oplaxAssoc : {X Y Z : ℂ.obj}
      → ω-at (X ℂ.⊗ Y) Z 𝕂.▷ ω-at X Y ∥ 𝕂.id (J Z) 𝕂.▷ J₁ (ℂ.α-at (J X) (J Y) (J Z))
        ≡ (J₁ (ℂ.α-at X Y Z) 𝕂.▷ ω-at X (Y ℂ.⊗ Z) 𝕂.▷ 𝕂.id (J X) ∥ ω-at Y Z)
    oplaxLunital : {X : ℂ.obj} → J₁ (ℂ.λ-at X)
        ≡ ω-at ℂ.I X 𝕂.▷ ω⁰ ∥ 𝕂.id (J X) 𝕂.▷ J₁ (ℂ.λ-at (J X))
    oplaxRunital : {X : ℂ.obj} → J₁ (ℂ.ρ-at (J X))
        ≡ J₁ (ℂ.ρ-at X) 𝕂.▷ ω-at X ℂ.I 𝕂.▷ 𝕂.id (J X) ∥ ω⁰

    preserveI₁ : J₁ ℂ.I₁ 𝕂.≤ 𝕂.jd
    preserve⊗₁ : {X Y U V : ℂ.obj} (f : ℂ.hom X Y) (g : ℂ.hom U V)
                  → J₁ (f ℂ.⊗₁ g) 𝕂.≤ J₁ f ∥ J₁ g
                  
record JFunctor
       {c : Set} {⊗₀ : c × c → c} {I₀ : ⊤ → c}
       (ℂ : ParamMonoidalCategory c ⊗₀ I₀)
       (𝕂 : ParamMonoidalLikeCategory c ⊗₀ I₀)  : Set where
  field
    F : ParamFunctor (ParamMonoidalCategory.P ℂ) (ParamMonoidalLikeCategory.P 𝕂) (λ C → C)
    isJOplaxMonoidalFunctor : IsJOplaxMonoidalFunctor {c} {⊗₀} {I₀} {ℂ} {𝕂} F
  open ParamFunctor F public

record KFunctor {c : Set} {⊗₀ : c × c → c} {I₀ : ⊤ → c}
           (𝕂 : ParamMonoidalLikeCategory c ⊗₀ I₀) (ℂ : ParamMonoidalCategory c ⊗₀ I₀) (J : JFunctor ℂ 𝕂) : Set where
  field
    F : Functor (ParamMonoidalLikeCategory.U 𝕂) (ParamMonoidalCategory.U ℂ)
    isKLaxMonoidalFunctor : IsKLaxMonoidalFunctor {c} {⊗₀} {I₀} {𝕂} {ℂ} (JFunctor.F J) F
  open Functor F public
  open IsKLaxMonoidalFunctor isKLaxMonoidalFunctor public

record IsConcurrentCategory
       {c : Set} {⊗₀ : c × c → c} {I₀ : ⊤ → c}
       (ℂ : ParamMonoidalCategory c ⊗₀ I₀) (𝕂 : ParamMonoidalLikeCategory c ⊗₀ I₀)
       (funcJ : JFunctor ℂ 𝕂) : Set where
  open JFunctor funcJ renaming (F₁ to J₁)
  private
    module ℂ = ParamMonoidalCategory ℂ
    module 𝕂 = ParamMonoidalLikeCategory 𝕂
  open ParamMonoidalCategory ℂ using (_⊗₁_)
  open ParamMonoidalLikeCategory 𝕂 using (_∥_; jd; _▷_)
  field
    λ-naturality : ∀ {A B} {f : 𝕂.hom A B} → J₁ (ℂ.λ-at A) ▷ f ≡ jd ∥ f ▷ J₁ (ℂ.λ-at B)
    ρ-naturality : ∀ {A B} {f : 𝕂.hom A B} → J₁ (ℂ.ρ-at A) ▷ f ∥ jd ≡ f ▷ J₁ (ℂ.ρ-at B)
    α-naturality : ∀ {A B C X Y Z} {f : 𝕂.hom A X} {g : 𝕂.hom B Y} {h : 𝕂.hom C Z}
      → (f ∥ g) ∥ h ▷ J₁ (ℂ.α-at X Y Z) ≡ J₁ (ℂ.α-at A B C) ▷ f ∥ (g ∥ h)
    ich4a : ∀ {A B C X Y Z} {f : ℂ.hom A B} {g : ℂ.hom X Y}
                            {m : 𝕂.hom B C} {n : 𝕂.hom Y Z}
            → J₁ (f ⊗₁ g) ▷ (m ∥ n) ≡ (J₁ f ▷ m) ∥ (J₁ g ▷ n)
    ich4b : ∀ {A B C X Y Z} {k : 𝕂.hom A B} {ℓ : 𝕂.hom X Y}
                            {h : ℂ.hom B C} {i : ℂ.hom Y Z}
            → (k ∥ ℓ) ▷ J₁ (h ⊗₁ i) ≡ (k ▷ J₁ h) ∥ (ℓ ▷ J₁ i)


record ConcurrentCategory (ℂ : MonoidalCategory) : Set where
  open MonoidalCategory ℂ
  field
    𝕂 : ParamMonoidalLikeCategory obj MonoidalProduct₀ Identity₀
    J : JFunctor P-monoidal 𝕂 
    isConcurrentCategory : IsConcurrentCategory P-monoidal 𝕂 J
  𝕂-contained : MonoidalLikeCategory
  𝕂-contained = record
    { c = obj
    ; t⊗₀ = MonoidalProduct₀
    ; tI₀ = Identity₀
    ; P-monoidallike = 𝕂
    }
  open IsConcurrentCategory isConcurrentCategory public

-- the base is a monoidal category but the functor structure is not necessarily monidal
record IsConcurrentMonad {ℂ : MonoidalCategory}
       (M : Functor (MonoidalCategory.U ℂ)
                    (MonoidalCategory.U ℂ)) : Set where
  open MonoidalCategory ℂ
  open Functor M public
  F = F₀
  field
    η-at : (C : obj) → hom C (F C)
    η-naturality : {C D : obj} → {f : hom C D}
      → f ▷ η-at D ≡ η-at C ▷ F₁ f
    μ-at : (C : obj) → hom (F (F C)) (F C)
    μ-naturality : {C D : obj} → {f : hom C D}
      → F₁ (F₁ f) ▷ μ-at D ≡ μ-at C ▷ F₁ f
    ψ⁰ : hom I (F I)
    ψ-at : (X Y : obj) → hom (F X ⊗ F Y) (F (X ⊗ Y))
    ψ-naturality : {X Y Z W : obj} → {f : hom X Y} → {g : hom Z W}
      → F₁ f ⊗₁ F₁ g ▷ ψ-at Y W ≡ ψ-at X Z ▷ F₁ (f ⊗₁ g)

    diagram1 : {X : obj} → η-at (F X) ▷ μ-at X ≡ id (F X)
    diagram2 : {X : obj} → F₁ (η-at X) ▷ μ-at X ≡ id (F X)
    diagram3 : {X : obj} → F₁ (μ-at X) ▷ μ-at X ≡ μ-at (F X) ▷ μ-at X
    diagram4 : {X : obj} → λ-at (F X)
             ≡ ψ⁰ ⊗₁ id (F X) ▷ ψ-at I X ▷ F₁ (λ-at X)
    diagram5 : {X : obj} → ρ-at (F X) ▷ id (F X) ⊗₁ ψ⁰ ▷ ψ-at X I
                       ≡ F₁ (ρ-at X)
    diagram6 : {X Y Z : obj} → α-at (F X) (F Y) (F Z) ▷ id (F X) ⊗₁ ψ-at Y Z
                                  ▷ ψ-at X (Y ⊗ Z)
                           ≡ ψ-at X Y ⊗₁ id (F Z) ▷ ψ-at (X ⊗ Y) Z ▷ F₁ (α-at X Y Z)
    inequation1 : η-at I ≤ ψ⁰
    inequation2 : ψ⁰ ▷ F₁ ψ⁰ ▷ μ-at I ≤ ψ⁰
    inequation3 : {X Y : obj} → η-at (X ⊗ Y) ≤ η-at X ⊗₁ η-at Y ▷ ψ-at X Y
    inequation4 : {X Y : obj} → ψ-at (F X) (F Y) ▷ F₁ (ψ-at X Y) ▷ μ-at (X ⊗ Y)
                                ≤ μ-at X ⊗₁ μ-at Y ▷ ψ-at X Y

record ConcurrentMonad (this-ℂ : MonoidalCategory) : Set where
  module ℂ = MonoidalCategory this-ℂ
  field
    M : Functor ℂ.U ℂ.U
    isConcurrentMonad : IsConcurrentMonad {this-ℂ} M
  open IsConcurrentMonad isConcurrentMonad public