module Cat.Functor.Hom.Displayed {o β oβ² ββ²} {β¬ : Precategory o β} (β° : Displayed β¬ oβ² ββ²) where
Displayed Hom Functorsπ
Let be a displayed category over . For every in the base, we can obtain a bifunctor from to , where denotes the fibre category of at . The action of on is given by , just as in the non-displayed case.
Hom-over : β {x y} β Hom x y β Functor (Fibre β° x ^op ΓαΆ Fibre β° y) (Sets ββ²) Hom-over u .Fβ (a , b) = el (Hom[ u ] a b) (Hom[ u ]-set a b) Hom-over u .Fβ (f , h) g = hom[ idl _ β idr _ ] (h ββ² g ββ² f) Hom-over u .F-id = funext Ξ» f β aprβ² {q = idl _} (idrβ² f) β idl[] Hom-over u .F-β (f , h) (f' , h') = funext Ξ» g β hom[] (hom[] (h ββ² h') ββ² g ββ² hom[] (f' ββ² f)) β‘β¨ disp! β° β©β‘ hom[] (h ββ² hom[] (h' ββ² g ββ² f') ββ² f) β
We can also define partially applied versions of this functor.
Hom-over-from : β {x y} β Hom x y β Ob[ x ] β Functor (Fibre β° y) (Sets ββ²) Hom-over-from u xβ² .Fβ yβ² = el (Hom[ u ] xβ² yβ²) (Hom[ u ]-set xβ² yβ²) Hom-over-from u xβ² .Fβ f g = hom[ idl u ] (f ββ² g) Hom-over-from u xβ² .F-id = funext Ξ» f β idl[] Hom-over-from u xβ² .F-β f g = funext Ξ» h β smashl _ _ β sym assoc[] β sym (smashr _ _) Hom-over-into : β {x y} β Hom x y β Ob[ y ] β Functor (Fibre β° x ^op) (Sets ββ²) Hom-over-into u yβ² .Fβ xβ² = el (Hom[ u ] xβ² yβ²) (Hom[ u ]-set xβ² yβ²) Hom-over-into u yβ² .Fβ f g = hom[ idr u ] (g ββ² f) Hom-over-into u yβ² .F-id = funext Ξ» f β idr[] Hom-over-into u yβ² .F-β f g = funext Ξ» h β smashr _ _ β assoc[] β (sym $ smashl _ _ )