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

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 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.

 : ∀ {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′ _)

    : ∀ {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.

    : ∀ {x} → Lifting {J = J} E (Const x) → Functor J (Fibre E x)
    : ∀ {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.

    : ∀ {x} {F G : Functor J (Fibre E x)}
    → Diagram→ConstL F =[ const-nt id ]=>l Diagram→ConstL G
    → F => G

    : ∀ {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
      (λ α' → Nat-lift-pathp (λ _ → refl))
      (λ α → Nat-path (λ _ → refl))
  Fibrewise-diagram-is-iso .is-precat-iso.has-is-iso =
    is-iso→is-equiv $ iso
      (λ F' → Lifting-pathp E refl (λ _ → refl) (λ _ → refl))
      (λ F → Functor-path (λ _ → refl) (λ _ → refl))