open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Reasoning as CR
import Cat.Displayed.Morphism as DM

module Cat.Displayed.Total
  {o β„“ oβ€² β„“β€²} {B : Precategory o β„“} (E : Displayed B oβ€² β„“β€²) where

open Displayed E
open DM E
open CR B

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 ∈ Ob ] 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 Total-hom (X Y : Total) : Type (β„“ βŠ” β„“β€²) where
  constructor total-hom
  field
    hom       : Hom (X .fst) (Y .fst)
    preserves : Hom[ hom ] (X .snd) (Y .snd)

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

total-hom-is-set : βˆ€ (X Y : Total) β†’ is-set (Total-hom X Y)
total-hom-is-set X Y = Iso→is-hlevel 2 eqv $
  Ξ£-is-hlevel 2 (hlevel 2) (Ξ» a β†’ Hom[ _ ]-set _ _)

total-hom-path : βˆ€ {X Y : Total} {f g : Total-hom X Y}
               β†’ (p : f .hom ≑ g .hom) β†’ f .preserves ≑[ p ] g .preserves β†’ f ≑ g
total-hom-path p pβ€² i .hom = p i
total-hom-path {f = f} {g = g} p pβ€² i .preserves = pβ€² i

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

∫ : Precategory (o βŠ” oβ€²) (β„“ βŠ” β„“β€²)
∫ .Precategory.Ob = Total
∫ .Precategory.Hom = Total-hom
∫ .Precategory.Hom-set = total-hom-is-set
∫ .Precategory.id = total-hom id idβ€²
∫ .Precategory._∘_ f g = total-hom (f .hom ∘ g .hom) (f .preserves βˆ˜β€² g .preserves)
∫ .Precategory.idr _ = total-hom-path (idr _) (idrβ€² _)
∫ .Precategory.idl _ = total-hom-path (idl _) (idlβ€² _)
∫ .Precategory.assoc _ _ _ = total-hom-path (assoc _ _ _) (assocβ€² _ _ _)

Morphisms in the total categoryπŸ”—

Isomorphisms in the total category of EE consist of pairs of isomorphisms in BB and EE.

private module ∫E = CR ∫

total-isoβ†’iso : βˆ€ {x y} β†’ x ∫E.β‰… y β†’ x .fst β‰… y .fst
total-iso→iso f = make-iso
    (∫E._β‰…_.to f .hom)
    (∫E._β‰…_.from f .hom)
    (ap hom $ ∫E._β‰…_.invl f)
    (ap hom $ ∫E._β‰…_.invr f)

total-isoβ†’iso[] : βˆ€ {x y} β†’ (f : x ∫E.β‰… y) β†’ x .snd β‰…[ total-isoβ†’iso f ] y .snd
total-iso→iso[] f = make-iso[ total-iso→iso f ]
    (∫E._β‰…_.to f .preserves)
    (∫E._β‰…_.from f .preserves)
    (ap preserves $ ∫E._β‰…_.invl f)
    (ap preserves $ ∫E._β‰…_.invr f)