open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Closure
open import 1Lab.Reflection
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 _β‘[_]_


Finally, 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')


For convenience, we also introduce displayed analogues for equational chain reasoning:

  _β[]_ : β {a b x y} {f g h : Hom a b} {p : f β‘ g} {q : g β‘ h}
β {f' : Hom[ f ] x y} {g' : Hom[ g ] x y} {h' : Hom[ h ] x y}
β f' β‘[ p ] g' β g' β‘[ q ] h' β f' β‘[ p β q ] h'
_β[]_ {x = x} {y = y} p' q' = _βP_ {B = Ξ» f β Hom[ f ] x y} p' q'

β[-]-syntax : β {a b x y} {f g h : Hom a b} (p : f β‘ g) {q : g β‘ h}
β {f' : Hom[ f ] x y} {g' : Hom[ g ] x y} {h' : Hom[ h ] x y}
β f' β‘[ p ] g' β g' β‘[ q ] h' β f' β‘[ p β q ] h'
β[-]-syntax {x = x} {y = y} p p' q' = _βP_ {B = Ξ» f β Hom[ f ] x y} p' q'

β‘[]β¨β©-syntax : β {a b x y} {f g h : Hom a b} {p : f β‘ g} {q : g β‘ h}
β (f' : Hom[ f ] x y) {g' : Hom[ g ] x y} {h' : Hom[ h ] x y}
β g' β‘[ q ] h' β f' β‘[ p ] g' β f' β‘[ p β q ] h'
β‘[]β¨β©-syntax f' q' p' = p' β[] q'

β‘[-]β¨β©-syntax : β {a b x y} {f g h : Hom a b} (p : f β‘ g) {q : g β‘ h}
β (f' : Hom[ f ] x y) {g' : Hom[ g ] x y} {h' : Hom[ h ] x y}
β g' β‘[ q ] h' β f' β‘[ p ] g' β f' β‘[ p β q ] h'
β‘[-]β¨β©-syntax f' p q' p' = p' β[] q'

_β‘[]Λβ¨_β©_ : β {a b x y} {f g h : Hom a b} {p : g β‘ f} {q : g β‘ h}
β (f' : Hom[ f ] x y) {g' : Hom[ g ] x y} {h' : Hom[ h ] x y}
β g' β‘[ p ] f' β g' β‘[ q ] h' β f' β‘[ sym p β q ] h'
f' β‘[]Λβ¨ p' β©β‘[]Λ q' = symP p' β[] q'

syntax β[-]-syntax p p' q' = p' β[ p ] q'
syntax β‘[-]β¨β©-syntax p f' q' p' = f' β‘[ p ]β¨ p' β© q'

infixr 30 _β[]_ β[-]-syntax

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 []

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