import Graded.Modality
module Graded.Context
{a} {M : Set a}
(open Graded.Modality M)
(𝕄 : Modality)
where
open Modality 𝕄
open import Graded.Modality.Natrec-star-instances
open import Tools.Fin
open import Tools.Nat using (Nat; 1+) renaming (_+_ to _+ⁿ_)
open import Tools.PropositionalEquality
infixl 24 _∙_
infixr 40 _+ᶜ_
infixr 40 _∧ᶜ_
infixr 45 _·ᶜ_
infixr 45 _*_
infix 50 _⊛ᶜ_▷_
infix 10 _≤ᶜ_
infix 35 _,_≔_
infix 60 _⟨_⟩
private
variable
m n : Nat
data Conₘ : Nat → Set a where
ε : Conₘ 0
_∙_ : (γ : Conₘ n) → (p : M) → Conₘ (1+ n)
data _≈ᶜ_ : (γ δ : Conₘ n) → Set a where
ε : ε ≈ᶜ ε
_∙_ : {γ δ : Conₘ n} {p q : M} → γ ≈ᶜ δ → p ≡ q → (γ ∙ p) ≈ᶜ (δ ∙ q)
headₘ : (γ : Conₘ (1+ n)) → M
headₘ (γ ∙ p) = p
tailₘ : (γ : Conₘ (1+ n)) → Conₘ n
tailₘ (γ ∙ p) = γ
_,_≔_ : (γ : Conₘ n) (x : Fin n) (p : M) → Conₘ n
(γ ∙ q) , x0 ≔ p = γ ∙ p
(γ ∙ q) , (x +1) ≔ p = (γ , x ≔ p) ∙ q
_⟨_⟩ : (γ : Conₘ n) → (x : Fin n) → M
(γ ∙ p) ⟨ x0 ⟩ = p
(γ ∙ p) ⟨ x +1 ⟩ = γ ⟨ x ⟩
_*_ : (γ δ : Conₘ n) → M
ε * ε = 𝟘
(γ ∙ p) * (δ ∙ q) = γ * δ + p · q
_+ᶜ_ : (γ δ : Conₘ n) → Conₘ n
ε +ᶜ ε = ε
(γ ∙ p) +ᶜ (δ ∙ q) = (γ +ᶜ δ) ∙ (p + q)
_∧ᶜ_ : (γ δ : Conₘ n) → Conₘ n
ε ∧ᶜ ε = ε
(γ ∙ p) ∧ᶜ (δ ∙ q) = (γ ∧ᶜ δ) ∙ (p ∧ q)
_·ᶜ_ : (p : M) (γ : Conₘ n) → Conₘ n
p ·ᶜ ε = ε
p ·ᶜ (γ ∙ q) = (p ·ᶜ γ) ∙ (p · q)
_≤ᶜ_ : (γ δ : Conₘ n) → Set a
γ ≤ᶜ δ = γ ≈ᶜ γ ∧ᶜ δ
_⊛ᶜ_▷_ :
⦃ has-star : Has-star semiring-with-meet ⦄ →
Conₘ n → Conₘ n → M → Conₘ n
ε ⊛ᶜ ε ▷ r = ε
(γ ∙ p) ⊛ᶜ δ ∙ q ▷ r = (γ ⊛ᶜ δ ▷ r) ∙ (p ⊛ q ▷ r)
𝟘ᶜ : Conₘ n
𝟘ᶜ {n = 0} = ε
𝟘ᶜ {n = 1+ n} = 𝟘ᶜ ∙ 𝟘
𝟙ᶜ : Conₘ n
𝟙ᶜ {n = 0} = ε
𝟙ᶜ {n = 1+ n} = 𝟙ᶜ ∙ 𝟙