rachel/cwfs
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

define the category of families

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2022-10-06 19:43:55 +02:00
parent 41339d381d
commit f1644f56c7
1 changed files with 41 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
src/Fams.lagda.md
View File

@ -1,40 +1,60 @@
``` ```
module Fams where
open import 1Lab.HLevel.Universe
open import 1Lab.HLevel.Retracts
open import 1Lab.Type.Sigma
open import Cat.Prelude open import Cat.Prelude
module Fams where
``` ```
Families of sets are sets # The category of families (of sets)
```
Fam-is-set : {o : _} → is-set (Σ[ B ∈ Set o ] (∣ B ∣ → Set o))
Fam-is-set = Σ-is-hlevel 2 (λ x y → {! !}) {! !}
```
Given a universe level there is a category $\mathcal Fam$ of the families of sets of that level. Given a universe level there is a category $\mathcal Fam$ of the families of sets of that level.
``` ```
module _ where module _ where
open Precategory open Precategory
Fams : (o : _) → Precategory (lsuc o) o Fams : (o : _) → Precategory (lsuc o) o
``` ```
Objects in $\mathcal Fam$ are pairs $B = (B^0,B^1)$ where $B^0$ is a set and $B^1$ is a family of sets indexed over $B^0$. Objects in $\mathcal Fam$ are pairs $B = (B^0,B^1)$ where $B^0$ is a set and $B^1$ is a family of sets indexed over $B^0$.
``` ```
Fams o .Ob = Σ[ B ∈ Set o ] (∣ B ∣ → Set o) Fams o .Ob = Σ[ B ∈ Set o ] (∣ B ∣ → Set o)
``` ```
A morphism between $B$ and $C$ in $\mathcal Fam$ is a pair of functions $(f^0,f^1)$ where $f^0$ is a function $f^0 : B^0 \to C^0$ and $f^1$ is a family of functions in $B^0$, $b : B^0 \mapsto f^1 : B^1(b) \to C^1(f^0(b))$.
A morphism between objects $B$ and $C$ in $\mathcal Fam$ is a pair of functions $(f^0,f^1)$ where $f^0$ is a function $f^0 : B^0 \to C^0$ and $f^1$ is a family of functions in $B^0$, $b : B^0 \mapsto f^1 : B^1(b) \to C^1(f^0(b))$.
``` ```
Fams o .Hom B C = Σ[ f ∈ (∣ B .fst ∣ → ∣ C .fst ∣) ] Fams o .Hom B C =
((b : ∣ B .fst ∣) → ∣ B .snd b ∣ → ∣ C .snd (f b) ∣) Σ[ f ∈ (∣ B .fst ∣ → ∣ C .fst ∣) ]
((b : ∣ B .fst ∣) → ∣ B .snd b ∣ → ∣ C .snd (f b) ∣)
``` ```
Remaning proofs are fairly trivial due to working with sets.
The identity is given by a pair of identity functions.
``` ```
Fams o .Hom-set B C f g p q i j = {! !} Fams o .id .fst x = x
Fams o .id = {! !} Fams o .id .snd b x = x
Fams o ._∘_ = {! !} ```
Fams o .idr = {! !}
Fams o .idl = {! !} Composition follows from regular function composition for $(f \circ g)^0$, and function composition with a translation of $b : B^0$ for $(f \circ g)^1$
Fams o .assoc = {! !} ```
(Fams o ∘ (f⁰ , f¹)) (g⁰ , g¹) .fst x = f⁰ (g⁰ x)
(Fams o ∘ (f⁰ , f¹)) (g⁰ , g¹) .snd b x = f¹ (g⁰ b) (g¹ b x)
```
This computes nicely.
```
Fams o .idr f = refl
Fams o .idl f = refl
Fams o .assoc f g h = refl
```
Since homs are functions between families of sets, they form a set.
```
Fams o .Hom-set B C = Σ-is-hlevel 2 p⁰ p¹
where
p⁰ : is-set (∣ B .fst ∣ → ∣ C .fst ∣)
p⁰ f g p q i j x = C .fst .is-tr (f x) (g x) (happly p x)
(happly q x) i j
p¹ : (f⁰ : ∣ B .fst ∣ → ∣ C .fst ∣)
→ is-set ((b : ∣ B .fst ∣) → ∣ B .snd b ∣ → ∣ C .snd (f⁰ b) ∣)
p¹ h f g p q i j b x = C .snd (h b) .is-tr (f b x)
(g b x)
(λ k → p k b x)
(λ k → q k b x) i j
``` ```