Skip to content

Commit

Permalink
prepend map- to (obj/hom)-functor
Browse files Browse the repository at this point in the history
  • Loading branch information
@fredrik-bakke
fredrik-bakke committed Sep 18, 2023
1 parent 43ee8e8 commit 08af608
Show file tree
Hide file tree
Showing 11 changed files with 143 additions and 142 deletions.
36 changes: 18 additions & 18 deletions src/category-theory/adjunctions-large-precategories.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,8 +59,8 @@ module _
equiv-is-adjoint-pair-Large-Precategory :
{l1 l2 : Level} (X : obj-Large-Precategory C l1)
(Y : obj-Large-Precategory D l2) →
( type-hom-Large-Precategory C X (obj-functor-Large-Precategory G Y)) ≃
( type-hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y)
( type-hom-Large-Precategory C X (map-obj-functor-Large-Precategory G Y)) ≃
( type-hom-Large-Precategory D (map-obj-functor-Large-Precategory F X) Y)
naturality-equiv-is-adjoint-pair-Large-Precategory :
{ l1 l2 l3 l4 : Level}
{ X1 : obj-Large-Precategory C l1} {X2 : obj-Large-Precategory C l2}
Expand All @@ -72,37 +72,37 @@ module _
( λ h →
comp-hom-Large-Precategory C
( comp-hom-Large-Precategory C
( hom-functor-Large-Precategory G g) h)
( map-hom-functor-Large-Precategory G g) h)
( f))
( λ h →
comp-hom-Large-Precategory D
( comp-hom-Large-Precategory D g h)
( hom-functor-Large-Precategory F f))
( map-hom-functor-Large-Precategory F f))
( map-equiv (equiv-is-adjoint-pair-Large-Precategory X2 Y2))

open is-adjoint-pair-Large-Precategory public

map-equiv-is-adjoint-pair-Large-Precategory :
(H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level}
(X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) →
( type-hom-Large-Precategory C X (obj-functor-Large-Precategory G Y)) →
( type-hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y)
( type-hom-Large-Precategory C X (map-obj-functor-Large-Precategory G Y)) →
( type-hom-Large-Precategory D (map-obj-functor-Large-Precategory F X) Y)
map-equiv-is-adjoint-pair-Large-Precategory H X Y =
map-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y)

inv-equiv-is-adjoint-pair-Large-Precategory :
(H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level}
(X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) →
( type-hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y) ≃
( type-hom-Large-Precategory C X (obj-functor-Large-Precategory G Y))
( type-hom-Large-Precategory D (map-obj-functor-Large-Precategory F X) Y) ≃
( type-hom-Large-Precategory C X (map-obj-functor-Large-Precategory G Y))
inv-equiv-is-adjoint-pair-Large-Precategory H X Y =
inv-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y)

map-inv-equiv-is-adjoint-pair-Large-Precategory :
(H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level}
(X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) →
( type-hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y) →
( type-hom-Large-Precategory C X (obj-functor-Large-Precategory G Y))
( type-hom-Large-Precategory D (map-obj-functor-Large-Precategory F X) Y) →
( type-hom-Large-Precategory C X (map-obj-functor-Large-Precategory G Y))
map-inv-equiv-is-adjoint-pair-Large-Precategory H X Y =
map-inv-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y)

Expand All @@ -118,10 +118,10 @@ module _
( λ h →
comp-hom-Large-Precategory D
( comp-hom-Large-Precategory D g h)
( hom-functor-Large-Precategory F f))
( map-hom-functor-Large-Precategory F f))
( λ h →
comp-hom-Large-Precategory C
( comp-hom-Large-Precategory C (hom-functor-Large-Precategory G g) h)
( comp-hom-Large-Precategory C (map-hom-functor-Large-Precategory G g) h)
( f))
( map-inv-equiv-is-adjoint-pair-Large-Precategory H X2 Y2)
naturality-inv-equiv-is-adjoint-pair-Large-Precategory
Expand All @@ -130,12 +130,12 @@ module _
( equiv-is-adjoint-pair-Large-Precategory H X1 Y1)
( λ h →
comp-hom-Large-Precategory C
( comp-hom-Large-Precategory C (hom-functor-Large-Precategory G g) h)
( comp-hom-Large-Precategory C (map-hom-functor-Large-Precategory G g) h)
( f))
( λ h →
comp-hom-Large-Precategory D
( comp-hom-Large-Precategory D g h)
( hom-functor-Large-Precategory F f))
( map-hom-functor-Large-Precategory F f))
( equiv-is-adjoint-pair-Large-Precategory H X2 Y2)
( naturality-equiv-is-adjoint-pair-Large-Precategory H f g)

Expand Down Expand Up @@ -186,7 +186,7 @@ module _
obj-Large-Precategory C l →
obj-Large-Precategory D (level-left-adjoint-Adjunction FG l)
obj-left-adjoint-Adjunction FG =
obj-functor-Large-Precategory (left-adjoint-Adjunction FG)
map-obj-functor-Large-Precategory (left-adjoint-Adjunction FG)

hom-left-adjoint-Adjunction :
(FG : Adjunction) {l1 l2 : Level}
Expand All @@ -196,7 +196,7 @@ module _
( obj-left-adjoint-Adjunction FG X)
( obj-left-adjoint-Adjunction FG Y)
hom-left-adjoint-Adjunction FG =
hom-functor-Large-Precategory (left-adjoint-Adjunction FG)
map-hom-functor-Large-Precategory (left-adjoint-Adjunction FG)

preserves-id-left-adjoint-Adjunction :
(FG : Adjunction) {l1 : Level} (X : obj-Large-Precategory C l1) →
Expand All @@ -210,7 +210,7 @@ module _
obj-Large-Precategory D l1 →
obj-Large-Precategory C (level-right-adjoint-Adjunction FG l1)
obj-right-adjoint-Adjunction FG =
obj-functor-Large-Precategory (right-adjoint-Adjunction FG)
map-obj-functor-Large-Precategory (right-adjoint-Adjunction FG)

hom-right-adjoint-Adjunction :
(FG : Adjunction) {l1 l2 : Level} {X : obj-Large-Precategory D l1}
Expand All @@ -220,7 +220,7 @@ module _
( obj-right-adjoint-Adjunction FG X)
( obj-right-adjoint-Adjunction FG Y)
hom-right-adjoint-Adjunction FG =
hom-functor-Large-Precategory (right-adjoint-Adjunction FG)
map-hom-functor-Large-Precategory (right-adjoint-Adjunction FG)

preserves-id-right-adjoint-Adjunction :
(FG : Adjunction) {l : Level} (Y : obj-Large-Precategory D l) →
Expand Down
26 changes: 13 additions & 13 deletions src/category-theory/anafunctors-precategories.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,16 +85,16 @@ module _
anafunctor-functor-Precategory :
functor-Precategory C D → anafunctor-Precategory l4 C D
pr1 (anafunctor-functor-Precategory F) X Y =
iso-Precategory D (obj-functor-Precategory C D F X) Y
iso-Precategory D (map-obj-functor-Precategory C D F X) Y
pr1 (pr2 (anafunctor-functor-Precategory F)) X Y U u V v f =
comp-hom-Precategory D
( comp-hom-Precategory D
( hom-iso-Precategory D v)
( hom-functor-Precategory C D F f))
( map-hom-functor-Precategory C D F f))
( hom-inv-iso-Precategory D u)
pr1 (pr2 (pr2 (anafunctor-functor-Precategory F))) X =
unit-trunc-Prop
( pair (obj-functor-Precategory C D F X) (id-iso-Precategory D))
( pair (map-obj-functor-Precategory C D F X) (id-iso-Precategory D))
pr1 (pr2 (pr2 (pr2 (anafunctor-functor-Precategory F)))) X U u =
( ap
( comp-hom-Precategory' D (hom-inv-iso-Precategory D u))
Expand All @@ -113,44 +113,44 @@ module _
( ( inv
( associative-comp-hom-Precategory D
( hom-iso-Precategory D w)
( hom-functor-Precategory C D F g)
( hom-functor-Precategory C D F f))) ∙
( map-hom-functor-Precategory C D F g)
( map-hom-functor-Precategory C D F f))) ∙
( ap
( comp-hom-Precategory' D (hom-functor-Precategory C D F f))
( comp-hom-Precategory' D (map-hom-functor-Precategory C D F f))
( ( inv
( right-unit-law-comp-hom-Precategory D
( comp-hom-Precategory D
( hom-iso-Precategory D w)
( hom-functor-Precategory C D F g)))) ∙
( map-hom-functor-Precategory C D F g)))) ∙
( ( ap
( comp-hom-Precategory D
( comp-hom-Precategory D
( hom-iso-Precategory D w)
( hom-functor-Precategory C D F g)))
( map-hom-functor-Precategory C D F g)))
( inv (is-retraction-hom-inv-iso-Precategory D v))) ∙
( inv
( associative-comp-hom-Precategory D
( comp-hom-Precategory D
( hom-iso-Precategory D w)
( hom-functor-Precategory C D F g))
( map-hom-functor-Precategory C D F g))
( hom-inv-iso-Precategory D v)
( hom-iso-Precategory D v)))))))) ∙
( associative-comp-hom-Precategory D
( comp-hom-Precategory D
( comp-hom-Precategory D
( hom-iso-Precategory D w)
( hom-functor-Precategory C D F g))
( map-hom-functor-Precategory C D F g))
( hom-inv-iso-Precategory D v))
( hom-iso-Precategory D v)
( hom-functor-Precategory C D F f)))) ∙
( map-hom-functor-Precategory C D F f)))) ∙
( associative-comp-hom-Precategory D
( comp-hom-Precategory D
( comp-hom-Precategory D
( hom-iso-Precategory D w)
( hom-functor-Precategory C D F g))
( map-hom-functor-Precategory C D F g))
( hom-inv-iso-Precategory D v))
( comp-hom-Precategory D
( hom-iso-Precategory D v)
( hom-functor-Precategory C D F f))
( map-hom-functor-Precategory C D F f))
( hom-inv-iso-Precategory D u))
```
18 changes: 9 additions & 9 deletions src/category-theory/functors-categories.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,30 +36,30 @@ module _
functor-Category =
functor-Precategory (precategory-Category C) (precategory-Category D)

obj-functor-Category : functor-Category → obj-Category C → obj-Category D
obj-functor-Category = pr1
map-obj-functor-Category : functor-Category → obj-Category C → obj-Category D
map-obj-functor-Category = pr1

hom-functor-Category :
map-hom-functor-Category :
(F : functor-Category) →
{x y : obj-Category C} →
(f : type-hom-Category C x y) →
type-hom-Category D (obj-functor-Category F x) (obj-functor-Category F y)
hom-functor-Category F = pr1 (pr2 F)
type-hom-Category D (map-obj-functor-Category F x) (map-obj-functor-Category F y)
map-hom-functor-Category F = pr1 (pr2 F)

preserves-comp-functor-Category :
( F : functor-Category) {x y z : obj-Category C}
( g : type-hom-Category C y z) (f : type-hom-Category C x y) →
( hom-functor-Category F (comp-hom-Category C g f)) ＝
( comp-hom-Category D (hom-functor-Category F g) (hom-functor-Category F f))
( map-hom-functor-Category F (comp-hom-Category C g f)) ＝
( comp-hom-Category D (map-hom-functor-Category F g) (map-hom-functor-Category F f))
preserves-comp-functor-Category F =
preserves-comp-functor-Precategory
( precategory-Category C)
( precategory-Category D) F

preserves-id-functor-Category :
(F : functor-Category) (x : obj-Category C) →
hom-functor-Category F (id-hom-Category C {x}) ＝
id-hom-Category D {obj-functor-Category F x}
map-hom-functor-Category F (id-hom-Category C {x}) ＝
id-hom-Category D {map-obj-functor-Category F x}
preserves-id-functor-Category F =
preserves-id-functor-Precategory
( precategory-Category C)
Expand Down
38 changes: 19 additions & 19 deletions src/category-theory/functors-large-precategories.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,31 +40,31 @@ module _
where
constructor make-functor
field
obj-functor-Large-Precategory :
map-obj-functor-Large-Precategory :
{ l1 : Level} →
obj-Large-Precategory C l1 → obj-Large-Precategory D (γ l1)
hom-functor-Large-Precategory :
map-hom-functor-Large-Precategory :
{ l1 l2 : Level}
{ X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2} →
type-hom-Large-Precategory C X Y →
type-hom-Large-Precategory D
( obj-functor-Large-Precategory X)
( obj-functor-Large-Precategory Y)
( map-obj-functor-Large-Precategory X)
( map-obj-functor-Large-Precategory Y)
preserves-comp-functor-Large-Precategory :
{ l1 l2 l3 : Level}
{ X : obj-Large-Precategory C l1}
{ Y : obj-Large-Precategory C l2}
{ Z : obj-Large-Precategory C l3}
( g : type-hom-Large-Precategory C Y Z)
( f : type-hom-Large-Precategory C X Y) →
( hom-functor-Large-Precategory (comp-hom-Large-Precategory C g f)) ＝
( map-hom-functor-Large-Precategory (comp-hom-Large-Precategory C g f)) ＝
( comp-hom-Large-Precategory D
( hom-functor-Large-Precategory g)
( hom-functor-Large-Precategory f))
( map-hom-functor-Large-Precategory g)
( map-hom-functor-Large-Precategory f))
preserves-id-functor-Large-Precategory :
{ l1 : Level} {X : obj-Large-Precategory C l1} →
( hom-functor-Large-Precategory (id-hom-Large-Precategory C {X = X})) ＝
( id-hom-Large-Precategory D {X = obj-functor-Large-Precategory X})
( map-hom-functor-Large-Precategory (id-hom-Large-Precategory C {X = X})) ＝
( id-hom-Large-Precategory D {X = map-obj-functor-Large-Precategory X})

open functor-Large-Precategory public
```
Expand All @@ -80,8 +80,8 @@ id-functor-Large-Precategory :
{αC : Level → Level} {βC : Level → Level → Level} →
{C : Large-Precategory αC βC} →
functor-Large-Precategory C C (λ l → l)
obj-functor-Large-Precategory id-functor-Large-Precategory = id
hom-functor-Large-Precategory id-functor-Large-Precategory = id
map-obj-functor-Large-Precategory id-functor-Large-Precategory = id
map-hom-functor-Large-Precategory id-functor-Large-Precategory = id
preserves-comp-functor-Large-Precategory id-functor-Large-Precategory g f = refl
preserves-id-functor-Large-Precategory id-functor-Large-Precategory = refl
```
Expand All @@ -99,21 +99,21 @@ comp-functor-Large-Precategory :
{E : Large-Precategory αE βE} →
functor-Large-Precategory D E γG → functor-Large-Precategory C D γF →
functor-Large-Precategory C E (λ l → γG (γF l))
obj-functor-Large-Precategory (comp-functor-Large-Precategory G F) =
obj-functor-Large-Precategory G ∘ obj-functor-Large-Precategory F
hom-functor-Large-Precategory (comp-functor-Large-Precategory G F) =
hom-functor-Large-Precategory G ∘ hom-functor-Large-Precategory F
map-obj-functor-Large-Precategory (comp-functor-Large-Precategory G F) =
map-obj-functor-Large-Precategory G ∘ map-obj-functor-Large-Precategory F
map-hom-functor-Large-Precategory (comp-functor-Large-Precategory G F) =
map-hom-functor-Large-Precategory G ∘ map-hom-functor-Large-Precategory F
preserves-comp-functor-Large-Precategory
( comp-functor-Large-Precategory G F) g f =
( ap
( hom-functor-Large-Precategory G)
( map-hom-functor-Large-Precategory G)
( preserves-comp-functor-Large-Precategory F g f)) ∙
( preserves-comp-functor-Large-Precategory G
( hom-functor-Large-Precategory F g)
( hom-functor-Large-Precategory F f))
( map-hom-functor-Large-Precategory F g)
( map-hom-functor-Large-Precategory F f))
preserves-id-functor-Large-Precategory (comp-functor-Large-Precategory G F) =
( ap
( hom-functor-Large-Precategory G)
( map-hom-functor-Large-Precategory G)
( preserves-id-functor-Large-Precategory F)) ∙
( preserves-id-functor-Large-Precategory G)
```
Loading

0 comments on commit 08af608

Please sign in to comment.