Skip to content

Commit 5a4dfe7

Browse files
JacquesCaretteJacquesCarette
authored
Merge pull request #477 from Taneb/distributive-monads
Add distributive monads and comonads
2 parents c2e7c13 + 2e29bb6 commit 5a4dfe7

File tree

2 files changed

+191
-0
lines changed

2 files changed

+191
-0
lines changed

‎src/Categories/Comonad/Distributive.agda‎

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
open import Categories.Category.Core using (Category)
4+
open import Categories.Functor using (Endofunctor; Functor)
5+
6+
module Categories.Comonad.Distributive {o ℓ e} (C : Category o ℓ e) (F : Endofunctor C) where
7+
8+
open import Categories.Category.Construction.F-Algebras using (F-Algebras)
9+
open import Categories.Comonad using (Comonad) renaming (id to idW)
10+
open import Categories.Functor.Algebra using (F-Algebra; F-Algebra-Morphism)
11+
open import Categories.Functor.DistributiveLaw using (DistributiveLaw)
12+
open import Categories.Functor.Properties using ([_]-resp-square)
13+
open import Categories.Morphism.Reasoning C
14+
open import Categories.NaturalTransformation using (NaturalTransformation)
15+
16+
open import Level using (_⊔_)
17+
18+
private
19+
module C = Category C
20+
module F = Functor F
21+
22+
open C using (_∘_; _≈_)
23+
open C.HomReasoning
24+
25+
record DistributiveComonad : Set (o ⊔ ℓ ⊔ e) where
26+
field
27+
comonad : Comonad C
28+
open Comonad comonad public renaming (F to N; module F to N)
29+
field
30+
distrib : DistributiveLaw F N
31+
module distrib = NaturalTransformation distrib
32+
33+
field
34+
ε-distrib : ∀ {A} → ε.η (F.₀ A) ∘ distrib.η A ≈ F.₁ (ε.η A)
35+
δ-distrib : ∀ {A} → δ.η (F.₀ A) ∘ distrib.η A ≈ N.₁ (distrib.η A) ∘ distrib.η (N.₀ A) ∘ F.₁ (δ.η A)
36+
37+
-- An F-distributive comonad lifts to a comonad on F-algebras
38+
lifted : Comonad (F-Algebras F)
39+
lifted = record
40+
{ F = record
41+
{ F₀ = λ X → record
42+
{ A = N.₀ (F-Algebra.A X)
43+
; α = N.₁ (F-Algebra.α X) ∘ distrib.η _
44+
}
45+
; F₁ = λ f → record
46+
{ f = N.₁ (F-Algebra-Morphism.f f)
47+
; commutes = glue′
48+
([ N ]-resp-square (F-Algebra-Morphism.commutes f))
49+
(distrib.sym-commute (F-Algebra-Morphism.f f))
50+
}
51+
; identity = N.identity
52+
; homomorphism = N.homomorphism
53+
; F-resp-≈ = N.F-resp-≈
54+
}
55+
; ε = record
56+
{ η = λ X → record
57+
{ f = ε.η _
58+
; commutes = glue◽◃ (ε.commute _) ε-distrib
59+
}
60+
; commute = λ f → ε.commute _
61+
; sym-commute = λ f → ε.sym-commute _
62+
}
63+
; δ = record
64+
{ η = λ X → record
65+
{ f = δ.η _
66+
; commutes = begin
67+
δ.η _ ∘ (N.₁ _ ∘ distrib.η _) ≈⟨ pullˡ (δ.commute _) ⟩
68+
(N.₁ (N.₁ _) ∘ δ.η _) ∘ distrib.η _ ≈⟨ pullʳ δ-distrib ⟩
69+
N.₁ (N.₁ _) ∘ (N.₁ (distrib.η _) ∘ (distrib.η _ ∘ F.₁ (δ.η _))) ≈⟨ pullˡ (C.Equiv.sym N.homomorphism) ⟩
70+
N.₁ (N.₁ _ ∘ distrib.η _) ∘ (distrib.η _ ∘ F.₁ (δ.η _)) ≈⟨ C.sym-assoc ⟩
71+
(N.₁ (N.₁ _ ∘ distrib.η _) ∘ distrib.η _) ∘ F.₁ (δ.η _) ∎
72+
}
73+
; commute = λ f → δ.commute _
74+
; sym-commute = λ f → δ.sym-commute _
75+
}
76+
; assoc = assoc
77+
; sym-assoc = sym-assoc
78+
; identityˡ = identityˡ
79+
; identityʳ = identityʳ
80+
}
81+
82+
-- The identity comonad distributes over any endofunctor
83+
id : DistributiveComonad
84+
id = record
85+
{ comonad = idW C
86+
; distrib = record
87+
{ η = λ X → C.id
88+
; commute = λ _ → id-comm-sym
89+
; sym-commute = λ _ → id-comm
90+
}
91+
; ε-distrib = begin
92+
C.id C.∘ C.id ≈⟨ C.identity² ⟩
93+
C.id ≈⟨ F.identity ⟨
94+
F.₁ C.id ∎
95+
; δ-distrib = C.∘-resp-≈ʳ (introʳ F.identity)
96+
}

‎src/Categories/Monad/Distributive.agda‎

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
open import Categories.Category.Core using (Category)
4+
open import Categories.Functor using (Endofunctor; Functor)
5+
6+
module Categories.Monad.Distributive {o ℓ e} (C : Category o ℓ e) (F : Endofunctor C) where
7+
8+
open import Categories.Category.Construction.F-Coalgebras using (F-Coalgebras)
9+
open import Categories.Functor.Coalgebra using (F-Coalgebra; F-Coalgebra-Morphism)
10+
open import Categories.Functor.DistributiveLaw using (DistributiveLaw)
11+
open import Categories.Functor.Properties using ([_]-resp-square)
12+
open import Categories.Monad using (Monad) renaming (id to idM)
13+
open import Categories.Morphism.Reasoning C
14+
open import Categories.NaturalTransformation using (NaturalTransformation)
15+
open import Level using (_⊔_)
16+
17+
private
18+
module C = Category C
19+
module F = Functor F
20+
21+
open C using (_∘_; _≈_)
22+
open C.HomReasoning
23+
24+
record DistributiveMonad : Set (o ⊔ ℓ ⊔ e) where
25+
field
26+
monad : Monad C
27+
open Monad monad public renaming (F to N; module F to N)
28+
field
29+
distrib : DistributiveLaw N F
30+
module distrib = NaturalTransformation distrib
31+
32+
field
33+
η-distrib : ∀ {A} → distrib.η A ∘ η.η (F.F₀ A) ≈ F.₁ (η.η A)
34+
μ-distrib : ∀ {A} → distrib.η A ∘ μ.η (F.₀ A) ≈ (F.₁ (μ.η A) ∘ distrib.η (N.₀ A)) ∘ N.₁ (distrib.η A)
35+
36+
-- An F-distributive monad lifts to a monad on F-coalgebras
37+
lifted : Monad (F-Coalgebras F)
38+
lifted = record
39+
{ F = record
40+
{ F₀ = λ X → record
41+
{ A = N.₀ (F-Coalgebra.A X)
42+
; α = distrib.η _ ∘ N.₁ (F-Coalgebra.α X)
43+
}
44+
; F₁ = λ f → record
45+
{ f = N.₁ (F-Coalgebra-Morphism.f f)
46+
; commutes = glue
47+
(distrib.commute (F-Coalgebra-Morphism.f f))
48+
([ N ]-resp-square (F-Coalgebra-Morphism.commutes f))
49+
}
50+
; identity = N.identity
51+
; homomorphism = N.homomorphism
52+
; F-resp-≈ = N.F-resp-≈
53+
}
54+
; η = record
55+
{ η = λ X → record
56+
{ f = η.η _
57+
; commutes = glue◃◽ η-distrib (η.sym-commute _)
58+
}
59+
; commute = λ _ → η.commute _
60+
; sym-commute = λ _ → η.sym-commute _
61+
}
62+
; μ = record
63+
{ η = λ X → record
64+
{ f = μ.η _
65+
; commutes = begin
66+
(distrib.η _ ∘ N.₁ _) ∘ μ.η _ ≈⟨ pullʳ (μ.sym-commute _) ⟩
67+
distrib.η _ ∘ (μ.η _ ∘ N.₁ (N.₁ _)) ≈⟨ pullˡ μ-distrib ⟩
68+
((F.₁ (μ.η _) ∘ distrib.η _) ∘ N.₁ (distrib.η _)) ∘ N.₁ (N.₁ _) ≈⟨ pullʳ (C.Equiv.sym N.homomorphism) ⟩
69+
(F.₁ (μ.η _) ∘ distrib.η _) ∘ N.₁ (distrib.η _ ∘ N.₁ _) ≈⟨ C.assoc ⟩
70+
F.₁ (μ.η _) ∘ distrib.η _ ∘ N.₁ (distrib.η _ ∘ N.₁ _) ∎
71+
}
72+
; commute = λ _ → μ.commute _
73+
; sym-commute = λ _ → μ.sym-commute _
74+
}
75+
; assoc = assoc
76+
; sym-assoc = sym-assoc
77+
; identityˡ = identityˡ
78+
; identityʳ = identityʳ
79+
}
80+
81+
-- The identity monad distributes over any functor
82+
id : DistributiveMonad
83+
id = record
84+
{ monad = idM C
85+
; distrib = record
86+
{ η = λ _ → C.id
87+
; commute = λ _ → id-comm-sym
88+
; sym-commute = λ _ → id-comm
89+
}
90+
; η-distrib = begin
91+
C.id C.∘ C.id ≈⟨ C.identity² ⟩
92+
C.id ≈⟨ F.identity ⟨
93+
F.₁ C.id ∎
94+
; μ-distrib = C.∘-resp-≈ˡ (introˡ F.identity)
95+
}

0 commit comments

Comments
 (0)