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′)