open import Cat.Displayed.Cartesian
open import Cat.Diagram.Pullback
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Displayed.Morphism
import Cat.Reasoning

module Cat.Displayed.Total where

module _ {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') where
  open Cat.Reasoning B
  open Displayed E
  open Cat.Displayed.Reasoning E
  open Cat.Displayed.Morphism E

The total category of a displayed category🔗

So far, we’ve been thinking of displayed categories as “categories of structures” over some base category. However, it’s often useful to consider a more “bundled up” notion of structure, where the carrier and the structure are considered as a singular object. For instance, if we consider the case of algebraic structures, we often want to think about “a monoid” as a singular thing, as opposed to structure imposed atop some set.

Constructing the total category does exactly this. The objects are pairs of an object from the base, an object from the displayed category that lives over it.

Note that we use a sigma type here instead of a record for technical reasons: this makes it simpler to work with algebraic structures.

  Total : Type (o ⊔ o')
  Total = Σ[ Carrier ∈ B ] Ob[ Carrier ]

The situation is similar for morphisms: we bundle up a morphism from the base category along with a morphism that lives above it.

  record ∫Hom (X Y : Total) : Type (ℓ ⊔ ℓ') where
    constructor ∫hom
    field
      fst : Hom (X .fst) (Y .fst)
      snd : Hom[ fst ] (X .snd) (Y .snd)

  open ∫Hom public

  unquoteDecl H-Level-∫Hom = declare-record-hlevel 2 H-Level-∫Hom (quote ∫Hom)

As is tradition, we need to prove some silly lemmas showing that the bundled morphisms form an hset, and another characterizing the paths between morphisms.

  ∫Hom-path
    : ∀ {X Y : Total} {f g : ∫Hom X Y}
    → (p : f .fst ≡ g .fst) → f .snd ≡[ p ] g .snd → f ≡ g
  ∫Hom-path p p' i .fst = p i
  ∫Hom-path {f = f} {g = g} p p' i .snd = p' i

  ∫Hom-pathp
    : ∀ {X X' Y Y' : Total} {f : ∫Hom X Y} {g : ∫Hom X' Y'}
    → (p : X ≡ X') (q : Y ≡ Y')
    → (r : PathP (λ z → Hom (p z .fst) (q z .fst)) (f .fst) (g .fst))
    → PathP (λ z → Hom[ r z ] (p z .snd) (q z .snd)) (f .snd) (g .snd)
    → PathP (λ i → ∫Hom (p i) (q i)) f g
  ∫Hom-pathp p q r s i .fst = r i
  ∫Hom-pathp p q r s i .snd = s i

  ∫-fst-snd-is-Σ-basis
    : ∀ {x y : Total}
    → is-Σ-basis (∫Hom x y)
        (Hom (x .fst) (y .fst))
        (λ u → Hom[ u ] (x .snd) (y .snd))
        fst
        snd
  ∫-fst-snd-is-Σ-basis .is-Σ-basis.⟨⟩-equiv .is-eqv (u , f) = contr (fib .fst) (fib .snd)
    where fib = strict-fibres (uncurry ∫hom) (u , f)

  ∫Hom-Σ-basis
    : ∀ {x y : Total}
    → Σ-basis (∫Hom x y)
        (Hom (x .fst) (y .fst))
        (λ u → Hom[ u ] (x .snd) (y .snd))
  ∫Hom-Σ-basis = is-Σ-basis→Σ-basis ∫-fst-snd-is-Σ-basis

With all that in place, we can construct the total category!

  ∫ : Precategory (o ⊔ o') (ℓ ⊔ ℓ')
  ∫ .Precategory.Ob = Total
  ∫ .Precategory.Hom = ∫Hom
  ∫ .Precategory.Hom-set _ _ = hlevel 2
  ∫ .Precategory.id .fst = id
  ∫ .Precategory.id .snd = id'
  ∫ .Precategory._∘_ f g .fst = f .fst ∘ g .fst
  ∫ .Precategory._∘_ f g .snd = f .snd ∘' g .snd
  ∫ .Precategory.idr _ = ∫Hom-path (idr _) (idr' _)
  ∫ .Precategory.idl _ = ∫Hom-path (idl _) (idl' _)
  ∫ .Precategory.assoc _ _ _ = ∫Hom-path (assoc _ _ _) (assoc' _ _ _)

  πᶠ : Functor ∫ B
  πᶠ .Functor.F₀ = fst
  πᶠ .Functor.F₁ = ∫Hom.fst
  πᶠ .Functor.F-id = refl
  πᶠ .Functor.F-∘ f g = refl

module _ {o ℓ o' ℓ'} {B : Precategory o ℓ} {E : Displayed B o' ℓ'} where
  private
    module B = Cat.Reasoning B
    module E where
      open Cat.Displayed.Morphism E public
      open Displayed E public
    module ∫E = Cat.Reasoning (∫ E)

Morphisms in the total category🔗

Isomorphisms in the total category of $E$ consist of pairs of isomorphisms in $B$ and $E .$

  ∫-Inverses-Σ-basis
    : ∀ {x y : Total E} {f : ∫E.Hom x y} {g : ∫E.Hom y x}
    → Σ-basis (∫E.Inverses f g)
        (B.Inverses (f .fst) (g .fst))
        (λ inv → E.Inverses[ inv ] (f .snd) (g .snd))
  ∫-Inverses-Σ-basis =
    Σ-basis-shuffle ∫E.Inverses-Σ-basis B.Inverses-Σ-basis E.Inverses[]-Σ-basis
      (Path-Σ-basis (∫Hom-Σ-basis E))
      (Path-Σ-basis (∫Hom-Σ-basis E))

  ∫-is-invertible-Σ-basis
    : ∀ {x y : Total E} {f : ∫E.Hom x y}
    → Σ-basis (∫E.is-invertible f)
        (B.is-invertible (f .fst))
        (λ inv → E.is-invertible[ inv ] (f .snd))
  ∫-is-invertible-Σ-basis =
    Σ-basis-shuffle ∫E.is-invertible-Σ-basis B.is-invertible-Σ-basis E.is-invertible[]-Σ-basis
      (∫Hom-Σ-basis E)
      ∫-Inverses-Σ-basis

  ∫-≅-Σ-basis
    : {x y : Total E}
    → Σ-basis (x ∫E.≅ y)
        (x .fst B.≅ y .fst)
        (λ f → x .snd E.≅[ f ] y .snd)
  ∫-≅-Σ-basis =
    Σ-basis-shuffle ∫E.≅-Σ-basis B.≅-Σ-basis E.≅[]-Σ-basis
      (∫Hom-Σ-basis E)
      ∫-is-invertible-Σ-basis

Pullbacks in the total category🔗

module _
  {o ℓ o' ℓ'} {B : Precategory o ℓ} {E : Displayed B o' ℓ'}
  (let open Cat.Reasoning B) (let open Displayed E)
  {p x y z p' x' y' z'}
  {p₁ : Hom p x} {f : Hom x z} {p₂ : Hom p y} {g : Hom y z}
  {p₁' : Hom[ p₁ ] p' x'} {f' : Hom[ f ] x' z'}
  {p₂' : Hom[ p₂ ] p' y'} {g' : Hom[ g ] y' z'}
  where
  private
    open Cat.Reasoning B
    open Cat.Displayed.Morphism E
    module ∫E = Cat.Reasoning (∫ E)

Pullbacks in the total category of $E$ have a particularly nice characterization. Consider the following pair of commuting squares.

If the bottom square is a pullback square, and both $p_{1}^{'}$ and $g^{'}$ are cartesian, then the upper square is a pullback in the total category of $E .$

  cartesian+pullback→total-pullback
    : is-cartesian E p₁ p₁'
    → is-cartesian E g g'
    → (pb : is-pullback B p₁ f p₂ g)
    → (open is-pullback pb)
    → f' ∘' p₁' ≡[ square ] g' ∘' p₂'
    → is-pullback (∫ E)
        (∫hom p₁ p₁') (∫hom f f')
        (∫hom p₂ p₂') (∫hom g g')

As the lower square is already a pullback, all that remains is constructing a suitable universal morphism in $E .$ Luckily, $p_{1}^{'}$ is cartesian, so we can factorise maps $A^{'} \to X^{'}$ in $E$ to obtain a map $A^{'} \to P^{'} .$ We then use the fact that $g^{'}$ is cartesian to show that the map we’ve constructed factorises maps $A^{'} \to Y^{'}$ as well. Uniqueness follows from the fact that $p_{1}^{'}$ is cartesian.

  cartesian+pullback→total-pullback p₁-cart g-cart pb square' = total-pb where
    open is-pullback
    open ∫Hom
    module p₁' = is-cartesian p₁-cart
    module g' = is-cartesian g-cart

    total-pb : is-pullback (∫ E) _ _ _ _
    total-pb .square = ∫Hom-path E (pb .square) square'
    total-pb .universal {a , a'} {p₁''} {p₂''} p =
      ∫hom (pb .universal (ap fst p))
        (p₁'.universal' (pb .p₁∘universal) (p₁'' .snd))
    total-pb .p₁∘universal =
      ∫Hom-path E (pb .p₁∘universal) (p₁'.commutesp _ _)
    total-pb .p₂∘universal {p₁' = q₁} {p₂' = q₂} {p = p}  =
      ∫Hom-path E (pb .p₂∘universal) $
      cartesian→weak-monic E g-cart _ _ (p₂∘universal pb) $ cast[] $
      via-Σ-basis (∫Hom-Σ-basis E) $
        g' ∘' (p₂' ∘' p₁'.universal' _ (q₁ .snd)) ≡Σ⟨ ∫E.pulll (∫Hom-path E _ (symP square')) ⟩
        (f' ∘' p₁') ∘' p₁'.universal' _ (q₁ .snd) ≡Σ⟨ ∫E.pullr (∫Hom-path E (pb .p₁∘universal) (p₁'.commutesp _ (q₁ .snd))) ⟩
        (f' ∘' q₁ .snd)                           ≡Σ⟨ p ⟩
        (g' ∘' q₂ .snd)                           ∎Σ
    total-pb .unique p q =
      ∫Hom-path E (pb .unique (ap fst p) (ap fst q)) $
        p₁'.uniquep _ _ (pb .p₁∘universal) _ (ap snd p)

We can also show the converse, provided that $E$ is a fibration.

  cartesian+total-pullback→pullback
    : Cartesian-fibration E
    → is-cartesian E p₁ p₁'
    → is-cartesian E g g'
    → is-pullback (∫ E)
        (∫hom p₁ p₁') (∫hom f f')
        (∫hom p₂ p₂') (∫hom g g')
    → is-pullback B p₁ f p₂ g

As we already have a pullback in the total category, the crux will be constructing enough structure in $E$ so that we can invoke the universal property of the pullback. We can do this by appealing to the fact that $E$ is a fibration, which allows us to lift morphisms in the base to obtain a cone in $E .$ From here, we use the fact that $p_{1}^{'}$ and $g^{'}$ are cartesian to construct the relevant paths.

  cartesian+total-pullback→pullback fib p₁-cart g-cart total-pb = pb where
    open is-pullback
    open ∫Hom
    open Cartesian-fibration E fib
    module p₁' = is-cartesian p₁-cart
    module g' = is-cartesian g-cart

    pb : is-pullback B _ _ _ _
    pb .square = ap fst (total-pb .square)
    pb .universal {P} {p₁''} {p₂''} sq =
      total-pb .universal
        {p₁' = ∫hom p₁'' (π* p₁'' _)}
        {p₂' = ∫hom p₂'' (g'.universal' (sym sq) (f' ∘' π* p₁'' _))}
        (∫Hom-path E sq (symP (g'.commutesp (sym sq) _))) .fst
    pb .p₁∘universal =
      ap fst $ total-pb .p₁∘universal
    pb .p₂∘universal =
      ap fst $ total-pb .p₂∘universal
    pb .unique {p = p} q r =
      ap fst $ total-pb .unique
        (∫Hom-path E q (p₁'.commutesp q _))
        (∫Hom-path E r $
          g'.uniquep _ _ _ _ $
          via-Σ-basis (∫Hom-Σ-basis E) $
            g' ∘' (p₂' ∘' p₁'.universal' q (π* _ x')) ≡Σ⟨ ∫E.pulll (sym $ total-pb .square) ⟩
            (f' ∘' p₁') ∘' p₁'.universal' q (π* _ x') ≡Σ⟨ ∫E.pullr (∫Hom-path E q (p₁'.commutesp q (π* _ x'))) ⟩
            (f' ∘' π* _ x')                           ∎Σ)

module _ {o ℓ o' ℓ'} {B : Precategory o ℓ} {E : Displayed B o' ℓ'} where
  open Cat.Reasoning B

  instance
    Funlike-∫Hom
      : ∀ {ℓ'' ℓ'''} {A : Type ℓ''} {B : A → Type ℓ'''}
      → {X Y : Total E} ⦃ i : Funlike (Hom (X .fst) (Y .fst)) A B ⦄
      → Funlike (∫Hom E X Y) A B
    Funlike-∫Hom ⦃ i ⦄ .Funlike._·_ f x = f .∫Hom.fst · x

    H-Level-∫Hom' : ∀ {X Y} {n} → H-Level (∫Hom E X Y) (2 + n)
    H-Level-∫Hom' = H-Level-∫Hom E