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 $\mathcal{E}, \mathcal{F}$ displayed over a common base category $\mathcal{B}$, it makes immediate sense to talk about functors $F : \mathcal{E} \to \mathcal{F}$: you’d have an assignment of objects $F_x : \mathcal{E}^*(x) \to \mathcal{F}^*(x)$ and an assignment of morphisms

$$F_{a,b,f} : (a' \to_f b') \to (F_a(a') \to_f F_b(b'))\text{,}$$

which makes sense because $F_a(a')$ lies over $a$, just as $a'$ did, that a morphism $F_a(a') \to F_b(b')$ is allowed to lie over a morphism $f : 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 ${\mathbf{F}} : \mathcal{E} \to \mathcal{F}$ lying over an ordinary functor $F : \mathcal{A} \to \mathcal{B}$ to mediate between the bases.

  record Displayed-functor : Type lvl where
    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 $F$. 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 $\mathcal{E}$ and $\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
    field
      disp : Displayed-functor

    open Displayed-functor disp public

    field
      F-cartesian
        : ∀ {a b a′ b′} {f : A.Hom a b} (f′ : ℰ.Hom[ f ] a′ b′)
        → is-cartesian ℰ f f′ → is-cartesian ℱ (F.₁ f) (F₁′ f′)