module Cat.Functor.Pullback {o ℓ} {C : Precategory o ℓ} where
open Cat.Reasoning C open is-pullback open Pullback open Initial open Functor open _=>_ open /-Obj open /-Hom
Base change🔗
Let be a category with all pullbacks, and a morphism in Then we have a functor called the base change, where the action on objects is given by pulling back along
On objects, the functor maps as in the diagram below. It’s a bit busy, so look at it in parts: On the left we have the object of and on the right we have the whole pullback diagram, showing how the parts fit together. The actual object of the functor gives is the vertical arrow
module _ (pullbacks : ∀ {X Y Z} f g → Pullback C {X} {Y} {Z} f g) {X Y : Ob} (f : Hom Y X) where Base-change : Functor (Slice C X) (Slice C Y) Base-change .F₀ x = ob where ob : /-Obj Y ob .domain = pullbacks (x .map) f .apex ob .map = pullbacks (x .map) f .p₂
On morphisms, we use the universal property of the pullback to obtain a map by observing that the square diagram below is a cone over
Base-change .F₁ {x} {y} dh = dh' where module ypb = Pullback (pullbacks (y .map) f) module xpb = Pullback (pullbacks (x .map) f) dh' : /-Hom _ _ dh' .map = ypb.universal {p₁' = dh .map ∘ xpb.p₁} (pulll (dh .commutes) ∙ xpb.square) dh' .commutes = ypb.p₂∘universal
The properties of pullbacks also guarantee that this operation is functorial, but the details are not particularly enlightening.
Base-change .F-id {x} = ext (sym (xpb.unique id-comm (idr _))) where module xpb = Pullback (pullbacks (x .map) f) Base-change .F-∘ {x} {y} {z} am bm = ext (sym (zpb.unique (pulll zpb.p₁∘universal ∙ pullr ypb.p₁∘universal ∙ assoc _ _ _) (pulll zpb.p₂∘universal ∙ ypb.p₂∘universal))) where module ypb = Pullback (pullbacks (y .map) f) module zpb = Pullback (pullbacks (z .map) f)
Properties🔗
The base change functor is a right adjoint. We construct the left adjoint directly, then give the unit and counit, and finally prove the triangle identities.
The left adjoint, called dependent sum and written is given on objects by precomposition with and on morphisms by what is essentially the identity function — only the witness of commutativity must change.
module _ {X Y : Ob} (f : Hom Y X) where Σf : Functor (Slice C Y) (Slice C X) Σf .F₀ o = cut (f ∘ o .map) Σf .F₁ dh = record { map = dh .map ; commutes = pullr (dh .commutes) } Σf .F-id = trivial! Σf .F-∘ f g = trivial! open _⊣_
Σ-iso-equiv : {X Y : Ob} {f : Hom Y X} → Cat.Reasoning.is-invertible C f → is-equivalence (Σf f) Σ-iso-equiv {X} {f = f} isom = ff+split-eso→is-equivalence Σ-ff Σ-seso where module Sl = Cat.Reasoning (Slice C X) module isom = is-invertible isom func = Σf f Σ-ff : ∀ {x y} → is-equiv (func .F₁ {x} {y}) Σ-ff = is-iso→is-equiv (iso ∘inv (λ x → trivial!) λ x → trivial!) where ∘inv : /-Hom _ _ → /-Hom _ _ ∘inv o .map = o .map ∘inv o .commutes = invertible→monic isom _ _ (assoc _ _ _ ∙ o .commutes) Σ-seso : is-split-eso func Σ-seso y = cut (isom.inv ∘ y .map) , Sl.make-iso into from' (ext (eliml refl)) (ext (eliml refl)) where into : /-Hom _ _ into .map = id into .commutes = id-comm ∙ sym (pulll isom.invl) from' : /-Hom _ _ from' .map = id from' .commutes = elimr refl ∙ cancell isom.invl
The adjunction unit and counit are given by the universal properties of pullbacks.
module _ (pullbacks : ∀ {X Y Z} f g → Pullback C {X} {Y} {Z} f g) {X Y : Ob} (f : Hom Y X) where open _⊣_ open _=>_ Σf⊣f* : Σf f ⊣ Base-change pullbacks f Σf⊣f* .unit .η obj = dh where module pb = Pullback (pullbacks (f ∘ obj .map) f) dh : /-Hom _ _ dh .map = pb.universal {p₁' = id} {p₂' = obj .map} (idr _) dh .commutes = pb.p₂∘universal Σf⊣f* .unit .is-natural x y g = ext (pb.unique₂ {p = (f ∘ y .map) ∘ id ∘ g .map ≡⟨ cat! C ⟩≡ f ∘ y .map ∘ g .map ∎} (pulll pb.p₁∘universal) (pulll pb.p₂∘universal) (pulll pb.p₁∘universal ∙ pullr pb'.p₁∘universal ∙ id-comm) (pulll pb.p₂∘universal ∙ pb'.p₂∘universal ∙ sym (g .commutes))) where module pb = Pullback (pullbacks (f ∘ y .map) f) module pb' = Pullback (pullbacks (f ∘ x .map) f) Σf⊣f* .counit .η obj = dh where module pb = Pullback (pullbacks (obj .map) f) dh : /-Hom _ _ dh .map = pb.p₁ dh .commutes = pb.square Σf⊣f* .counit .is-natural x y g = ext pb.p₁∘universal where module pb = Pullback (pullbacks (y .map) f) Σf⊣f* .zig {A} = ext pb.p₁∘universal where module pb = Pullback (pullbacks (f ∘ A .map) f) Σf⊣f* .zag {B} = ext (sym (pb.unique₂ {p = pb.square} (idr _) (idr _) (pulll pb.p₁∘universal ∙ pullr pb'.p₁∘universal ∙ idr _) (pulll pb.p₂∘universal ∙ pb'.p₂∘universal))) where module pb = Pullback (pullbacks (B .map) f) module pb' = Pullback (pullbacks (f ∘ pb.p₂) f)
This adjunction is comonadic; this generalises the fact that the forgetful functor is comonadic, which we recover by taking
The idea is the same, only with more dependent types: thinking of as a family of types over the comonad sends a map to the projection map Therefore, a coalgebra for this comonad consists of a map over but the coalgebra laws force to be the identity on so all that is left is the map an object of or in other words
Σf-comonadic : is-comonadic Σf⊣f* Σf-comonadic = is-precat-iso→is-equivalence (iso (is-iso→is-equiv ff) (is-iso→is-equiv eso)) where open is-iso eso : is-iso (Comparison-CoEM Σf⊣f* .F₀) eso .from (A , c) = cut (pb.p₂ ∘ c .ρ .map) where module pb = Pullback (pullbacks (A .map) f) eso .rinv (A , c) = Σ-pathp (/-Obj-path refl path) $ Coalgebra-on-pathp _ $ /-Hom-pathp _ _ $ symP $ Hom-pathp-reflr C $ pb≡.unique i0 (pulll (from-pathp-to' C _ λ i → pb≡.p₁ i) ∙ unext (c .ρ-counit)) (pulll (from-pathp-to' C _ λ i → pb≡.p₂ i)) where module pb = Pullback (pullbacks (A .map) f) path : f ∘ pb.p₂ ∘ c .ρ .map ≡ A .map path = assoc _ _ _ ∙ unext (c .ρ .commutes) module pb≡ i = Pullback (pullbacks (path i) f) eso .linv p = /-Obj-path refl pb.p₂∘universal where module pb = Pullback (pullbacks (f ∘ p .map) f) ff : ∀ {x y} → is-iso (Comparison-CoEM Σf⊣f* .F₁ {x} {y}) ff .from g .map = g .hom .map ff {x} {y} .from g .commutes = y .map ∘ g .hom .map ≡˘⟨ pulll pby.p₂∘universal ⟩≡˘ pby.p₂ ∘ pby.universal _ ∘ g .hom .map ≡˘⟨ refl⟩∘⟨ unext (g .preserves) ⟩≡˘ pby.p₂ ∘ pby.universal _ ∘ pbx.universal _ ≡⟨ pulll pby.p₂∘universal ⟩≡ pbx.p₂ ∘ pbx.universal _ ≡⟨ pbx.p₂∘universal ⟩≡ x .map ∎ where module pbx = Pullback (pullbacks (f ∘ x .map) f) module pby = Pullback (pullbacks (f ∘ y .map) f) ff .rinv _ = trivial! ff .linv _ = trivial!
Equifibred natural transformations🔗
A natural transformation is called equifibred, or cartesian, if each of its naturality squares is a pullback:
is-equifibred : ∀ {oj ℓj} {J : Precategory oj ℓj} {F G : Functor J C} → F => G → Type _ is-equifibred {J = J} {F} {G} α = ∀ {x y} (f : J .Precategory.Hom x y) → is-pullback C (F .F₁ f) (α .η y) (α .η x) (G .F₁ f)
An easy property of equifibered transformations is that they are closed under pre-whiskering:
◂-equifibred : ∀ {oj ℓj ok ℓk} {J : Precategory oj ℓj} {K : Precategory ok ℓk} → {F G : Functor J C} (H : Functor K J) (α : F => G) → is-equifibred α → is-equifibred (α ◂ H) ◂-equifibred H α eq f = eq (H .F₁ f)