module Cat.Displayed.Cocartesian.Weak {o ℓ o' ℓ'} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o' ℓ') where
open CR ℬ open Displayed ℰ open Cocart ℰ open Cat.Displayed.Morphism ℰ open Cat.Displayed.Morphism.Duality ℰ open Cat.Displayed.Reasoning ℰ private module Fib {x} = Precategory (Fibre ℰ x)
Weak cocartesian morphisms🔗
We can define a weaker notion of cocartesian morphism much like we can with their cartesian counterparts.
record is-weak-cocartesian {a b a' b'} (f : Hom a b) (f' : Hom[ f ] a' b') : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where no-eta-equality field universal : ∀ {x'} → (g' : Hom[ f ] a' x') → Hom[ id ] b' x' commutes : ∀ {x'} → (g' : Hom[ f ] a' x') → universal g' ∘' f' ≡[ idl _ ] g' unique : ∀ {x'} {g' : Hom[ f ] a' x'} → (h' : Hom[ id ] b' x') → h' ∘' f' ≡[ idl _ ] g' → h' ≡ universal g' open is-weak-cocartesian
Duality🔗
Weak cartesian maps in the total opposite category are equivalent to weak cocartesian maps.
weak-co-cartesian→weak-cocartesian : ∀ {x y} {f : Hom x y} {x' y'} {f' : Hom[ f ] x' y'} → is-weak-cartesian (ℰ ^total-op) f f' → is-weak-cocartesian f f' weak-cocartesian→weak-co-cartesian : ∀ {x y} {f : Hom x y} {x' y'} {f' : Hom[ f ] x' y'} → is-weak-cocartesian f f' → is-weak-cartesian (ℰ ^total-op) f f'
These functions just shuffle data around, so we omit their definitions.
weak-co-cartesian→weak-cocartesian wcart .is-weak-cocartesian.universal = is-weak-cartesian.universal wcart weak-co-cartesian→weak-cocartesian wcart .is-weak-cocartesian.commutes = is-weak-cartesian.commutes wcart weak-co-cartesian→weak-cocartesian wcart .is-weak-cocartesian.unique = is-weak-cartesian.unique wcart weak-cocartesian→weak-co-cartesian wcocart .is-weak-cartesian.universal = is-weak-cocartesian.universal wcocart weak-cocartesian→weak-co-cartesian wcocart .is-weak-cartesian.commutes = is-weak-cocartesian.commutes wcocart weak-cocartesian→weak-co-cartesian wcocart .is-weak-cartesian.unique = is-weak-cocartesian.unique wcocart
Weak cocartesian maps satisfy the dual properties of weak cartesian maps.
weak-cocartesian-codomain-unique : ∀ {x y} {f : Hom x y} → ∀ {x' y' y''} {f' : Hom[ f ] x' y'} {f'' : Hom[ f ] x' y''} → is-weak-cocartesian f f' → is-weak-cocartesian f f'' → y' ≅↓ y'' cocartesian→weak-cocartesian : ∀ {x y x' y'} {f : Hom x y} {f' : Hom[ f ] x' y'} → is-cocartesian f f' → is-weak-cocartesian f f' weak-cocartesian→cocartesian : ∀ {x y x' y'} {f : Hom x y} {f' : Hom[ f ] x' y'} → Cocartesian-fibration → is-weak-cocartesian f f' → is-cocartesian f f' precompose-equiv→weak-cocartesian : ∀ {x y x' y'} {f : Hom x y} → (f' : Hom[ f ] x' y') → (∀ {y''} → is-equiv {A = Hom[ id ] y' y''} (_∘' f')) → is-weak-cocartesian f f' weak-cocartesian→precompose-equiv : ∀ {x y x' y' y''} {f : Hom x y} {f' : Hom[ f ] x' y'} → is-weak-cocartesian f f' → is-equiv {A = Hom[ id ] y' y''} (_∘' f') fibre-precompose-equiv→weak-cocartesian : ∀ {x} {x' x'' : Ob[ x ]} → (f' : Hom[ id ] x' x'') → (∀ {x'''} → is-equiv {A = Hom[ id ] x'' x'''} (Fib._∘ f')) → is-weak-cocartesian id f' weak-cocartesian→fibre-precompose-equiv : ∀ {x} {x' x'' x''' : Ob[ x ]} {f' : Hom[ id ] x' x''} → is-weak-cocartesian id f' → is-equiv {A = Hom[ id ] x'' x'''} (Fib._∘ f')
The proofs consist of tedious applications of duality.
weak-cocartesian-codomain-unique f'-cocart f''-cocart = vertical-co-iso→vertical-iso $ weak-cartesian-domain-unique (ℰ ^total-op) (weak-cocartesian→weak-co-cartesian f''-cocart) (weak-cocartesian→weak-co-cartesian f'-cocart) cocartesian→weak-cocartesian cocart = weak-co-cartesian→weak-cocartesian $ cartesian→weak-cartesian (ℰ ^total-op) $ cocartesian→co-cartesian cocart weak-cocartesian→cocartesian opfib wcocart = co-cartesian→cocartesian $ weak-cartesian→cartesian (ℰ ^total-op) (opfibration→op-fibration opfib) (weak-cocartesian→weak-co-cartesian wcocart) precompose-equiv→weak-cocartesian f eqv = weak-co-cartesian→weak-cocartesian $ (postcompose-equiv→weak-cartesian (ℰ ^total-op) f eqv) weak-cocartesian→precompose-equiv cocart = weak-cartesian→postcompose-equiv (ℰ ^total-op) $ weak-cocartesian→weak-co-cartesian cocart fibre-precompose-equiv→weak-cocartesian f' eqv .universal v = equiv→inverse eqv v fibre-precompose-equiv→weak-cocartesian f' eqv .commutes v = to-pathp $ equiv→counit eqv v fibre-precompose-equiv→weak-cocartesian f' eqv .unique v p = sym (equiv→unit eqv v) ∙ ap (equiv→inverse eqv) (from-pathp p) weak-cocartesian→fibre-precompose-equiv wcocart = is-iso→is-equiv $ iso (wcocart .universal) (λ v → from-pathp (wcocart .commutes v)) (λ v → sym (wcocart .unique v (to-pathp refl)))
Notably, if is a Cartesian fibration, then all weak cocartesian morphisms are cocartesian.
fibration+weak-cocartesian→cocartesian : ∀ {x y x' y'} {f : Hom x y} {f' : Hom[ f ] x' y'} → Cartesian-fibration ℰ → is-weak-cocartesian f f' → is-cocartesian f f' fibration+weak-cocartesian→cocartesian {x} {y} {x'} {y'} {f} {f'} fib weak = cocart where open Cartesian-fibration fib module weak = is-weak-cocartesian weak
To see show this, we need to construct a unique factorisation of some morphism as depicted in the following diagram
We start by taking the cartesian lift of to obtain the map which we have highlighted in red.
module Morphisms {u} {u' : Ob[ u ]} (m : Hom y u) (h' : Hom[ m ∘ f ] x' u') where y* : Ob[ y ] y* = Cartesian-lift.x' (has-lift m u') m* : Hom[ m ] y* u' m* = Cartesian-lift.lifting (has-lift m u') module m* = is-cartesian (Cartesian-lift.cartesian (has-lift m u'))
Next, we can construct the morphism (highlighted in red) as the universal factorisation of through
h* : Hom[ f ] x' y* h* = m*.universal f h'
Finally, we can construct a vertical morphism as is weakly cartesian.
h** : Hom[ id ] y' y* h** = weak.universal h*
Composing and gives the desired factorisation.
cocart : is-cocartesian f f' cocart .is-cocartesian.universal m h' = hom[ idr _ ] (m* ∘' h**) where open Morphisms m h'
Showing that is best understood diagrammatically; both the and cells commute.
cocart .is-cocartesian.commutes m h' = hom[] (m* ∘' h**) ∘' f' ≡˘⟨ yank _ _ _ ⟩≡˘ m* ∘' hom[] (h** ∘' f') ≡⟨ ap (m* ∘'_) (from-pathp (weak.commutes _)) ⟩≡ m* ∘' m*.universal f h' ≡⟨ m*.commutes f h' ⟩≡ h' ∎ where open Morphisms m h'
Uniqueness is somewhat more delicate. We need to show that the blue cell in the following diagram commutes.
As a general fact, every morphism in a cartesian fibration factors into a composite of a cartesian and vertical morphism, obtained by taking the universal factorisation of We shall denote this morphism as
However, is the unique vertical map that factorises through so it suffices to show that the cell highlighted in blue commutes.
is the unique vertical map that factorises through and by our hypothesis, so it suffices to show that This commutes because is cartesian, thus finishing the proof.
cocart .is-cocartesian.unique {m = m} {h' = h'} m' p = m' ≡⟨ from-pathp⁻ (symP (m*.commutesp (idr _) m')) ⟩≡ hom[] (m* ∘' id*) ≡⟨ hom[]⟩⟨ ap (m* ∘'_) (weak.unique _ (to-pathp $ m*.unique _ path )) ⟩≡ hom[] (m* ∘' h**) ∎ where open Morphisms m h' id* : Hom[ id ] y' y* 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*.commutesv m')) ⟩≡ m' ∘' f' ≡⟨ p ⟩≡ h' ∎
Weak cocartesian lifts🔗
We can also define the dual to weak cartesian lifts.
record Weak-cocartesian-lift {x y} (f : Hom x y) (x' : Ob[ x ]) : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where no-eta-equality field {y'} : Ob[ y ] lifting : Hom[ f ] x' y' weak-cocartesian : is-weak-cocartesian f lifting open is-weak-cocartesian weak-cocartesian public
As expected, weak cocartesian lifts are dual to weak cartesian lifts.
weak-co-cartesian-lift→weak-cocartesian-lift : ∀ {x y} {f : Hom x y} {x' : Ob[ x ]} → Weak-cartesian-lift (ℰ ^total-op) f x' → Weak-cocartesian-lift f x' weak-cocartesian-lift→weak-co-cartesian-lift : ∀ {x y} {f : Hom x y} {x' : Ob[ x ]} → Weak-cocartesian-lift f x' → Weak-cartesian-lift (ℰ ^total-op) f x'
We omit the proofs, as they are even more applications of duality.
weak-co-cartesian-lift→weak-cocartesian-lift wlift .Weak-cocartesian-lift.y' = Weak-cartesian-lift.x' wlift weak-co-cartesian-lift→weak-cocartesian-lift wlift .Weak-cocartesian-lift.lifting = Weak-cartesian-lift.lifting wlift weak-co-cartesian-lift→weak-cocartesian-lift wlift .Weak-cocartesian-lift.weak-cocartesian = weak-co-cartesian→weak-cocartesian (Weak-cartesian-lift.weak-cartesian wlift) weak-cocartesian-lift→weak-co-cartesian-lift wlift .Weak-cartesian-lift.x' = Weak-cocartesian-lift.y' wlift weak-cocartesian-lift→weak-co-cartesian-lift wlift .Weak-cartesian-lift.lifting = Weak-cocartesian-lift.lifting wlift weak-cocartesian-lift→weak-co-cartesian-lift wlift .Weak-cartesian-lift.weak-cartesian = weak-cocartesian→weak-co-cartesian (Weak-cocartesian-lift.weak-cocartesian wlift)
A displayed category with all weak cocartesian lifts is called a 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.
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')
rebase : ∀ {x y x' x''} → (f : Hom x y) → Hom[ id ] x' x'' → Hom[ id ] (weak-lift.y' f x') (weak-lift.y' f x'') rebase f vert = weak-lift.universal f _ (hom[ idr _ ] (weak-lift.lifting f _ ∘' vert))
Weak opfibrations are dual to weak fibrations.
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.
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'
Every opfibration is a weak opfibration.
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
cocartesian-lift→weak-cocartesian-lift cocart .Weak-cocartesian-lift.y' = Cocartesian-lift.y' cocart cocartesian-lift→weak-cocartesian-lift cocart .Weak-cocartesian-lift.lifting = Cocartesian-lift.lifting cocart cocartesian-lift→weak-cocartesian-lift cocart .Weak-cocartesian-lift.weak-cocartesian = cocartesian→weak-cocartesian (Cocartesian-lift.cocartesian cocart) opfibration→weak-opfibration opfib .is-weak-cocartesian-fibration.weak-lift f x' = cocartesian-lift→weak-cocartesian-lift (Cocartesian-fibration.has-lift opfib f x')
A weak opfibration is an opfibration when weak cocartesian morphisms are closed under composition. This follows via duality.
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-opfibration→opfibration wopfib weak-∘ = op-fibration→opfibration $ weak-fibration→fibration (ℰ ^total-op) (weak-opfibration→weak-op-fibration wopfib) (λ f g → weak-cocartesian→weak-co-cartesian $ weak-∘ (weak-co-cartesian→weak-cocartesian g) (weak-co-cartesian→weak-cocartesian f))
If
is cartesian, we can drop the requirement that weak cocartesian maps are
closed under composition, thanks to fibration+weak-cocartesian→cocartesian.
cartesian+weak-opfibration→opfibration : Cartesian-fibration ℰ → is-weak-cocartesian-fibration → Cocartesian-fibration 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 is a weak opfibration, then the hom sets and are equivalent, where is the codomain of the lift of along
module _ (wopfib : is-weak-cocartesian-fibration) where open is-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'}) 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')) 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
Furthermore, this equivalence is natural.
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') 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 a lifting of
objects Ob[ x ] → Ob[ y ] for every morphism
in
along with a equivalence of homs as above, then
is a weak opfibration.
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'))
module _ (U : ∀ {x y} → Hom x y → Functor (Fibre ℰ x) (Fibre ℰ y)) where open Functor open _=>_ 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 hom-iso→weak-opfibration hom-iso = vertical-equiv→weak-opfibration (λ u → U u .F₀) (λ u' → Isoⁿ.to (hom-iso _) .η _ u') (natural-iso-to-is-equiv (hom-iso _) _) λ f' g' → to-pathp⁻ $ happly (Isoⁿ.to (hom-iso _) .is-natural _ _ f') g'
module _ (opfib : Cocartesian-fibration) where open Cocartesian-fibration opfib open Indexing ℰ opfib opfibration→hom-iso-from : ∀ {x y x'} (u : Hom x y) → Hom-over-from ℰ u x' ≅ⁿ Hom-from (Fibre ℰ y) (has-lift.y' u x') opfibration→hom-iso-from u = weak-opfibration→hom-iso-from (opfibration→weak-opfibration opfib) u opfibration→hom-iso-into : ∀ {x y y'} (u : Hom x y) → Hom-over-into ℰ u y' ≅ⁿ Hom-into (Fibre ℰ y) y' F∘ Functor.op (cobase-change u) opfibration→hom-iso-into {y = y} {y' = y'} u = to-natural-iso mi where open make-natural-iso mi : make-natural-iso (Hom-over-into ℰ u y') (Hom-into (Fibre ℰ y) y' F∘ Functor.op (cobase-change u) ) mi .eta x u' = has-lift.universalv u x u' mi .inv x v' = hom[ idl u ] (v' ∘' has-lift.lifting u _) 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 $ smashl _ _ ·· revive₁ (pullr[] _ (has-lift.commutesv u _ _)) ·· smashr _ _ ·· weave _ (pulll (idl u)) _ (pulll[] _ (has-lift.commutesv u _ _)) ·· duplicate id-comm _ (idr u) opfibration→hom-iso : ∀ {x y} (u : Hom x y) → Hom-over ℰ u ≅ⁿ Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (cobase-change u) F× Id) opfibration→hom-iso {y = y} u = to-natural-iso mi where open make-natural-iso open _=>_ open Functor module into-iso {y'} = Isoⁿ (opfibration→hom-iso-into {y' = y'} u) module from-iso {x'} = Isoⁿ (opfibration→hom-iso-from {x' = x'} u) module Fibre {x} = CR (Fibre ℰ x) mi : make-natural-iso (Hom-over ℰ u) (Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (cobase-change u) F× Id)) mi .eta x u' = has-lift.universalv u _ u' mi .inv x v' = hom[ idl u ] (v' ∘' has-lift.lifting u _) 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' → Fibre.pulll (sym (happly (from-iso.to .is-natural _ _ v₂') u')) ·· sym (happly (into-iso.to .is-natural _ _ v₁') (hom[ idl _ ] (v₂' ∘' u'))) ·· ap (into-iso.to .η _) (smashl _ _ ∙ sym assoc[]) opfibration→universal-is-equiv : ∀ {x y x' y'} → (u : Hom x y) → is-equiv (has-lift.universalv u y' {x'}) opfibration→universal-is-equiv u = weak-opfibration→universal-is-equiv (opfibration→weak-opfibration opfib) u opfibration→vertical-equiv : ∀ {x y x' y'} → (u : Hom x y) → Hom[ u ] x' y' ≃ Hom[ id ] (has-lift.y' u x') y' opfibration→vertical-equiv u = weak-opfibration→vertical-equiv (opfibration→weak-opfibration opfib) u