module Cat.Displayed.Instances.Diagrams
  {o β„“ o' β„“'}
  {B : Precategory o β„“}
  (E : Displayed B o' β„“')
  where

open Precategory B
open Displayed E
open Cat.Displayed.Reasoning E
open Functor
open _=>_

The diagram fibrationπŸ”—

The appropriate notion of structure for a displayed category EB\mathcal{E} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B} is fibrewise structure: structure found in each fibre category, preserved by the reindexing functors when E\mathcal{E} is an (op)fibration.

For instance, the correct notion of J\mathcal{J}-shaped limit in E\mathcal{E} are the fibred limits: where every fibre category has limits of shape J\mathcal{J}, and these are preserved by reindexing. Unfortunately, proof assistants: since none of the commutativity conditions for limits are definitional, this definition condemns the formaliser to transport hell.

Instead, we opt for a more abstract approach, which starts with a reorganization of what a fibrewise diagram in E\mathcal{E} is. Recall that the fibration of liftings describes liftings of functors Jβ†’B\mathcal{J} \to \mathcal{B} along the projection functor Ο€:∫Eβ†’B\pi : \int \mathcal{E} \to \mathcal{B}. If we focus on liftings along a constant functor Ξ”x:Jβ†’B\Delta_{x} : \mathcal{J} \to \mathcal{B}, we get a diagram in E\mathcal{E} that lies entirely in the fibre Ex\mathcal{E}_{x}: a fibrewise diagram!

This allows us to concisely define the fibration of fibrewise diagrams as the base change of E→B\mathcal{E} \to \mathcal{B} along the functor B→[J,B]\mathcal{B} \to [\mathcal{J}, \mathcal{B}] that takes an object to the constant diagram on that object.

Diagrams
 : βˆ€ {oj β„“j} (J : Precategory oj β„“j)
 β†’ Displayed B _ _
Diagrams J = Change-of-base ConstD (Liftings E J)

When E\mathcal{E} is a fibration, then so is the fibration of diagrams.

  Diagram-fibration : Cartesian-fibration E β†’ Cartesian-fibration (Diagrams J)
  Diagram-fibration fib =
    Change-of-base-fibration ConstD (Liftings E _)
      (Liftings-fibration E _ fib)

The constant fibrewise diagram functorπŸ”—

Crucially, we have a β€œconstant fibrewise diagram functor” that takes an object xβ€²:Exx' : E_{x} to the constant diagram. However, defining this functor will require a small bit of machinery.

To begin, we characterize liftings of the constant functor, and natural transformations between them.

  ConstL : βˆ€ {x} β†’ Ob[ x ] β†’ Lifting {J = J} E (Const x)
  ConstL x' .Fβ‚€' _ = x'
  ConstL x' .F₁' _ = id'
  ConstL x' .F-id' = refl
  ConstL x' .F-∘' _ _ = symP (idr' _)

  const-ntl
    : βˆ€ {x y x' y'} {f : Hom x y} β†’ Hom[ f ] x' y'
    β†’ (ConstL x') =[ const-nt f ]=>l (ConstL y')
  const-ntl f' .Ξ·' _ = f'
  const-ntl f' .is-natural' _ _ _ =
    idr' _ βˆ™[] symP (idl' _)

We also have a vertical functor from E\mathcal{E} to the fibration of diagrams of shape J\mathcal{J}, which takes an xβ€²x' to the constant diagram.

  ConstFibD : Vertical-functor E (Diagrams J)
  ConstFibD .Vertical-functor.Fβ‚€' = ConstL
  ConstFibD .Vertical-functor.F₁' = const-ntl
  ConstFibD .Vertical-functor.F-id' =
    Nat-lift-pathp (Ξ» x β†’ sym (transport-refl _))
  ConstFibD .Vertical-functor.F-∘' =
    Nat-lift-pathp (Ξ» x β†’ sym (transport-refl _))

Next, we note that liftings of the constant functor correspond with diagrams in fibre categories.

  ConstL→Diagram
    : βˆ€ {x} β†’ Lifting {J = J} E (Const x) β†’ Functor J (Fibre E x)
  Diagram→ConstL
    : βˆ€ {x} β†’ Functor J (Fibre E x) β†’ Lifting {J = J} E (Const x)

Furthermore, natural transformations between diagrams in a fibre of EE correspond to natural transformations between liftings of a constant functor.

  ConstL-natl→Diagram-nat
    : βˆ€ {x} {F G : Functor J (Fibre E x)}
    → Diagram→ConstL F =[ const-nt id ]=>l Diagram→ConstL G
    β†’ F => G

  Diagram-nat→ConstL-natl
    : βˆ€ {x} {F G : Functor J (Fibre E x)}
    β†’ F => G
    → Diagram→ConstL F =[ const-nt id ]=>l Diagram→ConstL G

Fibre categoriesπŸ”—

The fibre category of the fibration of diagrams are equivalent to functor categories [J,Ex][\mathcal{J}, \mathcal{E}_x].

  Fibrewise-diagram : βˆ€ {x} β†’ Functor Cat[ J , Fibre E x ] (Fibre (Diagrams J) x)
  Fibrewise-diagram .F₀ = Diagram→ConstL
  Fibrewise-diagram .F₁ = Diagram-natβ†’ConstL-natl
  Fibrewise-diagram .F-id = Nat-lift-pathp Ξ» _ β†’ sym Regularity.reduce!
  Fibrewise-diagram .F-∘ _ _ = Nat-lift-pathp Ξ» _ β†’ sym Regularity.reduce!

Again, this isomorphism is almost definitional.

  Fibrewise-diagram-is-iso : βˆ€ {x} β†’ is-precat-iso (Fibrewise-diagram {x})
  Fibrewise-diagram-is-iso .is-precat-iso.has-is-ff =
    is-iso→is-equiv $ iso
      (ConstL-natl→Diagram-nat)
      (Ξ» Ξ±' β†’ Nat-lift-pathp (Ξ» _ β†’ refl))
      (Ξ» Ξ± β†’ Nat-path (Ξ» _ β†’ refl))
  Fibrewise-diagram-is-iso .is-precat-iso.has-is-iso =
    is-iso→is-equiv $ iso
      ConstL→Diagram
      (Ξ» F' β†’ Lifting-pathp E refl (Ξ» _ β†’ refl) (Ξ» _ β†’ refl))
      (Ξ» F β†’ Functor-path (Ξ» _ β†’ refl) (Ξ» _ β†’ refl))