From f1644f56c7e32fa577c9771efb8885dbbafef97e Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Thu, 6 Oct 2022 19:43:55 +0200
Subject: [PATCH] define the category of families

---
 src/Fams.lagda.md | 62 +++++++++++++++++++++++++++++++----------------
 1 file changed, 41 insertions(+), 21 deletions(-)

diff --git a/src/Fams.lagda.md b/src/Fams.lagda.md
index fb41a74..24dd591 100644
--- a/src/Fams.lagda.md
+++ b/src/Fams.lagda.md
@@ -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
+
+module Fams where
 ```
-Families of sets are sets
-```
-Fam-is-set : {o : _} → is-set (Σ[ B ∈ Set o ] (∣ B ∣ → Set o))
-Fam-is-set = Σ-is-hlevel 2 (λ x y → {!   !}) {!   !}
-```
+# The category of families (of sets)
 
 Given a universe level there is a category $\mathcal Fam$ of the families of sets of that level.
-
 ```
 module _ where
   open Precategory
 
   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$.
 ```
   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 ∣) ] 
-                      ((b : ∣ B .fst ∣) → ∣ B .snd b ∣ → ∣ C .snd (f b) ∣)
+  Fams o .Hom B C =
+    Σ[ 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 = {!   !}
-  Fams o ._∘_ = {!   !}
-  Fams o .idr = {!   !}
-  Fams o .idl = {!   !}
-  Fams o .assoc = {!   !}
+  Fams o .id .fst x = x
+  Fams o .id .snd b x = x
+```
+
+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 ∘ (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
 ```
\ No newline at end of file