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:ABf : 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 FfGF \To f*G, where fGf*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 idF\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 umfyu \To m*f*y' entails giving a natural transformation u(fm)yu \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′