Skip to content

Commit 8a39e48

Browse files
ben-connorsben-connors
authored
Dualize limits, right Kan extensions, and monads (#1442)
This explicitly dualizes limits, right Kan extensions, and monads. The definitions and proofs are exactly dual, save for certain parts of cocones where re-use of `coherence-triangle-hom-Precategory` meant a rotation was needed. This also fixes a minor indendation problem in monads.
1 parent 8749a19 commit 8a39e48

22 files changed

+2948
-128
lines changed

‎src/category-theory.lagda.md

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,22 +25,28 @@ open import category-theory.category-of-functors public
2525
open import category-theory.category-of-functors-from-small-to-large-categories public
2626
open import category-theory.category-of-maps-categories public
2727
open import category-theory.category-of-maps-from-small-to-large-categories public
28+
open import category-theory.coalgebras-comonads-on-precategories public
29+
open import category-theory.cocones-precategories public
2830
open import category-theory.codensity-monads-on-precategories public
31+
open import category-theory.colimits-precategories public
2932
open import category-theory.commuting-squares-of-morphisms-in-large-precategories public
3033
open import category-theory.commuting-squares-of-morphisms-in-precategories public
3134
open import category-theory.commuting-squares-of-morphisms-in-set-magmoids public
3235
open import category-theory.commuting-triangles-of-morphisms-in-precategories public
3336
open import category-theory.commuting-triangles-of-morphisms-in-set-magmoids public
37+
open import category-theory.comonads-on-precategories public
3438
open import category-theory.complete-precategories public
3539
open import category-theory.composition-operations-on-binary-families-of-sets public
3640
open import category-theory.cones-precategories public
3741
open import category-theory.conservative-functors-precategories public
3842
open import category-theory.constant-functors public
43+
open import category-theory.copointed-endofunctors-precategories public
3944
open import category-theory.copresheaf-categories public
4045
open import category-theory.coproducts-in-precategories public
4146
open import category-theory.cores-categories public
4247
open import category-theory.cores-precategories public
4348
open import category-theory.coslice-precategories public
49+
open import category-theory.density-comonads-on-precategories public
4450
open import category-theory.dependent-composition-operations-over-precategories public
4551
open import category-theory.dependent-products-of-categories public
4652
open import category-theory.dependent-products-of-large-categories public
@@ -102,6 +108,8 @@ open import category-theory.large-function-precategories public
102108
open import category-theory.large-precategories public
103109
open import category-theory.large-subcategories public
104110
open import category-theory.large-subprecategories public
111+
open import category-theory.left-extensions-precategories public
112+
open import category-theory.left-kan-extensions-precategories public
105113
open import category-theory.limits-precategories public
106114
open import category-theory.maps-categories public
107115
open import category-theory.maps-from-small-to-large-categories public
@@ -112,6 +120,7 @@ open import category-theory.monads-on-categories public
112120
open import category-theory.monads-on-precategories public
113121
open import category-theory.monomorphisms-in-large-precategories public
114122
open import category-theory.morphisms-algebras-monads-on-precategories public
123+
open import category-theory.morphisms-coalgebras-comonads-on-precategories public
115124
open import category-theory.natural-isomorphisms-functors-categories public
116125
open import category-theory.natural-isomorphisms-functors-large-precategories public
117126
open import category-theory.natural-isomorphisms-functors-precategories public
@@ -138,6 +147,7 @@ open import category-theory.pointed-endofunctors-categories public
138147
open import category-theory.pointed-endofunctors-precategories public
139148
open import category-theory.precategories public
140149
open import category-theory.precategory-of-algebras-monads-on-precategories public
150+
open import category-theory.precategory-of-coalgebras-comonads-on-precategories public
141151
open import category-theory.precategory-of-elements-of-a-presheaf public
142152
open import category-theory.precategory-of-free-algebras-monads-on-precategories public
143153
open import category-theory.precategory-of-functors public

‎src/category-theory/algebras-monads-on-precategories.lagda.md

Lines changed: 22 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -41,34 +41,36 @@ object `A` and morphism `a : TA → A` satisfying two compatibility laws:
4141
module _
4242
{l1 l2 : Level} (C : Precategory l1 l2)
4343
(T : monad-Precategory C)
44+
{A : obj-Precategory C}
45+
(a : hom-Precategory C (obj-endofunctor-monad-Precategory C T A) A)
4446
where
4547
46-
module _
47-
{A : obj-Precategory C}
48-
(a : hom-Precategory C (obj-endofunctor-monad-Precategory C T A) A)
49-
where
48+
has-unit-law-algebra-monad-Precategory : UU l2
49+
has-unit-law-algebra-monad-Precategory =
50+
comp-hom-Precategory C a (hom-unit-monad-Precategory C T A) ＝
51+
id-hom-Precategory C
5052
51-
has-unit-law-algebra-monad-Precategory : UU l2
52-
has-unit-law-algebra-monad-Precategory =
53-
comp-hom-Precategory C a (hom-unit-monad-Precategory C T A) ＝
54-
id-hom-Precategory C
53+
has-mul-law-algebra-monad-Precategory : UU l2
54+
has-mul-law-algebra-monad-Precategory =
55+
comp-hom-Precategory C a (hom-endofunctor-monad-Precategory C T a) ＝
56+
comp-hom-Precategory C a (hom-mul-monad-Precategory C T A)
5557
56-
has-mul-law-algebra-monad-Precategory : UU l2
57-
has-mul-law-algebra-monad-Precategory =
58-
comp-hom-Precategory C a (hom-endofunctor-monad-Precategory C T a) ＝
59-
comp-hom-Precategory C a (hom-mul-monad-Precategory C T A)
58+
is-algebra-monad-Precategory : UU l2
59+
is-algebra-monad-Precategory =
60+
has-unit-law-algebra-monad-Precategory ×
61+
has-mul-law-algebra-monad-Precategory
6062
61-
is-algebra-monad-Precategory : UU l2
62-
is-algebra-monad-Precategory =
63-
has-unit-law-algebra-monad-Precategory ×
64-
has-mul-law-algebra-monad-Precategory
63+
module _
64+
{l1 l2 : Level} (C : Precategory l1 l2)
65+
(T : monad-Precategory C)
66+
where
6567
6668
algebra-monad-Precategory : UU (l1 ⊔ l2)
6769
algebra-monad-Precategory =
6870
Σ ( obj-Precategory C)
6971
( λ A →
7072
Σ ( hom-Precategory C (obj-endofunctor-monad-Precategory C T A) A)
71-
( λ a → is-algebra-monad-Precategory a))
73+
( λ a → is-algebra-monad-Precategory C T a))
7274
7375
obj-algebra-monad-Precategory : algebra-monad-Precategory → obj-Precategory C
7476
obj-algebra-monad-Precategory = pr1
@@ -82,16 +84,16 @@ module _
8284
8385
comm-algebra-monad-Precategory :
8486
(f : algebra-monad-Precategory) →
85-
is-algebra-monad-Precategory (hom-algebra-monad-Precategory f)
87+
is-algebra-monad-Precategory C T (hom-algebra-monad-Precategory f)
8688
comm-algebra-monad-Precategory f = pr2 (pr2 f)
8789
8890
unit-law-algebra-monad-Precategory :
8991
(f : algebra-monad-Precategory) →
90-
has-unit-law-algebra-monad-Precategory (hom-algebra-monad-Precategory f)
92+
has-unit-law-algebra-monad-Precategory C T (hom-algebra-monad-Precategory f)
9193
unit-law-algebra-monad-Precategory f = pr1 (pr2 (pr2 f))
9294
9395
mul-law-algebra-monad-Precategory :
9496
(f : algebra-monad-Precategory) →
95-
has-mul-law-algebra-monad-Precategory (hom-algebra-monad-Precategory f)
97+
has-mul-law-algebra-monad-Precategory C T (hom-algebra-monad-Precategory f)
9698
mul-law-algebra-monad-Precategory f = pr2 (pr2 (pr2 f))
9799
```

‎src/category-theory/coalgebras-comonads-on-precategories.lagda.md

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
# Coalgebras over comonads on precategories
2+
3+
```agda
4+
module category-theory.coalgebras-comonads-on-precategories where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import category-theory.commuting-squares-of-morphisms-in-precategories
11+
open import category-theory.comonads-on-precategories
12+
open import category-theory.functors-precategories
13+
open import category-theory.natural-transformations-functors-precategories
14+
open import category-theory.natural-transformations-maps-precategories
15+
open import category-theory.precategories
16+
17+
open import foundation.action-on-identifications-functions
18+
open import foundation.dependent-pair-types
19+
open import foundation.identity-types
20+
open import foundation.sets
21+
open import foundation.universe-levels
22+
23+
open import foundation-core.cartesian-product-types
24+
```
25+
26+
</details>
27+
28+
## Idea
29+
30+
A
31+
{{#concept "coalgebra" Disambiguation="over a comonad on a precategory" Agda=coalgebra-comonad-Precategory}}
32+
over a [comonad](category-theory.comonads-on-precategories.md) `T` consists of
33+
an object `A` and morphism `a : A → TA` satisfying two compatibility laws:
34+
35+
- **Counit law**: `ε_A ∘ a = id_A`
36+
- **Comultiplication law**: `Ta ∘ a = δ ∘ a`
37+
38+
## Definitions
39+
40+
```agda
41+
module _
42+
{l1 l2 : Level} (C : Precategory l1 l2)
43+
(T : comonad-Precategory C)
44+
{A : obj-Precategory C}
45+
(a : hom-Precategory C A (obj-endofunctor-comonad-Precategory C T A))
46+
where
47+
48+
has-counit-law-coalgebra-comonad-Precategory : UU l2
49+
has-counit-law-coalgebra-comonad-Precategory =
50+
comp-hom-Precategory C (hom-counit-comonad-Precategory C T A) a ＝
51+
id-hom-Precategory C
52+
53+
has-comul-law-coalgebra-comonad-Precategory : UU l2
54+
has-comul-law-coalgebra-comonad-Precategory =
55+
comp-hom-Precategory C (hom-endofunctor-comonad-Precategory C T a) a ＝
56+
comp-hom-Precategory C (hom-comul-comonad-Precategory C T A) a
57+
58+
is-coalgebra-comonad-Precategory : UU l2
59+
is-coalgebra-comonad-Precategory =
60+
has-counit-law-coalgebra-comonad-Precategory ×
61+
has-comul-law-coalgebra-comonad-Precategory
62+
63+
module _
64+
{l1 l2 : Level} (C : Precategory l1 l2)
65+
(T : comonad-Precategory C)
66+
where
67+
68+
coalgebra-comonad-Precategory : UU (l1 ⊔ l2)
69+
coalgebra-comonad-Precategory =
70+
Σ ( obj-Precategory C)
71+
( λ A →
72+
Σ ( hom-Precategory C A (obj-endofunctor-comonad-Precategory C T A))
73+
( λ a → is-coalgebra-comonad-Precategory C T a))
74+
75+
obj-coalgebra-comonad-Precategory :
76+
coalgebra-comonad-Precategory → obj-Precategory C
77+
obj-coalgebra-comonad-Precategory = pr1
78+
79+
hom-coalgebra-comonad-Precategory :
80+
(f : coalgebra-comonad-Precategory) →
81+
hom-Precategory C
82+
( obj-coalgebra-comonad-Precategory f)
83+
( obj-endofunctor-comonad-Precategory C T
84+
( obj-coalgebra-comonad-Precategory f))
85+
hom-coalgebra-comonad-Precategory f = pr1 (pr2 f)
86+
87+
comm-coalgebra-comonad-Precategory :
88+
(f : coalgebra-comonad-Precategory) →
89+
is-coalgebra-comonad-Precategory C T (hom-coalgebra-comonad-Precategory f)
90+
comm-coalgebra-comonad-Precategory f = pr2 (pr2 f)
91+
92+
counit-law-coalgebra-comonad-Precategory :
93+
(f : coalgebra-comonad-Precategory) →
94+
has-counit-law-coalgebra-comonad-Precategory C T
95+
( hom-coalgebra-comonad-Precategory f)
96+
counit-law-coalgebra-comonad-Precategory f = pr1 (pr2 (pr2 f))
97+
98+
comul-law-coalgebra-comonad-Precategory :
99+
(f : coalgebra-comonad-Precategory) →
100+
has-comul-law-coalgebra-comonad-Precategory C T
101+
( hom-coalgebra-comonad-Precategory f)
102+
comul-law-coalgebra-comonad-Precategory f = pr2 (pr2 (pr2 f))
103+
```

0 commit comments

Comments
 (0)