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

Fams: less clutter in description of morphisms

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2022-10-08 13:12:39 +02:00
parent ece686e955
commit e704dde2a3
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Fams.lagda.md
View File

@ -20,7 +20,7 @@ Objects in $\mathcal Fam$ are pairs $B = (B^0,B^1)$ where $B^0$ is a set and $B^
Fams o .Ob = Σ[ B ∈ Set o ] (∣ B ∣ → Set o) Fams o .Ob = Σ[ B ∈ Set o ] (∣ B ∣ → Set o)
``` ```
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))$. 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 $b : B^0 \mapsto f^1 : B^1(b) \to C^1(f^0(b))$.
``` ```
Fams o .Hom B C = Fams o .Hom B C =
Σ[ f ∈ (∣ B .fst ∣ → ∣ C .fst ∣) ] Σ[ f ∈ (∣ B .fst ∣ → ∣ C .fst ∣) ]
@ -59,4 +59,4 @@ Since homs are functions between families of sets, they form a set.
(g b x) (g b x)
(λ k → p k b x) (λ k → p k b x)
(λ k → q k b x) i j (λ k → q k b x) i j
``` ```