🔍

Equations Inline Footnotes

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

import Cat.Displayed.Reasoning

open Make-bifunctor
open Functor

module Cat.Functor.Hom.Displayed
  {o ℓ o' ℓ'} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o' ℓ')
  where

open Precategory ℬ
open Cat.Displayed.Reasoning ℰ

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 → Bifunctor (Fibre ℰ x ^op) (Fibre ℰ y) (Sets ℓ')
Hom-over u = make-bifunctor λ where
  .F₀ a b  → el! (Hom[ u ] a b)
  .lmap f g → hom[ idr u ] (g ∘' f)
  .rmap f g → hom[ idl u ] (f ∘' g)
  .lmap-id → ext λ h → from-pathp[] (idr' _)
  .rmap-id → ext λ h → from-pathp[] (idl' _)
  .lmap-∘ f g → funext λ h →
    hom[] (h ∘' hom[] (g ∘' f)) ≡⟨ disp! ℰ ⟩≡
    hom[] (hom[] (h ∘' g) ∘' f) ∎
  .rmap-∘ f g → funext λ h →
    hom[] (hom[] (f ∘' g) ∘' h) ≡⟨ disp! ℰ ⟩≡
    hom[] (f ∘' hom[] (g ∘' h)) ∎
  .lrmap  f g → funext λ h →
    hom[] (hom[] (g ∘' h) ∘' f) ≡⟨ disp! ℰ ⟩≡
    hom[] (g ∘' hom[] (h ∘' 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' = Bifunctor.Right (Hom-over u) x'

Hom-over-into : ∀ {x y} → Hom x y → Ob[ y ] → Functor (Fibre ℰ x ^op) (Sets ℓ')
Hom-over-into u y' = Bifunctor.Left (Hom-over u) y'