module Cat.Displayed.Total.Op where open Functor open Total-hom
Total Oppositesπ
Opposites of displayed categories are somewhat subtle, as there are multiple constructions that one could reasonably call the βoppositeβ. The most obvious construction is to construct a new displayed category over ; we call this category the total opposite of .
module _ {o β oβ² ββ²} {β¬ : Precategory o β} (β° : Displayed β¬ oβ² ββ²) where open Precategory β¬ open Displayed β° _^total-op : Displayed (β¬ ^op) oβ² ββ² _^total-op .Displayed.Ob[_] x = Ob[ x ] _^total-op .Displayed.Hom[_] f x y = Hom[ f ] y x _^total-op .Displayed.Hom[_]-set f x y = Hom[ f ]-set y x _^total-op .Displayed.idβ² = idβ² _^total-op .Displayed._ββ²_ fβ² gβ² = gβ² ββ² fβ² _^total-op .Displayed.idrβ² fβ² = idlβ² fβ² _^total-op .Displayed.idlβ² fβ² = idrβ² fβ² _^total-op .Displayed.assocβ² fβ² gβ² hβ² = symP $ assocβ² hβ² gβ² fβ²
Much like the opposite of categories, the total opposite is an involution on displayed categories.
total-op-involution : β {o β oβ² ββ²} {β¬ : Precategory o β} {β° : Displayed β¬ oβ² ββ²} β (β° ^total-op) ^total-op β‘ β° total-op-involution {β° = β°} = path where open Displayed path : (β° ^total-op) ^total-op β‘ β° path i .Ob[_] = β° .Ob[_] path i .Hom[_] = β° .Hom[_] path i .Hom[_]-set = β° .Hom[_]-set path i .idβ² = β° .idβ² path i ._ββ²_ = β° ._ββ²_ path i .idrβ² = β° .idrβ² path i .idlβ² = β° .idlβ² path i .assocβ² = β° .assocβ²
private displayed-double-dual : β {o β oβ² ββ²} {β¬ : Precategory o β} {β° : Displayed β¬ oβ² ββ²} β ((β° ^total-op) ^total-op) β‘rw β° displayed-double-dual {β° = β°} = make-rewrite (total-op-involution {β° = β°}) {-# REWRITE displayed-double-dual #-}
The Total Opposites and Total Categoriesπ
The reason we refer to this construction as the total opposite is that its total is equal to the opposite of the total category! To show this, we first need to prove some lemmas relating the morphisms of the total category of the total opposite to those in the opposite of the total category. These functions are essentially the identity function, but we canβt convince Agda that this is the case due to definitional equality reasons.
total-opβtotal-hom : β {o β oβ² ββ²} {β¬ : Precategory o β} {β° : Displayed β¬ oβ² ββ²} β β {x y} β Total-hom (β° ^total-op) x y β Total-hom β° y x total-opβtotal-hom f = total-hom (f .hom) (f .preserves) total-homβtotal-op : β {o β oβ² ββ²} {β¬ : Precategory o β} {β° : Displayed β¬ oβ² ββ²} β β {x y} β Total-hom β° y x β Total-hom (β° ^total-op) x y total-homβtotal-op f = total-hom (f .hom) (f .preserves)
Furthermore, these two maps constitute an equivalence, and thus yield an equality of types via univalence.
total-opβtotal-hom-is-equiv : β {o β oβ² ββ²} {β¬ : Precategory o β} {β° : Displayed β¬ oβ² ββ²} β β {x y} β is-equiv (total-opβtotal-hom {β° = β°} {x = x} {y = y}) total-opβtotal-hom-is-equiv = is-isoβis-equiv $ iso total-homβtotal-op (Ξ» _ β refl) (Ξ» _ β refl) total-opβ‘total-hom : β {o β oβ² ββ²} {β¬ : Precategory o β} {β° : Displayed β¬ oβ² ββ²} β β {x y} β Total-hom (β° ^total-op) x y β‘ Total-hom β° y x total-opβ‘total-hom = ua $ total-opβtotal-hom , total-opβtotal-hom-is-equiv
We can use the fact that total-opβtotal-hom
is an
equivalence to construct an isomorphism of precategories.
β«total-opββ«^op : β {o β oβ² ββ²} {β¬ : Precategory o β} (β° : Displayed β¬ oβ² ββ²) β Functor (β« (β° ^total-op)) ((β« β°) ^op) β«total-opββ«^op _ .Fβ x = x β«total-opββ«^op _ .Fβ f = total-opβtotal-hom f β«total-opββ«^op _ .F-id = refl β«total-opββ«^op _ .F-β _ _ = refl β«total-opβ β«^op : β {o β oβ² ββ²} {β¬ : Precategory o β} (β° : Displayed β¬ oβ² ββ²) β is-precat-iso (β«total-opββ«^op β°) β«total-opβ β«^op β° .is-precat-iso.has-is-ff = total-opβtotal-hom-is-equiv β«total-opβ β«^op β° .is-precat-iso.has-is-iso = id-equiv
Finally, we show that this extends to an equality of categories.
β«total-opβ‘β«^op : β {o β oβ² ββ²} {β¬ : Precategory o β} (β° : Displayed β¬ oβ² ββ²) β β« (β° ^total-op) β‘ (β« β°) ^op β«total-opβ‘β«^op β° = Precategory-path (β«total-opββ«^op β°) (β«total-opβ β«^op β°)
Functors between fibresπ
If there is a functor between the fibres of a displayed category , then we also obtain a functor between the fibres of the total opposite of .
fibre-functor-total-op : β {o β oβ² ββ²} {β¬ : Precategory o β} {β° : Displayed β¬ oβ² ββ²} {x y} β Functor (Fibre β° x) (Fibre β° y) β Functor (Fibre (β° ^total-op) x) (Fibre (β° ^total-op) y) fibre-functor-total-op F .Fβ = F .Fβ fibre-functor-total-op F .Fβ = F .Fβ fibre-functor-total-op F .F-id = F .F-id fibre-functor-total-op {β° = β°} F .F-β f g = ap (F .Fβ) (DR.reindex β° _ _ ) Β·Β· F .F-β g f Β·Β· DR.reindex β° _ _
fibre-functor-total-op-total-op : β {o β oβ² ββ²} {β¬ : Precategory o β} {β° : Displayed β¬ oβ² ββ²} {x y} β {F : Functor (Fibre β° x) (Fibre β° y)} β fibre-functor-total-op (fibre-functor-total-op F) β‘ F fibre-functor-total-op-total-op {F = F} i .Fβ = F .Fβ fibre-functor-total-op-total-op {F = F} i .Fβ = F .Fβ fibre-functor-total-op-total-op {F = F} i .F-id = F .F-id fibre-functor-total-op-total-op {β° = β°} {y = y} {F = F} i .F-β f g = is-propβpathp (Ξ» i β Hom-set _ _ _ (F .Fβ f β F .Fβ g)) ((fibre-functor-total-op (fibre-functor-total-op F)) .F-β f g) (F .F-β f g) i where open Precategory (Fibre β° y) private fibre-functor-double-dual : β {o β oβ² ββ²} {β¬ : Precategory o β} {β° : Displayed β¬ oβ² ββ²} {x y} β {F : Functor (Fibre β° x) (Fibre β° y)} β fibre-functor-total-op (fibre-functor-total-op F) β‘rw F fibre-functor-double-dual = make-rewrite fibre-functor-total-op-total-op {-# REWRITE fibre-functor-double-dual #-}