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 over is equivalent to the data of a functor into the forward direction of this equivalence is witnessed by the total category of along with the canonical projection functor from the total category into This suggests that we ought to be able to compose displayed categories. That is, if is displayed over and is displayed over then we can construct a new category displayed over that contains the data of both and

To actually construct the composite, we bundle up the data of and into pairs, so an object in over consists of a pair objects of over and over and 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 to that projects out the data of 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 displayed over and also an displayed over 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)