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 subst
s 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'
_β[]_ : β {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 f' q' p' = f' β‘[]β¨ p' β© q' syntax β‘[-]β¨β©-syntax p f' q' p' = f' β‘[ p ]β¨ p' β© q' infixr 30 _β[]_ β[-]-syntax infixr 2 β‘[]β¨β©-syntax β‘[-]β¨β©-syntax _β‘[]Λβ¨_β©_ 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 β' β¦ 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 β' β¦ 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[_]) 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' ; _β'_) 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