open import Cat.Displayed.Cartesian
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Reasoning as CR

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
      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:

  record Fibred-functor : Type (lvl βŠ” oβ‚‚ βŠ” β„“β‚‚) where
      disp : Displayed-functor

    open Displayed-functor disp public

        : βˆ€ {a b aβ€² bβ€²} {f : A.Hom a b} (fβ€² : β„°.Hom[ f ] aβ€² bβ€²)
        β†’ is-cartesian β„° f fβ€² β†’ is-cartesian β„± (F.₁ f) (F₁′ fβ€²)