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}\text{.}$ 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}\text{,}$ where ${\mathcal{E}}_x$ denotes the fibre category of $\mathcal{E}$ at $x\text{.}$ The action of $(f,h)$ on $g$ is given by $h\circ g\circ f\text{,}$ 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 _ _ )