Skip to content

Commit be8636a

Browse files
arnoudvanderleerarnoudvanderleer
committed
Add functor currying
1 parent c3fa85a commit be8636a

File tree

3 files changed

+338
-0
lines changed

3 files changed

+338
-0
lines changed

‎src/category-theory.lagda.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,7 @@ open import category-theory.fully-faithful-functors-precategories public
7070
open import category-theory.fully-faithful-maps-precategories public
7171
open import category-theory.function-categories public
7272
open import category-theory.function-precategories public
73+
open import category-theory.functor-curry public
7374
open import category-theory.functors-categories public
7475
open import category-theory.functors-from-small-to-large-categories public
7576
open import category-theory.functors-from-small-to-large-precategories public

‎src/category-theory/functor-curry.lagda.md

Lines changed: 319 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,319 @@
1+
# The Currying of Functors on a Product Category
2+
3+
```agda
4+
module category-theory.functor-curry where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import category-theory.functors-precategories
11+
open import category-theory.maps-precategories
12+
open import category-theory.natural-transformations-functors-precategories
13+
open import category-theory.precategories
14+
open import category-theory.precategory-of-functors
15+
open import category-theory.products-of-precategories
16+
17+
open import foundation.action-on-identifications-functions
18+
open import foundation.cartesian-product-types
19+
open import foundation.dependent-pair-types
20+
open import foundation.identity-types
21+
open import foundation.universe-levels
22+
```
23+
24+
</details>
25+
26+
## Idea
27+
28+
In the context of sets, currying means that we can view a function
29+
`f : S × T → U` as a function `f : S → (T → U)`. We can view this as a function
30+
`curry : (S × T → U) → (S → T → U)`. In the context of categories, there is a
31+
similar situation: this file constructs the functor between functor categories
32+
33+
```text
34+
curry-functor : [C × D, E] → [C, [D, E]].
35+
```
36+
37+
## Definition
38+
39+
```agda
40+
module CurryFunctor
41+
{lc₁ lc₂ ld₁ ld₂ le₁ le₂ : Level}
42+
(C : Precategory lc₁ lc₂)
43+
(D : Precategory ld₁ ld₂)
44+
(E : Precategory le₁ le₂) where
45+
private
46+
CD = product-Precategory C D
47+
CDE1 = functor-precategory-Precategory CD E
48+
DE = functor-precategory-Precategory D E
49+
CDE2 = functor-precategory-Precategory C DE
50+
51+
module _
52+
(F : obj-Precategory CDE1)
53+
where
54+
55+
module _
56+
(c : obj-Precategory C)
57+
where
58+
59+
obj-obj-obj-curry-functor : obj-Precategory D → obj-Precategory E
60+
obj-obj-obj-curry-functor d = obj-functor-Precategory CD E F (c , d)
61+
62+
hom-obj-obj-curry-functor :
63+
{d₁ d₂ : obj-Precategory D}
64+
→ hom-Precategory D d₁ d₂
65+
→ hom-Precategory E
66+
(obj-obj-obj-curry-functor d₁)
67+
(obj-obj-obj-curry-functor d₂)
68+
hom-obj-obj-curry-functor f =
69+
hom-functor-Precategory CD E F (id-hom-Precategory C , f)
70+
71+
map-obj-obj-curry-functor : map-Precategory D E
72+
pr1 map-obj-obj-curry-functor = obj-obj-obj-curry-functor
73+
pr2 map-obj-obj-curry-functor = hom-obj-obj-curry-functor
74+
75+
opaque
76+
preserves-comp-obj-obj-curry-functor :
77+
preserves-comp-hom-map-Precategory D E map-obj-obj-curry-functor
78+
preserves-comp-obj-obj-curry-functor f g = equational-reasoning
79+
hom-functor-Precategory CD E F
80+
(id-hom-Precategory C , comp-hom-Precategory D f g)
81+
＝ hom-functor-Precategory CD E F (comp-hom-Precategory CD
82+
(id-hom-Precategory C , f) (id-hom-Precategory C , g))
83+
by ap (λ x → hom-functor-Precategory CD E F (x , _)) (inv
84+
(left-unit-law-comp-hom-Precategory C (id-hom-Precategory C)))
85+
＝ comp-hom-Precategory E
86+
(hom-functor-Precategory CD E F (id-hom-Precategory C , f))
87+
(hom-functor-Precategory CD E F (id-hom-Precategory C , g))
88+
by preserves-comp-functor-Precategory CD E F
89+
(id-hom-Precategory C , f)
90+
(id-hom-Precategory C , g)
91+
92+
preserves-id-obj-obj-curry-functor :
93+
preserves-id-hom-map-Precategory D E map-obj-obj-curry-functor
94+
preserves-id-obj-obj-curry-functor d =
95+
preserves-id-functor-Precategory CD E F (c , d)
96+
97+
obj-obj-curry-functor : obj-Precategory DE
98+
pr1 obj-obj-curry-functor = obj-obj-obj-curry-functor
99+
pr1 (pr2 obj-obj-curry-functor) = hom-obj-obj-curry-functor
100+
pr1 (pr2 (pr2 obj-obj-curry-functor)) =
101+
preserves-comp-obj-obj-curry-functor
102+
pr2 (pr2 (pr2 obj-obj-curry-functor)) = preserves-id-obj-obj-curry-functor
103+
104+
module _
105+
{c₁ c₂ : obj-Precategory C}
106+
(f : hom-Precategory C c₁ c₂)
107+
where
108+
109+
hom-hom-obj-curry-functor :
110+
(d : obj-Precategory D)
111+
→ hom-Precategory E
112+
(obj-obj-obj-curry-functor c₁ d)
113+
(obj-obj-obj-curry-functor c₂ d)
114+
hom-hom-obj-curry-functor d =
115+
hom-functor-Precategory CD E F (f , id-hom-Precategory D)
116+
117+
opaque
118+
is-natural-hom-obj-curry-functor :
119+
is-natural-transformation-Precategory D E
120+
(obj-obj-curry-functor c₁) (obj-obj-curry-functor c₂)
121+
hom-hom-obj-curry-functor
122+
is-natural-hom-obj-curry-functor {d₁} {d₂} g = equational-reasoning
123+
comp-hom-Precategory E
124+
(hom-obj-obj-curry-functor c₂ g)
125+
(hom-hom-obj-curry-functor d₁)
126+
＝ hom-functor-Precategory CD E F (comp-hom-Precategory CD
127+
(id-hom-Precategory C , g)
128+
(f , id-hom-Precategory D))
129+
by inv (preserves-comp-functor-Precategory CD E F
130+
(id-hom-Precategory C , g)
131+
(f , id-hom-Precategory D))
132+
＝ hom-functor-Precategory CD E F (comp-hom-Precategory CD
133+
(f , id-hom-Precategory D)
134+
(id-hom-Precategory C , g))
135+
by ap (hom-functor-Precategory CD E F) (identity-product
136+
(left-unit-law-comp-hom-Precategory C f
137+
∙ inv (right-unit-law-comp-hom-Precategory C f))
138+
(right-unit-law-comp-hom-Precategory D g
139+
∙ inv (left-unit-law-comp-hom-Precategory D g)))
140+
＝ comp-hom-Precategory E
141+
(hom-hom-obj-curry-functor d₂)
142+
(hom-obj-obj-curry-functor c₁ g)
143+
by preserves-comp-functor-Precategory CD E F
144+
(f , id-hom-Precategory D)
145+
(id-hom-Precategory C , g)
146+
147+
hom-obj-curry-functor :
148+
hom-Precategory DE (obj-obj-curry-functor c₁) (obj-obj-curry-functor c₂)
149+
pr1 hom-obj-curry-functor = hom-hom-obj-curry-functor
150+
pr2 hom-obj-curry-functor = is-natural-hom-obj-curry-functor
151+
152+
map-obj-curry-functor : map-Precategory C DE
153+
pr1 map-obj-curry-functor = obj-obj-curry-functor
154+
pr2 map-obj-curry-functor = hom-obj-curry-functor
155+
156+
opaque
157+
preserves-comp-obj-curry-functor :
158+
preserves-comp-hom-map-Precategory C DE map-obj-curry-functor
159+
preserves-comp-obj-curry-functor {c₁} {c₂} {c₃} f g =
160+
eq-htpy-hom-family-natural-transformation-Precategory
161+
D E
162+
(obj-obj-curry-functor c₁) (obj-obj-curry-functor c₃)
163+
(hom-obj-curry-functor (comp-hom-Precategory C f g))
164+
(comp-hom-Precategory DE
165+
{obj-obj-curry-functor c₁}
166+
{obj-obj-curry-functor c₂}
167+
{obj-obj-curry-functor c₃}
168+
(hom-obj-curry-functor f)
169+
(hom-obj-curry-functor g))
170+
(λ d → equational-reasoning
171+
hom-functor-Precategory CD E F
172+
(comp-hom-Precategory C f g , id-hom-Precategory D)
173+
＝ hom-functor-Precategory CD E F (comp-hom-Precategory CD
174+
(f , id-hom-Precategory D)
175+
(g , id-hom-Precategory D))
176+
by ap
177+
(λ h → hom-functor-Precategory CD E F
178+
(comp-hom-Precategory C f g , h))
179+
(inv
180+
(left-unit-law-comp-hom-Precategory D (id-hom-Precategory D)))
181+
＝ comp-hom-Precategory E
182+
(hom-functor-Precategory CD E F (f , id-hom-Precategory D))
183+
(hom-functor-Precategory CD E F (g , id-hom-Precategory D))
184+
by preserves-comp-functor-Precategory CD E F
185+
(f , id-hom-Precategory D)
186+
(g , id-hom-Precategory D))
187+
188+
preserves-id-obj-curry-functor :
189+
preserves-id-hom-map-Precategory C DE map-obj-curry-functor
190+
preserves-id-obj-curry-functor c =
191+
eq-htpy-hom-family-natural-transformation-Precategory
192+
D E
193+
(obj-obj-curry-functor c)
194+
(obj-obj-curry-functor c)
195+
(hom-obj-curry-functor (id-hom-Precategory C))
196+
(id-hom-Precategory DE {obj-obj-curry-functor c})
197+
(λ d → preserves-id-functor-Precategory CD E F (c , d))
198+
199+
obj-curry-functor : obj-Precategory CDE2
200+
pr1 obj-curry-functor = obj-obj-curry-functor
201+
pr1 (pr2 obj-curry-functor) = hom-obj-curry-functor
202+
pr1 (pr2 (pr2 obj-curry-functor)) = preserves-comp-obj-curry-functor
203+
pr2 (pr2 (pr2 obj-curry-functor)) = preserves-id-obj-curry-functor
204+
205+
module _
206+
{F₁ F₂ : obj-Precategory CDE1}
207+
(α : hom-Precategory CDE1 F₁ F₂)
208+
where
209+
210+
module _
211+
(c : obj-Precategory C)
212+
where
213+
214+
hom-hom-hom-curry-functor :
215+
(d : obj-Precategory D)
216+
→ hom-Precategory E
217+
(obj-obj-obj-curry-functor F₁ c d)
218+
(obj-obj-obj-curry-functor F₂ c d)
219+
hom-hom-hom-curry-functor d =
220+
hom-family-natural-transformation-Precategory CD E F₁ F₂ α (c , d)
221+
222+
opaque
223+
is-natural-hom-hom-curry-functor :
224+
is-natural-transformation-Precategory D E
225+
(obj-obj-curry-functor F₁ c) (obj-obj-curry-functor F₂ c)
226+
hom-hom-hom-curry-functor
227+
is-natural-hom-hom-curry-functor {d₁} {d₂} f =
228+
naturality-natural-transformation-Precategory CD E F₁ F₂ α
229+
(id-hom-Precategory C , f)
230+
231+
hom-hom-curry-functor :
232+
hom-Precategory DE
233+
(obj-obj-curry-functor F₁ c) (obj-obj-curry-functor F₂ c)
234+
pr1 hom-hom-curry-functor = hom-hom-hom-curry-functor
235+
pr2 hom-hom-curry-functor = is-natural-hom-hom-curry-functor
236+
237+
opaque
238+
is-natural-hom-curry-functor :
239+
is-natural-transformation-Precategory C DE
240+
(obj-curry-functor F₁) (obj-curry-functor F₂)
241+
hom-hom-curry-functor
242+
is-natural-hom-curry-functor {c₁} {c₂} f =
243+
eq-htpy-hom-family-natural-transformation-Precategory
244+
D E
245+
(obj-obj-curry-functor F₁ c₁) (obj-obj-curry-functor F₂ c₂)
246+
(comp-hom-Precategory DE
247+
{obj-obj-curry-functor F₁ c₁}
248+
{obj-obj-curry-functor F₂ c₁}
249+
{obj-obj-curry-functor F₂ c₂}
250+
(hom-obj-curry-functor F₂ f)
251+
(hom-hom-curry-functor c₁))
252+
(comp-hom-Precategory DE
253+
{obj-obj-curry-functor F₁ c₁}
254+
{obj-obj-curry-functor F₁ c₂}
255+
{obj-obj-curry-functor F₂ c₂}
256+
(hom-hom-curry-functor c₂)
257+
(hom-obj-curry-functor F₁ f))
258+
(λ d → naturality-natural-transformation-Precategory CD E F₁ F₂ α
259+
(f , id-hom-Precategory D))
260+
261+
hom-curry-functor :
262+
hom-Precategory CDE2 (obj-curry-functor F₁) (obj-curry-functor F₂)
263+
pr1 hom-curry-functor = hom-hom-curry-functor
264+
pr2 hom-curry-functor = is-natural-hom-curry-functor
265+
266+
map-curry-functor : map-Precategory CDE1 CDE2
267+
pr1 map-curry-functor = obj-curry-functor
268+
pr2 map-curry-functor {F₁} {F₂} = hom-curry-functor {F₁} {F₂}
269+
270+
opaque
271+
preserves-comp-curry-functor :
272+
preserves-comp-hom-map-Precategory CDE1 CDE2 map-curry-functor
273+
preserves-comp-curry-functor {F₁} {F₂} {F₃} α₁ α₂ =
274+
eq-htpy-hom-family-natural-transformation-Precategory
275+
C DE
276+
(obj-curry-functor F₁) (obj-curry-functor F₃)
277+
(hom-curry-functor {F₁} {F₃}
278+
(comp-hom-Precategory CDE1 {F₁} {F₂} {F₃} α₁ α₂))
279+
(comp-hom-Precategory CDE2
280+
{obj-curry-functor F₁}
281+
{obj-curry-functor F₂}
282+
{obj-curry-functor F₃}
283+
(hom-curry-functor {F₂} {F₃} α₁)
284+
(hom-curry-functor {F₁} {F₂} α₂))
285+
(λ c → eq-htpy-hom-family-natural-transformation-Precategory
286+
D E
287+
(obj-obj-curry-functor F₁ c) (obj-obj-curry-functor F₃ c)
288+
(hom-hom-curry-functor {F₁} {F₃}
289+
(comp-hom-Precategory CDE1 {F₁} {F₂} {F₃} α₁ α₂) c)
290+
(comp-hom-Precategory DE
291+
{obj-obj-curry-functor F₁ c}
292+
{obj-obj-curry-functor F₂ c}
293+
{obj-obj-curry-functor F₃ c}
294+
(hom-hom-curry-functor {F₂} {F₃} α₁ c)
295+
(hom-hom-curry-functor {F₁} {F₂} α₂ c))
296+
(λ d → refl))
297+
298+
preserves-id-curry-functor :
299+
preserves-id-hom-map-Precategory CDE1 CDE2 map-curry-functor
300+
preserves-id-curry-functor F =
301+
eq-htpy-hom-family-natural-transformation-Precategory
302+
C DE
303+
(obj-curry-functor F) (obj-curry-functor F)
304+
(hom-curry-functor {F} {F} (id-hom-Precategory CDE1 {F}))
305+
(id-hom-Precategory CDE2 {obj-curry-functor F})
306+
(λ c → eq-htpy-hom-family-natural-transformation-Precategory
307+
D E
308+
(obj-obj-curry-functor F c) (obj-obj-curry-functor F c)
309+
(hom-hom-curry-functor {F} {F} (id-hom-Precategory CDE1 {F}) c)
310+
(id-hom-Precategory DE {obj-obj-curry-functor F c})
311+
(λ d → refl))
312+
313+
curry-functor : functor-Precategory CDE1 CDE2
314+
pr1 curry-functor = obj-curry-functor
315+
pr1 (pr2 curry-functor) {F₁} {F₂} = hom-curry-functor {F₁} {F₂}
316+
pr1 (pr2 (pr2 curry-functor)) {F₁} {F₂} {F₃} =
317+
preserves-comp-curry-functor {F₁} {F₂} {F₃}
318+
pr2 (pr2 (pr2 curry-functor)) = preserves-id-curry-functor
319+
```

‎src/foundation/cartesian-product-types.lagda.md

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,24 @@ tr-product :
3131
tr-product B C refl u = refl
3232
```
3333

34+
### Identities of products
35+
36+
```agda
37+
identity-product :
38+
{l1 l2 : Level}
39+
{A : UU l1} {B : UU l2}
40+
{a a' : A} {b b' : B}
41+
→ a ＝ a' → b ＝ b' → (a , b) ＝ (a' , b')
42+
identity-product refl refl = refl
43+
44+
identity-product' :
45+
{l1 l2 : Level}
46+
{A : UU l1} {B : UU l2}
47+
{ab ab' : A × B}
48+
→ pr1 ab ＝ pr1 ab' → pr2 ab ＝ pr2 ab' → ab ＝ ab'
49+
identity-product' refl refl = refl
50+
```
51+
3452
### Subuniverses closed under cartesian product types
3553

3654
```agda

0 commit comments

Comments
 (0)