From ced3fa3df0617ed72553c839e5e358f133aeda8b Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Sat, 8 Feb 2025 16:30:43 -0500 Subject: [PATCH] refactor: banish wrapper records from weak (co)cartesian fibrations I also removed some bad 'is-' prefixes --- src/Cat/Displayed/Cartesian/Weak.lagda.md | 176 ++++++++---------- src/Cat/Displayed/Cocartesian/Weak.lagda.md | 89 ++++----- .../Displayed/Instances/Subobjects.lagda.md | 5 +- 3 files changed, 125 insertions(+), 145 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md index eff338978..0c00d6951 100644 --- a/src/Cat/Displayed/Cartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md @@ -216,14 +216,26 @@ fibrations **prefibred categories**, though we avoid this name as it conflicts with the precategory/category distinction. ```agda -record is-weak-cartesian-fibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where - no-eta-equality - field - weak-lift : ∀ {x y} → (f : Hom x y) → (y' : Ob[ y ]) → Weak-cartesian-lift f y' +Weak-cartesian-fibration : Type _ +Weak-cartesian-fibration = ∀ {x y} → (f : Hom x y) → (y' : Ob[ y ]) → Weak-cartesian-lift f y' + +module Weak-cartesian-fibration (wfib : Weak-cartesian-fibration) where +``` + + 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 @@ -235,9 +247,9 @@ unless $\cE$ is a fibration. ```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'') + → Hom[ id ] (f ^* y') (f ^* y'') rebase f vert = - weak-lift.universal f _ (hom[ idl _ ] (vert ∘' weak-lift.lifting f _)) + π*.universal (hom[ idl _ ] (vert ∘' π* f _)) ``` Every fibration is a weak fibration. @@ -250,7 +262,7 @@ cartesian-lift→weak-cartesian-lift fibration→weak-fibration : Cartesian-fibration - → is-weak-cartesian-fibration + → Weak-cartesian-fibration ```
@@ -265,7 +277,7 @@ cartesian-lift→weak-cartesian-lift cart .Weak-cartesian-lift.lifting = cartesian-lift→weak-cartesian-lift cart .Weak-cartesian-lift.weak-cartesian = cartesian→weak-cartesian (Cartesian-lift.cartesian cart) -fibration→weak-fibration fib .is-weak-cartesian-fibration.weak-lift x y' = +fibration→weak-fibration fib x y' = cartesian-lift→weak-cartesian-lift (fib x y') ```
@@ -276,22 +288,17 @@ are closed under composition. ```agda module _ where - open Cartesian-fibration open is-cartesian weak-fibration→fibration - : is-weak-cartesian-fibration + : 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-∘ {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 _)) + open Weak-cartesian-fibration weak-fib ``` To show that $f$ has a cartesian lift, we begin by taking the weak @@ -309,19 +316,6 @@ cartesian lift $f^{*}$ of $f$. \end{tikzcd} ~~~ -```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) -``` - We must now show that the weak cartesian morphism $f^{*}$ is actually cartesian. To do this, we must construct the following unique universal map: @@ -351,28 +345,17 @@ 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) -``` + f*∘m*-weak-cartesian + : ∀ {u u'} (m : Hom u x) (h' : Hom[ f ∘ m ] u' y') + → is-weak-cartesian (f ∘ m) (π* f y' ∘' π* m (f ^* y')) + f*∘m*-weak-cartesian m h' = weak-∘ π*.weak-cartesian π*.weak-cartesian + module f*∘m* {u u'} (m : Hom u x) (h' : Hom[ f ∘ m ] u' y') = + is-weak-cartesian (f*∘m*-weak-cartesian m h') -```agda - f*-cartesian : is-cartesian f f* + f*-cartesian : is-cartesian f (π* f y') f*-cartesian .universal {u = u} {u' = u'} m h' = - hom[ idr m ] (m* ∘' f*∘m*.universal h') - where open Morphisms m h' + hom[ idr m ] (π* m (f ^* y') ∘' f*∘m*.universal m h' h') ```
@@ -383,16 +366,14 @@ $h'$ via $f^{*} \cdot m^{*}$ commutes. ```agda 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 y' ∘' hom[ idr m ] (π* m (f ^* y') ∘' f*∘m*.universal m h' 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 y' ∘' hom[] (π* m (f ^* y') ∘' f*∘m*.universal m h' h') ≡⟨ whisker-r _ ⟩ + hom[] (π* f y' ∘' π* m (f ^* y') ∘' f*∘m*.universal m h' h') ≡⟨ assoc[] {q = idr _} ⟩ + hom[] ((π* f y' ∘' π* m (f ^* y')) ∘' f*∘m*.universal m h' h') ≡⟨ hom[]⟩⟨ from-pathp⁻ (f*∘m*.commutes m h' h') ⟩ + hom[] (hom[] h') ≡⟨ hom[]-∙ _ _ ∙ liberate _ ⟩ + h' ∎ ```
@@ -404,23 +385,22 @@ maps. ```agda 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 : (π* f y' ∘' π* m (f ^* y')) ∘' π*.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 ⟩ + hom[] ((π* f y' ∘' π* m (f ^* y')) ∘' π*.universal m') ≡˘⟨ assoc[] {p = ap (f ∘_) (idr m)} ⟩ + hom[] (π* f y' ∘' (π* m (f ^* y') ∘' π*.universal m')) ≡⟨ hom[]⟩⟨ ap (π* f y' ∘'_) (from-pathp⁻ (π*.commutes m')) ⟩ + hom[] (π* f y' ∘' hom[] m') ≡⟨ smashr _ _ ∙ liberate _ ⟩ + π* f y' ∘' m' ≡⟨ p ⟩ h' ∎ - path : m' ≡ hom[ idr m ] (m* ∘' f*∘m*.universal h') + path : m' ≡ hom[ idr m ] (π* m (f ^* y') ∘' f*∘m*.universal m h' 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') ∎ + m' ≡˘⟨ from-pathp (π*.commutes m') ⟩ + hom[] (π* m (f ^* y') ∘' π*.universal m') ≡⟨ reindex _ (idr m) ⟩ + hom[] (π* m (f ^* y') ∘' π*.universal m') ≡⟨ hom[]⟩⟨ ap (π* m (f ^* y') ∘'_) (f*∘m*.unique m h' _ universal-path) ⟩ + hom[] (π* m (f ^* y') ∘' f*∘m*.universal m h' h') ∎ ``` @@ -429,8 +409,8 @@ 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.x' = (f ^* y') + f-lift .Cartesian-lift.lifting = π* f y' f-lift .Cartesian-lift.cartesian = f*-cartesian ``` @@ -455,7 +435,7 @@ record weak-cartesian-factorisation weak-fibration→weak-cartesian-factors : ∀ {x y x' y'} {f : Hom x y} - → is-weak-cartesian-fibration + → Weak-cartesian-fibration → (f' : Hom[ f ] x' y') → weak-cartesian-factorisation f' ``` @@ -468,16 +448,15 @@ $f'$ by the lift of $f$. ```agda weak-fibration→weak-cartesian-factors {y' = y'} {f = f} wfib f' = weak-factor where - open is-weak-cartesian-fibration wfib - module f-lift = weak-lift f y' + open Weak-cartesian-fibration wfib open weak-cartesian-factorisation weak-factor : weak-cartesian-factorisation f' - weak-factor .x'' = f-lift.x' - weak-factor .vertical = f-lift.universal f' - weak-factor .weak-cart = f-lift.lifting - weak-factor .has-weak-cartesian = f-lift.weak-cartesian - weak-factor .factors = symP $ f-lift.commutes f' + weak-factor .x'' = f ^* y' + weak-factor .vertical = π*.universal f' + weak-factor .weak-cart = π* f y' + weak-factor .has-weak-cartesian = π*.weak-cartesian + weak-factor .factors = symP $ π*.commutes f' ``` ## Weak fibrations and equivalence of Hom sets @@ -490,24 +469,24 @@ factorisation of $f'$; this forms an equivalence, as this factorisation is unique. ```agda -module _ (wfib : is-weak-cartesian-fibration) where - open is-weak-cartesian-fibration wfib +module _ (wfib : Weak-cartesian-fibration) where + open Weak-cartesian-fibration wfib weak-fibration→universal-is-equiv : ∀ {x y x' y'} → (f : Hom x y) - → is-equiv (weak-lift.universal f y' {x'}) + → is-equiv (π*.universal {f = f} {y' = y'} {x'}) weak-fibration→universal-is-equiv {y' = y'} f = is-iso→is-equiv $ - iso (λ f' → hom[ idr f ] (weak-lift.lifting f y' ∘' f') ) - (λ f' → sym $ weak-lift.unique f y' f' (to-pathp refl)) - (λ f' → cancel _ _ (weak-lift.commutes f y' f')) + iso (λ f' → hom[ idr f ] (π* f y' ∘' f') ) + (λ f' → sym $ π*.unique f' (to-pathp refl)) + (λ f' → cancel _ _ (π*.commutes f')) weak-fibration→vertical-equiv : ∀ {x y x' y'} → (f : Hom x y) - → Hom[ f ] x' y' ≃ Hom[ id ] x' (weak-lift.x' f y') + → Hom[ f ] x' y' ≃ Hom[ id ] x' (f ^* y') weak-fibration→vertical-equiv {y' = y'} f = - weak-lift.universal f y' , + π*.universal , weak-fibration→universal-is-equiv f ``` @@ -517,24 +496,22 @@ between $\cE_{u}(-,y')$ and $\cE_{x}(-,u^{*}(y'))$. ```agda weak-fibration→hom-iso-into : ∀ {x y y'} (u : Hom x y) - → Hom-over-into ℰ u y' ≅ⁿ Hom-into (Fibre ℰ x) (weak-lift.x' u y') + → Hom-over-into ℰ u y' ≅ⁿ Hom-into (Fibre ℰ 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 : make-natural-iso (Hom-over-into ℰ u y') (Hom-into (Fibre ℰ x) (u ^* y')) + mi .eta x u' = π*.universal u' + mi .inv x v' = hom[ idr u ] (π* u y' ∘' v') mi .eta∘inv x = funext λ v' → - sym $ weak-lift.unique u _ _ (to-pathp refl) + sym $ π*.unique _ (to-pathp refl) mi .inv∘eta x = funext λ u' → - from-pathp (weak-lift.commutes u _ _) + from-pathp (π*.commutes _) mi .natural x y v' = funext λ u' → - weak-lift.unique u _ _ $ to-pathp $ + π*.unique _ $ to-pathp $ smashr _ _ - ∙ weave _ (ap (u ∘_) (idl id)) _ (pulll' _ (weak-lift.commutes _ _ _)) + ∙ weave _ (ap (u ∘_) (idl id)) _ (pulll' _ (π*.commutes _)) ``` An *extremely* useful fact is that the converse is true: if there is some @@ -549,7 +526,6 @@ construct weak fibrations. ```agda module _ (_*₀_ : ∀ {x y} → Hom x y → Ob[ y ] → Ob[ x ]) where - open is-weak-cartesian-fibration open Weak-cartesian-lift open is-weak-cartesian @@ -566,8 +542,8 @@ module _ (_*₀_ : ∀ {x y} → Hom x y → Ob[ y ] → Ob[ x ]) where : (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 + → Weak-cartesian-fibration + vertical-equiv→weak-fibration to* to-eqv natural f y' = f-lift where ``` To start, we note that the inverse portion of the equivalence is also @@ -628,7 +604,7 @@ module _ (U : ∀ {x y} → Hom x y → Functor (Fibre ℰ y) (Fibre ℰ x)) whe hom-iso→weak-fibration : (∀ {x y y'} (u : Hom x y) → Hom-over-into ℰ u y' ≅ⁿ Hom-into (Fibre ℰ x) (U u .F₀ y')) - → is-weak-cartesian-fibration + → Weak-cartesian-fibration hom-iso→weak-fibration hom-iso = vertical-equiv→weak-fibration (λ u → U u .F₀) diff --git a/src/Cat/Displayed/Cocartesian/Weak.lagda.md b/src/Cat/Displayed/Cocartesian/Weak.lagda.md index 05490776f..726022d15 100644 --- a/src/Cat/Displayed/Cocartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cocartesian/Weak.lagda.md @@ -489,22 +489,30 @@ as **weak opfibrations** These are also sometimes called conflicts with the precategory/category distinction. ```agda -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-cocartesian-fibration : Type _ +Weak-cocartesian-fibration = ∀ {x y} → (f : Hom x y) → (x' : Ob[ x ]) → Weak-cocartesian-lift f x' ``` @@ -514,12 +522,12 @@ Weak opfibrations are dual to [weak fibrations]. ```agda weak-op-fibration→weak-opfibration - : is-weak-cartesian-fibration (ℰ ^total-op) - → is-weak-cocartesian-fibration + : Weak-cartesian-fibration (ℰ ^total-op) + → Weak-cocartesian-fibration weak-opfibration→weak-op-fibration - : is-weak-cocartesian-fibration - → is-weak-cartesian-fibration (ℰ ^total-op) + : Weak-cocartesian-fibration + → Weak-cartesian-fibration (ℰ ^total-op) ``` @@ -527,13 +535,13 @@ weak-opfibration→weak-op-fibration 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-op-fibration→weak-opfibration wlift f x' = weak-co-cartesian-lift→weak-cocartesian-lift $ - is-weak-cartesian-fibration.weak-lift wlift f x' + wlift f x' -weak-opfibration→weak-op-fibration wlift .is-weak-cartesian-fibration.weak-lift f y' = +weak-opfibration→weak-op-fibration wlift f y' = weak-cocartesian-lift→weak-co-cartesian-lift $ - is-weak-cocartesian-fibration.weak-lift wlift f y' + wlift f y' ``` @@ -547,7 +555,7 @@ cocartesian-lift→weak-cocartesian-lift opfibration→weak-opfibration : Cocartesian-fibration - → is-weak-cocartesian-fibration + → Weak-cocartesian-fibration ``` @@ -571,7 +579,7 @@ closed under composition. This follows via duality. ```agda weak-opfibration→opfibration - : is-weak-cocartesian-fibration + : 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' @@ -595,7 +603,7 @@ cocartesian maps are closed under composition, thanks to ```agda cartesian+weak-opfibration→opfibration : Cartesian-fibration ℰ - → is-weak-cocartesian-fibration + → Weak-cocartesian-fibration → Cocartesian-fibration cartesian+weak-opfibration→opfibration fib wlifts = weak-opfibration→opfibration wlifts λ f-weak g-weak → @@ -612,25 +620,25 @@ $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 +module _ (wopfib : Weak-cocartesian-fibration) where + open Weak-cocartesian-fibration wopfib weak-opfibration→universal-is-equiv : ∀ {x y y' x'} → (u : Hom x y) - → is-equiv (weak-lift.universal u x' {y'}) + → is-equiv (ι!.universal {f = u} {x' = x'} {y'}) 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)) - (λ u' → cancel _ _ (weak-lift.commutes u x' u')) + iso (λ u' → hom[ idl u ] (u' ∘' ι! u x')) + (λ u' → sym $ ι!.unique u' (to-pathp refl)) + (λ u' → cancel _ _ (ι!.commutes 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' + → Hom[ u ] x' y' ≃ Hom[ id ] (u ^! x') y' weak-opfibration→vertical-equiv {x' = x'} u = - weak-lift.universal u x' , weak-opfibration→universal-is-equiv u + ι!.universal , weak-opfibration→universal-is-equiv u ``` Furthermore, this equivalence is natural. @@ -638,24 +646,21 @@ Furthermore, this equivalence is natural. ```agda weak-opfibration→hom-iso-from : ∀ {x y x'} (u : Hom x y) - → Hom-over-from ℰ u x' ≅ⁿ Hom-from (Fibre ℰ y) (weak-lift.y' u x') + → Hom-over-from ℰ u x' ≅ⁿ Hom-from (Fibre ℰ 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 : make-natural-iso (Hom-over-from ℰ u x') (Hom-from (Fibre ℰ y) (u ^! x')) + mi .eta x u' = ι!.universal u' + mi .inv x v' = hom[ idl u ] (v' ∘' ι! u x') mi .eta∘inv _ = funext λ v' → - sym $ weak-lift.unique u _ _ (to-pathp refl) + sym $ ι!.unique _ (to-pathp refl) mi .inv∘eta _ = funext λ u' → - from-pathp $ weak-lift.commutes u _ _ + from-pathp $ ι!.commutes _ mi .natural _ _ v' = funext λ u' → - weak-lift.unique _ _ _ $ to-pathp $ + ι!.unique _ $ to-pathp $ smashl _ _ - ∙ weave _ (ap (_∘ u) (idl id)) _ (pullr' _ (weak-lift.commutes _ _ _)) + ∙ weave _ (ap (_∘ u) (idl id)) _ (pullr' _ (ι!.commutes _)) ``` As in the [weak cartesian case], the converse is also true: if there is @@ -681,7 +686,7 @@ module _ (_*₀_ : ∀ {x y} → Hom x y → Ob[ x ] → Ob[ y ]) where : (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 + → 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' → @@ -697,7 +702,7 @@ module _ (U : ∀ {x y} → Hom x y → Functor (Fibre ℰ x) (Fibre ℰ y)) whe hom-iso→weak-opfibration : (∀ {x y x'} (u : Hom x y) → Hom-over-from ℰ u x' ≅ⁿ Hom-from (Fibre ℰ y) (U u .F₀ x')) - → is-weak-cocartesian-fibration + → Weak-cocartesian-fibration hom-iso→weak-opfibration hom-iso = vertical-equiv→weak-opfibration (λ u → U u .F₀) diff --git a/src/Cat/Displayed/Instances/Subobjects.lagda.md b/src/Cat/Displayed/Instances/Subobjects.lagda.md index e93b5401a..10b102f3d 100644 --- a/src/Cat/Displayed/Instances/Subobjects.lagda.md +++ b/src/Cat/Displayed/Instances/Subobjects.lagda.md @@ -115,7 +115,6 @@ Subobjects .idr' _ = prop! Subobjects .idl' _ = prop! Subobjects .assoc' _ _ _ = prop! -open is-weak-cocartesian-fibration open Weak-cocartesian-lift open is-weak-cocartesian open Cartesian-lift @@ -191,8 +190,8 @@ fibration. ```agda Subobject-weak-opfibration : (∀ {x y} (f : Hom x y) → Image B f) - → is-weak-cocartesian-fibration Subobjects -Subobject-weak-opfibration ims .weak-lift f x' = l where + → Weak-cocartesian-fibration Subobjects +Subobject-weak-opfibration ims f x' = l where module im = Image B (ims (f ∘ x' .map)) ```