cwfs/src/Fams.lagda.md

open import Cat.Prelude

module Fams where

The category of families of sets

This file defines the category \mathcal Fam 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 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 ∣) ] 
      ((b : ∣ B .fst ∣) → ∣ B .snd b ∣ → ∣ C .snd (f b) ∣)

The identity is given by a pair of identity functions.

  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)

Since composition is defined using regular function composition it 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