Skip to content

Commit

Permalink
Additions during work on material set theory in HoTT (#910)
Browse files Browse the repository at this point in the history 
Co-authored-by: Daniel Gratzer <danny.gratzer@gmail.com>
Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
  • Loading branch information
@elisabethstenholm @jozefg @EgbertRijke
3 people committed Nov 27, 2023
1 parent ba04d6a commit b410842
Show file tree
Hide file tree
Showing 66 changed files with 3,227 additions and 860 deletions.
1 change: 1 addition & 0 deletions src/category-theory.lagda.md
View file
Expand Up @@ -119,6 +119,7 @@ open import category-theory.opposite-large-precategories public
open import category-theory.opposite-precategories public
open import category-theory.opposite-preunivalent-categories public
open import category-theory.precategories public
open import category-theory.precategory-of-elements-of-a-presheaf public
open import category-theory.precategory-of-functors public
open import category-theory.precategory-of-functors-from-small-to-large-precategories public
open import category-theory.precategory-of-maps-from-small-to-large-precategories public
Expand Down
311 changes: 177 additions & 134 deletions src/category-theory/copresheaf-categories.lagda.md
View file
Expand Up @@ -9,13 +9,19 @@ module category-theory.copresheaf-categories where
```agda
open import category-theory.categories
open import category-theory.category-of-functors-from-small-to-large-categories
open import category-theory.functors-from-small-to-large-precategories
open import category-theory.functors-precategories
open import category-theory.large-categories
open import category-theory.large-precategories
open import category-theory.natural-transformations-functors-from-small-to-large-precategories
open import category-theory.precategories
open import category-theory.precategory-of-functors-from-small-to-large-precategories

open import foundation.category-of-sets
open import foundation.commuting-squares-of-maps
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels
Expand Down Expand Up @@ -47,133 +53,213 @@ module _
{l1 l2 : Level} (C : Precategory l1 l2)
where

copresheaf-Large-Precategory :
copresheaf-large-precategory-Precategory :
Large-Precategory (λ l → l1 ⊔ l2 ⊔ lsuc l) (λ l l' → l1 ⊔ l2 ⊔ l ⊔ l')
copresheaf-Large-Precategory =
copresheaf-large-precategory-Precategory =
functor-large-precategory-Small-Large-Precategory C Set-Large-Precategory

is-large-category-copresheaf-Large-Category :
is-large-category-Large-Precategory copresheaf-Large-Precategory
is-large-category-copresheaf-Large-Category =
is-large-category-copresheaf-large-category-Precategory :
is-large-category-Large-Precategory copresheaf-large-precategory-Precategory
is-large-category-copresheaf-large-category-Precategory =
is-large-category-functor-large-precategory-is-large-category-Small-Large-Precategory
( C)
( Set-Large-Precategory)
( is-large-category-Set-Large-Precategory)

copresheaf-Large-Category :
copresheaf-large-category-Precategory :
Large-Category (λ l → l1 ⊔ l2 ⊔ lsuc l) (λ l l' → l1 ⊔ l2 ⊔ l ⊔ l')
large-precategory-Large-Category copresheaf-Large-Category =
copresheaf-Large-Precategory
is-large-category-Large-Category copresheaf-Large-Category =
is-large-category-copresheaf-Large-Category
large-precategory-Large-Category copresheaf-large-category-Precategory =
copresheaf-large-precategory-Precategory
is-large-category-Large-Category copresheaf-large-category-Precategory =
is-large-category-copresheaf-large-category-Precategory

obj-copresheaf-Large-Category : (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l)
obj-copresheaf-Large-Category =
obj-Large-Precategory copresheaf-Large-Precategory

hom-set-copresheaf-Large-Category :
copresheaf-Precategory :
(l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l)
copresheaf-Precategory =
obj-Large-Precategory copresheaf-large-precategory-Precategory

module _
{l : Level} (P : copresheaf-Precategory l)
where

element-set-copresheaf-Precategory : obj-Precategory C → Set l
element-set-copresheaf-Precategory =
obj-functor-Small-Large-Precategory C Set-Large-Precategory P

element-copresheaf-Precategory : obj-Precategory C → UU l
element-copresheaf-Precategory X =
type-Set (element-set-copresheaf-Precategory X)

action-copresheaf-Precategory :
{X Y : obj-Precategory C} →
hom-Precategory C X Y →
element-copresheaf-Precategory X → element-copresheaf-Precategory Y
action-copresheaf-Precategory f =
hom-functor-Small-Large-Precategory C Set-Large-Precategory P f

preserves-id-action-copresheaf-Precategory :
{X : obj-Precategory C} →
action-copresheaf-Precategory {X} {X} (id-hom-Precategory C) ~ id
preserves-id-action-copresheaf-Precategory =
htpy-eq
( preserves-id-functor-Small-Large-Precategory C
( Set-Large-Precategory)
( P)
( _))

preserves-comp-action-copresheaf-Precategory :
{X Y Z : obj-Precategory C}
(g : hom-Precategory C Y Z) (f : hom-Precategory C X Y) →
action-copresheaf-Precategory (comp-hom-Precategory C g f) ~
action-copresheaf-Precategory g ∘ action-copresheaf-Precategory f
preserves-comp-action-copresheaf-Precategory g f =
htpy-eq
( preserves-comp-functor-Small-Large-Precategory C
( Set-Large-Precategory)
( P)
( g)
( f))

hom-set-copresheaf-Precategory :
{l3 l4 : Level}
(X : obj-copresheaf-Large-Category l3)
(Y : obj-copresheaf-Large-Category l4) → Set (l1 ⊔ l2 ⊔ l3 ⊔ l4)
hom-set-copresheaf-Large-Category =
hom-set-Large-Precategory copresheaf-Large-Precategory
(P : copresheaf-Precategory l3)
(Q : copresheaf-Precategory l4) → Set (l1 ⊔ l2 ⊔ l3 ⊔ l4)
hom-set-copresheaf-Precategory =
hom-set-Large-Precategory copresheaf-large-precategory-Precategory

hom-copresheaf-Large-Category :
hom-copresheaf-Precategory :
{l3 l4 : Level}
(X : obj-copresheaf-Large-Category l3)
(Y : obj-copresheaf-Large-Category l4) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
hom-copresheaf-Large-Category =
hom-Large-Precategory copresheaf-Large-Precategory
(X : copresheaf-Precategory l3) (Y : copresheaf-Precategory l4) →
UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
hom-copresheaf-Precategory =
hom-Large-Precategory copresheaf-large-precategory-Precategory

comp-hom-copresheaf-Large-Category :
module _
{l3 l4 : Level}
(P : copresheaf-Precategory l3) (Q : copresheaf-Precategory l4)
(h : hom-copresheaf-Precategory P Q)
where

map-hom-copresheaf-Precategory :
(X : obj-Precategory C) →
element-copresheaf-Precategory P X → element-copresheaf-Precategory Q X
map-hom-copresheaf-Precategory =
hom-natural-transformation-Small-Large-Precategory C
( Set-Large-Precategory)
( P)
( Q)
( h)

naturality-hom-copresheaf-Precategory :
{X Y : obj-Precategory C} (f : hom-Precategory C X Y) →
coherence-square-maps
( action-copresheaf-Precategory P f)
( map-hom-copresheaf-Precategory X)
( map-hom-copresheaf-Precategory Y)
( action-copresheaf-Precategory Q f)
naturality-hom-copresheaf-Precategory f =
htpy-eq
( naturality-natural-transformation-Small-Large-Precategory C
( Set-Large-Precategory)
( P)
( Q)
( h)
( f))

comp-hom-copresheaf-Precategory :
{l3 l4 l5 : Level}
(X : obj-copresheaf-Large-Category l3)
(Y : obj-copresheaf-Large-Category l4)
(Z : obj-copresheaf-Large-Category l5) →
hom-copresheaf-Large-Category Y Z → hom-copresheaf-Large-Category X Y →
hom-copresheaf-Large-Category X Z
comp-hom-copresheaf-Large-Category X Y Z =
comp-hom-Large-Precategory copresheaf-Large-Precategory {X = X} {Y} {Z}

id-hom-copresheaf-Large-Category :
{l3 : Level} (X : obj-copresheaf-Large-Category l3) →
hom-copresheaf-Large-Category X X
id-hom-copresheaf-Large-Category X =
id-hom-Large-Precategory copresheaf-Large-Precategory {X = X}

associative-comp-hom-copresheaf-Large-Category :
(X : copresheaf-Precategory l3)
(Y : copresheaf-Precategory l4)
(Z : copresheaf-Precategory l5) →
hom-copresheaf-Precategory Y Z →
hom-copresheaf-Precategory X Y →
hom-copresheaf-Precategory X Z
comp-hom-copresheaf-Precategory X Y Z =
comp-hom-Large-Precategory
( copresheaf-large-precategory-Precategory)
{ X = X}
{ Y}
{ Z}

id-hom-copresheaf-Precategory :
{l3 : Level} (X : copresheaf-Precategory l3) →
hom-copresheaf-Precategory X X
id-hom-copresheaf-Precategory X =
id-hom-Large-Precategory copresheaf-large-precategory-Precategory {X = X}

associative-comp-hom-copresheaf-Precategory :
{l3 l4 l5 l6 : Level}
(X : obj-copresheaf-Large-Category l3)
(Y : obj-copresheaf-Large-Category l4)
(Z : obj-copresheaf-Large-Category l5)
(W : obj-copresheaf-Large-Category l6)
(h : hom-copresheaf-Large-Category Z W)
(g : hom-copresheaf-Large-Category Y Z)
(f : hom-copresheaf-Large-Category X Y) →
comp-hom-copresheaf-Large-Category X Y W
( comp-hom-copresheaf-Large-Category Y Z W h g)
(X : copresheaf-Precategory l3)
(Y : copresheaf-Precategory l4)
(Z : copresheaf-Precategory l5)
(W : copresheaf-Precategory l6)
(h : hom-copresheaf-Precategory Z W)
(g : hom-copresheaf-Precategory Y Z)
(f : hom-copresheaf-Precategory X Y) →
comp-hom-copresheaf-Precategory X Y W
( comp-hom-copresheaf-Precategory Y Z W h g)
( f) ＝
comp-hom-copresheaf-Large-Category X Z W
comp-hom-copresheaf-Precategory X Z W
( h)
( comp-hom-copresheaf-Large-Category X Y Z g f)
associative-comp-hom-copresheaf-Large-Category X Y Z W =
( comp-hom-copresheaf-Precategory X Y Z g f)
associative-comp-hom-copresheaf-Precategory X Y Z W =
associative-comp-hom-Large-Precategory
( copresheaf-Large-Precategory)
( copresheaf-large-precategory-Precategory)
{ X = X}
{ Y}
{ Z}
{ W}

inv-associative-comp-hom-copresheaf-Large-Category :
inv-associative-comp-hom-copresheaf-Precategory :
{l3 l4 l5 l6 : Level}
(X : obj-copresheaf-Large-Category l3)
(Y : obj-copresheaf-Large-Category l4)
(Z : obj-copresheaf-Large-Category l5)
(W : obj-copresheaf-Large-Category l6)
(h : hom-copresheaf-Large-Category Z W)
(g : hom-copresheaf-Large-Category Y Z)
(f : hom-copresheaf-Large-Category X Y) →
comp-hom-copresheaf-Large-Category X Z W
(X : copresheaf-Precategory l3)
(Y : copresheaf-Precategory l4)
(Z : copresheaf-Precategory l5)
(W : copresheaf-Precategory l6)
(h : hom-copresheaf-Precategory Z W)
(g : hom-copresheaf-Precategory Y Z)
(f : hom-copresheaf-Precategory X Y) →
comp-hom-copresheaf-Precategory X Z W
( h)
( comp-hom-copresheaf-Large-Category X Y Z g f) ＝
comp-hom-copresheaf-Large-Category X Y W
( comp-hom-copresheaf-Large-Category Y Z W h g)
( comp-hom-copresheaf-Precategory X Y Z g f) ＝
comp-hom-copresheaf-Precategory X Y W
( comp-hom-copresheaf-Precategory Y Z W h g)
( f)
inv-associative-comp-hom-copresheaf-Large-Category X Y Z W =
inv-associative-comp-hom-copresheaf-Precategory X Y Z W =
inv-associative-comp-hom-Large-Precategory
( copresheaf-Large-Precategory)
( copresheaf-large-precategory-Precategory)
{ X = X}
{ Y}
{ Z}
{ W}

left-unit-law-comp-hom-copresheaf-Large-Category :
left-unit-law-comp-hom-copresheaf-Precategory :
{l3 l4 : Level}
(X : obj-copresheaf-Large-Category l3)
(Y : obj-copresheaf-Large-Category l4)
(f : hom-copresheaf-Large-Category X Y) →
comp-hom-copresheaf-Large-Category X Y Y
( id-hom-copresheaf-Large-Category Y)
(X : copresheaf-Precategory l3)
(Y : copresheaf-Precategory l4)
(f : hom-copresheaf-Precategory X Y) →
comp-hom-copresheaf-Precategory X Y Y
( id-hom-copresheaf-Precategory Y)
( f) ＝
f
left-unit-law-comp-hom-copresheaf-Large-Category X Y =
left-unit-law-comp-hom-copresheaf-Precategory X Y =
left-unit-law-comp-hom-Large-Precategory
( copresheaf-Large-Precategory)
( copresheaf-large-precategory-Precategory)
{ X = X}
{ Y}

right-unit-law-comp-hom-copresheaf-Large-Category :
right-unit-law-comp-hom-copresheaf-Precategory :
{l3 l4 : Level}
(X : obj-copresheaf-Large-Category l3)
(Y : obj-copresheaf-Large-Category l4)
(f : hom-copresheaf-Large-Category X Y) →
comp-hom-copresheaf-Large-Category X X Y
(X : copresheaf-Precategory l3)
(Y : copresheaf-Precategory l4)
(f : hom-copresheaf-Precategory X Y) →
comp-hom-copresheaf-Precategory X X Y
( f)
( id-hom-copresheaf-Large-Category X) ＝
( id-hom-copresheaf-Precategory X) ＝
f
right-unit-law-comp-hom-copresheaf-Large-Category X Y =
right-unit-law-comp-hom-copresheaf-Precategory X Y =
right-unit-law-comp-hom-Large-Precategory
( copresheaf-Large-Precategory)
( copresheaf-large-precategory-Precategory)
{ X = X}
{ Y}
```
Expand All @@ -185,58 +271,15 @@ module _
{l1 l2 : Level} (C : Precategory l1 l2) (l : Level)
where

copresheaf-Precategory : Precategory (l1 ⊔ l2 ⊔ lsuc l) (l1 ⊔ l2 ⊔ l)
copresheaf-Precategory =
precategory-Large-Precategory (copresheaf-Large-Precategory C) l

copresheaf-Category : Category (l1 ⊔ l2 ⊔ lsuc l) (l1 ⊔ l2 ⊔ l)
copresheaf-Category = category-Large-Category (copresheaf-Large-Category C) l
```

We also record the components of the category of small copresheaves on a
precategory.

```agda
obj-copresheaf-Category =
obj-Precategory copresheaf-Precategory

hom-set-copresheaf-Category =
hom-set-Precategory copresheaf-Precategory

hom-copresheaf-Category =
hom-Precategory copresheaf-Precategory

comp-hom-copresheaf-Category =
comp-hom-Precategory copresheaf-Precategory

id-hom-copresheaf-Category =
id-hom-Precategory copresheaf-Precategory

associative-comp-hom-copresheaf-Category =
associative-comp-hom-Precategory copresheaf-Precategory

left-unit-law-comp-hom-copresheaf-Category =
left-unit-law-comp-hom-Precategory copresheaf-Precategory

right-unit-law-comp-hom-copresheaf-Category =
right-unit-law-comp-hom-Precategory copresheaf-Precategory
```

### Sections of copresheaves

As a choice of universe level must be made to talk about sections of
copresheaves, this notion coincides for the large and small category of
copresheaves.

```agda
module _
{l1 l2 l3 : Level} (C : Precategory l1 l2)
where
copresheaf-category-Precategory :
Category (l1 ⊔ l2 ⊔ lsuc l) (l1 ⊔ l2 ⊔ l)
copresheaf-category-Precategory =
category-Large-Category (copresheaf-large-category-Precategory C) l

section-copresheaf-Category :
(F : obj-copresheaf-Category C l3) (c : obj-Precategory C) → UU l3
section-copresheaf-Category F c =
type-Set (obj-functor-Precategory C (Set-Precategory l3) F c)
copresheaf-precategory-Precategory :
Precategory (l1 ⊔ l2 ⊔ lsuc l) (l1 ⊔ l2 ⊔ l)
copresheaf-precategory-Precategory =
precategory-Large-Precategory (copresheaf-large-precategory-Precategory C) l
```

## See also
Expand Down

0 comments on commit b410842

Please sign in to comment.