module Cat.Bi.Instances.Displayed where
The bicategory of displayed categories over a base🔗
Since displayed categories provide a natural setting for “relative category theory”, i.e. the study of categories relative to a base, we should expect that the collection of displayed categories assembles into a bicategory, relativising the bicategory of categories. And, indeed, this is the case: fixing a base we can put together a bicategory where the objects are categories displayed over the 1-cells are vertical functors over and the 2-cells are vertical natural transformations over
The first step is to construct an ordinary category of vertical functors over This is very straightforward, since composition of vertical natural transformations happens at the level of fibre categories.
Vertical-functors : Displayed B o' ℓ' → Displayed B o'' ℓ'' → Precategory _ _ Vertical-functors E F .Ob = Vertical-functor E F Vertical-functors E F .Hom G H = G =>↓ H Vertical-functors E F .Hom-set _ _ = hlevel 2 Vertical-functors E F .id = idnt↓ Vertical-functors E F ._∘_ = _∘nt↓_ Vertical-functors E F .idr f = ext λ x → Cat.idr (Fibre F _) _ Vertical-functors E F .idl f = ext λ x → Cat.idl (Fibre F _) _ Vertical-functors E F .assoc f g h = ext λ x → Cat.assoc (Fibre F _) _ _ _
module _ {o ℓ} (B : Precategory o ℓ) (o' ℓ' : Level) where open Prebicategory private Vf : Displayed B o' ℓ' → Displayed B o'' ℓ'' → Precategory _ _ Vf = Vertical-functors open Vertical-functor open make-natural-iso open Functor open _=>↓_
We can then extend the whiskering operation between vertical natural transformations to the action of a “composition” functor between vertical functor categories, with the functoriality condition precisely as in the nondisplayed case.
∘V-functor : ∀ {E F G : Displayed B o' ℓ'} → Functor (Vf F G ×ᶜ Vf E F) (Vf E G) ∘V-functor .F₀ (G , F) = G ∘V F ∘V-functor .F₁ (f , g) = f ◆↓ g ∘V-functor {G = 𝒢} .F-id {F , G} = ext λ x → ap₂ G._∘_ (F .F-id') refl ∙ G.idr _ where module G {x} = Cat (Fibre 𝒢 x) ∘V-functor {F = ℱ} {G = 𝒢} .F-∘ {X , Y} {Z , W} {U , V} (α , β) (δ , γ) = ext λ x → U .F₁' (β .η' x F.∘ γ .η' x) G.∘ (α .η' _ G.∘ δ .η' _) ≡⟨ G.pushl (F-∘↓ U) ⟩≡ U .F₁' (β .η' x) G.∘ U .F₁' (γ .η' x) G.∘ α .η' _ G.∘ δ .η' _ ≡⟨ G.extend-inner (sym (is-natural↓ α _ _ _)) ⟩≡ U .F₁' (β .η' x) G.∘ α .η' _ G.∘ Z .F₁' (γ .η' _) G.∘ δ .η' _ ≡⟨ G.pulll refl ⟩≡ (U .F₁' (β .η' _) G.∘ α .η' _) G.∘ Z .F₁' (γ .η' _) G.∘ δ .η' _ ∎ where module G {x} = Cat (Fibre 𝒢 x) using (_∘_ ; pushl ; extend-inner ; pulll) module F {x} = Cat (Fibre ℱ x) using (_∘_)
private assoc : Associator-for Vf ∘V-functor assoc {D = D} = to-natural-iso ni where module D = Displayed D module D' {x} = Cat (Fibre D x) using (_∘_ ; idl ; idr ; elimr ; pushl ; introl) ni : make-natural-iso {D = Vf _ _} _ _ ni .eta _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] D) } ni .inv _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] D) } ni .eta∘inv _ = ext λ _ → D'.idl _ ni .inv∘eta _ = ext λ _ → D'.idl _ ni .natural x y f = ext λ _ → D'.idr _ ·· D'.pushl (F-∘↓ (y .fst)) ·· D'.introl refl
Finally, we can put together the bicategory structure itself. This is, again, exactly as in the nondisplayed case, with all the components of the structural isomorphisms being identities.
Disp[] : Prebicategory (o ⊔ ℓ ⊔ lsuc (o' ⊔ ℓ')) (o ⊔ ℓ ⊔ o' ⊔ ℓ') (o ⊔ ℓ ⊔ o' ⊔ ℓ') Disp[] .Ob = Displayed B o' ℓ' Disp[] .Hom = Vertical-functors Disp[] .id = Displayed-functor→Vertical-functor Id' Disp[] .compose = ∘V-functor Disp[] .unitor-l {B = B} = to-natural-iso ni where module B = Displayed B ni : make-natural-iso {D = Vf _ _} _ _ ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) } ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) } ni .eta∘inv _ = ext λ _ → Cat.idl (Fibre B _) _ ni .inv∘eta _ = ext λ _ → Cat.idl (Fibre B _) _ ni .natural x y f = ext λ _ → Cat.elimr (Fibre B _) refl ∙ Cat.id-comm (Fibre B _) Disp[] .unitor-r {B = B} = to-natural-iso ni where module B = Displayed B module B' {x} = Cat (Fibre B x) using (_∘_ ; idl ; elimr) ni : make-natural-iso {D = Vf _ _} _ _ ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) } ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) } ni .eta∘inv _ = ext λ _ → B'.idl _ ni .inv∘eta _ = ext λ _ → B'.idl _ ni .natural x y f = ext λ _ → B'.elimr refl ∙ ap₂ B'._∘_ (y .F-id') refl Disp[] .associator = assoc Disp[] .triangle {C = C} f g = ext λ _ → Cat.idr (Fibre C _) _ Disp[] .pentagon {E = E} f g h i = ext λ _ → ap₂ E._∘_ (E.eliml (ap (f .F₁') (ap (g .F₁') (h .F-id')) ·· ap (f .F₁') (g .F-id') ·· f .F-id')) (E.elimr (E.eliml (f .F-id'))) where module E {x} = Cat (Fibre E x) using (_∘_ ; eliml ; elimr)