module Cat.Functor.Hom.Displayed
  {o β„“ oβ€² β„“β€²} {ℬ : Precategory o β„“} (β„° : Displayed ℬ oβ€² β„“β€²)
  where

Displayed Hom FunctorsπŸ”—

Let E\mathcal{E} be a displayed category over B\mathcal{B}. For every u:xβ†’yu : x \to y in the base, we can obtain a bifunctor from ExopΓ—Ey\mathcal{E}_{x}^{\mathrm{op}} \times \mathcal{E}_{y} to Sets\mathbf{Sets}, where Ex\mathcal{E}_{x} denotes the fibre category of E\mathcal{E} at xx. The action of (f,h)(f, h) on gg is given by h∘g∘fh \circ g \circ f, just as in the non-displayed case.

Hom-over : βˆ€ {x y} β†’ Hom x y β†’ Functor (Fibre β„° x ^op Γ—αΆœ Fibre β„° y) (Sets β„“β€²)
Hom-over u .Fβ‚€ (a , b) = el (Hom[ u ] a b) (Hom[ u ]-set a b)
Hom-over u .F₁ (f , h) g = hom[ idl _ βˆ™ idr _ ] (h βˆ˜β€² g βˆ˜β€² f)
Hom-over u .F-id = funext Ξ» f β†’
  aprβ€² {q = idl _} (idrβ€² f) βˆ™ idl[]
Hom-over u .F-∘ (f , h) (f' , h') = funext Ξ» g β†’
  hom[] (hom[] (h βˆ˜β€² h') βˆ˜β€² g βˆ˜β€² hom[] (f' βˆ˜β€² f)) β‰‘βŸ¨ disp! β„° βŸ©β‰‘
  hom[] (h βˆ˜β€² hom[] (h' βˆ˜β€² g βˆ˜β€² f') βˆ˜β€² f) ∎

We can also define partially applied versions of this functor.

Hom-over-from : βˆ€ {x y} β†’ Hom x y β†’ Ob[ x ] β†’ Functor (Fibre β„° y) (Sets β„“β€²)
Hom-over-from u xβ€² .Fβ‚€ yβ€² = el (Hom[ u ] xβ€² yβ€²) (Hom[ u ]-set xβ€² yβ€²)
Hom-over-from u xβ€² .F₁ f g = hom[ idl u ] (f βˆ˜β€² g)
Hom-over-from u xβ€² .F-id = funext Ξ» f β†’ idl[]
Hom-over-from u xβ€² .F-∘ f g  = funext Ξ» h β†’
  smashl _ _ βˆ™ sym assoc[] βˆ™ sym (smashr _ _)

Hom-over-into : βˆ€ {x y} β†’ Hom x y β†’ Ob[ y ] β†’ Functor (Fibre β„° x ^op) (Sets β„“β€²)
Hom-over-into u yβ€² .Fβ‚€ xβ€² = el (Hom[ u ] xβ€² yβ€²) (Hom[ u ]-set xβ€² yβ€²)
Hom-over-into u yβ€² .F₁ f g = hom[ idr u ] (g βˆ˜β€² f)
Hom-over-into u yβ€² .F-id = funext Ξ» f β†’ idr[]
Hom-over-into u yβ€² .F-∘ f g = funext Ξ» h β†’
  smashr _ _ βˆ™ assoc[] βˆ™ (sym $ smashl _ _ )