module Cat.Displayed.Instances.Diagrams {o β o' β'} {B : Precategory o β} (E : Displayed B o' β') where open Precategory B open Displayed E open Cat.Displayed.Reasoning E open Functor open _=>_
The diagram fibrationπ
The appropriate notion of structure for a displayed category is fibrewise structure: structure found in each fibre category, preserved by the reindexing functors when is an (op)fibration.
For instance, the correct notion of -shaped limit in are the fibred limits: where every fibre category has limits of shape , and these are preserved by reindexing. Unfortunately, proof assistants: since none of the commutativity conditions for limits are definitional, this definition condemns the formaliser to transport hell.
Instead, we opt for a more abstract approach, which starts with a reorganization of what a fibrewise diagram in is. Recall that the fibration of liftings describes liftings of functors along the projection functor . If we focus on liftings along a constant functor , we get a diagram in that lies entirely in the fibre : a fibrewise diagram!
This allows us to concisely define the fibration of fibrewise diagrams as the base change of along the functor that takes an object to the constant diagram on that object.
Diagrams : β {oj βj} (J : Precategory oj βj) β Displayed B _ _ Diagrams J = Change-of-base ConstD (Liftings E J)
When is a fibration, then so is the fibration of diagrams.
module _ {oj βj} (J : Precategory oj βj) where private module J = Precategory J open Lifting open _=[_]=>l_
Diagram-fibration : Cartesian-fibration E β Cartesian-fibration (Diagrams J) Diagram-fibration fib = Change-of-base-fibration ConstD (Liftings E _) (Liftings-fibration E _ fib)
The constant fibrewise diagram functorπ
Crucially, we have a βconstant fibrewise diagram functorβ that takes an object to the constant diagram. However, defining this functor will require a small bit of machinery.
To begin, we characterize liftings of the constant functor, and natural transformations between them.
ConstL : β {x} β Ob[ x ] β Lifting {J = J} E (Const x) ConstL x' .Fβ' _ = x' ConstL x' .Fβ' _ = id' ConstL x' .F-id' = refl ConstL x' .F-β' _ _ = symP (idr' _) const-ntl : β {x y x' y'} {f : Hom x y} β Hom[ f ] x' y' β (ConstL x') =[ const-nt f ]=>l (ConstL y') const-ntl f' .Ξ·' _ = f' const-ntl f' .is-natural' _ _ _ = idr' _ β[] symP (idl' _)
We also have a vertical functor from to the fibration of diagrams of shape , which takes an to the constant diagram.
ConstFibD : Vertical-functor E (Diagrams J) ConstFibD .Vertical-functor.Fβ' = ConstL ConstFibD .Vertical-functor.Fβ' = const-ntl ConstFibD .Vertical-functor.F-id' = Nat-lift-pathp (Ξ» x β sym (transport-refl _)) ConstFibD .Vertical-functor.F-β' = Nat-lift-pathp (Ξ» x β sym (transport-refl _))
Next, we note that liftings of the constant functor correspond with diagrams in fibre categories.
ConstLβDiagram : β {x} β Lifting {J = J} E (Const x) β Functor J (Fibre E x) DiagramβConstL : β {x} β Functor J (Fibre E x) β Lifting {J = J} E (Const x)
ConstLβDiagram F' .Fβ = F' .Fβ' ConstLβDiagram F' .Fβ = F' .Fβ' ConstLβDiagram F' .F-id = F' .F-id' ConstLβDiagram F' .F-β f g = from-pathpβ» $ cast[] {q = sym (idl _)} (F' .F-β' f g) DiagramβConstL F .Fβ' = F .Fβ DiagramβConstL F .Fβ' = F .Fβ DiagramβConstL F .F-id' = F .F-id DiagramβConstL F .F-β' f g = cast[] {p = sym (idl _)} $ to-pathpβ» (F .F-β f g)
Furthermore, natural transformations between diagrams in a fibre of correspond to natural transformations between liftings of a constant functor.
ConstL-natlβDiagram-nat : β {x} {F G : Functor J (Fibre E x)} β DiagramβConstL F =[ const-nt id ]=>l DiagramβConstL G β F => G Diagram-natβConstL-natl : β {x} {F G : Functor J (Fibre E x)} β F => G β DiagramβConstL F =[ const-nt id ]=>l DiagramβConstL G
ConstL-natlβDiagram-nat Ξ±' .Ξ· = Ξ±' .Ξ·' ConstL-natlβDiagram-nat Ξ±' .is-natural x y f = ap hom[] (cast[] $ Ξ±' .is-natural' x y f) Diagram-natβConstL-natl Ξ± .Ξ·' = Ξ± .Ξ· Diagram-natβConstL-natl {F = F} {G = G} Ξ± .is-natural' x y f = cast[] $ to-pathp (Ξ± .is-natural x y f) β[] symP (transport-filler (Ξ» i β Hom[ idl id i ] _ _) (Fβ G f β' Ξ± .Ξ· x))
Fibre categoriesπ
The fibre category of the fibration of diagrams are equivalent to functor categories .
Fibrewise-diagram : β {x} β Functor Cat[ J , Fibre E x ] (Fibre (Diagrams J) x) Fibrewise-diagram .Fβ = DiagramβConstL Fibrewise-diagram .Fβ = Diagram-natβConstL-natl Fibrewise-diagram .F-id = Nat-lift-pathp Ξ» _ β sym Regularity.reduce! Fibrewise-diagram .F-β _ _ = Nat-lift-pathp Ξ» _ β sym Regularity.reduce!
Again, this isomorphism is almost definitional.
Fibrewise-diagram-is-iso : β {x} β is-precat-iso (Fibrewise-diagram {x}) Fibrewise-diagram-is-iso .is-precat-iso.has-is-ff = is-isoβis-equiv $ iso (ConstL-natlβDiagram-nat) (Ξ» Ξ±' β Nat-lift-pathp (Ξ» _ β refl)) (Ξ» Ξ± β Nat-path (Ξ» _ β refl)) Fibrewise-diagram-is-iso .is-precat-iso.has-is-iso = is-isoβis-equiv $ iso ConstLβDiagram (Ξ» F' β Lifting-pathp E refl (Ξ» _ β refl) (Ξ» _ β refl)) (Ξ» F β Functor-path (Ξ» _ β refl) (Ξ» _ β refl))