open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Closure
open import 1Lab.Reflection
open import 1Lab.Underlying
open import 1Lab.HLevel
open import 1Lab.Path
open import 1Lab.Type hiding (id ; _∘_)

open import Cat.Base

module Cat.Displayed.Base where

Displayed categoriesπŸ”—

The core idea behind displayed categories is that we want to capture the idea of being able to place extra structure over some sort of β€œbase” category. For instance, we can think of categories of algebraic objects (monoids, groups, rings, etc) as being extra structure placed atop the objects of Set, and extra conditions placed atop the morphisms of Set.

We start by defining a displayed category over a base category which will act as the category we add the extra structure to.

record Displayed {o β„“} (B : Precategory o β„“)
                 (o' β„“' : Level) : Type (o βŠ” β„“ βŠ” lsuc o' βŠ” lsuc β„“') where
  no-eta-equality
  open Precategory B

For each object of the base category, we associate a type of objects. Going back to our original example of algebraic structures over this would be something like Monoid-on : Set β†’ Type. This highlights an important point for intuition: we should think of the objects of the displayed category as structures over the objects of the base.

  field
    Ob[_] : Ob β†’ Type o'

We do a similar thing for morphisms: For each morphism f : Hom x y in the base category, there is a set of morphisms between objects in the displayed category. Keeping with our running example, given a function f : X β†’ Y and monoid structures M : Monoid-on X, N : Monoid-on Y, then Hom[ f ] M N is the proposition that β€œf is a monoid homomorphism”. Again, we should best think of these as structures over morphisms.

    Hom[_] : βˆ€ {x y} β†’ Hom x y β†’ Ob[ x ] β†’ Ob[ y ] β†’ Type β„“'
    Hom[_]-set
      : βˆ€ {a b} (f : Hom a b) (x : Ob[ a ]) (y : Ob[ b ])
      β†’ is-set (Hom[ f ] x y)

We also have identity and composition of displayed morphisms, but this is best thought of as witnessing that the identity morphism in the base has some structure, and that composition preserves that structure. For monoids, this would be a proof that the identity function is a monoid homomorphism, and that the composition of homomorphisms is indeed a homomorphism.

    id' : βˆ€ {a} {x : Ob[ a ]} β†’ Hom[ id ] x x
    _∘'_
      : βˆ€ {a b c x y z} {f : Hom b c} {g : Hom a b}
      β†’ Hom[ f ] y z β†’ Hom[ g ] x y β†’ Hom[ f ∘ g ] x z

Now, for the difficult part of displayed category theory: equalities. If we were to naively try to write out the right-identity law, we would immediately run into trouble. The problem is that f' ∘' id' : Hom[ f ∘ id ] x y, but f' : Hom [ f ] x y! IE: the laws only hold relative to equalities in the base category. Therefore, instead of using _≑_, we must use PathP. Let’s provide some helpful notation for doing so.

  infixr 40 _∘'_

  _≑[_]_
    : βˆ€ {a b x y} {f g : Hom a b} β†’ Hom[ f ] x y β†’ f ≑ g β†’ Hom[ g ] x y β†’ Type β„“'
  _≑[_]_ {a} {b} {x} {y} f' p g' = PathP (Ξ» i β†’ Hom[ p i ] x y) f' g'

  infix 30 _≑[_]_

Next, we have the laws. These are mostly what one would expect, just done over the equalities in the base.

  field
    idr' : βˆ€ {a b x y} {f : Hom a b} (f' : Hom[ f ] x y) β†’ (f' ∘' id') ≑[ idr f ] f'
    idl' : βˆ€ {a b x y} {f : Hom a b} (f' : Hom[ f ] x y) β†’ (id' ∘' f') ≑[ idl f ] f'
    assoc'
      : βˆ€ {a b c d w x y z} {f : Hom c d} {g : Hom b c} {h : Hom a b}
      β†’ (f' : Hom[ f ] y z) (g' : Hom[ g ] x y) (h' : Hom[ h ] w x)
      β†’ f' ∘' (g' ∘' h') ≑[ assoc f g h ] ((f' ∘' g') ∘' h')

Finally, we can equip displayed categories with a distinguished transport operation for moving displayed morphisms between equal bases. While in general there may be many such, we can pair the β€œhomwise transport” hom[_] operation with a coherence datum coh[_], and this pair inhabits a contractible type (the centre of contraction being the native subst operation paired with its filler). Therefore, these fields do not affect the β€œhomotopy type” of Displayed.

Their purpose is strictly as an aid in mechanisation: often (e.g. in the fundamental fibration the type consists of some β€œrelevant” data together with some β€œirrelevant” propositions, and, importantly, only the propositions mention the base morphism . This means that a β€œbespoke” hom[_] implementation can then choose to leave the data fields definitionally unchanged, whereas the native subst would surround them with reflexive transports.

Counterintuitively, this extra field actually increases reusability, despite nominally increasing the amount of data that goes into a displayed category: If another construction needs to transport morphisms in to work, e.g. the pullback fibration for sconing or Artin gluing, or fibre categories of subobjects, dealing with the leftover substs that arise in (e.g.) composition of morphisms can be quite annoying, and while cleaning them up can be automated, using the β€œbespoke” transport avoids introducing them in the first place.

  field
    hom[_]
      : βˆ€ {a b x y} {f g : Hom a b} (p : f ≑ g) (f' : Hom[ f ] x y)
      β†’ Hom[ g ] x y
    coh[_]
      : βˆ€ {a b x y} {f g : Hom a b} (p : f ≑ g) (f' : Hom[ f ] x y)
      β†’ f' ≑[ p ] hom[ p ] f'

Developer documentationπŸ”—

\ Warning

This section serves to document constructs derived from the definition of displayed categories that aid in the formalisation, and not necessarily interesting mathematical concepts.

  private variable
    a b : Ob
    a' b' x y : Ob[ a ]

    e f g h : Hom a b
    e' f' g' h' : Hom[ f ] a' b'
    p q r s : f ≑ g
    p' q' r' s' : f' ≑[ p ] g'

Operators for composing paths-overπŸ”—

Since Agda often struggles to infer the arguments to the generic displayed composition operator _βˆ™P_ in the setting of displayed categories, we provide variants which specify that the dependency is only on paths in the base category. One variant (βˆ™[-]-syntax) takes the path over which the left argument is displayed explicitly, and the other _βˆ™[]_ does this implicitly.

  βˆ™[-]-syntax
    : (p : f ≑ g) {q : g ≑ h}
    β†’ f' ≑[ p ] g' β†’ g' ≑[ q ] h' β†’ f' ≑[ p βˆ™ q ] h'
  βˆ™[-]-syntax p p' q' = _βˆ™P_ {B = Ξ» f β†’ Hom[ f ] _ _} p' q'

  syntax βˆ™[-]-syntax p p' q' = p' βˆ™[ p ] q'

  _βˆ™[]_ : {p : f ≑ g} {q : g ≑ h} β†’ f' ≑[ p ] g' β†’ g' ≑[ q ] h' β†’ f' ≑[ p βˆ™ q ] h'
  _βˆ™[]_ p' q' = p' βˆ™[ _ ] q'

  infixr 30 _βˆ™[]_ βˆ™[-]-syntax

Equational reasoning in displayed categoriesπŸ”—

Iterated composition of dependent paths incurs a quadratic overhead when compared to composition of ordinary paths, since the elaborated form of each composition operator must store the paths over which both sides are displayed:

  -- Generalisation really doesn't like generalising over the bases here
  module
    _ {a b} {d e f g h : Hom a b} {p : d ≑ e} {q : e ≑ f} {r : f ≑ g} {s : g ≑ h}
    where

    _ : p' βˆ™[] q' βˆ™[] r' βˆ™[] s' ≑
      _βˆ™[]_      {p = p} {q = q βˆ™ r βˆ™ s} p'
        (_βˆ™[]_   {p = q} {q = r βˆ™ s}     q'
          (_βˆ™[]_ {p = r} {q = s}         r'
            s'))
    _ = refl

Predictably, this is quite bad for performance: any part of the Agda implementation which needs to traverse terms will spend time going through this redundant information, which could in principle be recovered from the types of the arguments.

Surprisingly, we can alleviate this by working instead with paths in the total space of as a family over We introduce an auxiliary type _βˆ«β‰‘_, from which we can project a path in either over the constructed path between the base maps, or (because are sets) over an arbitrary path in the base.

  _βˆ«β‰‘_ : Hom[ f ] x y β†’ Hom[ g ] x y β†’ Type _
  f' βˆ«β‰‘ g' = Path (Ξ£ (Hom _ _) Ξ» f β†’ Hom[ f ] _ _) (_ , f') (_ , g')

  begin_ : (p : f' βˆ«β‰‘ g') β†’ f' ≑[ ap fst p ] g'
  begin_ = ap snd

  begin[]_ : f' βˆ«β‰‘ g' β†’ f' ≑[ p ] g'
  begin[]_ {f' = f'} {g' = g'} p = subst (f' ≑[_] g') prop! (ap snd p)

  infix 1 begin_ begin[]_

We can then provide combinators for composing a path in the total space with an ordinary dependent path, with variants for explicitly specifying the base path and for inverting the path to be composed.

  ≑[-]⟨⟩-syntax
    : (f' : Hom[ f ] x y) (p : f ≑ g) β†’ g' βˆ«β‰‘ h' β†’ f' ≑[ p ] g' β†’ f' βˆ«β‰‘ h'
  ≑[-]⟨⟩-syntax f' p q' p' = apβ‚‚ _,_ (p βˆ™ ap fst q') (p' βˆ™[] ap snd q')

  syntax ≑[-]⟨⟩-syntax f' p q' p' = f' ≑[ p ]⟨ p' ⟩ q'

  ≑[]⟨⟩-syntax : (f' : Hom[ f ] x y) β†’ g' βˆ«β‰‘ h' β†’ f' ≑[ p ] g' β†’ f' βˆ«β‰‘ h'
  ≑[]⟨⟩-syntax {p = p} f' q' p' = f' ≑[ _ ]⟨ p' ⟩] q'

  ≑[]˘⟨⟩-syntax : (f' : Hom[ f ] x y) β†’ g' βˆ«β‰‘ h' β†’ g' ≑[ p ] f' β†’ f' βˆ«β‰‘ h'
  ≑[]˘⟨⟩-syntax f' q' p' = f' ≑[]⟨ symP p' βŸ©β‰‘[] q'

  syntax ≑[]⟨⟩-syntax f' q' p' = f' ≑[]⟨ p' ⟩ q'
  syntax ≑[]˘⟨⟩-syntax f' q' p' = f' ≑[]˘⟨ p' ⟩ q'

  infixr 2 ≑[-]⟨⟩-syntax ≑[]⟨⟩-syntax ≑[]˘⟨⟩-syntax

Finally, for the final step, we must provide a slight variation on the reflexivity operator which pairs the given displayed map with its base.

  _∎[] : (f' : Hom[ f ] x y) β†’ f' βˆ«β‰‘ f'
  _∎[] _ = refl

  infix 3 _∎[]

record Trivially-graded {o β„“} (B : Precategory o β„“) (o' β„“' : Level) : Type (o βŠ” β„“ βŠ” lsuc o' βŠ” lsuc β„“') where
  open Precategory B
  field
    Ob[_]  : Ob β†’ Type o'
    Hom[_] : βˆ€ {x y} β†’ Hom x y β†’ Ob[ x ] β†’ Ob[ y ] β†’ Type β„“'

    instance
      ⦃ H-Level-Hom[_] ⦄
        : βˆ€ {a b} {f : Hom a b} {x : Ob[ a ]} {y : Ob[ b ]}
        β†’ H-Level (Hom[ f ] x y) 2

    id'  : βˆ€ {a} {x : Ob[ a ]} β†’ Hom[ id ] x x
    _∘'_ : βˆ€ {a b c x y z} {f : Hom b c} {g : Hom a b}
         β†’ Hom[ f ] y z β†’ Hom[ g ] x y β†’ Hom[ f ∘ g ] x z

  infixr 40 _∘'_

  _≑[_]_ : βˆ€ {a b x y} {f g : Hom a b} β†’ Hom[ f ] x y β†’ f ≑ g β†’ Hom[ g ] x y β†’ Type β„“'
  _≑[_]_ {a} {b} {x} {y} f' p g' = PathP (Ξ» i β†’ Hom[ p i ] x y) f' g'

  infix 30 _≑[_]_
  field
    idr' : βˆ€ {a b x y} {f : Hom a b} (f' : Hom[ f ] x y) β†’ (f' ∘' id') ≑[ idr f ] f'
    idl' : βˆ€ {a b x y} {f : Hom a b} (f' : Hom[ f ] x y) β†’ (id' ∘' f') ≑[ idl f ] f'
    assoc'
      : βˆ€ {a b c d w x y z} {f : Hom c d} {g : Hom b c} {h : Hom a b}
      β†’ (f' : Hom[ f ] y z) (g' : Hom[ g ] x y) (h' : Hom[ h ] w x)
      β†’ f' ∘' (g' ∘' h') ≑[ assoc f g h ] ((f' ∘' g') ∘' h')

{-# INLINE Displayed.constructor #-}

record Thinly-displayed {o β„“} (B : Precategory o β„“) (o' β„“' : Level) : Type (o βŠ” β„“ βŠ” lsuc o' βŠ” lsuc β„“') where
  open Precategory B
  field
    Ob[_]  : Ob β†’ Type o'
    Hom[_] : βˆ€ {x y} β†’ Hom x y β†’ Ob[ x ] β†’ Ob[ y ] β†’ Type β„“'

    instance
      ⦃ H-Level-Hom[_] ⦄
        : βˆ€ {a b} {f : Hom a b} {x : Ob[ a ]} {y : Ob[ b ]}
        β†’ H-Level (Hom[ f ] x y) 1

    id'  : βˆ€ {a} {x : Ob[ a ]} β†’ Hom[ id ] x x
    _∘'_ : βˆ€ {a b c x y z} {f : Hom b c} {g : Hom a b}
         β†’ Hom[ f ] y z β†’ Hom[ g ] x y β†’ Hom[ f ∘ g ] x z

with-trivial-grading
  : βˆ€ {o β„“} {B : Precategory o β„“} {o' β„“' : Level} β†’ Trivially-graded B o' β„“'
  β†’ Displayed B o' β„“'
{-# INLINE with-trivial-grading #-}
with-trivial-grading triv = record
  { Trivially-graded triv
  ; Hom[_]-set = Ξ» f x y β†’ hlevel 2
  ; hom[_]     = subst (Ξ» e β†’ Hom[ e ] _ _)
  ; coh[_]     = Ξ» p β†’ transport-filler _
  }
  where open Trivially-graded triv using (Hom[_] ; H-Level-Hom[_])

with-thin-display
  : βˆ€ {o β„“} {B : Precategory o β„“} {o' β„“' : Level} β†’ Thinly-displayed B o' β„“'
  β†’ Displayed B o' β„“'
{-# INLINE with-thin-display #-}
with-thin-display triv = with-trivial-grading record where
  open Thinly-displayed triv using (Ob[_] ; Hom[_] ; id' ; _∘'_) renaming (H-Level-Hom[_] to i)
  H-Level-Hom[_] = basic-instance 2 $ is-prop→is-set (hlevel 1)
  idr'   f     = prop!
  idl'   f     = prop!
  assoc' f g h = prop!

open hlevel-projection

private
  Hom[]-set
    : βˆ€ {o β„“ o' β„“'} {B : Precategory o β„“} (E : Displayed B o' β„“') {x y} {f : B .Precategory.Hom x y} {x' y'}
    β†’ is-set (E .Displayed.Hom[_] f x' y')
  Hom[]-set E = E .Displayed.Hom[_]-set _ _ _

instance
  Hom[]-hlevel-proj : hlevel-projection (quote Displayed.Hom[_])
  Hom[]-hlevel-proj .has-level   = quote Hom[]-set
  Hom[]-hlevel-proj .get-level _ = pure (lit (nat 2))
  Hom[]-hlevel-proj .get-argument (_ ∷ _ ∷ _ ∷ _ ∷ _ ∷ arg _ t ∷ _) =
    pure t
  {-# CATCHALL #-}
  Hom[]-hlevel-proj .get-argument _ =
    typeError []

  Funlike-Displayed : βˆ€ {o β„“ o' β„“'} {B : Precategory o β„“} β†’ Funlike (Displayed B o' β„“') ⌞ B ⌟ Ξ» _ β†’ Type o'
  Funlike-Displayed = record { _Β·_ = Displayed.Ob[_] }

module _ {o β„“ o' β„“'} {B : Precategory o β„“} {E : Displayed B o' β„“'} where
  _ : βˆ€ {x y} {f : B .Precategory.Hom x y} {x' y'} β†’ is-set (E .Displayed.Hom[_] f x' y')
  _ = hlevel 2