module Cat.Displayed.Composition where

Composition of Displayed Categories🔗

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

To actually construct the composite, we bundle up the data of E\mathcal{E} and F\mathcal{F} into pairs, so an object in EF\mathcal{E} \cdot \mathcal{F} over X:BX : \mathcal{B} consists of a pair objects of X:EX' : \mathcal{E} over XX, and X:FX'' : \mathcal{F} over XX and XX'. 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 EF\mathcal{E} \cdot \mathcal{F} to E\mathcal{E} that projects out the data of E\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.

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 hh' displayed over fmf \cdot m, and also an hh'' displayed over fm,hf \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)