open import Cat.Displayed.Cartesian open import Cat.Instances.Discrete open import Cat.Instances.Functor open import Cat.Displayed.Base open import Cat.Prelude module Cat.Displayed.Instances.Family {o h} (C : Precategory o h) where

# The family fibration🔗

We can canonically treat any Precategory $\mathcal{C}$ as being displayed over Sets, regardless of the size of the object- and Hom-spaces of $\mathcal{C}$.

The collection of displayed object over $S$ is given by the space of functors $[\id{Disc}(S),C]$, regarding $S$ as a discrete category. This is essentially an $S$-indexed family of objects of $C$, hence the name “family fibration”.

Family : ∀ {ℓ} → Displayed (Sets ℓ) _ _ Family .Ob[_] S = Functor (Disc′ S) C

Given a map $f : A \to B$ in Sets, and functors $F : [A,C]$ and $G : [B,C]$, we define the collection of displayed maps to be the set of all natural transformations $F \To f*G$, where $f*G$ is the precomposition of $f$ regarded as a functor between discrete categories. Since natural transformations form a Set, we’re clear to take this as the definition.

Family .Hom[_] {A} {B} f F G = F => (G F∘ lift-disc f) Family .Hom[_]-set f x y = Nat-is-set

The identity and composition operations are given by the identity and composite natural transformations; However, we can not reuse the existing implementations because $\id{id}*F$ is not the same term as $F$.

Family .id′ = NT (λ x → id) λ x y f → id-comm-sym Family ._∘′_ {a = A} {x = X} {Y} {Z} {F} {G} f g = NT (λ x → η f _ ∘ η g _) comm where abstract comm : ∀ x y (h : x ≡ y) → (f .η _ ∘ g .η y) ∘ F₁ X h ≡ F₁ (Z F∘ lift-disc {A = A} _) h ∘ f .η _ ∘ g .η _ comm x y h = (f .η _ ∘ g .η y) ∘ F₁ X h ≡⟨ extendr (g .is-natural _ _ _) ⟩≡ (f .η _ ∘ F₁ (Y F∘ lift-disc {A = A} _) h) ∘ g .η x ≡⟨ pushl (f .is-natural _ _ _) ⟩≡ F₁ (Z F∘ lift-disc {A = A} _) h ∘ f .η _ ∘ g .η _ ∎ Family .idr′ _ = Nat-path λ x → idr _ Family .idl′ _ = Nat-path λ x → idl _ Family .assoc′ _ _ _ = Nat-path λ x → assoc _ _ _

The family fibration is `a Cartesian fibration`

. This is because giving a Cartesian lift for a natural transformation $u \To m*f*y'$ entails giving a natural transformation $u \To (f\circ m)*y'$; But this is exactly the natural transformation we started with!

open Cartesian-fibration open Cartesian-lift open Cartesian Family-is-cartesian : ∀ {ℓ} → Cartesian-fibration (Family {ℓ = ℓ}) Family-is-cartesian = iscart where cart : ∀ {x y : Set _} (f : ∣ x ∣ → ∣ y ∣) (y′ : Functor (Disc′ y) C) → Cartesian Family f idnt cart f y′ .universal m nt = NT (η nt) (is-natural nt) cart f y′ .commutes m h′ = Nat-path λ x → idl _ cart f y′ .unique m′ p = Nat-path λ x → sym (idl _) ∙ ap (λ e → η e x) p iscart : Cartesian-fibration Family iscart .has-lift f y′ .x′ = y′ F∘ lift-disc f iscart .has-lift f y′ .lifting = idnt iscart .has-lift {x = x} {y} f y′ .cartesian = cart {x = x} {y} f y′