1.3 KiB
1.3 KiB
module Fams where
open import 1Lab.HLevel.Universe
open import 1Lab.HLevel.Retracts
open import 1Lab.Type.Sigma
open import Cat.Prelude
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 → {! !}) {! !}
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)).
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.
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 = {! !}