Distributive Laws of Monadic Containers

Cubical/Algebra/DirContainer.agda

@@ -0,0 +1,6 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.DirContainer where
+
+open import Cubical.Algebra.DirContainer.Base public
+open import Cubical.Algebra.DirContainer.Examples public

Cubical/Algebra/DirContainer/Base.agda

@@ -0,0 +1,30 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.DirContainer.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Containers.Set.Base
+
+private
+  variable
+    ℓs ℓp : Level
+
+open SetCon
+
+record DirContainer (C : SetCon {ℓs} {ℓp}) : Type (ℓ-suc (ℓ-max ℓs ℓp)) where
+  S = Shape C
+  P = Position C
+  field
+    o : (s : S) → P s
+    _↓_ : (s : S) → P s → S
+    _⊕_ : {s : S} → (p : P s) → P (s ↓ p) → P s 
+    unitl-↓ : (s : S) → s ↓ (o _) ≡ s
+    distr-↓-⊕ : (s : S) (p : P s) (p' : P (s ↓ p)) →
+                s ↓ (p ⊕ p') ≡ (s ↓ p) ↓ p'
+    unitl-⊕ : (s : S) (p : P (s ↓ o s)) → 
+              PathP (λ i → P (unitl-↓ s (~ i))) (o s ⊕ p) p
+    unitr-⊕ : (s : S) (p : P s) → p ⊕ (o (s ↓ p)) ≡ p
+    assoc-⊕ : (s : S) (p : P s) (p' : P (s ↓ p)) →
+              PathP (λ i → P (distr-↓-⊕ s p p' i) → P s)
+                    (λ p'' → (p ⊕ p') ⊕ p'')
+                    (λ p'' → p ⊕ (p' ⊕ p''))

Cubical/Algebra/DirContainer/Examples.agda

@@ -0,0 +1,54 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.DirContainer.Examples where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
+open import Cubical.Algebra.DirContainer.Base
+open import Cubical.Data.Containers.Set.Base
+open import Cubical.Data.Unit
+open import Cubical.Data.Nat hiding (_·_)
+open import Cubical.Data.Bool hiding (_⊕_ ; ⊕-assoc)
+open import Cubical.Data.Empty
+open import Cubical.Data.Sum
+
+
+private
+  variable
+    ℓs ℓp : Level
+
+open DirContainer
+
+-- Examples of directed containers
+
+WriterC : (A : hSet ℓs) → DirContainer {ℓs} {ℓp} (fst A ◁ (const (Unit* {ℓp})) & snd A & isSetUnit*)
+o (WriterC A) _ = tt* 
+_↓_ (WriterC A) a tt* = a
+_⊕_ (WriterC A) tt* tt* = tt*
+unitl-↓ (WriterC A) a = refl
+distr-↓-⊕ (WriterC A) a tt* tt* = refl
+unitl-⊕ (WriterC A) a tt* = refl
+unitr-⊕ (WriterC A) a tt* = refl
+assoc-⊕ (WriterC A) a tt* tt* i tt* = tt*
+
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.Monoid.Instances.Nat
+open import Cubical.Algebra.Semigroup
+open MonoidStr
+open IsMonoid
+open IsSemigroup
+
+ReaderC : (A : Type ℓp) (mon : MonoidStr A) →
+          DirContainer {ℓs} {ℓp} ((Unit* {ℓs}) ◁ (const A) & isSetUnit* & mon .isMonoid .isSemigroup .is-set)
+o (ReaderC A mon) tt* = mon .ε
+_↓_ (ReaderC A mon) tt* a = tt*
+_⊕_ (ReaderC A mon) = mon ._·_
+unitl-↓ (ReaderC A mon) tt* = refl
+distr-↓-⊕ (ReaderC A mon) tt* a a' = refl
+unitl-⊕ (ReaderC A mon) tt* = mon .isMonoid .·IdL
+unitr-⊕ (ReaderC A mon) tt* = mon .isMonoid .·IdR
+assoc-⊕ (ReaderC A mon) tt* a a' i a'' = mon .isMonoid .·Assoc a a' a'' (~ i)
+
+StreamC : DirContainer {ℓs} {ℓ-zero} ((Unit* {ℓs}) ◁ (const ℕ) & isSetUnit* & isSetℕ)
+StreamC = ReaderC (fst NatMonoid) (snd NatMonoid)

Cubical/Algebra/DistributiveLaw.agda

@@ -0,0 +1,13 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.DistributiveLaw where
+
+open import Cubical.Algebra.DistributiveLaw.Base public
+
+open import Cubical.Algebra.DistributiveLaw.Mnd public
+open import Cubical.Algebra.DistributiveLaw.Dir public
+open import Cubical.Algebra.DistributiveLaw.MndDir public
+open import Cubical.Algebra.DistributiveLaw.DirMnd public
+
+open import Cubical.Algebra.DistributiveLaw.NoGoTheorem public
+

Cubical/Algebra/DistributiveLaw/Base.agda

@@ -0,0 +1,21 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.DistributiveLaw.Base where
+
+open import Cubical.Foundations.Prelude
+
+private
+  variable
+    ℓs ℓp ℓt ℓr ℓq : Level
+
+-- ⟨_,_⟩ notation - extremely dependent function pairing
+[_,_,_]⟨_,_⟩ : {S : Type ℓs} {T : Type ℓt} {R : Type ℓr}
+               (P : S → Type ℓp) (Q : T → Type ℓq) (s : S) (f : P s → T)
+               (g : (Σ[ p ∈ P s ] Q (f p)) → R) (x : P s) → Σ[ t ∈ T ] (Q t → R)
+[ P , Q , s ]⟨ f , g ⟩ x = (f x , λ y → g (x , y))
+
+-- A curried version of the above (i.e. where the second function can be curried)
+[_,_,_]⟨_,_⟩' : {S : Type ℓs} {T : Type ℓt} {R : Type ℓr} (P : S → Type ℓp)
+                (Q : T → Type ℓq) (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → R) (x : P s) →
+                Σ[ t ∈ T ] (Q t → R)
+[ P , Q , s ]⟨ f , g ⟩' x = (f x , g x)

Cubical/Algebra/DistributiveLaw/Dir.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.DistributiveLaw.Dir where
+
+open import Cubical.Algebra.DistributiveLaw.Dir.Base public

Cubical/Algebra/DistributiveLaw/Dir/Base.agda

@@ -0,0 +1,84 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.DistributiveLaw.Dir.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Algebra.DirContainer as DC
+open import Cubical.Algebra.DistributiveLaw.Base
+open import Cubical.Data.Containers.Set.Base
+
+open DC.DirContainer
+
+private
+  variable
+    ℓs ℓp : Level
+
+-- Distributive law direction: Aₘ ∘ Bₘ → Bₘ ∘ Aₘ
+record DirectedDistributiveLaw (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s))
+                               (T : Type ℓs) (Q : T → Type ℓp) (setT : isSet T) (setQ : ∀ {t} → isSet (Q t))
+                               (Aₘ : DirContainer (S ◁ P & setS & setP)) (Bₘ : DirContainer (T ◁ Q & setT & setQ)) :
+                               Type (ℓ-suc (ℓ-max ℓs ℓp)) where
+
+  _⊕ᵃ_ = _⊕_ Aₘ
+  _↓ᵃ_ = _↓_ Aₘ
+  _⊕ᵇ_ = _⊕_ Bₘ
+  _↓ᵇ_ = _↓_ Bₘ
+
+  field
+    u₁ : (s : S) (f : P s → T) → T
+    u₂ : (s : S) (f : P s → T) → Q (u₁ s f) → S
+
+    v₁ : {s : S} {f : P s → T} (q : Q (u₁ s f)) → P (u₂ s f q) → P s
+    v₂ : {s : S} {f : P s → T} (q : Q (u₁ s f)) (p : P (u₂ s f q)) → Q (f (v₁ q p))
+
+    unit-oA-shape : (s : S) (f : P s → T) → u₁ s f ≡ f (o Aₘ s)
+    unit-oA-pos₁ : (s : S) (f : P s → T) → 
+                   PathP (λ i → (q : Q (unit-oA-shape s f i)) → P s) 
+                         (λ q → v₁ q (o Aₘ (u₂ s f q))) 
+                         (λ q → o Aₘ s)
+    unit-oA-pos₂ : (s : S) (f : P s → T) →
+                   PathP (λ i → (q : Q (unit-oA-shape s f i)) → Q (f (unit-oA-pos₁ s f i q)))
+                         (λ q → v₂ q (o Aₘ (u₂ s f q)))
+                         (λ q → q)
+
+    mul-A-shape₁ : (s : S) (f : P s → T) → u₁ s f ≡ u₁ s (λ p → u₁ (s ↓ᵃ p) (λ p' → f (p ⊕ᵃ p')))
+    mul-A-shape₂ : (s : S) (f : P s → T) → 
+                   PathP (λ i → (q : Q (mul-A-shape₁ s f i)) → S) 
+                         (λ q → u₂ s f q)
+                         (λ q → u₂ s (λ p → u₁ (s ↓ᵃ p) (λ p' → f (p ⊕ᵃ p'))) q)
+    mul-A-shape₃ : (s : S) (f : P s → T) → 
+                   PathP (λ i → (q : Q (mul-A-shape₁ s f i)) (p : P (mul-A-shape₂ s f i q)) → S)
+                         (λ q p → u₂ s f q ↓ᵃ p) 
+                         (λ q p → u₂ (s ↓ᵃ v₁ q p) (λ p' → f (v₁ q p ⊕ᵃ p')) (v₂ q p))
+
+    mul-A-pos₁ : (s : S) (f : P s → T) →
+                 PathP (λ i → (q : Q (mul-A-shape₁ s f i)) (p : P (mul-A-shape₂ s f i q)) → P (mul-A-shape₃ s f i q p) → P s)
+                       (λ q p p' → v₁ q (p ⊕ᵃ p'))
+                       (λ q p p' → v₁ q p ⊕ᵃ v₁ (v₂ q p) p')
+    mul-A-pos₂ : (s : S) (f : P s → T) →
+                 PathP (λ i → (q : Q (mul-A-shape₁ s f i)) (p : P (mul-A-shape₂ s f i q)) → (p' : P (mul-A-shape₃ s f i q p)) → Q (f (mul-A-pos₁ s f i q p p')))
+                       (λ q p p' → v₂ q (p ⊕ᵃ p'))
+                       (λ q p p' → v₂ (v₂ q p) p')
+
+    unit-oB-shape : (s : S) (f : P s → T) → u₂ s f (o Bₘ _) ≡ s
+    unit-oB-pos₁ : (s : S) (f : P s → T) (p : P (u₂ s f (o Bₘ _))) → 
+                   PathP (λ i → P (unit-oB-shape s f (~ i))) 
+                   (v₁ (o Bₘ _) p)
+                   p
+    unit-oB-pos₂ : (s : S) (f : P s → T) (p : P (u₂ s f (o Bₘ _))) → v₂ (o Bₘ _) p ≡ o Bₘ _
+
+    mul-B-shape₁ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → u₁ s f ↓ᵇ q ≡ u₁ (u₂ s f q) (λ p → f (v₁ q p) ↓ᵇ v₂ q p)
+
+    mul-B-shape₂ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → 
+                   PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) → S)
+                         (λ q' → u₂ s f (q ⊕ᵇ q'))
+                         (λ q' → u₂ (u₂ s f q) ((λ p → f (v₁ q p) ↓ᵇ v₂ q p)) q')
+
+    mul-B-pos₁ : (s : S) (f : P s → T) (q : Q (u₁ s f)) →
+                 PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) (p : P (mul-B-shape₂ s f q i q')) → P s) 
+                       (λ q' p → v₁ (q ⊕ᵇ q') p)
+                       (λ q' p → v₁ q (v₁ q' p))
+    mul-B-pos₂ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → 
+                 PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) (p : P (mul-B-shape₂ s f q i q')) → Q (f (mul-B-pos₁ s f q i q' p))) 
+                       (λ q' p → v₂ (q ⊕ᵇ q') p) 
+                       (λ q' p → v₂ q (v₁ q' p) ⊕ᵇ (v₂ q' p))

Cubical/Algebra/DistributiveLaw/DirMnd.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.DistributiveLaw.DirMnd where
+
+open import Cubical.Algebra.DistributiveLaw.DirMnd.Base public

Cubical/Algebra/DistributiveLaw/DirMnd/Base.agda

@@ -0,0 +1,97 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.DistributiveLaw.DirMnd.Base where
+
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Prelude
+open import Cubical.Algebra.DirContainer as DC
+open import Cubical.Algebra.MndContainer as MC
+open import Cubical.Algebra.DistributiveLaw.Base
+open import Cubical.Data.Containers.Set.Base
+
+open DC.DirContainer
+open MC.MndContainer
+
+private
+  variable
+    ℓs ℓp : Level
+
+-- Distributive law direction: Aₘ ∘ Bₘ → Bₘ ∘ Aₘ
+record DirMndDistributiveLaw (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s))
+                             (T : Type ℓs) (Q : T → Type ℓp) (setT : isSet T) (setQ : ∀ {t} → isSet (Q t))
+                             (Aₘ : MndContainer (S ◁ P & setS & setP)) (Bₘ : DirContainer (T ◁ Q & setT & setQ)) :
+                             Type (ℓ-suc (ℓ-max ℓs ℓp)) where
+
+  _⊕ᵇ_ = _⊕_ Bₘ
+  _↓ᵇ_ = _↓_ Bₘ
+
+  field
+    u₁ : (s : S) (f : P s → T) → T
+    u₂ : (s : S) (f : P s → T) → Q (u₁ s f) → S
+
+    v₁ : {s : S} {f : P s → T} (q : Q (u₁ s f)) → P (u₂ s f q) → P s
+    v₂ : {s : S} {f : P s → T} (q : Q (u₁ s f)) (p : P (u₂ s f q)) → Q (f (v₁ q p))
+
+    unit-ιA-shape₁ : (t : T) → u₁ (ι Aₘ) (const t) ≡ t
+    unit-ιA-shape₂ : (t : T) → 
+                     PathP (λ i → (q : Q (unit-ιA-shape₁ t i)) → S)
+                           (u₂ (ι Aₘ) (const t)) 
+                           (const (ι Aₘ))
+
+    unit-ιA-pos₁ : (t : T) →
+                   PathP (λ i → (q : Q (unit-ιA-shape₁ t i)) → P (unit-ιA-shape₂ t i q) → P (ι Aₘ))
+                         v₁
+                         (λ q p → p)
+
+    unit-ιA-pos₂ : (t : T) →
+                   PathP (λ i → (q : Q (unit-ιA-shape₁ t i)) → P (unit-ιA-shape₂ t i q) → Q t)
+                         v₂
+                         (λ q p → q)
+
+    mul-A-shape₁ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) →
+                   u₁ (σ Aₘ s f) (uncurry g ∘ (pr Aₘ _ _)) ≡
+                   u₁ s (uncurry u₁ ∘ [ P , _ , _ ]⟨ f , g ⟩')
+
+    mul-A-shape₂ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) →
+                   PathP (λ i → Q (mul-A-shape₁ s f g i) → S)
+                         (λ q → (u₂ (σ Aₘ s f) (uncurry g ∘ pr Aₘ _ _)) q)
+                         (λ q → uncurry (σ Aₘ) ([ Q , P , _ ]⟨ u₂ s (uncurry u₁ ∘ [ P , _ , _ ]⟨ f , g ⟩') ,
+                                                               (λ q p → (uncurry u₂ ∘ [ P , _ , _ ]⟨ f , g ⟩') (v₁ q p) (v₂ q p)) ⟩' q))
+
+    mul-A-pos₁ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) →
+                 PathP (λ i → (q : Q (mul-A-shape₁ s f g i)) → P (mul-A-shape₂ s f g i q) → P s)
+                       (λ q p → pr₁ Aₘ s _ (v₁ q p))
+                       (λ q p → v₁ q (pr₁ Aₘ _ _ p))
+
+    mul-A-pos₂₁ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) →
+                  PathP (λ i → (q : Q (mul-A-shape₁ s f g i)) (p : P (mul-A-shape₂ s f g i q)) → P (f (mul-A-pos₁ s f g i q p)))
+                        (λ q p → pr₂ Aₘ _ _ (v₁ q p))
+                        (λ q p → v₁ (v₂ q (pr₁ Aₘ _ _ p)) (pr₂ Aₘ _ _ p))     
+
+    mul-A-pos₂₂ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) →
+                  PathP (λ i → (q : Q (mul-A-shape₁ s f g i)) (p : P (mul-A-shape₂ s f g i q)) → Q (g (mul-A-pos₁ s f g i q p) (mul-A-pos₂₁ s f g i q p)))
+                        (λ q p → v₂ q p) 
+                        (λ q p → v₂ (v₂ q (pr₁ Aₘ _ _ p)) (pr₂ Aₘ _ _ p))  
+
+    unit-oB-shape : (s : S) (f : P s → T) → u₂ s f (o Bₘ _) ≡ s
+    unit-oB-pos₁ : (s : S) (f : P s → T) (p : P (u₂ s f (o Bₘ _))) → 
+                   PathP (λ i → P (unit-oB-shape s f (~ i))) 
+                   (v₁ (o Bₘ _) p)
+                   p
+    unit-oB-pos₂ : (s : S) (f : P s → T) (p : P (u₂ s f (o Bₘ _))) → v₂ (o Bₘ _) p ≡ o Bₘ _
+
+    mul-B-shape₁ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → u₁ s f ↓ᵇ q ≡ u₁ (u₂ s f q) (λ p → f (v₁ q p) ↓ᵇ v₂ q p)
+
+    mul-B-shape₂ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → 
+                   PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) → S)
+                         (λ q' → u₂ s f (q ⊕ᵇ q'))
+                         (λ q' → u₂ (u₂ s f q) (λ p → f (v₁ q p) ↓ᵇ v₂ q p) q')
+
+    mul-B-pos₁ : (s : S) (f : P s → T) (q : Q (u₁ s f)) →
+                 PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) (p : P (mul-B-shape₂ s f q i q')) → P s) 
+                       (λ q' p → v₁ (q ⊕ᵇ q') p)
+                       (λ q' p → v₁ q (v₁ q' p))
+    mul-B-pos₂ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → 
+                 PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) (p : P (mul-B-shape₂ s f q i q')) → Q (f (mul-B-pos₁ s f q i q' p))) 
+                       (λ q' p → v₂ (q ⊕ᵇ q') p) 
+                       (λ q' p → v₂ q (v₁ q' p) ⊕ᵇ (v₂ q' p))

Cubical/Algebra/DistributiveLaw/Mnd.agda

@@ -0,0 +1,6 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.DistributiveLaw.Mnd where
+
+open import Cubical.Algebra.DistributiveLaw.Mnd.Base public
+open import Cubical.Algebra.DistributiveLaw.Mnd.Examples public