Comonads¶
Comonad definitions with counits, comultiplications, and comonad laws.
comonads
¶
Comonads and coKleisli categories on V-enriched FinSet.
A comonad (W, ε, δ) consists of an endofunctor W, a counit ε: W ⇒ Id, and a comultiplication δ: W ⇒ W² satisfying:
W(δ) ∘ δ = δ_W ∘ δ (coassociativity)
ε_W ∘ δ = id (left counit)
W(ε) ∘ δ = id (right counit)
The coKleisli category of a comonad has the same objects but morphisms A → B are morphisms W(A) → B in the base category, composed via:
f =>> g = g ∘ W(f) ∘ δ_A
This module provides:
Comonad (abstract)
├── CofreeComonad — cofree comonad from a functor
└── DiagonalComonad — W(A) = A × A with diagonal/projection
CoKleisliCategory — wraps a comonad for composition
Comonad
¶
Bases: ABC
Abstract comonad (W, ε, δ) on V-enriched FinSet.
Subclasses must implement endofunctor, counit, and comultiply. CoKleisli composition is derived.
counit
abstractmethod
¶
The counit component ε_A: W(A) → A.
| PARAMETER | DESCRIPTION |
|---|---|
obj
|
The object A.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Morphism
|
The counit morphism ε_A. |
Source code in src/quivers/monadic/comonads.py
46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 | |
comultiply
abstractmethod
¶
The comultiplication component δ_A: W(A) → W(W(A)).
| PARAMETER | DESCRIPTION |
|---|---|
obj
|
The object A.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Morphism
|
The comultiplication morphism δ_A. |
Source code in src/quivers/monadic/comonads.py
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 | |
cokleisli_compose
¶
CoKleisli composition: f =>> g = g ∘ W(f) ∘ δ_A.
For f: W(A) → B and g: W(B) → C, produces W(A) → C.
| PARAMETER | DESCRIPTION |
|---|---|
f
|
Left coKleisli morphism W(A) → B.
TYPE:
|
g
|
Right coKleisli morphism W(B) → C.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Morphism
|
Composed coKleisli morphism W(A) → C. |
Source code in src/quivers/monadic/comonads.py
78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 | |
CoKleisliCategory
¶
CoKleisliCategory(comonad: Comonad)
The coKleisli category of a comonad.
Objects are the same as the base category. Morphisms A → B in the coKleisli category are morphisms W(A) → B in the base category.
| PARAMETER | DESCRIPTION |
|---|---|
comonad
|
The underlying comonad.
TYPE:
|
Source code in src/quivers/monadic/comonads.py
132 133 | |
identity
¶
CoKleisli identity at object A: ε_A: W(A) → A.
| PARAMETER | DESCRIPTION |
|---|---|
obj
|
The object A.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Morphism
|
The coKleisli identity morphism. |
Source code in src/quivers/monadic/comonads.py
140 141 142 143 144 145 146 147 148 149 150 151 152 153 | |
compose
¶
CoKleisli composition: f =>> g.
| PARAMETER | DESCRIPTION |
|---|---|
f
|
Left morphism W(A) → B.
TYPE:
|
g
|
Right morphism W(B) → C.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Morphism
|
Composed morphism W(A) → C. |
Source code in src/quivers/monadic/comonads.py
155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 | |
DiagonalComonad
¶
DiagonalComonad(quantale: Quantale | None = None)
Bases: Comonad
The diagonal comonad W(A) = A × A with projection and diagonal.
ε_A: A × A → A is the first projection. δ_A: A × A → (A × A) × (A × A) is the diagonal on pairs.
This comonad models "contexts" where each element has access to a pair of values. It arises from the product adjunction Δ ⊣ ×.
| PARAMETER | DESCRIPTION |
|---|---|
quantale
|
The enrichment algebra. Defaults to PRODUCT_FUZZY.
TYPE:
|
Source code in src/quivers/monadic/comonads.py
189 190 191 | |
counit
¶
ε_A: A × A → A is first projection.
| PARAMETER | DESCRIPTION |
|---|---|
obj
|
The object A.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ObservedMorphism
|
The projection morphism. |
Source code in src/quivers/monadic/comonads.py
203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 | |
comultiply
¶
δ_A: A × A → (A × A) × (A × A) is diagonal on pairs.
Maps (a1, a2) to ((a1, a2), (a1, a2)).
| PARAMETER | DESCRIPTION |
|---|---|
obj
|
The object A.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ObservedMorphism
|
The comultiplication morphism. |
Source code in src/quivers/monadic/comonads.py
225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 | |
cokleisli_compose
¶
CoKleisli composition using the diagonal comonad.
Source code in src/quivers/monadic/comonads.py
252 253 254 255 256 | |
CofreeComonad
¶
Bases: Comonad
The cofree comonad W(A) = A × S for a fixed store object S.
Also known as the "store comonad" or "costate comonad" on finite sets.
ε_A: A × S → A is the first projection (extract the value). δ_A: A × S → (A × S) × S duplicates the store component.
| PARAMETER | DESCRIPTION |
|---|---|
store
|
The fixed store/environment object S.
TYPE:
|
quantale
|
The enrichment algebra. Defaults to PRODUCT_FUZZY.
TYPE:
|
Source code in src/quivers/monadic/comonads.py
299 300 301 302 | |
counit
¶
ε_A: A × S → A is the first projection.
| PARAMETER | DESCRIPTION |
|---|---|
obj
|
The object A.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ObservedMorphism
|
The extraction morphism. |
Source code in src/quivers/monadic/comonads.py
319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 | |
comultiply
¶
δ_A: A × S → (A × S) × S duplicates the store.
Maps (a, s) to ((a, s), s).
| PARAMETER | DESCRIPTION |
|---|---|
obj
|
The object A.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ObservedMorphism
|
The comultiplication morphism. |
Source code in src/quivers/monadic/comonads.py
341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 | |