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 C\mathcal{C} as being displayed over Sets, regardless of the size of the object- and Hom-spaces of C\mathcal{C}.

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

Family : βˆ€ {β„“} β†’ Displayed (Sets β„“) _ _
Family .Ob[_] S = Functor (Discβ€² S) C

Given a map f:Aβ†’Bf : A \to B in Sets, and functors F:[A,C]F : [A,C] and G:[B,C]G : [B,C], we define the collection of displayed maps to be the set of all natural transformations Fβ‡’fβˆ—GF \To f*G, where fβˆ—Gf*G is the precomposition of ff 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βˆ—F\id{id}*F is not the same term as FF.

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β‡’mβˆ—fβˆ—yβ€²u \To m*f*y' entails giving a natural transformation uβ‡’(f∘m)βˆ—yβ€²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β€²