open import Cat.Displayed.Cartesian
open import Cat.Displayed.Functor
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning as DR

module Cat.Displayed.Composition where


# Composition of Displayed Categories🔗

A displayed category $\mathcal{E}$ over $\mathcal{B}$ is equivalent to the data of a functor into $\mathcal{B}$; the forward direction of this equivalence is witnessed by the total category of $\mathcal{E}$, along with the canonical projection functor from the total category into $\mathcal{B}$. This suggests that we ought to be able to compose displayed categories. That is, if $\mathcal{E}$ is displayed over $\mathcal{B}$, and $\mathcal{F}$ is displayed over $\int \mathcal{E}$, then we can construct a new category $\mathcal{E} \cdot \mathcal{F}$ displayed over $\mathcal{B}$ that contains the data of both $\mathcal{E}$ and $\mathcal{F}$.

To actually construct the composite, we bundle up the data of $\mathcal{E}$ and $\mathcal{F}$ into pairs, so an object in $\mathcal{E} \cdot \mathcal{F}$ over $X : \mathcal{B}$ consists of a pair objects of $X' : \mathcal{E}$ over $X$, and $X'' : \mathcal{F}$ over $X$ and $X'$. Morphisms are defined similarly, as do equations.

_D∘_ : ∀ {o ℓ o′ ℓ′ o″ ℓ″}
→ {ℬ : Precategory o ℓ}
→ (ℰ : Displayed ℬ o′ ℓ′) → (ℱ : Displayed (∫ ℰ) o″ ℓ″)
→ Displayed ℬ (o′ ⊔ o″) (ℓ′ ⊔ ℓ″)
_D∘_ {ℬ = ℬ} ℰ ℱ = disp where
module ℰ = Displayed ℰ
module ℱ = Displayed ℱ

disp : Displayed ℬ _ _
Displayed.Ob[ disp ] X =
Σ[ X′ ∈ ℰ.Ob[ X ] ] ℱ.Ob[ X , X′ ]
Displayed.Hom[ disp ] f X Y =
Σ[ f′ ∈ ℰ.Hom[ f ] (X .fst) (Y .fst) ] ℱ.Hom[ total-hom f f′ ] (X .snd) (Y .snd)
Displayed.Hom[ disp ]-set f x y =
Σ-is-hlevel 2 (ℰ.Hom[ f ]-set (x .fst) (y .fst)) λ f′ →
ℱ.Hom[ total-hom f f′ ]-set (x .snd) (y .snd)
disp .Displayed.id′ =
ℰ.id′ , ℱ.id′
disp .Displayed._∘′_ f′ g′ =
(f′ .fst ℰ.∘′ g′ .fst) , (f′ .snd ℱ.∘′ g′ .snd)
disp .Displayed.idr′ f′ =
ℰ.idr′ (f′ .fst) ,ₚ ℱ.idr′ (f′ .snd)
disp .Displayed.idl′ f′ =
ℰ.idl′ (f′ .fst) ,ₚ ℱ.idl′ (f′ .snd)
disp .Displayed.assoc′ f′ g′ h′ =
(ℰ.assoc′ (f′ .fst) (g′ .fst) (h′ .fst)) ,ₚ (ℱ.assoc′ (f′ .snd) (g′ .snd) (h′ .snd))


We also obtain a displayed functor from $\mathcal{E} \cdot \mathcal{F}$ to $\mathcal{E}$ that projects out the data of $\mathcal{E}$ from the composite.

πᵈ : ∀ {o ℓ o′ ℓ′ o″ ℓ″}
→ {ℬ : Precategory o ℓ}
→ {ℰ : Displayed ℬ o′ ℓ′} {ℱ : Displayed (∫ ℰ) o″ ℓ″}
→ Displayed-functor (ℰ D∘ ℱ) ℰ Id
πᵈ .Displayed-functor.F₀′ = fst
πᵈ .Displayed-functor.F₁′ = fst
πᵈ .Displayed-functor.F-id′ = refl
πᵈ .Displayed-functor.F-∘′ = refl


## Composition of fibrations🔗

As one may expect, the composition of fibrations is itself a fibration.

module _
{o ℓ o′ ℓ′ o″ ℓ″}
{ℬ : Precategory o ℓ}
{ℰ : Displayed ℬ o′ ℓ′} {ℱ : Displayed (∫ ℰ) o″ ℓ″}
where

private
open Precategory ℬ
module ℰ = Displayed ℰ
module ℱ = Displayed ℱ
module ℱR = DR ℱ


The idea of the proof is that we can take lifts of lifts, and in fact, this is exactly how we construct the liftings.

  fibration-∘ : Cartesian-fibration ℰ → Cartesian-fibration ℱ
→ Cartesian-fibration (ℰ D∘ ℱ)
fibration-∘ ℰ-fib ℱ-fib = ℰ∘ℱ-fib where
open Cartesian-fibration
open Cartesian-lift

ℰ∘ℱ-fib : Cartesian-fibration (ℰ D∘ ℱ)
ℰ∘ℱ-fib .has-lift f (y′ , y″) = cart-lift where

ℰ-lift = ℰ-fib .has-lift f y′
ℱ-lift = ℱ-fib .has-lift (total-hom f (ℰ-lift .lifting)) y″

cart-lift : Cartesian-lift (ℰ D∘ ℱ) f (y′ , y″)
cart-lift .x′ = ℰ-lift .x′ , ℱ-lift .x′
cart-lift .lifting = ℰ-lift .lifting , ℱ-lift .lifting


However, showing that the constructed lift is cartesian is somewhat more subtle. The issue is that when we go to construct the universal map, we are handed an $h'$ displayed over $f \cdot m$, and also an $h''$ displayed over $f \cdot m, h'$, which is not a composite definitionally. However, it is propositionally a composite, as is witnessed by ℰ-lift .commutes, so we can use the generalized propositional functions of ℱ-lift to construct the universal map, and show that it is indeed universal.

      cart-lift .cartesian .is-cartesian.universal m (h′ , h″) =
ℰ-lift .universal m h′ ,
universal′ ℱ-lift (total-hom-path ℰ refl (ℰ-lift .commutes m h′)) h″
cart-lift .cartesian .is-cartesian.commutes m h′ =
ℰ-lift .commutes m (h′ .fst) ,ₚ
commutesp ℱ-lift _ (h′ .snd)
cart-lift .cartesian .is-cartesian.unique m′ p =
ℰ-lift .unique (m′ .fst) (ap fst p) ,ₚ
uniquep ℱ-lift _ _
(total-hom-path ℰ refl (ℰ-lift .commutes _ _))
(m′ .snd)
(ap snd p)