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

open Cat.Reasoning 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 JB\mathcal{J} \to \mathcal{B} along the projection functor π:EB\pi : \int \mathcal{E} \to \mathcal{B}. If we focus on liftings along a constant functor Δx:JB\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 EB\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 xx' 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))