open import Cat.Instances.Functor
open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Displayed.Cartesian
import Cat.Displayed.Reasoning as DR
import Cat.Functor.Reasoning as FR
import Cat.Reasoning as CR
module Cat.Displayed.Functor where

Displayed and fibred functorsπŸ”—

If you have a pair of categories displayed over a common base category it makes immediate sense to talk about functors you’d have an assignment of objects and an assignment of morphisms

which makes sense because lies over just as did, that a morphism is allowed to lie over a morphism But, in the spirit of relativising category theory, it makes more sense to consider functors between categories displayed over different bases, as in

with our displayed functor lying over an ordinary functor to mediate between the bases.

module
  _ {oa β„“a ob β„“b oe β„“e of β„“f}
    {A : Precategory oa β„“a}
    {B : Precategory ob β„“b}
    (F : Functor A B)
    (β„° : Displayed A oe β„“e)
    (β„± : Displayed B of β„“f)
  where
  private
    module F = FR F
    module A = CR A
    module B = CR B
    module β„° = DR β„°
    module β„± = DR β„±
  record Displayed-functor : Type (oa βŠ” β„“a βŠ” oe βŠ” β„“e βŠ” of βŠ” β„“f) where
    no-eta-equality
    field
      Fβ‚€' : βˆ€ {x} (x' : β„°.Ob[ x ]) β†’ β„±.Ob[ F.β‚€ x ]
      F₁'
        : βˆ€ {a b} {f : A.Hom a b} {a' b'}
        β†’ β„°.Hom[ f ] a' b' β†’ β„±.Hom[ F.₁ f ] (Fβ‚€' a') (Fβ‚€' b')

In order to state the displayed functoriality laws, we require functoriality for our mediating functor Functors between categories displayed over the same base can be recovered as the β€œvertical displayed functors”, i.e., those lying over the identity functor.

      F-id'
        : βˆ€ {x} {x' : β„°.Ob[ x ]}
        β†’ F₁' (β„°.id' {x} {x'}) β„±.≑[ F.F-id ] (β„±.id' {F.β‚€ x} {Fβ‚€' x'})
      F-∘'
        : βˆ€ {a b c} {f : A.Hom b c} {g : A.Hom a b} {a' b' c'}
        β†’ {f' : β„°.Hom[ f ] b' c'} {g' : β„°.Hom[ g ] a' b'}
        β†’ F₁' (f' β„°.∘' g') β„±.≑[ F.F-∘ f g ] (F₁' f' β„±.∘' F₁' g')

    β‚€' = Fβ‚€'
    ₁' = F₁'
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 A = Precategory A
    module B = Precategory B
    module β„° = Displayed β„°
    module β„± = Displayed β„±

  open Functor
  open Displayed-functor
  private unquoteDecl eqv = declare-record-iso eqv (quote Displayed-functor)

  Displayed-functor-pathp
    : {F G : Functor A B}
    β†’ {F' : Displayed-functor F β„° β„±} {G' : Displayed-functor G β„° β„±}
    β†’ (p : F ≑ G)
    β†’ (q0 : βˆ€ {x} β†’ (x' : β„°.Ob[ x ]) β†’ PathP (Ξ» i β†’ β„±.Ob[ p i .Fβ‚€ x ]) (F' .Fβ‚€' x') (G' .Fβ‚€' x'))
    β†’ (q1 : βˆ€ {x y x' y'} {f : A.Hom x y} β†’ (f' : β„°.Hom[ f ] x' y')
            β†’ PathP (Ξ» i β†’ β„±.Hom[ p i .F₁ f ] (q0 x' i) (q0 y' i)) (F' .F₁' f') (G' .F₁' f'))
    β†’ PathP (Ξ» i β†’ Displayed-functor (p i) β„° β„±) F' G'
  Displayed-functor-pathp {F = F} {G = G} {F' = F'} {G' = G'} p q0 q1 =
    injectiveP (Ξ» _ β†’ eqv) ((Ξ» i x' β†’ q0 x' i) ,β‚š (Ξ» i f' β†’ q1 f' i) ,β‚š prop!)

Note that, if and are fibred categories over their bases (rather than just displayed categories), then the appropriate notion of 1-cell are displayed functors that take cartesian morphisms to cartesian morphisms.

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}
    {F : Functor A B}
  where
  private
    module F = Functor F
    module A = CR A
    module B = CR B
    module β„° where
      open Displayed β„° public
      open Cat.Displayed.Cartesian β„° public
    module β„± where
      open Displayed β„± public
      open Cat.Displayed.Cartesian β„± public

    lvl : Level
    lvl = oa βŠ” β„“a βŠ” ob βŠ” β„“b βŠ” oe βŠ” β„“e βŠ” of βŠ” β„“f
  record is-fibred-functor (F' : Displayed-functor F β„° β„±) : Type lvl where
    no-eta-equality
    open Displayed-functor F'
    field
      F-cartesian
        : βˆ€ {a b a' b'} {f : A.Hom a b} {f' : β„°.Hom[ f ] a' b'}
        β†’ β„°.is-cartesian f f'
        β†’ β„±.is-cartesian (F.₁ f) (F₁' f')
  instance
    H-Level-is-fibred-functor
      : βˆ€ {F' : Displayed-functor F β„° β„±}
      β†’ {n : Nat}
      β†’ H-Level (is-fibred-functor F') (suc n)
    H-Level-is-fibred-functor {n = n} =
      hlevel-instance (Iso→is-hlevel (suc n) eqv (hlevel (suc n)))
      where
        unquoteDecl eqv = declare-record-iso eqv (quote is-fibred-functor)
        open β„± -- Needed for the is-cartesian H-Level instances.

Just like with isomorphisms and limits, it makes sense to consider the converse property: displayed functors that reflect cartesian morphisms. An example is given by fully faithful displayed functors.

  record reflects-cartesian-maps (F' : Displayed-functor F β„° β„±) : Type lvl where
    no-eta-equality
    open Displayed-functor F'
    field
      reflects
        : βˆ€ {a b a' b'} {f : A.Hom a b} {f' : β„°.Hom[ f ] a' b'}
        β†’ β„±.is-cartesian (F.₁ f) (F₁' f')
        β†’ β„°.is-cartesian f f'
  instance
    H-Level-reflects-cartesian-maps
      : βˆ€ {F' : Displayed-functor F β„° β„±}
      β†’ {n : Nat}
      β†’ H-Level (reflects-cartesian-maps F') (suc n)
    H-Level-reflects-cartesian-maps {n = n} =
      hlevel-instance (Iso→is-hlevel (suc n) eqv (hlevel (suc n)))
      where
        unquoteDecl eqv = declare-record-iso eqv (quote reflects-cartesian-maps)
        open β„± -- Needed for the is-cartesian H-Level instances.

One can also define the composition of displayed functors, which lies over the composition of the underlying functors.

module
  _ {oa β„“a ob β„“b oc β„“c oe β„“e of β„“f oh β„“h}
    {A : Precategory oa β„“a}
    {B : Precategory ob β„“b}
    {C : Precategory oc β„“c}
    {β„° : Displayed A oe β„“e}
    {β„± : Displayed B of β„“f}
    {β„‹ : Displayed C oh β„“h}
    {F : Functor B C} {G : Functor A B}
  where
  private
    module A = Precategory A
    module B = Precategory B
    module β„° = Displayed β„°
    module β„± = Displayed β„±
    module F = Functor F
    module G = Functor G
    module β„‹ = DR β„‹

    open DR β„‹
    open Displayed-functor
    open is-fibred-functor

  infixr 30 _F∘'_
  _F∘'_
    : Displayed-functor F β„± β„‹
    β†’ Displayed-functor G β„° β„±
    β†’ Displayed-functor (F F∘ G) β„° β„‹
  (F' F∘' G') .Fβ‚€' x = F' .Fβ‚€' (G' .Fβ‚€' x)
  (F' F∘' G') .F₁' f = F' .F₁' (G' .F₁' f)
  (F' F∘' G') .F-id' =
    β„‹.cast[] $
      F' .F₁' (G' .F₁' β„°.id') β„‹.≑[]⟨ apd (Ξ» i β†’ F' .F₁') (G' .F-id') ⟩
      F' .F₁' β„±.id'            β„‹.≑[]⟨ F' .F-id' ⟩
      β„‹.id'                   ∎
  (F' F∘' G') .F-∘' {f = f} {g = g} {f' = f'} {g' = g'} =
    β„‹.cast[] $
      F' .F₁' (G' .F₁' (f' β„°.∘' g'))                   β„‹.≑[]⟨ apd (Ξ» i β†’ F' .F₁') (G' .F-∘') ⟩
      F₁' F' (G' .F₁' f' β„±.∘' G' .F₁' g')              β„‹.≑[]⟨ F' .F-∘' ⟩
      (F' .F₁' (G' .F₁' f') β„‹.∘' F' .F₁' (G' .F₁' g')) ∎

The composite of two fibred functors is a fibred functor.

  F∘'-fibred
    : βˆ€ {F' : Displayed-functor F β„± β„‹} {G' : Displayed-functor G β„° β„±}
    β†’ is-fibred-functor F' β†’ is-fibred-functor G'
    β†’ is-fibred-functor (F' F∘' G')
  F∘'-fibred F'-fibred G'-fibred .F-cartesian f'-cart =
    F'-fibred .F-cartesian (G'-fibred .F-cartesian f'-cart)

Furthermore, there is a displayed identity functor that lies over the identity functor.

module _
  {ob β„“b oe β„“e}
  {B : Precategory ob β„“b}
  {β„° : Displayed B oe β„“e}
  where
  open Displayed-functor
  open is-fibred-functor
  Id' : Displayed-functor Id β„° β„°
  Id' .Fβ‚€' x = x
  Id' .F₁' f = f
  Id' .F-id' = refl
  Id' .F-∘'  = refl

The identity functor is obviously fibred.

  Id'-fibred : is-fibred-functor Id'
  Id'-fibred .F-cartesian f'-cart = f'-cart

Vertical functorsπŸ”—

Functors displayed over the identity functor are of particular interest. Such functors are known as vertical functors, and are commonly used to define fibrewise structure. However, they are somewhat difficult to work with if we define them directly as such, as the composite of two identity functors is not definitionally equal to the identity functor! To avoid this problem, we provide the following specialized definition.

module
  _ {o β„“ o' β„“' o'' β„“''}
    {B : Precategory o β„“}
    (β„° : Displayed B o' β„“')
    (β„± : Displayed B o'' β„“'')
  where
  private
    module B = Precategory B
    module β„° = Displayed β„°
    module β„± = Displayed β„±
    module F = DR β„± using (hom[])
    module ℰ↓ {x} = Precategory (Fibre β„° x) using (_∘_)
    module ℱ↓ {x} = Precategory (Fibre β„± x) using (_∘_)
  Vertical-functor : Type (o βŠ” β„“ βŠ” o' βŠ” β„“' βŠ” o'' βŠ” β„“'')
  Vertical-functor = Displayed-functor Id β„° β„±

As promised, composition of vertical functors is much simpler.

module _
  {ob β„“b oe β„“e of β„“f oh β„“h}
  {B : Precategory ob β„“b}
  {β„° : Displayed B oe β„“e}
  {β„± : Displayed B of β„“f}
  {β„‹ : Displayed B oh β„“h}
  where
  open Displayed-functor
  open is-fibred-functor

  infixr 30 _∘V_
  _∘V_ : Vertical-functor β„± β„‹ β†’ Vertical-functor β„° β„± β†’ Vertical-functor β„° β„‹
  (F' ∘V G') .Fβ‚€' x' = F' .Fβ‚€' (G' .Fβ‚€' x')
  (F' ∘V G') .F₁' f' = F' .F₁' (G' .F₁' f')
  (F' ∘V G') .F-id' = ap (F' .F₁') (G' .F-id') βˆ™ F' .F-id'
  (F' ∘V G') .F-∘' = ap (F' .F₁') (G' .F-∘') βˆ™ (F' .F-∘')

General and vertical composition of vertical functors definitionnally agree on both the actions on objects and morphisms: the only difference is in how the result is indexed.

  F∘'-∘V-pathp
    : βˆ€ {F' : Vertical-functor β„± β„‹} {G' : Vertical-functor β„° β„±}
    β†’ PathP (Ξ» i β†’ Displayed-functor (F∘-id2 i) β„° β„‹) (F' F∘' G') (F' ∘V G')
  F∘'-∘V-pathp =
    Displayed-functor-pathp (Ξ» i β†’ F∘-id2 i)
      (Ξ» x' β†’ refl)
      (Ξ» f' β†’ refl)

As such, the composite of vertical fibred functors is also fibred.

  ∘V-fibred
    : βˆ€ {F' : Vertical-functor β„± β„‹} {G' : Vertical-functor β„° β„±}
    β†’ is-fibred-functor F' β†’ is-fibred-functor G' β†’ is-fibred-functor (F' ∘V G')
  ∘V-fibred F'-fib G'-fib .F-cartesian cart =
    F'-fib .F-cartesian (G'-fib .F-cartesian cart)
module
  _ {o β„“ o' β„“' o'' β„“''}
    {B : Precategory o β„“}
    {β„° : Displayed B o' β„“'}
    {β„± : Displayed B o'' β„“''}
  where
  private
    module B = Precategory B
    module β„° = DR β„°
    module β„± = DR β„±

    module ℰ↓ {x} = Precategory (Fibre β„° x) using (_∘_)
    module ℱ↓ {x} = Precategory (Fibre β„± x) using (_∘_)

  module Vertical-functor (F : Vertical-functor β„° β„±) where
    open Displayed-functor F public

    abstract
      F-βˆ˜β†“
        : βˆ€ {x} {a b c : β„°.Ob[ x ]} {f : β„°.Hom[ B.id ] b c} {g : β„°.Hom[ B.id ] a b}
        β†’ F₁' (f ℰ↓.∘ g) ≑ F₁' f ℱ↓.∘ F₁' g
      F-βˆ˜β†“ = β„±.cast[] (apd (Ξ» i β†’ F₁') (β„°.unwrap _) β„±.βˆ™[] F-∘' β„±.βˆ™[] β„±.wrap _)

    Fibre-map : βˆ€ x β†’ Functor (Fibre β„° x) (Fibre β„± x)
    Fibre-map x .Functor.Fβ‚€ = Fβ‚€'
    Fibre-map x .Functor.F₁ = F₁'
    Fibre-map x .Functor.F-id = F-id'
    Fibre-map x .Functor.F-∘ f g = F-βˆ˜β†“

  open Vertical-functor

  Vertical-functor-path
    : {F G : Vertical-functor β„° β„±}
    β†’ (p0 : βˆ€ {x} β†’ (x' : β„°.Ob[ x ]) β†’ F .Fβ‚€' x' ≑ G .Fβ‚€' x')
    β†’ (p1 : βˆ€ {x y x' y'} {f : B.Hom x y} β†’ (f' : β„°.Hom[ f ] x' y')
            β†’ PathP (Ξ» i β†’ β„±.Hom[ f ] (p0 x' i) (p0 y' i)) (F .F₁' f') (G .F₁' f'))
    β†’ F ≑ G
  Vertical-functor-path = Displayed-functor-pathp refl

Displayed natural transformationsπŸ”—

Just like we have defined a displayed functor lying over an ordinary functor we can define a displayed natural transformation. Assume are displayed functors over resp. and we have a natural transformation Than one can define a displayed natural transformation lying over 

module
  _ {o β„“ o' β„“' oβ‚‚ β„“β‚‚ oβ‚‚' β„“β‚‚'}
    {A : Precategory o β„“}
    {B : Precategory oβ‚‚ β„“β‚‚}
    {β„° : Displayed A o' β„“'}
    {β„± : Displayed B oβ‚‚' β„“β‚‚'}
  where
  private
    module A = CR A
    module β„° = Displayed β„°
    module β„± = Displayed β„±
    module ℰ↓ {x} = Precategory (Fibre β„° x) using (_∘_)
    module ℱ↓ {x} = Precategory (Fibre β„± x) using (_∘_)

    open Displayed-functor
    open _=>_

    lvl : Level
    lvl = o βŠ” o' βŠ” β„“ βŠ” β„“' βŠ” β„“β‚‚'
  infix 20 _=[_]=>_
  record _=[_]=>_
    {F : Functor A B} {G : Functor A B}
    (F' : Displayed-functor F β„° β„±)
    (Ξ± : F => G)
    (G' : Displayed-functor G β„° β„±)
    : Type lvl
    where
    no-eta-equality

    field
      Ξ·' : βˆ€ {x} (x' : β„°.Ob[ x ]) β†’ β„±.Hom[ Ξ± .Ξ· x ] (F' .Fβ‚€' x') (G' .Fβ‚€' x')
      is-natural'
        : βˆ€ {x y f} (x' : β„°.Ob[ x ]) (y' : β„°.Ob[ y ]) (f' : β„°.Hom[ f ] x' y')
        β†’ Ξ·' y' β„±.∘' F' .F₁' f' β„±.≑[ Ξ± .is-natural x y f ] G' .F₁' f' β„±.∘' Ξ·' x'

Let be two vertical functors. A displayed natural transformation between and is called a vertical natural transformation if all components of the natural transformation are vertical.

module _
  {ob β„“b oe β„“e of β„“f}
  {B : Precategory ob β„“b}
  {β„° : Displayed B oe β„“e}
  {β„± : Displayed B of β„“f}
  where
  private
    open CR B
    module β„° = Displayed β„°
    module β„± = DR β„±
    module ℱ↓ {x} = CR (Fibre β„± x)

    open Displayed-functor

  infix 20 _=>↓_
  _=>↓_  : Vertical-functor β„° β„± β†’ Vertical-functor β„° β„± β†’ Type _
  F' =>↓ G' = F' =[ idnt ]=> G'
  module _=>↓_ {F' G' : Vertical-functor β„° β„±} (Ξ± : F' =>↓ G') where
    open _=[_]=>_ Ξ± public

    abstract
      is-natural↓
        : βˆ€ {x} (x' y' : β„°.Ob[ x ]) (f' : β„°.Hom[ id ] x' y')
        β†’ Ξ·' y' ℱ↓.∘ F' .F₁' f' ≑ G' .F₁' f' ℱ↓.∘ Ξ·' x'
      is-natural↓ x y f =
        ap β„±.hom[] (β„±.from-pathp[]⁻ (is-natural' x y f))
        βˆ™ sym (β„±.duplicate _ _ _)

  private unquoteDecl eqv = declare-record-iso eqv (quote _=[_]=>_)

  instance
    Extensional-=>↓
      : βˆ€ {β„“r F' G'}
      β†’ ⦃ _ : Extensional (βˆ€ {x} (x' : β„°.Ob[ x ]) β†’ β„±.Hom[ id ] (F' .Fβ‚€' x') (G' .Fβ‚€' x')) β„“r ⦄
      β†’ Extensional (F' =>↓ G') β„“r
    Extensional-=>↓ {F' = F'} {G' = G'}  ⦃ e ⦄  = injectionβ†’extensional! {f = _=>↓_.Ξ·'}
      (Ξ» p β†’ Iso.injective eqv (Ξ£-prop-path! p)) e

    H-Level-=>↓ : βˆ€ {F' G'} {n} β†’ H-Level (F' =>↓ G') (2 + n)
    H-Level-=>↓ = basic-instance 2 (Isoβ†’is-hlevel 2 eqv (hlevel 2))

  open _=>↓_

  idnt↓ : βˆ€ {F} β†’ F =>↓ F
  idnt↓ .Ξ·' x' = β„±.id'
  idnt↓ .is-natural' x' y' f' = β„±.to-pathp[] (DR.id-comm[] β„±)

  _∘nt↓_ : βˆ€ {F G H} β†’ G =>↓ H β†’ F =>↓ G β†’ F =>↓ H
  (f ∘nt↓ g) .Ξ·' x' = f .Ξ·' _ ℱ↓.∘ g .Ξ·' x'
  _∘nt↓_ {F = F} {G = G} {H = H} f g .is-natural' {f = b} x' y' f' =
    let open DR β„± in to-pathp[] (
        ap hom[] (whisker-l (idl id))
    βˆ™βˆ™ sym (duplicate (ap (_∘ b) (idl id) βˆ™ id-comm-sym) _ _)
    βˆ™βˆ™ ap hom[] (from-pathp[]⁻ (pullr' id-comm-sym (g .is-natural' _ _ _)
          {q = ap (_∘ b) (idl id) βˆ™ id-comm-sym βˆ™ introl refl}))
    βˆ™βˆ™ sym (duplicate (eliml refl) _ _)
    βˆ™βˆ™ ap hom[] (from-pathp[]⁻ (extendl' id-comm-sym (f .is-natural' x' y' f') {q = extendl id-comm-sym}))
    βˆ™βˆ™ sym (duplicate (ap (b ∘_) (idl id)) (eliml refl) _)
    βˆ™βˆ™ unwhisker-r _ _)

module _
  {ob β„“b oc β„“c od β„“d oe β„“e}
  {B : Precategory ob β„“b}
  {π’ž : Displayed B oc β„“c}
  {π’Ÿ : Displayed B od β„“d}
  {β„° : Displayed B oe β„“e}
  {F G : Vertical-functor π’Ÿ β„°} {H K : Vertical-functor π’ž π’Ÿ}
  (Ξ± : F =>↓ G) (Ξ² : H =>↓ K) where

  open Displayed-functor
  open _=>↓_
  open CR B
  private module E {x} = CR (Fibre β„° x) using (_∘_)

  _◆↓_ : (F ∘V H) =>↓ (G ∘V K)
  _◆↓_ .Ξ·' x' = G .F₁' (Ξ² .Ξ·' _) E.∘ Ξ± .Ξ·' _
  _◆↓_ .is-natural' x' y' f' = to-pathp[] (
      ap hom[] (whisker-l (idl id))
      βˆ™βˆ™ sym (duplicate (ap (_∘ _) (idl id) βˆ™ id-comm-sym) _ _)
      βˆ™βˆ™ ap hom[] (from-pathp[]⁻ (pullr' _ (Ξ± .is-natural' _ _ _) {q = pullr id-comm-sym}))
      βˆ™βˆ™ sym (duplicate (eliml refl) _ _)
      βˆ™βˆ™ ap hom[] (from-pathp[]⁻
        (extendl' _ (symP (G .F-∘') βˆ™[] (apd (Ξ» i β†’ G .F₁') (Ξ² .is-natural' _ _ _) βˆ™[] G .F-∘'))
          {q = extendl id-comm-sym}))
      βˆ™βˆ™ sym (duplicate (ap (_ ∘_) (idl id)) _ _) βˆ™βˆ™ unwhisker-r _ _)
    where open DR β„°