🔍

Equations Inline Footnotes

open import Cat.Displayed.Reasoning as Dr
open import Cat.Displayed.Functor
open import Cat.Displayed.Base
open import Cat.Functor.Base
open import Cat.Reasoning as Cr
open import Cat.Prelude

module Cat.Displayed.Instances.Functor where

open _=>_
open _=[_]=>_
open Functor
open Displayed-functor

Displayed functor (pre)categories🔗

Just as the functors between precategories $\mathcal{A}$ and $\mathcal{B}$ form a precategory $[\mathcal{A},\mathcal{B}]\text{,}$ the displayed functors between displayed precategories $\mathcal{E}$ and $\mathcal{F}$ over $\mathcal{A}$ and $\mathcal{B}$ form a displayed precategory $[\mathcal{E},\mathcal{F}]$ over $[\mathcal{A},\mathcal{B}]\text{,}$ with displayed natural transformations as morphisms. The construction is analogous to the non-displayed functor category. For instance, we define identity displayed natural transformations by

module _
  {oa ℓa ob ℓb oe ℓe of ℓf}
  {A : Precategory oa ℓa} {B : Precategory ob ℓb}
  {ℰ : Displayed A oe ℓe} {ℱ : Displayed B of ℓf}
  where

  private
    variable
      F G H : Functor A B
      F' : Displayed-functor F ℰ ℱ
      G' : Displayed-functor G ℰ ℱ
      H' : Displayed-functor H ℰ ℱ

    module A = Cr A
    module B = Cr B
    module ℱ = Dr ℱ
    module ℰ = Dr ℰ

  idnt' : F' =[ idnt ]=> F'
  idnt' .η' _ = ℱ.id'
  idnt' .is-natural' _ _ _ = ℱ.to-pathp[] ℱ.id-comm-sym[]

Composition of displayed natural transformations is defined by

  _∘nt'_ : ∀ {α β} → G' =[ α ]=> H' → F' =[ β ]=> G' → F' =[ α ∘nt β ]=> H'
  (α' ∘nt' β') .η' x' = α' .η' x' ℱ.∘' β' .η' x'
  _∘nt'_ {G' = G'} {H' = H'} {F' = F'} {α = α} {β = β} α' β'
    .is-natural' {x} {y} {f} x' y' f' = ℱ.begin[]
      (α' .η' y' ℱ.∘' β' .η' y') ℱ.∘' F₁' F' f' ℱ.≡[]⟨ ℱ.pullr[] (β .is-natural x y f) (is-natural' β' x' y' f') ⟩ℱ.≡[]
      α' .η' y' ℱ.∘' ₁' G' f' ℱ.∘' β' .η' x'    ℱ.≡[]⟨ ℱ.extendl[] (α .is-natural x y f) (is-natural' α' x' y' f') ⟩ℱ.≡[]
      ₁' H' f' ℱ.∘' α' .η' x' ℱ.∘' β' .η' x'    ℱ.∎[]

We then define the displayed category $[\mathcal{E},\mathcal{F}]$ over $[\mathcal{A},\mathcal{B}]$ so that an object over $F$ is a displayed functor over $F\text{,}$ and a displayed natural transformation over $\eta$ is a morphism over $\eta \text{.}$

module _
  {oa ℓa ob ℓb oe ℓe of ℓf}
  {A : Precategory oa ℓa} {B : Precategory ob ℓb}
  (ℰ : Displayed A oe ℓe) (ℱ : Displayed B of ℓf)
  where

  private module ℱ = Dr ℱ

  DisCat[_,_] : Displayed Cat[ A , B ] (oa ⊔ ℓa ⊔ oe ⊔ ℓe ⊔ of ⊔ ℓf) (oa ⊔ ℓa ⊔ oe ⊔ ℓe ⊔ ℓf)
  DisCat[_,_] .Ob[_] F = Displayed-functor F ℰ ℱ
  DisCat[_,_] .Hom[_] α F' G' = F' =[ α ]=> G'
  DisCat[_,_] .Hom[_]-set α F' G' = hlevel 

  DisCat[_,_] .id' = idnt'
  DisCat[_,_] ._∘'_ = _∘nt'_

  DisCat[_,_] .idr' α' = Nat'-path λ x' → ℱ.idr' (η' α' x')
  DisCat[_,_] .idl' α' = Nat'-path λ x' → ℱ.idl' (η' α' x')
  DisCat[_,_] .assoc' α' β' γ' = Nat'-path λ x' →
    ℱ.assoc' (η' α' x') (η' β' x') (η' γ' x')

  DisCat[_,_] .hom[_] {x = F'} {G'} p α' = record
    { η' = λ {x} x' → ℱ.hom[ p ηₚ x ] (α' .η' x')
    ; is-natural' = λ {x} {y} {f} x' y' f' → ℱ.begin[]
      ℱ.hom[ p ηₚ y ] (α' .η' y') ℱ.∘' ₁' F' f' ℱ.≡[]⟨ ℱ.unwrapl (p ηₚ y) ⟩ℱ.≡[]
      α' .η' y' ℱ.∘' ₁' F' f'                   ℱ.≡[]⟨ α' .is-natural' x' y' f' ⟩ℱ.≡[]
      ₁' G' f' ℱ.∘' α' .η' x'                   ℱ.≡[]⟨ ℱ.wrapr (p ηₚ x) ⟩ℱ.≡[]
      ₁' G' f' ℱ.∘' ℱ.hom[ p ηₚ x ] (α' .η' x') ℱ.∎[]
    }
  DisCat[_,_] .coh[_] p α' = Nat'-path λ {x} x' → ℱ.coh[ p ηₚ x ] (η' α' x')