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 is fibrewise structure: structure found in each fibre category, preserved by the reindexing functors when is an (op)fibration.

For instance, the correct notion of limit in are the fibred limits: where every fibre category has limits of shape 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 is. Recall that the fibration of liftings describes liftings of functors along the projection functor If we focus on liftings along a constant functor we get a diagram in that lies entirely in the fibre a fibrewise diagram!

This allows us to concisely define the fibration of fibrewise diagrams as the base change of along the functor 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 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 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' = cast[]  _  id')
  ConstL x' .F-∘' _ _ = cast[] (symP (idr' _))

  const-ntl
    :  {x y x' y'} {f : Hom x y}  Hom[ f ] x' y'
     (ConstL x') =[ constⁿ f ]=>l (ConstL y')
  const-ntl f' .η' _ = f'
  const-ntl f' .is-natural' _ _ _ =
    cast[] (idr' _ ∙[] (symP (idl' _)))

We also have a vertical functor from to the fibration of diagrams of shape which takes an 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 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ⁿ 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ⁿ id ]=>l Diagram→ConstL G

Fibre categories🔗

The fibre category of the fibration of diagrams are equivalent to functor categories

  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))
     α  trivial!)
  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))