open import Cat.Instances.Product
open import Cat.Displayed.Solver
open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning

module Cat.Functor.Hom.Displayed
{o β oβ² ββ²} {β¬ : Precategory o β} (β° : Displayed β¬ oβ² ββ²)
where

open Precategory β¬
open Displayed β°
open Cat.Displayed.Reasoning β°
open Functor


# Displayed Hom Functorsπ

Let $\mathcal{E}$ be a displayed category over $\mathcal{B}$. For every $u : x \to y$ in the base, we can obtain a bifunctor from $\mathcal{E}_{x}^{\mathrm{op}} \times \mathcal{E}_{y}$ to $\mathbf{Sets}$, where $\mathcal{E}_{x}$ denotes the fibre category of $\mathcal{E}$ at $x$. The action of $(f, h)$ on $g$ is given by $h \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 _ _ )