From e704dde2a32dc554eaea1c749af825a5f90f0d84 Mon Sep 17 00:00:00 2001 From: depsterr Date: Sat, 8 Oct 2022 13:12:39 +0200 Subject: [PATCH] Fams: less clutter in description of morphisms --- src/Fams.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Fams.lagda.md b/src/Fams.lagda.md index a72eccc..9c51a91 100644 --- a/src/Fams.lagda.md +++ b/src/Fams.lagda.md @@ -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) ``` -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 = Σ[ f ∈ (∣ B .fst ∣ → ∣ C .fst ∣) ] @@ -59,4 +59,4 @@ Since homs are functions between families of sets, they form a set. (g b x) (λ k → p k b x) (λ k → q k b x) i j -``` \ No newline at end of file +```