module Cat.Displayed.Functor where

Displayed and fibred functorsπŸ”—

If you have a pair of categories E,F\mathcal{E}, \mathcal{F} displayed over a common base category B\mathcal{B}, it makes immediate sense to talk about functors F:Eβ†’FF : \mathcal{E} \to \mathcal{F}: you’d have an assignment of objects Fx:Eβˆ—(x)β†’Fβˆ—(x)F_x : \mathcal{E}^*(x) \to \mathcal{F}^*(x) and an assignment of morphisms

Fa,b,f:(aβ€²β†’fbβ€²)β†’(Fa(aβ€²)β†’fFb(bβ€²)), F_{a,b,f} : (a' \to_f b') \to (F_a(a') \to_f F_b(b'))\text{,}

which makes sense because Fa(a′)F_a(a') lies over aa, just as a′a' did, that a morphism Fa(a′)→Fb(b′)F_a(a') \to F_b(b') is allowed to lie over a morphism f:a→bf : a \to b. But, in the spirit of relativising category theory, it makes more sense to consider functors between categories displayed over different bases, as in

with our displayed functor F:E→F\mathbf{F} : \mathcal{E} \to \mathcal{F} lying over an ordinary functor F:A→BF : \mathcal{A} \to \mathcal{B} to mediate between the bases.

  record Displayed-functor : Type lvl where
    no-eta-equality
    field
      Fβ‚€β€² : βˆ€ {x} (o : β„°.Ob[ x ]) β†’ β„±.Ob[ F.β‚€ x ]
      F₁′ : βˆ€ {a b} {f : A.Hom a b} {aβ€² bβ€²}
          β†’ β„°.Hom[ f ] aβ€² bβ€² β†’ β„±.Hom[ F.₁ f ] (Fβ‚€β€² aβ€²) (Fβ‚€β€² bβ€²)

In order to state the displayed functoriality laws, we require functoriality for our mediating functor FF. Functors between categories displayed over the same base can be recovered as the β€œvertical displayed functors”, i.e., those lying over the identity functor.

      F-idβ€² : βˆ€ {x} {o : β„°.Ob[ x ]}
            β†’ PathP (Ξ» i β†’ β„±.Hom[ F.F-id i ] (Fβ‚€β€² o) (Fβ‚€β€² o))
                    (F₁′ β„°.idβ€²) β„±.idβ€²
      F-βˆ˜β€² : βˆ€ {a b c} {f : A.Hom b c} {g : A.Hom a b} {aβ€² bβ€² cβ€²}
               {fβ€² : β„°.Hom[ f ] bβ€² cβ€²} {gβ€² : β„°.Hom[ g ] aβ€² bβ€²}
           β†’ PathP (Ξ» i β†’ β„±.Hom[ F.F-∘ f g i ] (Fβ‚€β€² aβ€²) (Fβ‚€β€² cβ€²))
                   (F₁′ (fβ€² β„°.βˆ˜β€² gβ€²))
                   (F₁′ fβ€² β„±.βˆ˜β€² F₁′ gβ€²)
    β‚€β€² = Fβ‚€β€²
    ₁′ = F₁′

Note that, if E\mathcal{E} and F\mathcal{F} are fibred categories over their bases (rather than just displayed categories), then the appropriate notion of 1-cell are displayed functors that take Cartesian morphisms to Cartesian morphisms:

  is-fibred-functor : Displayed-functor β„° β„± F β†’ Type _
  is-fibred-functor Fβ€² = 
    βˆ€ {a b aβ€² bβ€²} {f : A.Hom a b} (fβ€² : β„°.Hom[ f ] aβ€² bβ€²)
    β†’ is-cartesian β„° f fβ€² β†’ is-cartesian β„± (F.₁ f) (F₁′ fβ€²)
    where open Displayed-functor Fβ€²
  record Fibred-functor : Type (lvl βŠ” oβ‚‚ βŠ” β„“β‚‚) where
    no-eta-equality
    field
      disp : Displayed-functor β„° β„± F
      F-cartesian : is-fibred-functor disp

    open Displayed-functor disp public

One can also define the composition of displayed functors, which lies over the composition of the underlying functors.

  _Fβˆ˜β€²_
    : Displayed-functor β„± β„‹ F
    β†’ Displayed-functor β„° β„± G
    β†’ Displayed-functor β„° β„‹ (F F∘ G)
  (Fβ€² Fβˆ˜β€² Gβ€²) .Fβ‚€β€² x = Fβ€² .Fβ‚€β€² (Gβ€² .Fβ‚€β€² x)
  (Fβ€² Fβˆ˜β€² Gβ€²) .F₁′ f = Fβ€² .F₁′ (Gβ€² .F₁′ f)
  (Fβ€² Fβˆ˜β€² Gβ€²) .F-idβ€² = to-pathp $
    hom[] (Fβ€² .F₁′ (Gβ€² .F₁′ β„°.idβ€²))         β‰‘βŸ¨ reindex _ _ βˆ™ sym (hom[]-βˆ™ (ap F.F₁ G.F-id) F.F-id) βŸ©β‰‘
    hom[] (hom[] (Fβ€² .F₁′ (Gβ€² .F₁′ β„°.idβ€²))) β‰‘βŸ¨ ap hom[] (shiftl _ Ξ» i β†’ Fβ€² .F₁′ (Gβ€² .F-idβ€² i)) βŸ©β‰‘
    hom[] (Fβ€² .F₁′ β„±.idβ€²)                   β‰‘βŸ¨ from-pathp (Fβ€² .F-idβ€²) βŸ©β‰‘
    β„‹.idβ€²                                   ∎
  (Fβ€² Fβˆ˜β€² Gβ€²) .F-βˆ˜β€² {f = f} {g = g} {fβ€² = fβ€²} {gβ€² = gβ€²} = to-pathp $
    hom[] (Fβ€² .F₁′ (Gβ€² .F₁′ (fβ€² β„°.βˆ˜β€² gβ€²)))           β‰‘βŸ¨ reindex _ _ βˆ™ sym (hom[]-βˆ™ (ap F.F₁ (G.F-∘ f g)) (F.F-∘ (G.₁ f) (G.₁ g))) βŸ©β‰‘
    hom[] (hom[] (Fβ€² .F₁′ (Gβ€² .F₁′ (fβ€² β„°.βˆ˜β€² gβ€²))))   β‰‘βŸ¨ ap hom[] (shiftl _ Ξ» i β†’ Fβ€² .F₁′ (Gβ€² .F-βˆ˜β€² {fβ€² = fβ€²} {gβ€² = gβ€²} i)) βŸ©β‰‘
    hom[] (Fβ€² .F₁′ ((Gβ€² .F₁′ fβ€²) β„±.βˆ˜β€² (Gβ€² .F₁′ gβ€²))) β‰‘βŸ¨ from-pathp (Fβ€² .F-βˆ˜β€²) βŸ©β‰‘
    Fβ€² .F₁′ (Gβ€² .F₁′ fβ€²) β„‹.βˆ˜β€² Fβ€² .F₁′ (Gβ€² .F₁′ gβ€²)   ∎

Furthermore, there is a displayed identity functor that lies over the identity functor.

  Idβ€² : Displayed-functor β„° β„° Id
  Idβ€² .Fβ‚€β€² x = x
  Idβ€² .F₁′ f = f
  Idβ€² .F-idβ€² = refl
  Idβ€² .F-βˆ˜β€²  = refl

The identity functor is obviously fibred.

  Idβ€²-fibred : is-fibred-functor Idβ€²
  Idβ€²-fibred f cart = cart

  Idfβ€² : Fibred-functor β„° β„° Id
  Idfβ€² .Fibred-functor.disp = Idβ€²
  Idfβ€² .Fibred-functor.F-cartesian = Idβ€²-fibred

Vertical FunctorsπŸ”—

Functors displayed over the identity functor are of particular interest. Such functors are known as vertical functors, and are commonly used to define fibrewise structure. However, they are somewhat difficult to work with if we define them directly as such, as the composite of two identity functors is not definitionally equal to the identity functor! To avoid this problem, we provide the following specialized definition.

module
  _ {o β„“ oβ€² β„“β€² oβ€²β€² β„“β€²β€²}
    {B : Precategory o β„“}
    (β„° : Displayed B oβ€² β„“β€²)
    (β„± : Displayed B oβ€²β€² β„“β€²β€²)
  where
  private
    module B = Precategory B
    module β„° = Displayed β„°
    module β„± = Displayed β„±

  record Vertical-functor : Type (o βŠ” β„“ βŠ” oβ€² βŠ” β„“β€² βŠ” oβ€²β€² βŠ” β„“β€²β€²) where
    no-eta-equality
    field
      Fβ‚€β€² : βˆ€ {x} (o : β„°.Ob[ x ]) β†’ β„±.Ob[ x ]
      F₁′ : βˆ€ {a b} {f : B.Hom a b} {aβ€² bβ€²}
          β†’ β„°.Hom[ f ] aβ€² bβ€² β†’ β„±.Hom[ f ] (Fβ‚€β€² aβ€²) (Fβ‚€β€² bβ€²)
      F-idβ€² : βˆ€ {x} {o : β„°.Ob[ x ]}
            β†’ PathP ( Ξ» _ β†’  β„±.Hom[ B.id ] (Fβ‚€β€² o) (Fβ‚€β€² o))
                         (F₁′ β„°.idβ€²) β„±.idβ€² 
      F-βˆ˜β€² : βˆ€ {a b c} {f : B.Hom b c} {g : B.Hom a b} {aβ€² bβ€² cβ€²}
                 {fβ€² : β„°.Hom[ f ] bβ€² cβ€²} {gβ€² : β„°.Hom[ g ] aβ€² bβ€²} 
            β†’ PathP (Ξ» _ β†’ β„±.Hom[ f B.∘ g ] (Fβ‚€β€² aβ€²) (Fβ‚€β€² cβ€²)) (F₁′ (fβ€² β„°.βˆ˜β€² gβ€²))
                         (F₁′ fβ€² β„±.βˆ˜β€² F₁′ gβ€²)
    β‚€β€² = Fβ‚€β€²
    ₁′ = F₁′

This definition is equivalent to a displayed functor over the identity functor.

  Displayed-functor→Vertical-functor
    : Displayed-functor β„° β„± Id β†’ Vertical-functor β„° β„±
  Displayed-functor→Vertical-functor F′ = V where
    module Fβ€² = Displayed-functor Fβ€²
    open Vertical-functor

    V : Vertical-functor β„° β„±
    V .Fβ‚€β€² = Fβ€².β‚€β€²
    V .F₁′ = Fβ€².₁′
    V .F-idβ€² = Fβ€².F-idβ€²
    V .F-βˆ˜β€² = Fβ€².F-βˆ˜β€²

  Vertical-functor→Displayed-functor
    : Vertical-functor β„° β„± β†’ Displayed-functor β„° β„± Id
  Vertical-functor→Displayed-functor V = F′ where
    module V = Vertical-functor V
    open Displayed-functor

    Fβ€² : Displayed-functor β„° β„± Id
    Fβ€² .Fβ‚€β€² = V.β‚€β€²
    Fβ€² .F₁′ = V.₁′
    Fβ€² .F-idβ€² = V.F-idβ€²
    Fβ€² .F-βˆ˜β€² = V.F-βˆ˜β€²

We also provide a specialized definition for vertical fibred functors.

  is-vertical-fibred : Vertical-functor β„° β„± β†’ Type _
  is-vertical-fibred Fβ€² =
    βˆ€ {a b aβ€² bβ€²} {f : B.Hom a b} (fβ€² : β„°.Hom[ f ] aβ€² bβ€²)
    β†’ is-cartesian β„° f fβ€² β†’ is-cartesian β„± f (F₁′ fβ€²)
    where open Vertical-functor Fβ€²
  record Vertical-fibred-functor : Type lvl where
    no-eta-equality
    field
      vert : Vertical-functor β„° β„±
      F-cartesian : is-vertical-fibred vert
    open Vertical-functor vert public

A functor displayed over the identity functor is fibred if and only if it is a vertical fibred functor.

  is-fibred→is-vertical-fibred
    : βˆ€ (F' : Displayed-functor β„° β„± Id)
    β†’ is-fibred-functor F'
    → is-vertical-fibred (Displayed-functor→Vertical-functor F')
  is-fibred→is-vertical-fibred F' F-fib = F-fib

  is-vertical-fibred→is-fibred
    : βˆ€ (F' : Vertical-functor β„° β„±)
    β†’ is-vertical-fibred F'
    → is-fibred-functor (Vertical-functor→Displayed-functor F')
  is-vertical-fibred→is-fibred F' F-fib = F-fib

  Fibred→Vertical-fibred
    : Fibred-functor β„° β„± Id β†’ Vertical-fibred-functor β„° β„±
  Fibred→Vertical-fibred F' .Vertical-fibred-functor.vert =
    Displayed-functor→Vertical-functor (Fibred-functor.disp F')
  Fibred→Vertical-fibred F' .Vertical-fibred-functor.F-cartesian =
    is-fibred→is-vertical-fibred
      (Fibred-functor.disp F')
      (Fibred-functor.F-cartesian F')

  Vertical-Fibred→Vertical
    : Vertical-fibred-functor β„° β„± β†’ Fibred-functor β„° β„± Id
  Vertical-Fibred→Vertical F' .Fibred-functor.disp =
    Vertical-functor→Displayed-functor (Vertical-fibred-functor.vert F')
  Vertical-Fibred→Vertical F' .Fibred-functor.F-cartesian =
    is-vertical-fibred→is-fibred
      (Vertical-fibred-functor.vert F')
      (Vertical-fibred-functor.F-cartesian F')

As promised, composition of vertical functors is much simpler.

  _V∘_ : Vertical-functor β„± β„‹ β†’ Vertical-functor β„° β„± β†’ Vertical-functor β„° β„‹
  (Fβ€² V∘ Gβ€²) .Fβ‚€β€² xβ€² = Fβ€² .Fβ‚€β€² (Gβ€² .Fβ‚€β€² xβ€²)
  (Fβ€² V∘ Gβ€²) .F₁′ fβ€² = Fβ€² .F₁′ (Gβ€² .F₁′ fβ€²)
  (Fβ€² V∘ Gβ€²) .F-idβ€² = ap (Fβ€² .F₁′) (Gβ€² .F-idβ€²) βˆ™ Fβ€² .F-idβ€²
  (Fβ€² V∘ Gβ€²) .F-βˆ˜β€² = ap (Fβ€² .F₁′) (Gβ€² .F-βˆ˜β€²) βˆ™ (Fβ€² .F-βˆ˜β€²)

Furthermore, the composite of vertical fibred functors is also fibred.

  V∘-fibred
    : βˆ€ (Fβ€² : Vertical-functor β„± β„‹) (Gβ€² : Vertical-functor β„° β„±)
    β†’ is-vertical-fibred Fβ€² β†’ is-vertical-fibred Gβ€² β†’ is-vertical-fibred (Fβ€² V∘ Gβ€²)
  V∘-fibred Fβ€² Gβ€² Fβ€²-fib Gβ€²-fib fβ€² cart = Fβ€²-fib (Gβ€² .F₁′ fβ€²) (Gβ€²-fib fβ€² cart)

  _Vf∘_
    : Vertical-fibred-functor β„± β„‹
    β†’ Vertical-fibred-functor β„° β„±
    β†’ Vertical-fibred-functor β„° β„‹
  (Fβ€² Vf∘ Gβ€²) .Vertical-fibred-functor.vert =
    Vertical-fibred-functor.vert Fβ€² V∘ Vertical-fibred-functor.vert Gβ€²
  (Fβ€² Vf∘ Gβ€²) .Vertical-fibred-functor.F-cartesian =
    V∘-fibred
      (Vertical-fibred-functor.vert Fβ€²)
      (Vertical-fibred-functor.vert Gβ€²)
      (Vertical-fibred-functor.F-cartesian Fβ€²)
      (Vertical-fibred-functor.F-cartesian Gβ€²)

The identity functor is obviously fibred vertical.

  IdV : Vertical-functor β„° β„°
  IdV = Displayed-functor→Vertical-functor Id′

  IdV-fibred : is-vertical-fibred IdV
  IdV-fibred = is-fibred→is-vertical-fibred Id′ Id′-fibred

  IdVf : Vertical-fibred-functor β„° β„°
  IdVf = Fibred→Vertical-fibred Idf′

Displayed Natural TransformationsπŸ”—

Just like we have defined a displayed functor F:E→F\mathbf{F} : \mathcal{E} \to \mathcal{F} lying over an ordinary functor F:A→BF : \mathcal{A} \to \mathcal{B} we can define a displayed natural transformation. Assume F,G:E→F\mathbf{F}, \mathbf{G} : \mathcal{E} \to \mathcal{F} are displayed functors over F:A→BF : \mathcal{A} \to \mathcal{B} resp. G:A→BG : \mathcal{A} \to \mathcal{B} and we have a natural transformation η:F⇒G\eta : F \Rightarrow G. Than one can define a displayed natural transformation η:F⇒G\mathbf{\eta} : \mathbf{F} \Rightarrow \mathbf{G} lying over η\eta.

module
  _ {o β„“ oβ€² β„“β€² oβ‚‚ β„“β‚‚ oβ‚‚β€² β„“β‚‚β€²}
    {A : Precategory o β„“}
    {B : Precategory oβ‚‚ β„“β‚‚}
    {β„° : Displayed A oβ€² β„“β€²}
    {β„± : Displayed B oβ‚‚β€² β„“β‚‚β€²} 
  where
  private
    module β„° = Displayed β„°
    module β„± = Displayed β„±
    open Displayed-functor
    open _=>_

    lvl : Level
    lvl = o βŠ” oβ€² βŠ” β„“ βŠ” β„“β€² βŠ” β„“β‚‚β€²
  infix 20 _=[_]=>_

  record _=[_]=>_ {F : Functor A B} {G : Functor A B} (Fβ€² : Displayed-functor β„° β„± F)
                          (Ξ± : F => G) (Gβ€² : Displayed-functor β„° β„± G)
            : Type lvl where
    no-eta-equality

    field
      Ξ·β€² : βˆ€ {x} (xβ€² : β„°.Ob[ x ]) β†’ β„±.Hom[ Ξ± .Ξ· x ] (Fβ€² .Fβ‚€β€² xβ€²) (Gβ€² .Fβ‚€β€² xβ€²)
      is-naturalβ€²
        : βˆ€ {x y f} (xβ€² : β„°.Ob[ x ]) (yβ€² : β„°.Ob[ y ]) (fβ€² : β„°.Hom[ f ] xβ€² yβ€²)
        β†’ Ξ·β€² yβ€² β„±.βˆ˜β€² Fβ€² .F₁′ fβ€² β„±.≑[ Ξ± .is-natural x y f ] Gβ€² .F₁′ fβ€² β„±.βˆ˜β€² Ξ·β€² xβ€²

Let F,G:E→FF, G : \mathcal{E} \to \mathcal{F} be two vertical functors. A displayed natural transformation between FF and GG is called a vertical natural transformation if all components of the natural transformation are vertical.

  record _=>↓_ (Fβ€² Gβ€² : Vertical-functor β„° β„±) : Type lvl where
    no-eta-equality
    field
      Ξ·β€² : βˆ€ {x} (xβ€² : β„°.Ob[ x ]) β†’ β„±.Hom[ id ] (Fβ€² .Fβ‚€β€² xβ€²) (Gβ€² .Fβ‚€β€² xβ€²)
      is-naturalβ€²
        : βˆ€ {x y f} (xβ€² : β„°.Ob[ x ]) (yβ€² : β„°.Ob[ y ]) (fβ€² : β„°.Hom[ f ] xβ€² yβ€²)
        β†’ Ξ·β€² yβ€² β„±.βˆ˜β€² Fβ€² .F₁′ fβ€² β„±.≑[ id-comm-sym ] Gβ€² .F₁′ fβ€² β„±.βˆ˜β€² Ξ·β€² xβ€²

This notion of natural transformation is also the correct one for fibred vertical functors, as there is no higher structure that needs to be preserved.

  _=>f↓_ : (Fβ€² Gβ€² : Vertical-fibred-functor β„° β„±) β†’ Type _
  Fβ€² =>f↓ Gβ€² = Fβ€² .vert =>↓ Gβ€² .vert
    where open Vertical-fibred-functor