From a6ed11682a4d0b0d867f3dac2ac1d0f3751b2c7e Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 30 Jan 2023 13:41:42 -0800 Subject: [PATCH 01/18] defn: naturality of adjuncts --- src/Cat/Functor/Adjoint.lagda.md | 42 ++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/src/Cat/Functor/Adjoint.lagda.md b/src/Cat/Functor/Adjoint.lagda.md index 2a22bd1e4..0ea5bc3a0 100644 --- a/src/Cat/Functor/Adjoint.lagda.md +++ b/src/Cat/Functor/Adjoint.lagda.md @@ -574,6 +574,48 @@ $\hom(La,b) \cong \hom(a,Rb)$. (iso L-adjunct R-L-adjunct L-R-adjunct) ``` +Furthermore, these equivalences are natural. + +```agda + L-adjunct-naturall + : ∀ {a b c} (f : D.Hom (L.₀ b) c) (g : C.Hom a b) + → L-adjunct (f D.∘ L.₁ g) ≡ L-adjunct f C.∘ g + L-adjunct-naturall f g = + R.₁ (f D.∘ L.₁ g) C.∘ adj.unit.η _ ≡⟨ R.F-∘ _ _ C.⟩∘⟨refl ⟩ + (R.₁ f C.∘ R.₁ (L.₁ g)) C.∘ adj.unit.η _ ≡⟨ C.extendr (sym $ adj.unit.is-natural _ _ _) ⟩ + (R.₁ f C.∘ adj.unit.η _) C.∘ g ∎ + + L-adjunct-naturalr + : ∀ {a b c} (f : D.Hom b c) (g : D.Hom (L.₀ a) b) + → L-adjunct (f D.∘ g) ≡ R.₁ f C.∘ L-adjunct g + L-adjunct-naturalr f g = C.pushl (R.F-∘ f g) + + L-adjunct-natural₂ + : ∀ {a b c d} (f : D.Hom a b) (g : C.Hom c d) (x : D.Hom (L.F₀ d) a) + → L-adjunct (f D.∘ x D.∘ L.₁ g) ≡ R.₁ f C.∘ L-adjunct x C.∘ g + L-adjunct-natural₂ f g x = + L-adjunct-naturalr f (x D.∘ L.₁ g) ∙ ap (R.₁ f C.∘_) (L-adjunct-naturall x g) + + R-adjunct-naturall + : ∀ {a b c} (f : C.Hom b (R.₀ c)) (g : C.Hom a b) + → R-adjunct (f C.∘ g) ≡ R-adjunct f D.∘ L.₁ g + R-adjunct-naturall f g = D.pushr (L.F-∘ f g) + + R-adjunct-naturalr + : ∀ {a b c} (f : D.Hom b c) (g : C.Hom a (R.₀ b)) + → R-adjunct (R.₁ f C.∘ g) ≡ f D.∘ R-adjunct g + R-adjunct-naturalr f g = + adj.counit.ε _ D.∘ L.₁ (R.₁ f C.∘ g) ≡⟨ D.refl⟩∘⟨ L.F-∘ _ _ ⟩ + adj.counit.ε _ D.∘ L.₁ (R.₁ f) D.∘ L.₁ g ≡⟨ D.extendl (adj.counit.is-natural _ _ _) ⟩ + f D.∘ (adj.counit.ε _ D.∘ L.₁ g) ∎ + + R-adjunct-natural₂ + : ∀ {a b c d} (f : D.Hom a b) (g : C.Hom c d) (x : C.Hom d (R.F₀ a)) + → R-adjunct (R.₁ f C.∘ x C.∘ g) ≡ f D.∘ R-adjunct x D.∘ L.₁ g + R-adjunct-natural₂ f g x = + R-adjunct-naturalr f (x C.∘ g) ∙ ap (f D.∘_) (R-adjunct-naturall x g) +``` + diff --git a/src/Cat/Displayed/Cocartesian/Weak.lagda.md b/src/Cat/Displayed/Cocartesian/Weak.lagda.md index c3529cc7e..915281388 100644 --- a/src/Cat/Displayed/Cocartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cocartesian/Weak.lagda.md @@ -2,6 +2,7 @@ open import Cat.Displayed.Base open import Cat.Displayed.Cartesian open import Cat.Displayed.Cartesian.Weak +open import Cat.Displayed.Fibre open import Cat.Displayed.Total.Op open import Cat.Prelude @@ -368,12 +369,12 @@ $m^{*}$ is cartesian, thus finishing the proof. open Morphisms m h′ id* : Hom[ id ] y′ y* - id* = m*.universal′ (idr _) m′ + id* = m*.universalv m′ path : m* ∘′ hom[ idl _ ] (id* ∘′ f′) ≡ h′ path = m* ∘′ hom[] (id* ∘′ f′) ≡⟨ whisker-r _ ⟩ - hom[] (m* ∘′ id* ∘′ f′) ≡⟨ cancel _ (ap (m ∘_) (idl _)) (pulll′ (idr _) (m*.commutesp (idr _) m′)) ⟩ + hom[] (m* ∘′ id* ∘′ f′) ≡⟨ cancel _ (ap (m ∘_) (idl _)) (pulll′ (idr _) (m*.commutesv m′)) ⟩ m′ ∘′ f′ ≡⟨ p ⟩ h′ ∎ ``` @@ -434,22 +435,62 @@ weak-cocartesian-lift→weak-co-cartesian-lift wlift .Weak-cartesian-lift.weak-c A displayed category with all weak cocartesian lifts is called a -**preopfibered category**. A preopfibred category is opfibered when -weak cocartesian morphisms are closed under composition. This follows -via duality. +**weak cocartesian fibration**, though we will often refer to them +as **weak opfibrations** These are also sometimes called +**preopfibred categories**, though we avoid this terminology, as it +conflicts with the precategory/category distinction. ```agda -weak-cocartesian-lifts→opfibration - : (lifts : ∀ {x y} → (f : Hom x y) → (x′ : Ob[ x ]) → Weak-cocartesian-lift f x′) +record is-weak-cocartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where + no-eta-equality + field + weak-lift : ∀ {x y} → (f : Hom x y) → (x′ : Ob[ x ]) → Weak-cocartesian-lift f x′ + + module weak-lift {x y} (f : Hom x y) (x′ : Ob[ x ]) = + Weak-cocartesian-lift (weak-lift f x′) +``` + +Weak opfibrations are dual to [weak fibrations]. +```agda +weak-op-fibration→weak-opfibration + : is-weak-cartesian-fibration (ℰ ^total-op) + → is-weak-cocartesian-fibration + +weak-opfibration→weak-op-fibration + : is-weak-cocartesian-fibration + → is-weak-cartesian-fibration (ℰ ^total-op) +``` + + +
+As usual, we omit the duality proofs, as they are quite tedious. + +```agda +weak-op-fibration→weak-opfibration wlift .is-weak-cocartesian-fibration.weak-lift f x′ = + weak-co-cartesian-lift→weak-cocartesian-lift $ + is-weak-cartesian-fibration.weak-lift wlift f x′ + +weak-opfibration→weak-op-fibration wlift .is-weak-cartesian-fibration.weak-lift f y′ = + weak-cocartesian-lift→weak-co-cartesian-lift $ + is-weak-cocartesian-fibration.weak-lift wlift f y′ +``` +
+ +A weak opfibration is an opfibration when weak cocartesian morphisms are +closed under composition. This follows via duality. + +```agda +weak-opfibration→opfibration + : is-weak-cocartesian-fibration → (∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y} → {f′ : Hom[ f ] y′ z′} {g′ : Hom[ g ] x′ y′} → is-weak-cocartesian f f′ → is-weak-cocartesian g g′ → is-weak-cocartesian (f ∘ g) (f′ ∘′ g′)) → Cocartesian-fibration -weak-cocartesian-lifts→opfibration wlifts weak-∘ = +weak-opfibration→opfibration wopfib weak-∘ = op-fibration→opfibration $ - weak-cartesian-lifts→fibration (ℰ ^total-op) - (λ f y′ → weak-cocartesian-lift→weak-co-cartesian-lift (wlifts f y′)) + weak-fibration→fibration (ℰ ^total-op) + (weak-opfibration→weak-op-fibration wopfib) (λ f g → weak-cocartesian→weak-co-cartesian $ weak-∘ @@ -462,14 +503,89 @@ cocartesian maps are closed under composition, thanks to `fibration+weak-cocartesian→cocartesian`{.Agda}. ```agda -cartesian+weak-cocartesian-lifts→opfibration +cartesian+weak-opfibration→opfibration : Cartesian-fibration ℰ - → (∀ {x y} → (f : Hom x y) → (x′ : Ob[ x ]) → Weak-cocartesian-lift f x′) + → is-weak-cocartesian-fibration → Cocartesian-fibration -cartesian+weak-cocartesian-lifts→opfibration fib wlifts = - weak-cocartesian-lifts→opfibration wlifts λ f-weak g-weak → +cartesian+weak-opfibration→opfibration fib wlifts = + weak-opfibration→opfibration wlifts λ f-weak g-weak → cocartesian→weak-cocartesian $ cocartesian-∘ (fibration+weak-cocartesian→cocartesian fib f-weak) (fibration+weak-cocartesian→cocartesian fib g-weak) ``` + +# Weak Opfibrations and Equivalence of Hom Sets + +If $\cE$ is a weak opfibration, then the hom sets $x' \to_f y'$ and +$f^{*}(x') \to_{id} y'$ are equivalent, where $f^{*}(x')$ is the codomain +of the lift of $f$ along $y'$. + +```agda +module _ (wopfib : is-weak-cocartesian-fibration) where + open is-weak-cocartesian-fibration wopfib + + weak-opfibration→universal-is-equiv + : ∀ {x y y′} + → (u : Hom x y) + → (x′ : Ob[ x ]) + → is-equiv (weak-lift.universal u x′ {y′}) + weak-opfibration→universal-is-equiv u x′ = + is-iso→is-equiv $ + iso (λ u′ → hom[ idl u ] (u′ ∘′ weak-lift.lifting u x′)) + (λ u′ → sym $ weak-lift.unique u x′ u′ (to-pathp refl)) + (λ u′ → cancel _ _ (weak-lift.commutes u x′ u′)) + + weak-opfibration→vertical-equiv + : ∀ {x y x′ y′} + → (u : Hom x y) + → Hom[ u ] x′ y′ ≃ Hom[ id ] (weak-lift.y′ u x′) y′ + weak-opfibration→vertical-equiv {x′ = x′} u = + weak-lift.universal u x′ , weak-opfibration→universal-is-equiv u x′ +``` + +Furthermore, this equivalence is natural. + +```agda + weak-opfibration→vertical-equiv-natural + : ∀ {x y x′ y′ y″} {g : Hom x y} + → (f′ : Hom[ id ] y′ y″) (g′ : Hom[ g ] x′ y′) + → weak-lift.universal g x′ (hom[ idl g ] (f′ ∘′ g′)) ≡[ sym (idl id) ] + f′ ∘′ weak-lift.universal g x′ g′ + weak-opfibration→vertical-equiv-natural {g = g} f′ g′ = + to-pathp⁻ $ sym $ weak-lift.unique _ _ _ $ to-pathp $ + hom[] (hom[] (f′ ∘′ weak-lift.universal _ _ g′) ∘′ weak-lift.lifting g _) ≡⟨ smashl _ _ ⟩ + hom[] ((f′ ∘′ weak-lift.universal _ _ g′) ∘′ weak-lift.lifting g _) ≡⟨ weave _ (ap (_∘ g) (idl id)) _ (pullr′ _ (weak-lift.commutes _ _ _)) ⟩ + hom[] (f′ ∘′ g′) ∎ +``` + +As in the [weak cartesian case], the converse is also true: if there is +a lifting of objects `Ob[ x ] → Ob[ y ]` for every morphism $f : x \to y$ +in $\cB$, along with a equivalence of homs as above, then $\cE$ is a weak +opfibration. + +[weak cartesian case]: Cat.Cartesian.Weak.html#weak-fibrations-and-equivalence-of-hom-sets + +```agda +module _ (_*₀_ : ∀ {x y} → Hom x y → Ob[ x ] → Ob[ y ]) where + + private + vertical-equiv-iso-natural + : (∀ {x y x′ y′} {f : Hom x y} → Hom[ f ] x′ y′ → Hom[ id ] (f *₀ x′) y′) + → Type _ + vertical-equiv-iso-natural to = + ∀ {x y x′ y′ y″} {g : Hom x y} + → (f′ : Hom[ id ] y′ y″) (g′ : Hom[ g ] x′ y′) + → to (hom[ idl g ] (f′ ∘′ g′)) ≡[ sym (idl id) ] f′ ∘′ to g′ + + vertical-equiv→weak-opfibration + : (to : ∀ {x y x′ y′} {f : Hom x y} → Hom[ f ] x′ y′ → Hom[ id ] (f *₀ x′) y′) + → (eqv : ∀ {x y x′ y′} {f : Hom x y} → is-equiv (to {x} {y} {x′} {y′} {f})) + → (natural : vertical-equiv-iso-natural to) + → is-weak-cocartesian-fibration + vertical-equiv→weak-opfibration to to-eqv natural = + weak-op-fibration→weak-opfibration $ + vertical-equiv→weak-fibration (ℰ ^total-op) _*₀_ to to-eqv λ f′ g′ → + to-pathp (reindex _ _ ∙ from-pathp (natural g′ f′)) +``` + From d8eb8c932bbc85af907049a99ee1ac0a902341f4 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 30 Jan 2023 15:20:08 -0800 Subject: [PATCH 03/18] defn: small lemmas about postcomposition + cartesian maps --- src/Cat/Displayed/Cartesian.lagda.md | 29 +++++++++++++++++++++++ src/Cat/Displayed/Cartesian/Weak.lagda.md | 28 ++++++++++++++++++++++ 2 files changed, 57 insertions(+) diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md index 4045e97b3..f23271bef 100644 --- a/src/Cat/Displayed/Cartesian.lagda.md +++ b/src/Cat/Displayed/Cartesian.lagda.md @@ -420,6 +420,35 @@ vertical+cartesian→invertible {x′ = x′} {x″ = x″} {f′ = f′} f-cart hom[] id′ ∎ ``` +Furthermore, $f' : x' \to_{f} y'$ is cartesian if and only if the +function $f \cdot' -$ is an equivalence. + +```agda +postcompose-equiv→cartesian + : ∀ {x y x′ y′} {f : Hom x y} + → (f′ : Hom[ f ] x′ y′) + → (∀ {w w′} {g : Hom w x} → is-equiv {A = Hom[ g ] w′ x′} (f′ ∘′_)) + → is-cartesian f f′ +postcompose-equiv→cartesian f′ eqv .is-cartesian.universal m h′ = + equiv→inverse eqv h′ +postcompose-equiv→cartesian f′ eqv .is-cartesian.commutes m h′ = + equiv→counit eqv h′ +postcompose-equiv→cartesian f′ eqv .is-cartesian.unique m′ p = + sym (equiv→unit eqv m′) ∙ ap (equiv→inverse eqv) p + +cartesian→postcompose-equiv + : ∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y} {f′ : Hom[ f ] y′ z′} + → is-cartesian f f′ + → is-equiv {A = Hom[ g ] x′ y′} (f′ ∘′_) +cartesian→postcompose-equiv cart = + is-iso→is-equiv $ + iso (universal _) + (commutes _) + (λ g′ → sym (unique g′ refl)) + where open is-cartesian cart +``` + + ## Cartesian Lifts We call an object $a'$ over $a$ together with a Cartesian arrow $f' : a' diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md index de7a738ff..494c3c38f 100644 --- a/src/Cat/Displayed/Cartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md @@ -160,6 +160,34 @@ weak-cartesian→cartesian {x = x} {y′ = y′} {f = f} {f′ = f′} fib f-wea (f-weak.commutes f*) ``` +$f' : x' \to_{f} y'$ is a weak cartesian morphism if and only if +postcomposition of $f'$ onto vertical maps is an equivalence. + +```agda +postcompose-equiv→weak-cartesian + : ∀ {x y x′ y′} {f : Hom x y} + → (f′ : Hom[ f ] x′ y′) + → (∀ {x″} → is-equiv {A = Hom[ id ] x″ x′} (f′ ∘′_)) + → is-weak-cartesian f f′ +postcompose-equiv→weak-cartesian f′ eqv .is-weak-cartesian.universal h′ = + equiv→inverse eqv (hom[ idr _ ]⁻ h′) +postcompose-equiv→weak-cartesian f′ eqv .is-weak-cartesian.commutes h′ = + to-pathp⁻ (equiv→counit eqv (hom[ idr _ ]⁻ h′)) +postcompose-equiv→weak-cartesian f′ eqv .is-weak-cartesian.unique m′ p = + (sym $ equiv→unit eqv m′) ∙ ap (equiv→inverse eqv) (from-pathp⁻ p) + +weak-cartesian→postcompose-equiv + : ∀ {x y x′ x″ y′} {f : Hom x y} {f′ : Hom[ f ] x′ y′} + → is-weak-cartesian f f′ + → is-equiv {A = Hom[ id ] x″ x′} (f′ ∘′_) +weak-cartesian→postcompose-equiv wcart = + is-iso→is-equiv $ + iso (λ h′ → universal (hom[ idr _ ] h′)) + (λ h′ → from-pathp⁻ (commutes _) ·· hom[]-∙ _ _ ·· liberate _) + (λ h′ → sym $ unique _ (to-pathp refl)) + where open is-weak-cartesian wcart +``` + ## Weak Cartesian Lifts We can also define a notion of weak cartesian lifts, much like we can From d257f416f7c4267b461a4c50a6d5e4470df50756 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 08:59:23 -0800 Subject: [PATCH 04/18] defn: more naturality, add rebase combinators --- src/Cat/Displayed/Cartesian.lagda.md | 26 +++++ src/Cat/Displayed/Cartesian/Weak.lagda.md | 123 +++++++++++++++++----- src/Cat/Displayed/Reasoning.lagda.md | 60 ++++++++++- 3 files changed, 182 insertions(+), 27 deletions(-) diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md index f23271bef..b8876109d 100644 --- a/src/Cat/Displayed/Cartesian.lagda.md +++ b/src/Cat/Displayed/Cartesian.lagda.md @@ -168,6 +168,15 @@ every cartesian map is [weakly cartesian]. → f′ ∘′ h′ ≡[ idr _ ] g′ → h′ ≡ universalv g′ uniquev h′ p = uniquep (idr f) refl (idr f) h′ p + + uniquev₂ + : ∀ {x′} {g′ : Hom[ f ] x′ b′} + → (h′ h″ : Hom[ id ] x′ a′) + → f′ ∘′ h′ ≡[ idr _ ] g′ + → f′ ∘′ h″ ≡[ idr _ ] g′ + → h′ ≡ h″ + uniquev₂ h′ h″ p q = + uniquep₂ (idr f) refl (idr f) h′ h″ p q ``` ## Properties of Cartesian Morphisms @@ -488,6 +497,23 @@ record Cartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where Cartesian-lift (has-lift f y′) ``` +Note that if $\cE$ is a fibration, we can define an operation that +allows us to move vertical morphisms between fibres. This actually +extends to a collection of functors, called [base change functors]. +This operation is also definable for [weak fibrations], as it only +uses the universal property that yields a vertical morphism. + +[base change functors]: Cat.Displayed.Cartesian.Indexing.html +[weak fibrations]: Cat.Displayed.Cartesian.Weak.html#is-weak-cartesian-fibration + +```agda + rebase : ∀ {x y y′ y″} → (f : Hom x y) + → Hom[ id ] y′ y″ + → Hom[ id ] (has-lift.x′ f y′) (has-lift.x′ f y″) + rebase f vert = + has-lift.universalv f _ (hom[ idl _ ] (vert ∘′ has-lift.lifting f _)) +``` + A Cartesian fibration is a displayed category having Cartesian lifts for every right corner. diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md index 494c3c38f..f0776f179 100644 --- a/src/Cat/Displayed/Cartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md @@ -7,6 +7,7 @@ open import Cat.Prelude import Cat.Displayed.Cartesian as Cart import Cat.Displayed.Reasoning as DR import Cat.Displayed.Morphism as DM +import Cat.Reasoning as CR module Cat.Displayed.Cartesian.Weak {o ℓ o′ ℓ′} @@ -14,7 +15,7 @@ module Cat.Displayed.Cartesian.Weak (ℰ : Displayed ℬ o′ ℓ′) where -open Precategory ℬ +open CR ℬ open Displayed ℰ open Cart ℰ open DR ℰ @@ -222,6 +223,21 @@ record is-weak-cartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where Weak-cartesian-lift (weak-lift f y′) ``` +Note that if $\cE$ is a weak fibration, we can define an operation that +allows us to move vertical morphisms between fibres. This is actually +enough to define [base change functors], though they are not well behaved +unless $\cE$ is a fibration. + +[base change functors]: Cat.Displayed.Cartesian.Indexing.html + +```agda + rebase : ∀ {x y y′ y″} → (f : Hom x y) + → Hom[ id ] y′ y″ + → Hom[ id ] (weak-lift.x′ f y′) (weak-lift.x′ f y″) + rebase f vert = + weak-lift.universal f _ (hom[ idl _ ] (vert ∘′ weak-lift.lifting f _)) +``` + Every fibration is a weak fibration. ```agda @@ -493,20 +509,32 @@ module _ (wfib : is-weak-cartesian-fibration) where Furthermore, this equivalence is natural. ```agda - weak-fibration→vertical-equiv-naturall + weak-fibration→vertical-equiv-naturalr : ∀ {x y x′ x″ y′} {f : Hom x y} → (f′ : Hom[ f ] x″ y′) (g′ : Hom[ id ] x′ x″) → weak-lift.universal f y′ (hom[ idr _ ] (f′ ∘′ g′)) ≡[ sym (idl id) ] weak-lift.universal f y′ f′ ∘′ g′ - weak-fibration→vertical-equiv-naturall {f = f} f′ g′ = + weak-fibration→vertical-equiv-naturalr {f = f} f′ g′ = to-pathp⁻ $ sym $ weak-lift.unique f _ _ $ to-pathp $ hom[] (weak-lift.lifting f _ ∘′ hom[] (weak-lift.universal f _ f′ ∘′ g′)) ≡⟨ smashr _ _ ⟩ hom[] (weak-lift.lifting f _ ∘′ weak-lift.universal f _ f′ ∘′ g′) ≡⟨ weave _ (ap (f ∘_) (idl id)) _ (pulll′ _ (weak-lift.commutes _ _ _)) ⟩ hom[] (f′ ∘′ g′) ∎ + + weak-fibration→vertical-equiv-naturall + : ∀ {x y x′ y′ y″ } {g : Hom x y} + → (f′ : Hom[ id ] y′ y″) (g′ : Hom[ g ] x′ y′) + → weak-lift.universal g y″ (hom[ idl _ ] (f′ ∘′ g′)) ≡[ sym (idl id) ] + rebase g f′ ∘′ weak-lift.universal g y′ g′ + weak-fibration→vertical-equiv-naturall {g = g} f′ g′ = + to-pathp⁻ $ sym $ weak-lift.unique g _ _ $ to-pathp $ + smashr _ _ + ∙ revive₁ (pulll[] _ (weak-lift.commutes g _ _)) + ∙ smashl _ _ + ∙ weave _ (pullr (idr g)) _ (pullr[] _ (weak-lift.commutes g _ _)) ``` An *extremely* useful fact is that the converse is true: if there is some -lifting of objects `Ob[ y ] → Ob[ x ]` for every morphism $f : x \to y$ +lifting of objects $\cE_{y} \to \cE_{x}$ for every morphism $f : x \to y$ in $\cB$, along with a natural equivalence of homs as above, then $\cE$ is a weak fibration. @@ -533,28 +561,28 @@ module _ (_*₀_ : ∀ {x y} → Hom x y → Ob[ y ] → Ob[ x ]) where → to (hom[ idr _ ] (f′ ∘′ g′)) ≡[ sym (idl id) ] to f′ ∘′ g′ vertical-equiv→weak-fibration - : (to : ∀ {x y x′ y′} {f : Hom x y} → Hom[ f ] x′ y′ → Hom[ id ] x′ (f *₀ y′)) - → (∀ {x y x′ y′} {f : Hom x y} → is-equiv (to {x} {y} {x′} {y′} {f})) - → vertical-equiv-iso-natural to + : (to* : ∀ {x y x′ y′} {f : Hom x y} → Hom[ f ] x′ y′ → Hom[ id ] x′ (f *₀ y′)) + → (∀ {x y x′ y′} {f : Hom x y} → is-equiv (to* {x} {y} {x′} {y′} {f})) + → vertical-equiv-iso-natural to* → is-weak-cartesian-fibration - vertical-equiv→weak-fibration to to-eqv natural .weak-lift f y′ = f-lift where + vertical-equiv→weak-fibration to* to-eqv natural .weak-lift f y′ = f-lift where ``` To start, we note that the inverse portion of the equivalence is also natural. ```agda - from : ∀ {x y x′ y′} {f : Hom x y} → Hom[ id ] x′ (f *₀ y′) → Hom[ f ] x′ y′ - from = equiv→inverse to-eqv + from* : ∀ {x y x′ y′} {f : Hom x y} → Hom[ id ] x′ (f *₀ y′) → Hom[ f ] x′ y′ + from* = equiv→inverse to-eqv - from-natural + from*-natural : ∀ {x y} {f : Hom x y} {x′ x″ : Ob[ x ]} {y′ : Ob[ y ]} → (f′ : Hom[ id ] x″ (f *₀ y′)) (g′ : Hom[ id ] x′ x″) - → from (hom[ idl id ] (f′ ∘′ g′)) ≡[ sym (idr f) ] from f′ ∘′ g′ - from-natural {f = f} f′ g′ = + → from* (hom[ idl id ] (f′ ∘′ g′)) ≡[ sym (idr f) ] from* f′ ∘′ g′ + from*-natural {f = f} f′ g′ = to-pathp⁻ $ ap fst $ is-contr→is-prop (to-eqv .is-eqv (hom[ idl id ] (f′ ∘′ g′))) - (from (hom[ idl id ] (f′ ∘′ g′)) , equiv→counit to-eqv _) - (hom[ idr f ] (from f′ ∘′ g′) , from-pathp⁻ (natural (from f′) g′) ∙ + (from* (hom[ idl id ] (f′ ∘′ g′)) , equiv→counit to-eqv _) + (hom[ idr f ] (from* f′ ∘′ g′) , from-pathp⁻ (natural (from* f′) g′) ∙ (hom[]⟩⟨ ap (_∘′ g′) (equiv→counit to-eqv _))) ``` @@ -566,7 +594,7 @@ obtain the required lifting $x' \to_{f} f^{*}(y')$. ```agda f-lift : Weak-cartesian-lift f y′ f-lift .x′ = f *₀ y′ - f-lift .lifting = from id′ + f-lift .lifting = from* id′ ``` Now, we must show that the constructed lifting is weakly cartesian. We @@ -575,16 +603,59 @@ universal map; the remaining properties follow from the fact that the equivalence is natural. ```agda - f-lift .weak-cartesian .universal g′ = to g′ + f-lift .weak-cartesian .universal g′ = to* g′ f-lift .weak-cartesian .commutes g′ = to-pathp $ - hom[] (from id′ ∘′ to g′) ≡˘⟨ from-pathp⁻ (from-natural id′ (to g′)) ⟩ - from (hom[] (id′ ∘′ to g′)) ≡⟨ ap from idl[] ⟩ - from (to g′) ≡⟨ equiv→unit to-eqv g′ ⟩ - g′ ∎ + hom[] (from* id′ ∘′ to* g′) ≡˘⟨ from-pathp⁻ (from*-natural id′ (to* g′)) ⟩ + from* (hom[] (id′ ∘′ to* g′)) ≡⟨ ap from* idl[] ⟩ + from* (to* g′) ≡⟨ equiv→unit to-eqv g′ ⟩ + g′ ∎ f-lift .weak-cartesian .unique {g′ = g′} h′ p = - h′ ≡˘⟨ idl[] {p = idl id} ⟩ - hom[] (id′ ∘′ h′) ≡˘⟨ hom[]⟩⟨ ap (_∘′ h′) (equiv→counit to-eqv id′) ⟩ - hom[] (to (from id′) ∘′ h′) ≡˘⟨ from-pathp⁻ (natural (from id′) h′) ⟩ - to (hom[] (from id′ ∘′ h′)) ≡⟨ ap to (from-pathp p) ⟩ - to g′ ∎ + h′ ≡˘⟨ idl[] {p = idl id} ⟩ + hom[] (id′ ∘′ h′) ≡˘⟨ hom[]⟩⟨ ap (_∘′ h′) (equiv→counit to-eqv id′) ⟩ + hom[] (to* (from* id′) ∘′ h′) ≡˘⟨ from-pathp⁻ (natural (from* id′) h′) ⟩ + to* (hom[] (from* id′ ∘′ h′)) ≡⟨ ap to* (from-pathp p) ⟩ + to* g′ ∎ +``` + +Note that this result does *not* extend to fibrations; the equivalence +of homs can only get us weak cartesian lifts. To make the final step +to a fibration, we need to use other means. + +However, we still get the nice equivalence of hom sets if $\cE$ is a +fibration. + +```agda +module _ (fib : Cartesian-fibration) where + open Cartesian-fibration fib + + fibration→universal-is-equiv + : ∀ {x y x′ y′} + → (f : Hom x y) + → is-equiv (has-lift.universalv f y′ {x′}) + fibration→universal-is-equiv f = + weak-fibration→universal-is-equiv (fibration→weak-fibration fib) f + + fibration→vertical-equiv + : ∀ {x y x′ y′} + → (f : Hom x y) + → Hom[ f ] x′ y′ ≃ Hom[ id ] x′ (has-lift.x′ f y′) + fibration→vertical-equiv f = + weak-fibration→vertical-equiv (fibration→weak-fibration fib) f + + fibration→vertical-equiv-naturalr + : ∀ {x y x′ x″ y′} {f : Hom x y} + → (f′ : Hom[ f ] x″ y′) (g′ : Hom[ id ] x′ x″) + → has-lift.universalv f y′ (hom[ idr _ ] (f′ ∘′ g′)) ≡[ sym (idl id) ] + has-lift.universalv f y′ f′ ∘′ g′ + fibration→vertical-equiv-naturalr f′ g′ = + weak-fibration→vertical-equiv-naturalr (fibration→weak-fibration fib) f′ g′ + + fibration→vertical-equiv-naturall + : ∀ {x y x′ y′ y″ } {g : Hom x y} + → (f′ : Hom[ id ] y′ y″) (g′ : Hom[ g ] x′ y′) + → has-lift.universalv g y″ (hom[ idl _ ] (f′ ∘′ g′)) ≡[ sym (idl id) ] + rebase g f′ ∘′ has-lift.universalv g y′ g′ + fibration→vertical-equiv-naturall {g = g} f′ g′ = + weak-fibration→vertical-equiv-naturall (fibration→weak-fibration fib) f′ g′ ``` + diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md index 49cc5dc3a..1e42abb04 100644 --- a/src/Cat/Displayed/Reasoning.lagda.md +++ b/src/Cat/Displayed/Reasoning.lagda.md @@ -79,6 +79,12 @@ hom[]-∙ {f′ : E.Hom[ f ] x y} → hom[ q ] (hom[ p ] f′) ≡ hom[ p ∙ q ] f′ hom[]-∙ p q = sym (subst-∙ (λ h → E.Hom[ h ] _ _) _ _ _) + +duplicate + : ∀ {a b x y} {f f' g : B.Hom a b} (p : f ≡ g) (q : f' ≡ g) (r : f ≡ f') + {f′ : E.Hom[ f ] x y} + → hom[ p ] f′ ≡ hom[ q ] (hom[ r ] f′) +duplicate p q r = reindex _ _ ∙ sym (hom[]-∙ r q) ``` To understand why these whiskering lemmas have such complicated types, @@ -117,6 +123,24 @@ whisker-l {g = g} {a′} {_} {c′} {f′ = f′} {g′ = g′} p i = j (j = i0) → transport-filler (λ i → E.Hom[ p i B.∘ g ] _ _) (f′ E.∘′ g′) i ``` + + The rest of this module is made up of grueling applications of the three lemmas above: @@ -135,6 +159,20 @@ smashl → hom[ q ] (hom[ p ] f′ E.∘′ g′) ≡ hom[ ap (B._∘ g) p ∙ q ] (f′ E.∘′ g′) smashl p q = ap hom[ q ] (whisker-l p) ∙ hom[]-∙ _ _ +expandl + : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {h : B.Hom a c} {a′ b′ c′} + {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′} + → (p : f ≡ f') (q : f B.∘ g ≡ h) + → hom[ q ] (f′ E.∘′ g′) ≡ hom[ ap (B._∘ g) (sym p) ∙ q ] (hom[ p ] f′ E.∘′ g′) +expandl p q = reindex q _ ∙ (sym $ smashl _ _) + +expandr + : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {h : B.Hom a c} {a′ b′ c′} + {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′} + → (p : g ≡ g') (q : f B.∘ g ≡ h) + → hom[ q ] (f′ E.∘′ g′) ≡ hom[ ap (f B.∘_) (sym p) ∙ q ] (f′ E.∘′ hom[ p ] g′) +expandr p q = reindex q _ ∙ (sym $ smashr _ _) + yank : ∀ {a b c d} {f : B.Hom c d} {g : B.Hom b c} {h : B.Hom a b} {i : B.Hom a c} {j : B.Hom b d} @@ -404,14 +442,22 @@ module _ {a′ : Hom[ a ] y′ z′} {b′ : Hom[ b ] x′ y′} {c′ : Hom[ c hom[ refl ] (c′ ∘′ f′) ≡⟨ liberate _ ⟩ c′ ∘′ f′ ∎ + pulll[] : ∀ {f′ : Hom[ f ] w′ x′} + → a′ ∘′ (b′ ∘′ f′) ≡[ pulll p ] c′ ∘′ f′ + pulll[] = pulll′ + pullr′ : ∀ {f′ : Hom[ f ] z′ w′} {q : (f ∘ a) ∘ b ≡ f ∘ c} - → (f′ ∘′ a′) ∘′ b′ ≡[ q ] f′ ∘′ c′ + → (f′ ∘′ a′) ∘′ b′ ≡[ q ] f′ ∘′ c′ pullr′ {f = f} {f′ = f′} {q = q} = to-pathp $ hom[ q ] ((f′ ∘′ a′) ∘′ b′) ≡˘⟨ assoc[] ⟩ hom[ assoc f a b ∙ q ] (f′ ∘′ a′ ∘′ b′) ≡⟨ apr′ p′ ⟩ hom[ refl ] (f′ ∘′ c′) ≡⟨ liberate _ ⟩ f′ ∘′ c′ ∎ + pullr[] : ∀ {f′ : Hom[ f ] z′ w′} + → (f′ ∘′ a′) ∘′ b′ ≡[ pullr p ] f′ ∘′ c′ + pullr[] = pullr′ + module _ {a′ : Hom[ a ] y′ z′} {b′ : Hom[ b ] x′ y′} {c′ : Hom[ c ] x′ z′} (p : c ≡ a ∘ b) (p′ : c′ ≡[ p ] a′ ∘′ b′) where abstract @@ -420,11 +466,19 @@ module _ {a′ : Hom[ a ] y′ z′} {b′ : Hom[ b ] x′ y′} {c′ : Hom[ c pushl′ {f′ = f′} {q = q} i = pulll′ (sym p) (λ j → p′ (~ j)) {f′ = f′} {q = sym q} (~ i) + pushl[] : ∀ {f′ : Hom[ f ] w′ x′} + → c′ ∘′ f′ ≡[ pushl p ] a′ ∘′ (b′ ∘′ f′) + pushl[] = pushl′ + pushr′ : ∀ {f′ : Hom[ f ] z′ w′} {q : f ∘ c ≡ (f ∘ a) ∘ b} → f′ ∘′ c′ ≡[ q ] (f′ ∘′ a′) ∘′ b′ pushr′ {f′ = f′} {q = q} i = pullr′ (sym p) (λ j → p′ (~ j)) {f′ = f′} {q = sym q} (~ i) + pushr[] : ∀ {f′ : Hom[ f ] z′ w′} + → f′ ∘′ c′ ≡[ pushr p ] (f′ ∘′ a′) ∘′ b′ + pushr[] = pushr′ + module _ {f′ : Hom[ f ] y′ z′} {h′ : Hom[ h ] x′ y′} {g′ : Hom[ g ] y′ z′} {i′ : Hom[ i ] x′ y′} (p : f ∘ h ≡ g ∘ i) (p′ : f′ ∘′ h′ ≡[ p ] g′ ∘′ i′) where abstract @@ -473,6 +527,10 @@ module _ {a′ : Hom[ a ] y′ x′} {b′ : Hom[ b ] x′ y′} hom[ sym (assoc a b f) ∙ q ] ((a′ ∘′ b′) ∘′ f′) ≡⟨ shiftl _ (eliml′ p p′) ⟩ f′ ∎ + cancell[] : ∀ {f′ : Hom[ f ] z′ x′} + → a′ ∘′ b′ ∘′ f′ ≡[ cancell p ] f′ + cancell[] = cancell′ + cancelr′ : ∀ {f′ : Hom[ f ] x′ z′} {q : (f ∘ a) ∘ b ≡ f} → (f′ ∘′ a′) ∘′ b′ ≡[ q ] f′ cancelr′ {f = f} {f′ = f′} {q = q} = to-pathp $ From a78a66b0052cc399e102c91cf02d7447a52dc564 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 09:05:43 -0800 Subject: [PATCH 05/18] chore: refactor base change to use 'rebase' --- src/Cat/Displayed/Cartesian/Indexing.lagda.md | 135 ++++++++---------- 1 file changed, 59 insertions(+), 76 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md index 1f0aad341..36ab13d6b 100644 --- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md +++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md @@ -54,31 +54,24 @@ of base_ along $f$. module _ {𝒶 𝒷} (f : Hom 𝒶 𝒷) where base-change : Functor (Fibre E 𝒷) (Fibre E 𝒶) base-change .F₀ ob = has-lift f ob .x′ - base-change .F₁ {x} {y} vert = has-lift f y .universal id $ - hom[ id-comm-sym ] (vert ∘′ has-lift f x .lifting) + base-change .F₁ {x} {y} vert = rebase f vert ``` @@ -101,20 +94,14 @@ of heart. base-change-id = to-natural-iso mi where open make-natural-iso mi : make-natural-iso (base-change id) Id - mi .eta x = has-lift id x .lifting - mi .inv x = has-lift id x .universal _ (hom[ sym (idl id) ] id′) - mi .eta∘inv x = - ap hom[] (has-lift id x .commutes _ _) - ·· hom[]-∙ _ _ ·· reindex _ _ ∙ transport-refl id′ + mi .eta x = has-lift.lifting id x + mi .inv x = has-lift.universalv id x id′ + mi .eta∘inv x = cancel _ _ (has-lift.commutesv _ _ _) mi .inv∘eta x = sym $ - has-lift id x .unique Fa.id (shiftr (idr _) (idr′ _)) - ∙ sym (has-lift id x .unique _ (pulll-indexr _ (has-lift id x .commutes _ _) - ·· ap hom[] (whisker-l _ - ·· reindex _ (idl _ ∙ sym (idr _) ∙ ap (_∘ id) (sym (idr _))) - ·· sym (hom[]-∙ _ _) ∙ ap hom[] (from-pathp (idl′ _))) - ·· hom[]-∙ _ _ ∙ reindex _ _)) - mi .natural x y f = ap hom[] (sym (has-lift id y .commutes _ _) ∙ ap₂ _∘′_ refl - (ap (has-lift id y .universal _) (sym (reindex _ refl ∙ transport-refl _)))) + has-lift.uniquev₂ id x Fa.id _ (cast[] $ idr′ _) $ + to-pathp (smashr _ _ ∙ cancel _ _ (cancell[] _ (has-lift.commutesv _ _ _))) + mi .natural x y f = ap hom[] $ sym $ + has-lift.commutes _ _ _ _ ·· hom[]-∙ _ _ ·· liberate _ ``` @@ -138,47 +125,43 @@ properties and I recommend that nobody look at it, ever. . base-change-comp = to-natural-iso mi where open make-natural-iso mi : make-natural-iso (base-change (f ∘ g)) (base-change g F∘ base-change f) - mi .eta x = has-lift g _ .universal _ $ - has-lift f _ .universal _ $ - hom[ ap (f ∘_) (sym (idr g)) ] (has-lift (f ∘ g) x .lifting) - mi .inv x = has-lift (f ∘ g) _ .universal _ $ - hom[ sym (idr _) ] (has-lift f _ .lifting ∘′ has-lift g _ .lifting) - mi .eta∘inv x = sym $ - has-lift g _ .unique _ (shiftr (idr _) (idr′ _)) - ∙ sym (has-lift g _ .unique _ (pulll-indexr _ (has-lift g _ .commutes _ _) - ∙ has-lift f _ .unique _ (pulll-indexr _ (has-lift f _ .commutes _ _) - ∙ ap hom[] (whisker-l _ ∙ ap hom[] (has-lift (f ∘ g) _ .commutes _ _)) - ∙ hom[]-∙ _ _ ∙ hom[]-∙ _ _) ∙ sym (has-lift f x .unique _ - (whisker-r _ ∙ reindex _ _)))) - mi .inv∘eta x = sym $ - has-lift (f ∘ g) _ .unique _ (sym (from-pathp (symP (idr′ _)))) - ∙ sym (has-lift (f ∘ g) _ .unique _ (pulll-indexr _ - (has-lift (f ∘ g) _ .commutes _ _) - ∙ ap hom[] (whisker-l _ ∙ ap hom[] (sym (from-pathp (assoc′ _ _ _)) - ∙ ap hom[] (ap₂ _∘′_ refl (has-lift g _ .commutes _ _) - ∙ has-lift f _ .commutes _ _))) - ∙ hom[]-∙ _ _ ∙ hom[]-∙ _ _ ∙ hom[]-∙ _ _ ∙ reindex _ _)) - mi .natural x y f′ = ap hom[] - (has-lift g (has-lift f y .x′) .unique _ - (sym (from-pathp (symP (assoc′ _ _ _ ))) - ·· ap hom[ sym (assoc _ _ _) ] (ap₂ _∘′_ (has-lift g _ .commutes id _) refl) - ·· ap hom[ sym (assoc _ _ _) ] (whisker-l _) - ·· hom[]-∙ _ _ - ·· ap hom[] (sym (from-pathp (assoc′ (F₁ (base-change f) f′) - (has-lift g _ .lifting) (has-lift g _ .universal _ _))) - ∙ ap hom[] (ap₂ _∘′_ refl (has-lift g _ .commutes _ _))) - ∙ hom[]-∙ _ _ ∙ reindex _ (idl _ ∙ ap (g ∘_) (sym (idl id)))) - ) ∙ ap hom[] - ( sym (has-lift g _ .unique _ (sym (from-pathp (symP (assoc′ _ _ _))) - ∙ ap hom[ sym (assoc _ _ _) ] (ap₂ _∘′_ (has-lift g _ .commutes _ _) refl) - ∙ sym (has-lift f y .unique _ (pulll-indexr _ (has-lift f y .commutes _ _) - ∙ ap hom[] (whisker-l _ ∙ ap hom[] (sym (from-pathp (assoc′ _ _ _)) - ∙ ap hom[] (ap₂ _∘′_ refl (has-lift f x .commutes _ _))) ∙ hom[]-∙ _ _) - ∙ hom[]-∙ _ _ ∙ ap hom[] (whisker-r _) - ∙ reindex _ (idl _ ∙ ap (f ∘_) (ap (g ∘_) (sym (idl id))))) - ∙ sym (has-lift f y .unique _ (pulll-indexr _ (has-lift f y .commutes _ _) - ∙ ap hom[] (whisker-l _) ∙ hom[]-∙ _ _ - ∙ ap hom[] (has-lift (f ∘ g) y .commutes _ _) ∙ hom[]-∙ _ _ - ∙ sym (hom[]-∙ _ _ ∙ reindex _ _))))))) + mi .eta x = + has-lift.universalv g _ $ has-lift.universal f x g (has-lift.lifting (f ∘ g) x) + mi .inv x = + has-lift.universalv (f ∘ g) x (has-lift.lifting f _ ∘′ has-lift.lifting g _) + mi .eta∘inv x = + has-lift.uniquev₂ g _ _ _ + (to-pathp $ + smashr _ _ + ·· revive₁ (pulll[] _ (has-lift.commutesv g _ _)) + ·· has-lift.uniquep₂ f _ refl refl refl _ _ + (pulll-indexr _ (has-lift.commutes f _ _ _) + ∙ cancel _ _ (has-lift.commutesv (f ∘ g) _ _)) + refl) + (idr′ _) + mi .inv∘eta x = + has-lift.uniquev₂ (f ∘ g) _ _ _ + (to-pathp $ + smashr _ _ + ·· revive₁ (pulll[] _ (has-lift.commutesv (f ∘ g) _ _)) + ·· revive₁ (pullr[] _ (has-lift.commutesv g _ _)) + ∙ cancel _ _ (has-lift.commutes f _ _ _)) + (idr′ _) + mi .natural x y f′ = + ap hom[] $ cartesian→weak-monic E (has-lift.cartesian g _) _ _ $ + from-pathp⁻ (pulll[] _ (has-lift.commutes g _ _ _)) + ·· smashl _ _ ·· smashl _ _ + ·· revive₁ (pullr[] _ (has-lift.commutesv g _ _ )) + ·· (cartesian→weak-monic E (has-lift.cartesian f _) _ _ $ + whisker-r _ + ·· revive₁ (pulll[] _ (has-lift.commutesv f _ _)) + ·· smashl _ _ + ·· revive₁ (pullr[] _ (has-lift.commutes f _ _ _)) + ·· duplicate _ (ap (f ∘_) (intror (idl id))) _ + ·· revive₁ (symP (has-lift.commutesv (f ∘ g) _ _)) + ·· revive₁ (pushl[] _ (symP $ has-lift.commutes f _ _ _)) + ·· unwhisker-r _ (ap (g ∘_) (sym $ idl id)) + ·· ap (has-lift.lifting f _ ∘′_) (expandl _ _ ∙ reindex _ _)) + ∙ cancel (sym $ assoc _ _ _) _ (pushl[] _ (symP $ has-lift.commutes g _ _ _)) ``` From 5ca07b0697a1f3ce14a56b1aca2b1edde1382918 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 12:23:54 -0800 Subject: [PATCH 06/18] defn: opreindexing --- src/Cat/Displayed/Cocartesian.lagda.md | 48 ++++++++++++ .../Displayed/Cocartesian/Indexing.lagda.md | 75 +++++++++++++++++++ src/Cat/Displayed/Instances/Slice.lagda.md | 24 ++++++ 3 files changed, 147 insertions(+) create mode 100644 src/Cat/Displayed/Cocartesian/Indexing.lagda.md diff --git a/src/Cat/Displayed/Cocartesian.lagda.md b/src/Cat/Displayed/Cocartesian.lagda.md index 1a66a1b11..8d07823a2 100644 --- a/src/Cat/Displayed/Cocartesian.lagda.md +++ b/src/Cat/Displayed/Cocartesian.lagda.md @@ -122,6 +122,42 @@ to a unique universal factorisation of $h'$ through a map $b' \to_{m} u'$ → m′ ∘′ f′ ≡[ p ] h′ → m′ ≡[ q ] universal′ r h′ uniquep p q r {h′ = h′} m′ s = to-pathp⁻ (unique m′ (from-pathp⁻ s) ∙ from-pathp⁻ (universalp p q r h′)) + + uniquep₂ : ∀ {u u′} {m₁ m₂ : Hom b u} {k : Hom a u} + → (p : m₁ ∘ f ≡ k) (q : m₁ ≡ m₂) (r : m₂ ∘ f ≡ k) + → {h′ : Hom[ k ] a′ u′} + → (m₁′ : Hom[ m₁ ] b′ u′) + → (m₂′ : Hom[ m₂ ] b′ u′) + → m₁′ ∘′ f′ ≡[ p ] h′ + → m₂′ ∘′ f′ ≡[ r ] h′ + → m₁′ ≡[ q ] m₂′ + uniquep₂ p q r {h′ = h′} m₁′ m₂′ α β = to-pathp⁻ $ + unique m₁′ (from-pathp⁻ α) + ·· from-pathp⁻ (universalp p q r _) + ·· ap hom[] (sym (unique m₂′ (from-pathp⁻ β))) + + universalv : ∀ {b″} (f″ : Hom[ f ] a′ b″) → Hom[ id ] b′ b″ + universalv f″ = universal′ (idl _) f″ + + commutesv + : ∀ {x′} (g′ : Hom[ f ] a′ x′) + → universalv g′ ∘′ f′ ≡[ idl _ ] g′ + commutesv = commutesp (idl _) + + uniquev + : ∀ {x′} {g′ : Hom[ f ] a′ x′} + → (h′ : Hom[ id ] b′ x′) + → h′ ∘′ f′ ≡[ idl _ ] g′ + → h′ ≡ universalv g′ + uniquev h′ p = uniquep (idl _) refl (idl _) h′ p + + uniquev₂ + : ∀ {x′} {g′ : Hom[ f ] a′ x′} + → (h′ h″ : Hom[ id ] b′ x′) + → h′ ∘′ f′ ≡[ idl _ ] g′ + → h″ ∘′ f′ ≡[ idl _ ] g′ + → h′ ≡ h″ + uniquev₂ h′ h″ p q = uniquep₂ (idl _) refl (idl _) h′ h″ p q ``` --> @@ -362,6 +398,18 @@ record Cocartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where module has-lift {x y} (f : Hom x y) (x′ : Ob[ x ]) = Cocartesian-lift (has-lift f x′) ``` + + + As expected, opfibrations are dual to fibrations. ```agda op-fibration→opfibration : Cartesian-fibration (ℰ ^total-op) → Cocartesian-fibration diff --git a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md new file mode 100644 index 000000000..7e409f584 --- /dev/null +++ b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md @@ -0,0 +1,75 @@ +```agda +open import Cat.Displayed.Base +open import Cat.Displayed.Cocartesian +open import Cat.Displayed.Fibre +open import Cat.Instances.Functor +open import Cat.Prelude + +import Cat.Displayed.Reasoning +import Cat.Reasoning + +module Cat.Displayed.Cocartesian.Indexing + {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} + (ℰ : Displayed ℬ o′ ℓ′) + (opfibration : Cocartesian-fibration ℰ) + where +``` + + + +# Opreindexing for Cocartesian fibrations + +[opfibrations] are dual to [fibrations], so they inherit the ability +to [reindex along morphisms in the base]. However, this reindexing is +*covariant* for opfibrations, whereas it is *contravariant* for +fibrations. + +[opfibrations]: Cat.Displayed.Cocartesian.html +[fibrations]: Cat.Displayed.Cartesian.html +[reindex along morphisms in the base] Cat.Displayed.Cartesian.Indexing.html + +This gives distinction opfibrations a distinct character. Reindexing in +fibrations can be thought of a sort of restriction map. This can be +seen clearly with [the canonical self-indexing], where the reindexing +functors are given by [pullbacks]. On the other hand, opreindexing +can be thought of as an extension map. We can again use the the canonical +self-indexing as our example: opreindexing is given by postcomposition, +which extends families over $X$ to families over $Y$ by adding in +empty fibres. + +[the canonical self-indexing]: Cat.Displayed.Instances.Slice.html +[pullbacks]: Cat.Diagram.Pullback.html + +Continuing the analogy of indexing as pullback, we call the opreindexing +functors _pushouts_. + +```agda +push-out : ∀ {x y} (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y) +push-out f .F₀ ob = has-lift.y′ f ob +push-out f .F₁ vert = rebase f vert +``` + + diff --git a/src/Cat/Displayed/Instances/Slice.lagda.md b/src/Cat/Displayed/Instances/Slice.lagda.md index 33a31df41..36f53d5f4 100644 --- a/src/Cat/Displayed/Instances/Slice.lagda.md +++ b/src/Cat/Displayed/Instances/Slice.lagda.md @@ -1,5 +1,6 @@ ```agda open import Cat.Displayed.Cartesian +open import Cat.Displayed.Cocartesian open import Cat.Functor.Equivalence open import Cat.Diagram.Pullback open import Cat.Displayed.Fibre @@ -235,3 +236,26 @@ reinterpret the above results as, essentially, giving the [pullback functors] between slice categories. [pullback functors]: Cat.Functor.Pullback.html + +## As an Opfibration + +The canonical self-indexing is *always* an opfibration, where +opreindexing is given by postcomposition. If we think about slices as +families, then opreindexing along $X \to Y$ extends a family over $X$ +to a family over $Y$ by adding in empty fibres for all elements of $Y$ +that do not lie in the image of $f$. + +```agda +Codomain-opfibration : Cocartesian-fibration Slices +Codomain-opfibration .Cocartesian-fibration.has-lift f x′ = lift-f where + + lift-f : Cocartesian-lift Slices f x′ + lift-f .Cocartesian-lift.y′ = cut (f ∘ x′ .map) + lift-f .Cocartesian-lift.lifting = slice-hom id (sym (idr _)) + lift-f .Cocartesian-lift.cocartesian .is-cocartesian.universal m h′ = + slice-hom (h′ .to) (assoc _ _ _ ∙ h′ .commute) + lift-f .Cocartesian-lift.cocartesian .is-cocartesian.commutes m h′ = + Slice-pathp refl (idr _) + lift-f .Cocartesian-lift.cocartesian .is-cocartesian.unique m′ p = + Slice-pathp refl (sym (idr _) ∙ ap to p) +``` From 956c6e0e4094aba7372b47461e54d3ced5a558c6 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 12:24:13 -0800 Subject: [PATCH 07/18] chore: tidy up proof --- src/Cat/Displayed/Cartesian/Indexing.lagda.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md index 36ab13d6b..8911fd4eb 100644 --- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md +++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md @@ -61,17 +61,17 @@ module _ {𝒶 𝒷} (f : Hom 𝒶 𝒷) where ```agda base-change .F-id {x} = sym $ has-lift.uniquev _ _ _ $ to-pathp $ - idr[] ·· sym $ cancel (idl _) _ (idl′ _) ·· reindex _ _ + idr[] ∙ (sym $ cancel _ _ (idl′ _)) base-change .F-∘ {x} {y} {z} f′ g′ = sym $ has-lift.uniquev _ _ _ $ to-pathp $ - smashr _ _ ·· - revive₁ (pulll[] (idr f) (has-lift.commutesv _ _ _)) ·· - smashl _ _ ·· - revive₁ (pullr[] (idr f) (has-lift.commutesv _ _ _)) ·· - smashr _ _ ·· - assoc[] ·· - sym (smashl _ _) + smashr _ _ + ·· revive₁ (pulll[] (idr f) (has-lift.commutesv _ _ _)) + ·· smashl _ _ + ·· revive₁ (pullr[] (idr f) (has-lift.commutesv _ _ _)) + ·· smashr _ _ + ·· assoc[] + ·· sym (smashl _ _) ``` --> From 15c420f7a1995a0e6b6e6f55a1c2f15429eec5f0 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 12:24:27 -0800 Subject: [PATCH 08/18] defn: functors between total op fibres --- src/Cat/Displayed/Total/Op.lagda.md | 51 +++++++++++++++++++++++++++-- 1 file changed, 48 insertions(+), 3 deletions(-) diff --git a/src/Cat/Displayed/Total/Op.lagda.md b/src/Cat/Displayed/Total/Op.lagda.md index 67cab4e75..73c7b9058 100644 --- a/src/Cat/Displayed/Total/Op.lagda.md +++ b/src/Cat/Displayed/Total/Op.lagda.md @@ -1,5 +1,6 @@ ```agda open import Cat.Displayed.Base +open import Cat.Displayed.Fibre open import Cat.Displayed.Total open import Cat.Functor.Equivalence open import Cat.Functor.Equivalence.Path @@ -7,6 +8,8 @@ open import Cat.Prelude open import 1Lab.Rewrite +import Cat.Displayed.Reasoning as DR + module Cat.Displayed.Total.Op where open Functor @@ -18,7 +21,7 @@ open Total-hom 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 $\ca{B}\op$; we call this category the +displayed category over $\ca{B}op$; we call this category the **total opposite** of $\ca{E}$. ```agda @@ -102,8 +105,6 @@ total-op→total-hom-is-equiv 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 @@ -140,3 +141,47 @@ Finally, we show that this extends to an equality of categories. (∫total-op→∫^op ℰ) (∫total-op≅∫^op ℰ) ``` + +# Functors between fibres + +If there is a functor between the fibres of a displayed category $\cE$, +then we also obtain a functor between the fibres of the total opposite +of $\cE$. + +```agda +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 ℰ _ _ +``` + + From 06dd1ccfb992bbbfafba17f738765d84388d4e5f Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 22:18:56 -0800 Subject: [PATCH 09/18] defn: rework how natural hom isos are handled in weak (op)fibrations --- src/Cat/Displayed/Cartesian/Weak.lagda.md | 158 ++++++++++++----- src/Cat/Displayed/Cocartesian/Weak.lagda.md | 183 ++++++++++++++++++-- src/Cat/Functor/Hom.lagda.md | 12 +- src/Cat/Instances/Functor.lagda.md | 79 +++++++-- src/Cat/Instances/Product.lagda.md | 19 +- 5 files changed, 380 insertions(+), 71 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md index f0776f179..11b7212eb 100644 --- a/src/Cat/Displayed/Cartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md @@ -1,10 +1,14 @@ ```agda -{-# OPTIONS --allow-unsolved-metas #-} open import Cat.Displayed.Base open import Cat.Displayed.Fibre +open import Cat.Functor.Hom +open import Cat.Functor.Hom.Displayed +open import Cat.Instances.Functor +open import Cat.Instances.Product open import Cat.Prelude import Cat.Displayed.Cartesian as Cart +import Cat.Displayed.Cartesian.Indexing as Indexing import Cat.Displayed.Reasoning as DR import Cat.Displayed.Morphism as DM import Cat.Reasoning as CR @@ -14,7 +18,10 @@ module Cat.Displayed.Cartesian.Weak {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o′ ℓ′) where +``` + # Weak Cartesian Morphisms @@ -506,31 +514,30 @@ module _ (wfib : is-weak-cartesian-fibration) where weak-fibration→universal-is-equiv f ``` -Furthermore, this equivalence is natural. +Furthermore, this equivalence can be extended into a natural isomorphism +between $\cE_{u}(-,y')$ and $\cE_{x}(-,u^{*}(y'))$. ```agda - weak-fibration→vertical-equiv-naturalr - : ∀ {x y x′ x″ y′} {f : Hom x y} - → (f′ : Hom[ f ] x″ y′) (g′ : Hom[ id ] x′ x″) - → weak-lift.universal f y′ (hom[ idr _ ] (f′ ∘′ g′)) ≡[ sym (idl id) ] - weak-lift.universal f y′ f′ ∘′ g′ - weak-fibration→vertical-equiv-naturalr {f = f} f′ g′ = - to-pathp⁻ $ sym $ weak-lift.unique f _ _ $ to-pathp $ - hom[] (weak-lift.lifting f _ ∘′ hom[] (weak-lift.universal f _ f′ ∘′ g′)) ≡⟨ smashr _ _ ⟩ - hom[] (weak-lift.lifting f _ ∘′ weak-lift.universal f _ f′ ∘′ g′) ≡⟨ weave _ (ap (f ∘_) (idl id)) _ (pulll′ _ (weak-lift.commutes _ _ _)) ⟩ - hom[] (f′ ∘′ g′) ∎ - - weak-fibration→vertical-equiv-naturall - : ∀ {x y x′ y′ y″ } {g : Hom x y} - → (f′ : Hom[ id ] y′ y″) (g′ : Hom[ g ] x′ y′) - → weak-lift.universal g y″ (hom[ idl _ ] (f′ ∘′ g′)) ≡[ sym (idl id) ] - rebase g f′ ∘′ weak-lift.universal g y′ g′ - weak-fibration→vertical-equiv-naturall {g = g} f′ g′ = - to-pathp⁻ $ sym $ weak-lift.unique g _ _ $ to-pathp $ - smashr _ _ - ∙ revive₁ (pulll[] _ (weak-lift.commutes g _ _)) - ∙ smashl _ _ - ∙ weave _ (pullr (idr g)) _ (pullr[] _ (weak-lift.commutes g _ _)) + weak-fibration→hom-iso-into + : ∀ {x y y′} (u : Hom x y) + → natural-iso (Hom-over-into ℰ u y′) (Hom-into (Fibre ℰ x) (weak-lift.x′ u y′)) + weak-fibration→hom-iso-into {x} {y} {y′} u = to-natural-iso mi where + open make-natural-iso + + u*y′ : Ob[ x ] + u*y′ = weak-lift.x′ u y′ + + mi : make-natural-iso (Hom-over-into ℰ u y′) (Hom-into (Fibre ℰ x) u*y′) + mi .eta x u′ = weak-lift.universal u y′ u′ + mi .inv x v′ = hom[ idr u ] (weak-lift.lifting u y′ ∘′ v′) + mi .eta∘inv x = funext λ v′ → + sym $ weak-lift.unique u _ _ (to-pathp refl) + mi .inv∘eta x = funext λ u′ → + from-pathp (weak-lift.commutes u _ _) + mi .natural x y v′ = funext λ u′ → + weak-lift.unique u _ _ $ to-pathp $ + smashr _ _ + ∙ weave _ (ap (u ∘_) (idl id)) _ (pulll′ _ (weak-lift.commutes _ _ _)) ``` An *extremely* useful fact is that the converse is true: if there is some @@ -617,17 +624,67 @@ the equivalence is natural. to* g′ ∎ ``` + + + Note that this result does *not* extend to fibrations; the equivalence of homs can only get us weak cartesian lifts. To make the final step to a fibration, we need to use other means. -However, we still get the nice equivalence of hom sets if $\cE$ is a -fibration. +However, we do obtain a natural isomorphism between $\cE_{u}(x',-)$ and +$cE_{y}(x',u^{*}(-))$. ```agda module _ (fib : Cartesian-fibration) where open Cartesian-fibration fib + open Indexing ℰ fib + + fibration→hom-iso-from + : ∀ {x y x′} (u : Hom x y) + → natural-iso + (Hom-over-from ℰ u x′) + (Hom-from (Fibre ℰ x) x′ F∘ base-change u) + fibration→hom-iso-from {x} {y} {x′} u = to-natural-iso mi where + open make-natural-iso + + mi : make-natural-iso + (Hom-over-from ℰ u x′) + (Hom-from (Fibre ℰ x) x′ F∘ base-change u) + mi .eta x u′ = has-lift.universalv u x u′ + mi .inv x v′ = hom[ idr u ] (has-lift.lifting u x ∘′ v′) + mi .eta∘inv x = funext λ v′ → + sym $ has-lift.uniquev u _ _ (to-pathp refl) + mi .inv∘eta x = funext λ u′ → + from-pathp (has-lift.commutesv u _ _) + mi .natural _ _ v′ = funext λ u′ → + has-lift.unique u _ _ $ to-pathp $ + smashr _ _ + ·· revive₁ (pulll[] _ (has-lift.commutesv u _ _)) + ·· smashl _ _ + ·· weave _ (pullr (idr u)) _ (pullr[] _ (has-lift.commutesv u _ _)) + ·· duplicate id-comm-sym _ (idl u) +``` + +If we combine this with `weak-fibration→hom-iso-into`{.Agda}, we obtain +a natural iso between $\cE_{u}(-,-)$ and $\cE_{id}(-,u^{*}(-))$. + +```agda + fibration→hom-iso + : ∀ {x y} (u : Hom x y) + → natural-iso (Hom-over ℰ u) (Hom[-,-] (Fibre ℰ x) F∘ (Id F× base-change u)) + fibration→hom-iso {x = x} u = to-natural-iso mi where + open make-natural-iso + open _=>_ + + module into-iso {y′} = natural-iso (fibration→hom-iso-into {y′ = y′} u) + module from-iso {x′} = natural-iso (fibration→hom-iso-from {x′ = x′} u) + + mi : make-natural-iso (Hom-over ℰ u) (Hom[-,-] (Fibre ℰ x) F∘ (Id F× base-change u)) + mi .eta x u′ = has-lift.universalv u _ u′ + mi .inv x v′ = hom[ idr u ] (has-lift.lifting u _ ∘′ v′) + mi .eta∘inv x = funext λ v′ → + sym $ has-lift.uniquev u _ _ (to-pathp refl) + mi .inv∘eta x = funext λ u′ → + from-pathp (has-lift.commutesv u _ _) + mi .natural _ _ (v₁′ , v₂′) = funext λ u′ → + sym (apr′ (happly (into-iso.to .is-natural _ _ v₁′) u′)) + ·· sym (happly (from-iso.to .is-natural _ _ v₂′) (hom[ idr _ ] (u′ ∘′ v₁′))) + ·· ap (into-iso.to .η _) (smashr _ _ ∙ reindex _ _ ) +``` diff --git a/src/Cat/Displayed/Cocartesian/Weak.lagda.md b/src/Cat/Displayed/Cocartesian/Weak.lagda.md index 915281388..526ac1f92 100644 --- a/src/Cat/Displayed/Cocartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cocartesian/Weak.lagda.md @@ -4,12 +4,18 @@ open import Cat.Displayed.Cartesian open import Cat.Displayed.Cartesian.Weak open import Cat.Displayed.Fibre open import Cat.Displayed.Total.Op +open import Cat.Functor.Hom +open import Cat.Functor.Hom.Displayed +open import Cat.Instances.Functor +open import Cat.Instances.Product open import Cat.Prelude import Cat.Displayed.Cocartesian as Cocart +import Cat.Displayed.Cocartesian.Indexing as Indexing import Cat.Displayed.Morphism import Cat.Displayed.Morphism.Duality import Cat.Displayed.Reasoning +import Cat.Reasoning as CR module Cat.Displayed.Cocartesian.Weak {o ℓ o′ ℓ′} @@ -20,7 +26,7 @@ module Cat.Displayed.Cocartesian.Weak + Weak opfibrations are dual to [weak fibrations]. ```agda weak-op-fibration→weak-opfibration @@ -476,6 +493,35 @@ weak-opfibration→weak-op-fibration wlift .is-weak-cartesian-fibration.weak-lif ``` +Every opfibration is a weak opfibration. + +```agda +cocartesian-lift→weak-cocartesian-lift + : ∀ {x y} {f : Hom x y} {x′ : Ob[ x ]} + → Cocartesian-lift f x′ + → Weak-cocartesian-lift f x′ + +opfibration→weak-opfibration + : Cocartesian-fibration + → is-weak-cocartesian-fibration +``` + + + + + A weak opfibration is an opfibration when weak cocartesian morphisms are closed under composition. This follows via duality. @@ -526,11 +572,10 @@ module _ (wopfib : is-weak-cocartesian-fibration) where open is-weak-cocartesian-fibration wopfib weak-opfibration→universal-is-equiv - : ∀ {x y y′} + : ∀ {x y y′ x′} → (u : Hom x y) - → (x′ : Ob[ x ]) → is-equiv (weak-lift.universal u x′ {y′}) - weak-opfibration→universal-is-equiv u x′ = + weak-opfibration→universal-is-equiv {x′ = x′} u = is-iso→is-equiv $ iso (λ u′ → hom[ idl u ] (u′ ∘′ weak-lift.lifting u x′)) (λ u′ → sym $ weak-lift.unique u x′ u′ (to-pathp refl)) @@ -541,22 +586,32 @@ module _ (wopfib : is-weak-cocartesian-fibration) where → (u : Hom x y) → Hom[ u ] x′ y′ ≃ Hom[ id ] (weak-lift.y′ u x′) y′ weak-opfibration→vertical-equiv {x′ = x′} u = - weak-lift.universal u x′ , weak-opfibration→universal-is-equiv u x′ + weak-lift.universal u x′ , weak-opfibration→universal-is-equiv u ``` Furthermore, this equivalence is natural. ```agda - weak-opfibration→vertical-equiv-natural - : ∀ {x y x′ y′ y″} {g : Hom x y} - → (f′ : Hom[ id ] y′ y″) (g′ : Hom[ g ] x′ y′) - → weak-lift.universal g x′ (hom[ idl g ] (f′ ∘′ g′)) ≡[ sym (idl id) ] - f′ ∘′ weak-lift.universal g x′ g′ - weak-opfibration→vertical-equiv-natural {g = g} f′ g′ = - to-pathp⁻ $ sym $ weak-lift.unique _ _ _ $ to-pathp $ - hom[] (hom[] (f′ ∘′ weak-lift.universal _ _ g′) ∘′ weak-lift.lifting g _) ≡⟨ smashl _ _ ⟩ - hom[] ((f′ ∘′ weak-lift.universal _ _ g′) ∘′ weak-lift.lifting g _) ≡⟨ weave _ (ap (_∘ g) (idl id)) _ (pullr′ _ (weak-lift.commutes _ _ _)) ⟩ - hom[] (f′ ∘′ g′) ∎ + weak-opfibration→hom-iso-from + : ∀ {x y x′} (u : Hom x y) + → natural-iso (Hom-over-from ℰ u x′) (Hom-from (Fibre ℰ y) (weak-lift.y′ u x′)) + weak-opfibration→hom-iso-from {y = y} {x′ = x′} u = to-natural-iso mi where + open make-natural-iso + + u*x′ : Ob[ y ] + u*x′ = weak-lift.y′ u x′ + + mi : make-natural-iso (Hom-over-from ℰ u x′) (Hom-from (Fibre ℰ y) u*x′) + mi .eta x u′ = weak-lift.universal u x′ u′ + mi .inv x v′ = hom[ idl u ] (v′ ∘′ weak-lift.lifting u x′) + mi .eta∘inv _ = funext λ v′ → + sym $ weak-lift.unique u _ _ (to-pathp refl) + mi .inv∘eta _ = funext λ u′ → + from-pathp $ weak-lift.commutes u _ _ + mi .natural _ _ v′ = funext λ u′ → + weak-lift.unique _ _ _ $ to-pathp $ + smashl _ _ + ∙ weave _ (ap (_∘ u) (idl id)) _ (pullr′ _ (weak-lift.commutes _ _ _)) ``` As in the [weak cartesian case], the converse is also true: if there is @@ -589,3 +644,101 @@ module _ (_*₀_ : ∀ {x y} → Hom x y → Ob[ x ] → Ob[ y ]) where to-pathp (reindex _ _ ∙ from-pathp (natural g′ f′)) ``` + + + diff --git a/src/Cat/Functor/Hom.lagda.md b/src/Cat/Functor/Hom.lagda.md index 62b699314..1eac6bb12 100644 --- a/src/Cat/Functor/Hom.lagda.md +++ b/src/Cat/Functor/Hom.lagda.md @@ -49,7 +49,6 @@ Hom[ x ,-] .F-id = funext (λ f → idl f) Hom[ x ,-] .F-∘ f g = funext λ h → sym (assoc f g h) ``` - ## The Yoneda embedding Abstractly and nonsensically, one could say that the Yoneda embedding @@ -90,6 +89,17 @@ Hom[-,_] : Ob → Functor (C ^op) (Sets h) Hom[-,_] x = よ₀ x ``` + + + The morphism part takes a map $f$ to the transformation given by postcomposition; This is natural because we must show $f \circ x \circ g = (f \circ x) \circ g$, which is given by associativity in $C$. diff --git a/src/Cat/Instances/Functor.lagda.md b/src/Cat/Instances/Functor.lagda.md index b3e04765e..d9c6d29b2 100644 --- a/src/Cat/Instances/Functor.lagda.md +++ b/src/Cat/Instances/Functor.lagda.md @@ -37,27 +37,35 @@ $\eta$ and $\theta$. ```agda _∘nt_ : {F G H : Functor C D} → G => H → F => G → F => H -_∘nt_ {C = C} {D = D} {F} {G} {H} f g = nat where - module D = Cat.Reasoning D +_∘nt_ {C = C} {D = D} {F} {G} {H} f g = nat + module ∘nt where + module D = Cat.Reasoning D - nat : F => H - nat .η x = f .η _ D.∘ g .η _ + nat : F => H + nat .η x = f .η _ D.∘ g .η _ ``` + + + We can then show that these definitions assemble into a category where the objects are functors $F, G : C \to D$, and the morphisms are natural transformations $F \To G$. This is because natural @@ -434,6 +442,19 @@ module module D = Cat.Reasoning D module C = Cat.Reasoning C + natural-iso : (F G : Functor C D) → Type _ + natural-iso F G = F CD.≅ G + + module natural-iso {F G : Functor C D} (eta : F CD.≅ G) = CD._≅_ eta + + _ni∘_ : ∀ {F G H : Functor C D} + → natural-iso F G → natural-iso G H + → natural-iso F H + _ni∘_ = CD._∘Iso_ + + _ni⁻¹ : ∀ {F G : Functor C D} → natural-iso F G → natural-iso G F + _ni⁻¹ = CD._Iso⁻¹ + F∘-iso-id-l : {F : Functor D D} {G : Functor C D} → F DD.≅ Id → (F F∘ G) CD.≅ G @@ -509,5 +530,37 @@ module _ (λ i j → G .F₀ (cd.iso→path-id {A = G′} i j .F₀ x)) ∙ transport-refl _ ∙ sym (G .F-id) where module cd = Univalent cdcat + +module _ {o ℓ κ} {C : Precategory o ℓ} where + open Functor + open _=>_ + + natural-iso-to-is-equiv + : {F G : Functor C (Sets κ)} + → (eta : natural-iso F G) + → ∀ x → is-equiv (natural-iso.to eta .η x) + natural-iso-to-is-equiv eta x = + is-iso→is-equiv $ + iso (natural-iso.from eta .η x) + (λ x i → natural-iso.invl eta i .η _ x) + (λ x i → natural-iso.invr eta i .η _ x) + + natural-iso-from-is-equiv + : {F G : Functor C (Sets κ)} + → (eta : natural-iso F G) + → ∀ x → is-equiv (natural-iso.from eta .η x) + natural-iso-from-is-equiv eta x = + is-iso→is-equiv $ + iso (natural-iso.to eta .η x) + (λ x i → natural-iso.invr eta i .η _ x) + (λ x i → natural-iso.invl eta i .η _ x) + + natural-iso→equiv + : {F G : Functor C (Sets κ)} + → (eta : natural-iso F G) + → ∀ x → ∣ F .F₀ x ∣ ≃ ∣ G .F₀ x ∣ + natural-iso→equiv eta x = + natural-iso.to eta .η x , + natural-iso-to-is-equiv eta x ``` --> diff --git a/src/Cat/Instances/Product.lagda.md b/src/Cat/Instances/Product.lagda.md index 6676ea7f5..c7ef5680e 100644 --- a/src/Cat/Instances/Product.lagda.md +++ b/src/Cat/Instances/Product.lagda.md @@ -14,7 +14,7 @@ open Precategory open Functor private variable o₁ h₁ o₂ h₂ : Level - C D E : Precategory o₁ h₁ + B C D E : Precategory o₁ h₁ ``` --> @@ -101,7 +101,24 @@ Cat⟨ F , G ⟩ = f where f .F₁ f = F₁ F f , F₁ G f f .F-id i = F-id F i , F-id G i f .F-∘ f g i = F-∘ F f g i , F-∘ G f g i + +_F×_ : Functor B D → Functor C E → Functor (B ×ᶜ C) (D ×ᶜ E) +_F×_ {B = B} {D = D} {C = C} {E = E} G H = func + module F× where + + func : Functor (B ×ᶜ C) (D ×ᶜ E) + func .F₀ (x , y) = (G .F₀ x) , (H .F₀ y) + func .F₁ (f , g) = (G .F₁ f) , (H .F₁ g) + func .F-id = (G .F-id) ,ₚ (H .F-id) + func .F-∘ (f , g) (f' , g') = (G .F-∘ f f') ,ₚ H .F-∘ g g' +``` + + + ## Univalence From 796d991972a9ee39e6da1acb2e6f001abd39c073 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 22:20:02 -0800 Subject: [PATCH 10/18] defn: natural isos + adjoints --- src/Cat/Functor/Adjoint/Hom.lagda.md | 205 ++++++++++++++++++--------- 1 file changed, 140 insertions(+), 65 deletions(-) diff --git a/src/Cat/Functor/Adjoint/Hom.lagda.md b/src/Cat/Functor/Adjoint/Hom.lagda.md index a22ccc9f4..d791bdfbd 100644 --- a/src/Cat/Functor/Adjoint/Hom.lagda.md +++ b/src/Cat/Functor/Adjoint/Hom.lagda.md @@ -6,26 +6,30 @@ description: | --- ```agda open import Cat.Functor.Adjoint +open import Cat.Functor.Hom +open import Cat.Instances.Functor +open import Cat.Instances.Product open import Cat.Prelude import Cat.Functor.Reasoning as Func import Cat.Reasoning as Cat -module Cat.Functor.Adjoint.Hom - {o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′} - {L : Functor D C} {R : Functor C D} - where +module Cat.Functor.Adjoint.Hom where + +module _ {o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′} + {L : Functor D C} {R : Functor C D} + where ``` @@ -59,31 +63,31 @@ $\hom_\cD(-,R-)$ whose data has been "unfolded" into elementary terms. ```agda -hom-iso-natural - : (∀ {x y} → C.Hom (L.₀ x) y → D.Hom x (R.₀ y)) - → Type _ -hom-iso-natural f = - ∀ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x - → f (g C.∘ x C.∘ L.₁ h) ≡ R.₁ g D.∘ f x D.∘ h - -hom-iso→adjoints - : (f : ∀ {x y} → C.Hom (L.₀ x) y → D.Hom x (R.₀ y)) - → (eqv : ∀ {x y} → is-equiv (f {x} {y})) - → hom-iso-natural f - → L ⊣ R -hom-iso→adjoints f f-equiv natural = adj′ where - f⁻¹ : ∀ {x y} → D.Hom x (R.₀ y) → C.Hom (L.₀ x) y - f⁻¹ = equiv→inverse f-equiv - - inv-natural : ∀ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x - → f⁻¹ (R.₁ g D.∘ x D.∘ h) ≡ g C.∘ f⁻¹ x C.∘ L.₁ h - inv-natural g h x = ap fst $ is-contr→is-prop (f-equiv .is-eqv _) - (f⁻¹ (R.₁ g D.∘ x D.∘ h) , refl) - ( g C.∘ f⁻¹ x C.∘ L.₁ h - , natural _ _ _ - ∙ sym (equiv→counit f-equiv _) - ∙ ap (f ⊙ f⁻¹) - (D.extendl (ap (R.₁ g D.∘_) (equiv→counit f-equiv _)))) + hom-iso-natural + : (∀ {x y} → C.Hom (L.₀ x) y → D.Hom x (R.₀ y)) + → Type _ + hom-iso-natural f = + ∀ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x + → f (g C.∘ x C.∘ L.₁ h) ≡ R.₁ g D.∘ f x D.∘ h + + hom-iso→adjoints + : (f : ∀ {x y} → C.Hom (L.₀ x) y → D.Hom x (R.₀ y)) + → (eqv : ∀ {x y} → is-equiv (f {x} {y})) + → hom-iso-natural f + → L ⊣ R + hom-iso→adjoints f f-equiv natural = adj′ where + f⁻¹ : ∀ {x y} → D.Hom x (R.₀ y) → C.Hom (L.₀ x) y + f⁻¹ = equiv→inverse f-equiv + + inv-natural : ∀ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x + → f⁻¹ (R.₁ g D.∘ x D.∘ h) ≡ g C.∘ f⁻¹ x C.∘ L.₁ h + inv-natural g h x = ap fst $ is-contr→is-prop (f-equiv .is-eqv _) + (f⁻¹ (R.₁ g D.∘ x D.∘ h) , refl) + ( g C.∘ f⁻¹ x C.∘ L.₁ h + , natural _ _ _ + ∙ sym (equiv→counit f-equiv _) + ∙ ap (f ⊙ f⁻¹) + (D.extendl (ap (R.₁ g D.∘_) (equiv→counit f-equiv _)))) ``` We do not require an explicit naturality witness for the inverse of $f$, @@ -93,32 +97,103 @@ compute that $f(\id)$ and $f^{-1}(\id)$ do indeed give a system of adjunction units and co-units. ```agda - adj′ : L ⊣ R - adj′ .unit .η x = f C.id - adj′ .unit .is-natural x y h = - f C.id D.∘ h ≡⟨ D.introl R.F-id ⟩ - R.₁ C.id D.∘ f C.id D.∘ h ≡˘⟨ natural _ _ _ ⟩ - f (C.id C.∘ C.id C.∘ L.₁ h) ≡⟨ ap f (C.cancell (C.idl _) ∙ C.intror (C.idl _ ∙ L.F-id)) ⟩ - f (L.₁ h C.∘ C.id C.∘ L.₁ D.id) ≡⟨ natural _ _ C.id ⟩ - R.₁ (L.₁ h) D.∘ f C.id D.∘ D.id ≡⟨ D.refl⟩∘⟨ D.idr _ ⟩ - R.₁ (L.₁ h) D.∘ f C.id ∎ - adj′ .counit .η x = f⁻¹ D.id - adj′ .counit .is-natural x y f = - f⁻¹ D.id C.∘ L.₁ (R.₁ f) ≡⟨ C.introl refl ⟩ - C.id C.∘ f⁻¹ D.id C.∘ L.₁ (R.₁ f) ≡˘⟨ inv-natural _ _ _ ⟩ - f⁻¹ (R.₁ C.id D.∘ D.id D.∘ R.₁ f) ≡⟨ ap f⁻¹ (D.cancell (D.idr _ ∙ R.F-id) ∙ D.intror (D.idl _)) ⟩ - f⁻¹ (R.₁ f D.∘ D.id D.∘ D.id) ≡⟨ inv-natural _ _ _ ⟩ - f C.∘ f⁻¹ D.id C.∘ L.₁ D.id ≡⟨ C.refl⟩∘⟨ C.elimr L.F-id ⟩ - f C.∘ f⁻¹ D.id ∎ - adj′ .zig = - f⁻¹ D.id C.∘ L.₁ (f C.id) ≡⟨ C.introl refl ⟩ - C.id C.∘ f⁻¹ D.id C.∘ L.₁ (f C.id) ≡˘⟨ inv-natural _ _ _ ⟩ - f⁻¹ (R.₁ C.id D.∘ D.id D.∘ f C.id) ≡⟨ ap f⁻¹ (D.cancell (D.idr _ ∙ R.F-id)) ⟩ - f⁻¹ (f C.id) ≡⟨ equiv→unit f-equiv _ ⟩ - C.id ∎ - adj′ .zag = - R.₁ (f⁻¹ D.id) D.∘ f C.id ≡⟨ D.refl⟩∘⟨ D.intror refl ⟩ - R.₁ (f⁻¹ D.id) D.∘ f C.id D.∘ D.id ≡˘⟨ natural _ _ _ ⟩ - f (f⁻¹ D.id C.∘ C.id C.∘ L.₁ D.id) ≡⟨ ap f (C.elimr (C.idl _ ∙ L.F-id)) ⟩ - f (f⁻¹ D.id) ≡⟨ equiv→counit f-equiv _ ⟩ - D.id ∎ + adj′ : L ⊣ R + adj′ .unit .η x = f C.id + adj′ .unit .is-natural x y h = + f C.id D.∘ h ≡⟨ D.introl R.F-id ⟩ + R.₁ C.id D.∘ f C.id D.∘ h ≡˘⟨ natural _ _ _ ⟩ + f (C.id C.∘ C.id C.∘ L.₁ h) ≡⟨ ap f (C.cancell (C.idl _) ∙ C.intror (C.idl _ ∙ L.F-id)) ⟩ + f (L.₁ h C.∘ C.id C.∘ L.₁ D.id) ≡⟨ natural _ _ C.id ⟩ + R.₁ (L.₁ h) D.∘ f C.id D.∘ D.id ≡⟨ D.refl⟩∘⟨ D.idr _ ⟩ + R.₁ (L.₁ h) D.∘ f C.id ∎ + adj′ .counit .η x = f⁻¹ D.id + adj′ .counit .is-natural x y f = + f⁻¹ D.id C.∘ L.₁ (R.₁ f) ≡⟨ C.introl refl ⟩ + C.id C.∘ f⁻¹ D.id C.∘ L.₁ (R.₁ f) ≡˘⟨ inv-natural _ _ _ ⟩ + f⁻¹ (R.₁ C.id D.∘ D.id D.∘ R.₁ f) ≡⟨ ap f⁻¹ (D.cancell (D.idr _ ∙ R.F-id) ∙ D.intror (D.idl _)) ⟩ + f⁻¹ (R.₁ f D.∘ D.id D.∘ D.id) ≡⟨ inv-natural _ _ _ ⟩ + f C.∘ f⁻¹ D.id C.∘ L.₁ D.id ≡⟨ C.refl⟩∘⟨ C.elimr L.F-id ⟩ + f C.∘ f⁻¹ D.id ∎ + adj′ .zig = + f⁻¹ D.id C.∘ L.₁ (f C.id) ≡⟨ C.introl refl ⟩ + C.id C.∘ f⁻¹ D.id C.∘ L.₁ (f C.id) ≡˘⟨ inv-natural _ _ _ ⟩ + f⁻¹ (R.₁ C.id D.∘ D.id D.∘ f C.id) ≡⟨ ap f⁻¹ (D.cancell (D.idr _ ∙ R.F-id)) ⟩ + f⁻¹ (f C.id) ≡⟨ equiv→unit f-equiv _ ⟩ + C.id ∎ + adj′ .zag = + R.₁ (f⁻¹ D.id) D.∘ f C.id ≡⟨ D.refl⟩∘⟨ D.intror refl ⟩ + R.₁ (f⁻¹ D.id) D.∘ f C.id D.∘ D.id ≡˘⟨ natural _ _ _ ⟩ + f (f⁻¹ D.id C.∘ C.id C.∘ L.₁ D.id) ≡⟨ ap f (C.elimr (C.idl _ ∙ L.F-id)) ⟩ + f (f⁻¹ D.id) ≡⟨ equiv→counit f-equiv _ ⟩ + D.id ∎ +``` + + From 32a05262f07e4e7ff9fab0489eac9b4a01239091 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 22:20:27 -0800 Subject: [PATCH 11/18] defn: bifibrations --- src/Cat/Displayed/Bifibration.lagda.md | 130 +++++++++++++++++++++++++ 1 file changed, 130 insertions(+) create mode 100644 src/Cat/Displayed/Bifibration.lagda.md diff --git a/src/Cat/Displayed/Bifibration.lagda.md b/src/Cat/Displayed/Bifibration.lagda.md new file mode 100644 index 000000000..53050224d --- /dev/null +++ b/src/Cat/Displayed/Bifibration.lagda.md @@ -0,0 +1,130 @@ +```agda +open import Cat.Displayed.Base +open import Cat.Displayed.Fibre +open import Cat.Functor.Adjoint +open import Cat.Functor.Adjoint.Hom +open import Cat.Instances.Functor +open import Cat.Prelude + +import Cat.Displayed.Cartesian.Indexing +import Cat.Displayed.Cocartesian.Indexing +import Cat.Displayed.Cocartesian +import Cat.Displayed.Cocartesian.Weak +import Cat.Displayed.Cartesian +import Cat.Displayed.Cartesian.Weak +import Cat.Displayed.Reasoning +import Cat.Reasoning + +module Cat.Displayed.Bifibration + {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o′ ℓ′) where +``` + + + + +# Bifibrations + +A displayed category $\cE$ is a **bifibration** if it both a fibration +and an opfibration. This means that $\cE$ is equipped with both +[reindexing] and [opreindexing] functors, which allows us to both +restrict and extend along morphisms $X \to Y$ in the base. + +Note that a bifibration is *not* the same as a "profunctor of categories"; +these are called **two-sided fibrations**, and are a distinct concept. + +[reindexing]: Cat.Displayed.Cartesian.Indexing.html +[opreindexing]: Cat.Displayed.Cocartesian.Indexing.html + + + + +```agda +record is-bifibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where + field + fibration : Cartesian-fibration + opfibration : Cocartesian-fibration + + module fibration = Cartesian-fibration fibration + module opfibration = Cocartesian-fibration opfibration +``` + +# Bifibrations and Adjoints + +If $\cE$ is a bifibration, then opreindexing functors are [left adjoint] +to reindexing functors. To see this, note that we need to construct +a natural isomorphism between $\cE_{y}(u_{*}(-),-)$ and +$\cE_{x}(-,u^{*}(-))$. However, we have already shown that +$\cE_{y}(u_{*}(-),-)$ and $\cE_{x}(-,u^{*}(-))$ are both naturally +isomorphic to $\cE_{u}(-,-)$ (see `opfibration→hom-iso`{.Agda} and +`fibration→hom-iso`{.Agda}), so all we need to do is compose these +natural isomorphisms! + +```agda +module _ (bifib : is-bifibration) where + open is-bifibration bifib + open Cat.Displayed.Cartesian.Indexing ℰ fibration + open Cat.Displayed.Cocartesian.Indexing ℰ opfibration + + push-out⊣base-change + : ∀ {x y} (f : Hom x y) + → push-out f ⊣ base-change f + push-out⊣base-change {x} {y} f = + hom-natural-iso→adjoints $ + (opfibration→hom-iso opfibration f ni⁻¹) ni∘ fibration→hom-iso fibration f +``` + +In fact, if $\cE$ is a cartesian fibration where every reindexing +functor has a left adjoint, then $\cE$ is in fact a bifibration! +To see this, note that we have a natural iso +$\cE_{u}(x',-) \simeq \cE_{x}(x', u^{*}(-))$ for every $u : x \to y$ in +the base. However, $u^{*}$ has a left adjoint $L_{u}$ for every $u$, +so we also have a natural isomorphism +$\cE_{x}(x', u^{*}(-)) \simeq \cE_{y}(L_{u}(x'),-)$. Composing these +yields a natural iso $\cE_{u}(x',-) \simeq \cE_{y}(L_{u}(x'),-)$, which +implies that $\cE$ is a weak opfibration due to +`hom-iso→weak-opfibration`{.Agda}. + +Furthermore, $\cE$ is a fibration, which allows us to upgrade the +weak opfibration to an opfibration! + +```agda +module _ (fib : Cartesian-fibration) where + open Cartesian-fibration fib + open Cat.Displayed.Cartesian.Indexing ℰ fib + + left-adjoint-reindexing→opfibration + : (L : ∀ {x y} → (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y)) + → (∀ {x y} → (f : Hom x y) → (L f ⊣ base-change f)) + → Cocartesian-fibration + left-adjoint-reindexing→opfibration L adj = + cartesian+weak-opfibration→opfibration fib $ + hom-iso→weak-opfibration L λ u → + fibration→hom-iso-from fib u ni∘ (adjunct-hom-iso-from (adj u) _ ni⁻¹) +``` + +With some repackaging, we can see that this yields a bifibration. + +```agda + left-adjoint-reindexing→bifibration + : (L : ∀ {x y} → (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y)) + → (∀ {x y} → (f : Hom x y) → (L f ⊣ base-change f)) + → is-bifibration + left-adjoint-reindexing→bifibration L adj .is-bifibration.fibration = + fib + left-adjoint-reindexing→bifibration L adj .is-bifibration.opfibration = + left-adjoint-reindexing→opfibration L adj +``` From d28bbab72903594e2221c3f820946d90be44f6a6 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 22:22:36 -0800 Subject: [PATCH 12/18] defn: displayed hom functor --- src/Cat/Functor/Hom/Displayed.lagda.md | 64 ++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) create mode 100644 src/Cat/Functor/Hom/Displayed.lagda.md diff --git a/src/Cat/Functor/Hom/Displayed.lagda.md b/src/Cat/Functor/Hom/Displayed.lagda.md new file mode 100644 index 000000000..bb24611b0 --- /dev/null +++ b/src/Cat/Functor/Hom/Displayed.lagda.md @@ -0,0 +1,64 @@ +```agda +open import Cat.Displayed.Base +open import Cat.Displayed.Fibre +open import Cat.Displayed.Total +open import Cat.Displayed.Solver +open import Cat.Instances.Product +open import Cat.Prelude + +import Cat.Displayed.Reasoning + +module Cat.Functor.Hom.Displayed + {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o′ ℓ′) + where +``` + + + +# Displayed Hom Functors + +Let $\cE$ be a displayed category over $\cB$. For every $u : x \to y$ +in the base, we have obtain a bifunctor from $\cE_{x}\op \times \cE_{y}$ +to $\Sets$, where $\cE_{x}$ denotes the [fibre category] of $\cE$ at $x$. +The action of $(f, h)$ on $g$ is given by $h \circ g \circ f$, just as +in the [non-displayed case]. + +[bifunctor]: Cat.Functor.Bifunctor.html +[fibre category]: Cat.Displayed.Fibre.html +[non-displayed case]: Cat.Functor.Hom.html + +```agda +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. + +```agda +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 _ _ ) +``` From efffcddfd3af2c6edbf03a698f567f51adf8c2d8 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 23:26:56 -0800 Subject: [PATCH 13/18] fix: wording --- src/Cat/Displayed/Bifibration.lagda.md | 4 +++- src/Cat/Displayed/Cartesian/Weak.lagda.md | 2 +- src/Cat/Displayed/Cocartesian/Weak.lagda.md | 2 +- src/Cat/Functor/Hom/Displayed.lagda.md | 2 +- 4 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Cat/Displayed/Bifibration.lagda.md b/src/Cat/Displayed/Bifibration.lagda.md index 53050224d..228f56f5e 100644 --- a/src/Cat/Displayed/Bifibration.lagda.md +++ b/src/Cat/Displayed/Bifibration.lagda.md @@ -73,6 +73,8 @@ isomorphic to $\cE_{u}(-,-)$ (see `opfibration→hom-iso`{.Agda} and `fibration→hom-iso`{.Agda}), so all we need to do is compose these natural isomorphisms! +[left adjoint]: Cat.Functor.Adjoint.html + ```agda module _ (bifib : is-bifibration) where open is-bifibration bifib @@ -88,7 +90,7 @@ module _ (bifib : is-bifibration) where ``` In fact, if $\cE$ is a cartesian fibration where every reindexing -functor has a left adjoint, then $\cE$ is in fact a bifibration! +functor has a left adjoint, then $\cE$ is a bifibration! To see this, note that we have a natural iso $\cE_{u}(x',-) \simeq \cE_{x}(x', u^{*}(-))$ for every $u : x \to y$ in the base. However, $u^{*}$ has a left adjoint $L_{u}$ for every $u$, diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md index 11b7212eb..ed3a092f4 100644 --- a/src/Cat/Displayed/Cartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md @@ -550,7 +550,7 @@ already have a suite of tools for constructing natural equivalences of hom sets! Most notably, this allows us to use the theory of [adjuncts] to construct weak fibrations. -[adjuncts]: Cat.Functor.Adjoint#adjuncts +[adjuncts]: Cat.Functor.Adjoint.html#adjuncts ```agda module _ (_*₀_ : ∀ {x y} → Hom x y → Ob[ y ] → Ob[ x ]) where diff --git a/src/Cat/Displayed/Cocartesian/Weak.lagda.md b/src/Cat/Displayed/Cocartesian/Weak.lagda.md index 526ac1f92..ebfda8e26 100644 --- a/src/Cat/Displayed/Cocartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cocartesian/Weak.lagda.md @@ -619,7 +619,7 @@ a lifting of objects `Ob[ x ] → Ob[ y ]` for every morphism $f : x \to y$ in $\cB$, along with a equivalence of homs as above, then $\cE$ is a weak opfibration. -[weak cartesian case]: Cat.Cartesian.Weak.html#weak-fibrations-and-equivalence-of-hom-sets +[weak cartesian case]: Cat.Displayed.Cartesian.Weak.html#weak-fibrations-and-equivalence-of-hom-sets ```agda module _ (_*₀_ : ∀ {x y} → Hom x y → Ob[ x ] → Ob[ y ]) where diff --git a/src/Cat/Functor/Hom/Displayed.lagda.md b/src/Cat/Functor/Hom/Displayed.lagda.md index bb24611b0..ec2029d50 100644 --- a/src/Cat/Functor/Hom/Displayed.lagda.md +++ b/src/Cat/Functor/Hom/Displayed.lagda.md @@ -25,7 +25,7 @@ open Functor # Displayed Hom Functors Let $\cE$ be a displayed category over $\cB$. For every $u : x \to y$ -in the base, we have obtain a bifunctor from $\cE_{x}\op \times \cE_{y}$ +in the base, we can obtain a bifunctor from $\cE_{x}\op \times \cE_{y}$ to $\Sets$, where $\cE_{x}$ denotes the [fibre category] of $\cE$ at $x$. The action of $(f, h)$ on $g$ is given by $h \circ g \circ f$, just as in the [non-displayed case]. From 263e049992701bfc062c1f53cc21f2cb6460280d Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 31 Jan 2023 23:28:20 -0800 Subject: [PATCH 14/18] chore: update index --- src/index.lagda.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/index.lagda.md b/src/index.lagda.md index 86dda469f..bbdc2a361 100644 --- a/src/index.lagda.md +++ b/src/index.lagda.md @@ -446,6 +446,9 @@ lemma: open import Cat.Functor.Hom -- Hom functor, Yoneda embedding, Coyoneda lemma open import Cat.Functor.Hom.Cocompletion -- Universal property of PSh(C) open import Cat.Functor.Hom.Representable -- Representable functors + +open import Cat.Functor.Hom.Displayed + -- Hom functors of displayed categories ``` ## Univalent categories @@ -675,10 +678,21 @@ open import Cat.Displayed.Instances.Scone open import Cat.Displayed.Cocartesian -- Cocartesian lifts, opfibrations +open import Cat.Displayed.Cocartesian.Indexing + -- Opfibrations have covariant opreindexing + open import Cat.Displayed.Cocartesian.Weak -- Weak cocartesian morphisms ``` +### Bifibrations + +```agda +open import Cat.Displayed.Bifibration + -- Bifibrations, adjoints to base change +``` + + ## Bicategories From b85bed8b2e4bf0407cfae7360bb282e1f1fffd80 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 1 Feb 2023 09:51:22 -0800 Subject: [PATCH 15/18] defn: trivial fibration --- src/Cat/Displayed/Instances/Trivial.lagda.md | 114 +++++++++++++++++++ src/index.lagda.md | 2 + 2 files changed, 116 insertions(+) create mode 100644 src/Cat/Displayed/Instances/Trivial.lagda.md diff --git a/src/Cat/Displayed/Instances/Trivial.lagda.md b/src/Cat/Displayed/Instances/Trivial.lagda.md new file mode 100644 index 000000000..f841f2955 --- /dev/null +++ b/src/Cat/Displayed/Instances/Trivial.lagda.md @@ -0,0 +1,114 @@ +```agda +open import Cat.Displayed.Base +open import Cat.Displayed.Bifibration +open import Cat.Displayed.Cartesian +open import Cat.Displayed.Cocartesian +open import Cat.Displayed.Fibre +open import Cat.Displayed.Total +open import Cat.Instances.Shape.Terminal +open import Cat.Functor.Equivalence +open import Cat.Functor.Equivalence.Path +open import Cat.Prelude + +module Cat.Displayed.Instances.Trivial + {o ℓ} (𝒞 : Precategory o ℓ) + where +``` + + + +# The Trivial Bifibration + +Any category $\ca{C}$ can be regarded as being displayed over the +terminal category $\top$. + +```agda +Trivial : Displayed ⊤Cat o ℓ +Trivial .Displayed.Ob[_] _ = Ob +Trivial .Displayed.Hom[_] _ = Hom +Trivial .Displayed.Hom[_]-set _ _ _ = Hom-set _ _ +Trivial .Displayed.id′ = id +Trivial .Displayed._∘′_ = _∘_ +Trivial .Displayed.idr′ = idr +Trivial .Displayed.idl′ = idl +Trivial .Displayed.assoc′ = assoc +``` + +All morphisms in the trivial displayed category are vertical over the same object, +so producing cartesian lifts is extremely easy: just use the identity +morphism! + +```agda +open Cartesian-fibration +open Cocartesian-fibration +open Cartesian-lift +open Cocartesian-lift + +Trivial-fibration : Cartesian-fibration Trivial +Trivial-fibration .has-lift f y′ .x′ = y′ +Trivial-fibration .has-lift f y′ .lifting = id +Trivial-fibration .has-lift f y′ .cartesian = cartesian-id Trivial +``` + +We can use a similar line of argument to deduce that it is also an opfibration. + +```agda +Trivial-opfibration : Cocartesian-fibration Trivial +Trivial-opfibration .has-lift f x′ .y′ = + x′ +Trivial-opfibration .has-lift f x′ .lifting = id +Trivial-opfibration .has-lift f x′ .cocartesian = cocartesian-id Trivial +``` + +Therefore, it is also a bifibration. + +```agda +Trivial-bifibration : is-bifibration Trivial +Trivial-bifibration .is-bifibration.fibration = Trivial-fibration +Trivial-bifibration .is-bifibration.opfibration = Trivial-opfibration +``` + +Furthermore, the total category of the trivial bifibration is *isomorphic* +to the category we started with. + +```agda +trivial-total : Functor (∫ Trivial) 𝒞 +trivial-total .F₀ = snd +trivial-total .F₁ = preserves +trivial-total .F-id = refl +trivial-total .F-∘ _ _ = refl + +trivial-total-iso : is-precat-iso trivial-total +trivial-total-iso .is-precat-iso.has-is-ff = + is-iso→is-equiv $ + iso (total-hom tt) + (λ _ → refl) + (λ _ → total-hom-pathp Trivial refl refl refl refl) +trivial-total-iso .is-precat-iso.has-is-iso = + is-iso→is-equiv $ + iso (tt ,_) + (λ _ → refl) + (λ _ → refl ,ₚ refl) +``` + +As the trivial bifibration only has one fibre, this fibre is also +isomorphic to $\cE$. + +```agda +trivial-fibre : Functor (Fibre Trivial tt) 𝒞 +trivial-fibre .F₀ x = x +trivial-fibre .F₁ f = f +trivial-fibre .F-id = refl +trivial-fibre .F-∘ _ _ = transport-refl _ + +trivial→fibre-iso : is-precat-iso trivial-fibre +trivial→fibre-iso .is-precat-iso.has-is-ff = id-equiv +trivial→fibre-iso .is-precat-iso.has-is-iso = id-equiv +``` + diff --git a/src/index.lagda.md b/src/index.lagda.md index bbdc2a361..9c1d25bc5 100644 --- a/src/index.lagda.md +++ b/src/index.lagda.md @@ -670,6 +670,8 @@ open import Cat.Displayed.Instances.Scone -- We can consider *scones* over a category C with a terminal object as -- forming a displayed category over C. Moreover, it's a Cartesian -- fibration by construction. +open import Cat.Displayed.Instances.Trivial +-- Any category can be displayed over the terminal category. ``` ### Cocartesian fibrations From eb6770037bf6c56f3f50cdb060464339688ed6aa Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 1 Feb 2023 14:30:00 -0800 Subject: [PATCH 16/18] fix: wording, formatting --- src/Cat/Displayed/Bifibration.lagda.md | 14 +- src/Cat/Displayed/Cartesian/Weak.lagda.md | 187 +++++++++--------- .../Displayed/Cocartesian/Indexing.lagda.md | 20 +- 3 files changed, 113 insertions(+), 108 deletions(-) diff --git a/src/Cat/Displayed/Bifibration.lagda.md b/src/Cat/Displayed/Bifibration.lagda.md index 228f56f5e..02d347fd4 100644 --- a/src/Cat/Displayed/Bifibration.lagda.md +++ b/src/Cat/Displayed/Bifibration.lagda.md @@ -35,9 +35,9 @@ open Displayed ℰ # Bifibrations -A displayed category $\cE$ is a **bifibration** if it both a fibration -and an opfibration. This means that $\cE$ is equipped with both -[reindexing] and [opreindexing] functors, which allows us to both +A displayed category $\cE \liesover \cB$ is a **bifibration** if it both +a fibration and an opfibration. This means that $\cE$ is equipped with +both [reindexing] and [opreindexing] functors, which allows us to both restrict and extend along morphisms $X \to Y$ in the base. Note that a bifibration is *not* the same as a "profunctor of categories"; @@ -64,16 +64,16 @@ record is-bifibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where # Bifibrations and Adjoints -If $\cE$ is a bifibration, then opreindexing functors are [left adjoint] -to reindexing functors. To see this, note that we need to construct -a natural isomorphism between $\cE_{y}(u_{*}(-),-)$ and +If $\cE$ is a bifibration, then its opreindexing functors are +[left adjoints] to reindexing functors. To see this, note that we need +to construct a natural isomorphism between $\cE_{y}(u_{*}(-),-)$ and $\cE_{x}(-,u^{*}(-))$. However, we have already shown that $\cE_{y}(u_{*}(-),-)$ and $\cE_{x}(-,u^{*}(-))$ are both naturally isomorphic to $\cE_{u}(-,-)$ (see `opfibration→hom-iso`{.Agda} and `fibration→hom-iso`{.Agda}), so all we need to do is compose these natural isomorphisms! -[left adjoint]: Cat.Functor.Adjoint.html +[left adjoints]: Cat.Functor.Adjoint.html ```agda module _ (bifib : is-bifibration) where diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md index ed3a092f4..c2696eb45 100644 --- a/src/Cat/Displayed/Cartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md @@ -28,6 +28,7 @@ open Cart ℰ open DR ℰ open DM ℰ open Functor +open Functor ``` --> @@ -72,6 +73,8 @@ record is-weak-cartesian → (h′ : Hom[ id ] x′ a′) → f′ ∘′ h′ ≡[ idr _ ] g′ → h′ ≡ universal g′ + +open is-weak-cartesian ``` Like their stronger counterparts, weak cartesian lifts are unique @@ -125,11 +128,11 @@ cartesian→weak-cartesian {f = f} {f′ = f′} cart = weak-cart where open is-cartesian cart weak-cart : is-weak-cartesian f f′ - weak-cart .is-weak-cartesian.universal g′ = + weak-cart .universal g′ = universalv g′ - weak-cart .is-weak-cartesian.commutes g′ = + weak-cart .commutes g′ = commutesv g′ - weak-cart .is-weak-cartesian.unique h′ p = + weak-cart .unique h′ p = uniquev h′ p ``` @@ -151,13 +154,13 @@ weak-cartesian→cartesian {x = x} {y′ = y′} {f = f} {f′ = f′} fib f-wea module f-weak = is-weak-cartesian f-weak x* : Ob[ x ] - x* = Cartesian-lift.x′ (has-lift f y′) + x* = has-lift.x′ f y′ f* : Hom[ f ] x* y′ - f* = Cartesian-lift.lifting (has-lift f y′) + f* = has-lift.lifting f y′ f*-cart : is-cartesian f f* - f*-cart = Cartesian-lift.cartesian (has-lift f y′) + f*-cart = has-lift.cartesian f y′ f*-weak : is-weak-cartesian f f* f*-weak = cartesian→weak-cartesian f*-cart @@ -178,11 +181,11 @@ postcompose-equiv→weak-cartesian → (f′ : Hom[ f ] x′ y′) → (∀ {x″} → is-equiv {A = Hom[ id ] x″ x′} (f′ ∘′_)) → is-weak-cartesian f f′ -postcompose-equiv→weak-cartesian f′ eqv .is-weak-cartesian.universal h′ = +postcompose-equiv→weak-cartesian f′ eqv .universal h′ = equiv→inverse eqv (hom[ idr _ ]⁻ h′) -postcompose-equiv→weak-cartesian f′ eqv .is-weak-cartesian.commutes h′ = +postcompose-equiv→weak-cartesian f′ eqv .commutes h′ = to-pathp⁻ (equiv→counit eqv (hom[ idr _ ]⁻ h′)) -postcompose-equiv→weak-cartesian f′ eqv .is-weak-cartesian.unique m′ p = +postcompose-equiv→weak-cartesian f′ eqv .unique m′ p = (sym $ equiv→unit eqv m′) ∙ ap (equiv→inverse eqv) (from-pathp⁻ p) weak-cartesian→postcompose-equiv @@ -191,10 +194,9 @@ weak-cartesian→postcompose-equiv → is-equiv {A = Hom[ id ] x″ x′} (f′ ∘′_) weak-cartesian→postcompose-equiv wcart = is-iso→is-equiv $ - iso (λ h′ → universal (hom[ idr _ ] h′)) - (λ h′ → from-pathp⁻ (commutes _) ·· hom[]-∙ _ _ ·· liberate _) - (λ h′ → sym $ unique _ (to-pathp refl)) - where open is-weak-cartesian wcart + iso (λ h′ → wcart .universal (hom[ idr _ ] h′)) + (λ h′ → from-pathp⁻ (wcart .commutes _) ·· hom[]-∙ _ _ ·· liberate _) + (λ h′ → sym $ wcart .unique _ (to-pathp refl)) ``` ## Weak Cartesian Lifts @@ -281,19 +283,23 @@ Notably, weak fibrations are fibrations when weak cartesian morphisms are closed under composition. ```agda -weak-fibration→fibration - : is-weak-cartesian-fibration - → (∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y} - → {f′ : Hom[ f ] y′ z′} {g′ : Hom[ g ] x′ y′} - → is-weak-cartesian f f′ → is-weak-cartesian g g′ - → is-weak-cartesian (f ∘ g) (f′ ∘′ g′)) - → Cartesian-fibration -weak-fibration→fibration weak-fib weak-∘ .Cartesian-fibration.has-lift {x = x} f y′ = f-lift where - open is-weak-cartesian-fibration weak-fib - - module weak-∘ {x y z} (f : Hom y z) (g : Hom x y) (z′ : Ob[ z ]) = - is-weak-cartesian (weak-∘ (weak-lift.weak-cartesian f z′) - (weak-lift.weak-cartesian g _)) +module _ where + open Cartesian-fibration + open is-cartesian + + weak-fibration→fibration + : is-weak-cartesian-fibration + → (∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y} + → {f′ : Hom[ f ] y′ z′} {g′ : Hom[ g ] x′ y′} + → is-weak-cartesian f f′ → is-weak-cartesian g g′ + → is-weak-cartesian (f ∘ g) (f′ ∘′ g′)) + → Cartesian-fibration + weak-fibration→fibration weak-fib weak-∘ .has-lift {x = x} f y′ = f-lift where + open is-weak-cartesian-fibration weak-fib + + module weak-∘ {x y z} (f : Hom y z) (g : Hom x y) (z′ : Ob[ z ]) = + is-weak-cartesian (weak-∘ (weak-lift.weak-cartesian f z′) + (weak-lift.weak-cartesian g _)) ``` To show that $f$ has a cartesian lift, we begin by taking the weak @@ -312,16 +318,16 @@ cartesian lift $f^{*}$ of $f$. ~~~ ```agda - x* : Ob[ x ] - x* = weak-lift.x′ f y′ - - f* : Hom[ f ] x* y′ - f* = weak-lift.lifting f y′ - - f*-weak-cartesian : is-weak-cartesian f f* - f*-weak-cartesian = weak-lift.weak-cartesian f y′ - - module f* = is-weak-cartesian (f*-weak-cartesian) + x* : Ob[ x ] + x* = weak-lift.x′ f y′ + + f* : Hom[ f ] x* y′ + f* = weak-lift.lifting f y′ + + f*-weak-cartesian : is-weak-cartesian f f* + f*-weak-cartesian = weak-lift.weak-cartesian f y′ + + module f* = is-weak-cartesian (f*-weak-cartesian) ``` We must now show that the weak cartesian morphism $f^{*}$ is actually @@ -353,28 +359,28 @@ morphism $u' \to u^{*}$, which we can then compose with $m^{*}$ to obtain the requisite map. ```agda - module Morphisms - {u : Ob} {u′ : Ob[ u ]} (m : Hom u x) (h′ : Hom[ f ∘ m ] u′ y′) - where - u* : Ob[ u ] - u* = weak-lift.x′ m _ - - m* : Hom[ m ] u* x* - m* = weak-lift.lifting m _ - - m*-weak-cartesian : is-weak-cartesian m m* - m*-weak-cartesian = weak-lift.weak-cartesian m x* - - module m* = is-weak-cartesian m*-weak-cartesian - module f*∘m* = is-weak-cartesian (weak-∘ f*-weak-cartesian m*-weak-cartesian) + module Morphisms + {u : Ob} {u′ : Ob[ u ]} (m : Hom u x) (h′ : Hom[ f ∘ m ] u′ y′) + where + u* : Ob[ u ] + u* = weak-lift.x′ m _ + + m* : Hom[ m ] u* x* + m* = weak-lift.lifting m _ + + m*-weak-cartesian : is-weak-cartesian m m* + m*-weak-cartesian = weak-lift.weak-cartesian m x* + + module m* = is-weak-cartesian m*-weak-cartesian + module f*∘m* = is-weak-cartesian (weak-∘ f*-weak-cartesian m*-weak-cartesian) ``` ```agda - f*-cartesian : is-cartesian f f* - f*-cartesian .is-cartesian.universal {u = u} {u′ = u′} m h′ = - hom[ idr m ] (m* ∘′ f*∘m*.universal h′) - where open Morphisms m h′ + f*-cartesian : is-cartesian f f* + f*-cartesian .universal {u = u} {u′ = u′} m h′ = + hom[ idr m ] (m* ∘′ f*∘m*.universal h′) + where open Morphisms m h′ ```
@@ -383,18 +389,18 @@ yoga; the only real mathematical content is that the factorization of $h'$ via $f^{*} \cdot m^{*}$ commutes. ```agda - f*-cartesian .is-cartesian.commutes {u = u} {u′ = u′} m h′ = path - where - open Morphisms m h′ - - abstract - path : f* ∘′ hom[ idr m ] (m* ∘′ f*∘m*.universal h′) ≡ h′ - path = - f* ∘′ hom[] (m* ∘′ f*∘m*.universal h′) ≡⟨ whisker-r _ ⟩ - hom[] (f* ∘′ m* ∘′ f*∘m*.universal h′) ≡⟨ assoc[] {q = idr _} ⟩ - hom[] ((f* ∘′ m*) ∘′ f*∘m*.universal h′) ≡⟨ hom[]⟩⟨ from-pathp⁻ (f*∘m*.commutes h′) ⟩ - hom[] (hom[] h′) ≡⟨ hom[]-∙ _ _ ∙ liberate _ ⟩ - h′ ∎ + f*-cartesian .commutes {u = u} {u′ = u′} m h′ = path + where + open Morphisms m h′ + + abstract + path : f* ∘′ hom[ idr m ] (m* ∘′ f*∘m*.universal h′) ≡ h′ + path = + f* ∘′ hom[] (m* ∘′ f*∘m*.universal h′) ≡⟨ whisker-r _ ⟩ + hom[] (f* ∘′ m* ∘′ f*∘m*.universal h′) ≡⟨ assoc[] {q = idr _} ⟩ + hom[] ((f* ∘′ m*) ∘′ f*∘m*.universal h′) ≡⟨ hom[]⟩⟨ from-pathp⁻ (f*∘m*.commutes h′) ⟩ + hom[] (hom[] h′) ≡⟨ hom[]-∙ _ _ ∙ liberate _ ⟩ + h′ ∎ ```
@@ -404,25 +410,25 @@ the fact that both $m^{*}$ and $f^{*} \cdot m^{*}$ are weak cartesian maps. ```agda - f*-cartesian .is-cartesian.unique {u = u} {u′ = u′} {m = m} {h′ = h′} m′ p = path - where - open Morphisms m h′ - - abstract - universal-path : (f* ∘′ m*) ∘′ m*.universal m′ ≡[ idr (f ∘ m) ] h′ - universal-path = to-pathp $ - hom[] ((f* ∘′ m*) ∘′ m*.universal m′) ≡˘⟨ assoc[] {p = ap (f ∘_) (idr m)} ⟩ - hom[] (f* ∘′ (m* ∘′ m*.universal m′)) ≡⟨ hom[]⟩⟨ ap (f* ∘′_) (from-pathp⁻ (m*.commutes m′)) ⟩ - hom[] (f* ∘′ hom[] m′) ≡⟨ smashr _ _ ∙ liberate _ ⟩ - f* ∘′ m′ ≡⟨ p ⟩ - h′ ∎ - - path : m′ ≡ hom[ idr m ] (m* ∘′ f*∘m*.universal h′) - path = - m′ ≡˘⟨ from-pathp (m*.commutes m′) ⟩ - hom[] (m* ∘′ m*.universal m′) ≡⟨ reindex _ (idr m) ⟩ - hom[] (m* ∘′ m*.universal m′) ≡⟨ hom[]⟩⟨ ap (m* ∘′_) (f*∘m*.unique _ universal-path) ⟩ - hom[] (m* ∘′ f*∘m*.universal h′) ∎ + f*-cartesian .unique {u = u} {u′ = u′} {m = m} {h′ = h′} m′ p = path + where + open Morphisms m h′ + + abstract + universal-path : (f* ∘′ m*) ∘′ m*.universal m′ ≡[ idr (f ∘ m) ] h′ + universal-path = to-pathp $ + hom[] ((f* ∘′ m*) ∘′ m*.universal m′) ≡˘⟨ assoc[] {p = ap (f ∘_) (idr m)} ⟩ + hom[] (f* ∘′ (m* ∘′ m*.universal m′)) ≡⟨ hom[]⟩⟨ ap (f* ∘′_) (from-pathp⁻ (m*.commutes m′)) ⟩ + hom[] (f* ∘′ hom[] m′) ≡⟨ smashr _ _ ∙ liberate _ ⟩ + f* ∘′ m′ ≡⟨ p ⟩ + h′ ∎ + + path : m′ ≡ hom[ idr m ] (m* ∘′ f*∘m*.universal h′) + path = + m′ ≡˘⟨ from-pathp (m*.commutes m′) ⟩ + hom[] (m* ∘′ m*.universal m′) ≡⟨ reindex _ (idr m) ⟩ + hom[] (m* ∘′ m*.universal m′) ≡⟨ hom[]⟩⟨ ap (m* ∘′_) (f*∘m*.unique _ universal-path) ⟩ + hom[] (m* ∘′ f*∘m*.universal h′) ∎ ``` @@ -430,10 +436,10 @@ Putting this all together, we can finally deduce that $f^{*}$ is a cartesian lift of $f$. ```agda - f-lift : Cartesian-lift f y′ - f-lift .Cartesian-lift.x′ = x* - f-lift .Cartesian-lift.lifting = f* - f-lift .Cartesian-lift.cartesian = f*-cartesian + f-lift : Cartesian-lift f y′ + f-lift .Cartesian-lift.x′ = x* + f-lift .Cartesian-lift.lifting = f* + f-lift .Cartesian-lift.cartesian = f*-cartesian ``` ## Factorisations in Weak Fibrations @@ -510,7 +516,6 @@ module _ (wfib : is-weak-cartesian-fibration) where → Hom[ f ] x′ y′ ≃ Hom[ id ] x′ (weak-lift.x′ f y′) weak-fibration→vertical-equiv {y′ = y′} f = weak-lift.universal f y′ , - weak-fibration→universal-is-equiv f ``` @@ -546,7 +551,7 @@ in $\cB$, along with a natural equivalence of homs as above, then $\cE$ is a weak fibration. This result is the primary reason to care about weak fibrations, as we -already have a suite of tools for constructing natural equivalences of +already have a toolkit for constructing natural equivalences of hom sets! Most notably, this allows us to use the theory of [adjuncts] to construct weak fibrations. diff --git a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md index 7e409f584..fc1ba3fc7 100644 --- a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md +++ b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md @@ -27,23 +27,23 @@ open Functor # Opreindexing for Cocartesian fibrations -[opfibrations] are dual to [fibrations], so they inherit the ability +[Opfibrations] are dual to [fibrations], so they inherit the ability to [reindex along morphisms in the base]. However, this reindexing is *covariant* for opfibrations, whereas it is *contravariant* for fibrations. -[opfibrations]: Cat.Displayed.Cocartesian.html +[Opfibrations]: Cat.Displayed.Cocartesian.html [fibrations]: Cat.Displayed.Cartesian.html [reindex along morphisms in the base] Cat.Displayed.Cartesian.Indexing.html -This gives distinction opfibrations a distinct character. Reindexing in -fibrations can be thought of a sort of restriction map. This can be -seen clearly with [the canonical self-indexing], where the reindexing -functors are given by [pullbacks]. On the other hand, opreindexing -can be thought of as an extension map. We can again use the the canonical -self-indexing as our example: opreindexing is given by postcomposition, -which extends families over $X$ to families over $Y$ by adding in -empty fibres. +This difference in variance gives opfibrations a distinct character. +Reindexing in fibrations can be thought of a sort of restriction map. +This can be seen clearly with [the canonical self-indexing], where the +reindexing functors are given by [pullbacks]. On the other hand, +opreindexing can be thought of as an extension map. We can again use the +the canonical self-indexing as our example: opreindexing is given by +postcomposition, which extends families over $X$ to families over $Y$ by +adding in empty fibres. [the canonical self-indexing]: Cat.Displayed.Instances.Slice.html [pullbacks]: Cat.Diagram.Pullback.html From 5d1d4ef0eb92c3900a077482276ea27eef348ab5 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 1 Feb 2023 14:32:58 -0800 Subject: [PATCH 17/18] chore: push-out -> cobase-change --- src/Cat/Displayed/Bifibration.lagda.md | 16 ++++++++-------- src/Cat/Displayed/Cocartesian/Indexing.lagda.md | 13 +++++-------- src/Cat/Displayed/Cocartesian/Weak.lagda.md | 10 ++++++---- 3 files changed, 19 insertions(+), 20 deletions(-) diff --git a/src/Cat/Displayed/Bifibration.lagda.md b/src/Cat/Displayed/Bifibration.lagda.md index 02d347fd4..b8c6200b3 100644 --- a/src/Cat/Displayed/Bifibration.lagda.md +++ b/src/Cat/Displayed/Bifibration.lagda.md @@ -81,10 +81,10 @@ module _ (bifib : is-bifibration) where open Cat.Displayed.Cartesian.Indexing ℰ fibration open Cat.Displayed.Cocartesian.Indexing ℰ opfibration - push-out⊣base-change + cobase-change⊣base-change : ∀ {x y} (f : Hom x y) - → push-out f ⊣ base-change f - push-out⊣base-change {x} {y} f = + → cobase-change f ⊣ base-change f + cobase-change⊣base-change {x} {y} f = hom-natural-iso→adjoints $ (opfibration→hom-iso opfibration f ni⁻¹) ni∘ fibration→hom-iso fibration f ``` @@ -108,11 +108,11 @@ module _ (fib : Cartesian-fibration) where open Cartesian-fibration fib open Cat.Displayed.Cartesian.Indexing ℰ fib - left-adjoint-reindexing→opfibration + left-adjoint-base-change→opfibration : (L : ∀ {x y} → (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y)) → (∀ {x y} → (f : Hom x y) → (L f ⊣ base-change f)) → Cocartesian-fibration - left-adjoint-reindexing→opfibration L adj = + left-adjoint-base-change→opfibration L adj = cartesian+weak-opfibration→opfibration fib $ hom-iso→weak-opfibration L λ u → fibration→hom-iso-from fib u ni∘ (adjunct-hom-iso-from (adj u) _ ni⁻¹) @@ -125,8 +125,8 @@ With some repackaging, we can see that this yields a bifibration. : (L : ∀ {x y} → (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y)) → (∀ {x y} → (f : Hom x y) → (L f ⊣ base-change f)) → is-bifibration - left-adjoint-reindexing→bifibration L adj .is-bifibration.fibration = + left-adjoint-base-change→bifibration L adj .is-bifibration.fibration = fib - left-adjoint-reindexing→bifibration L adj .is-bifibration.opfibration = - left-adjoint-reindexing→opfibration L adj + left-adjoint-base-change→bifibration L adj .is-bifibration.opfibration = + left-adjoint-base-change→opfibration L adj ``` diff --git a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md index fc1ba3fc7..555069ca9 100644 --- a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md +++ b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md @@ -48,21 +48,18 @@ adding in empty fibres. [the canonical self-indexing]: Cat.Displayed.Instances.Slice.html [pullbacks]: Cat.Diagram.Pullback.html -Continuing the analogy of indexing as pullback, we call the opreindexing -functors _pushouts_. - ```agda -push-out : ∀ {x y} (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y) -push-out f .F₀ ob = has-lift.y′ f ob -push-out f .F₁ vert = rebase f vert +cobase-change : ∀ {x y} (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y) +cobase-change f .F₀ ob = has-lift.y′ f ob +cobase-change f .F₁ vert = rebase f vert ```