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 = Cat.Displayed.Fibre.Reasoning ℰ
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
: ∀ {x'} → (g' : Hom[ f ] a' x') → Hom[ id ] b' x'
universal : ∀ {x'} → (g' : Hom[ f ] a' x') → universal g' ∘' f' ≡[ idl _ ] g'
commutes : ∀ {x'} {g' : Hom[ f ] a' x'}
unique → (h' : Hom[ id ] b' x')
→ h' ∘' f' ≡[ idl _ ] g'
→ h' ≡ universal g'
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.
.is-weak-cocartesian.universal =
weak-co-cartesian→weak-cocartesian wcart .universal wcart
is-weak-cartesian.is-weak-cocartesian.commutes =
weak-co-cartesian→weak-cocartesian wcart .commutes wcart
is-weak-cartesian.is-weak-cocartesian.unique =
weak-co-cartesian→weak-cocartesian wcart .unique wcart
is-weak-cartesian
.is-weak-cartesian.universal =
weak-cocartesian→weak-co-cartesian wcocart .universal wcocart
is-weak-cocartesian.is-weak-cartesian.commutes =
weak-cocartesian→weak-co-cartesian wcocart .commutes wcocart
is-weak-cocartesian.is-weak-cartesian.unique =
weak-cocartesian→weak-co-cartesian wcocart .unique wcocart is-weak-cocartesian
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''} (λ h' → hom[ idl _ ] (h' ∘' 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''} (λ h' → hom[ idl _ ] (h' ∘' 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 $(ℰ ^total-op)
weak-cartesian-domain-unique (weak-cocartesian→weak-co-cartesian f''-cocart)
(weak-cocartesian→weak-co-cartesian f'-cocart)
=
cocartesian→weak-cocartesian cocart
weak-co-cartesian→weak-cocartesian $(ℰ ^total-op) $
cartesian→weak-cartesian
cocartesian→co-cartesian cocart
=
weak-cocartesian→cocartesian opfib wcocart
co-cartesian→cocartesian $(ℰ ^total-op)
weak-cartesian→cartesian (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 (ℰ ^total-op) $
weak-cartesian→postcompose-equiv
weak-cocartesian→weak-co-cartesian cocart
.is-weak-cocartesian.universal v =
fibre-precompose-equiv→weak-cocartesian f' eqv
equiv→inverse eqv v.is-weak-cocartesian.commutes v =
fibre-precompose-equiv→weak-cocartesian f' eqv
to-pathp $ equiv→counit eqv v.is-weak-cocartesian.unique v p =
fibre-precompose-equiv→weak-cocartesian f' eqv (equiv→unit eqv v) ∙ ap (equiv→inverse eqv) (from-pathp p)
sym
=
weak-cocartesian→fibre-precompose-equiv wcocart
is-iso→is-equiv $
iso universal(λ v → from-pathp (commutes v))
(λ v → sym (unique v (to-pathp refl)))
where open is-weak-cocartesian wcocart
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'
{x} {y} {x'} {y'} {f} {f'} fib weak = cocart
fibration+weak-cocartesian→cocartesian 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.
Next, we can construct the morphism (highlighted in red) as the universal factorisation of through
module Morphisms {u} {u' : Ob[ u ]} (m : Hom y u) (h' : Hom[ m ∘ f ] x' u') where
: Hom[ f ] x' (m ^* u')
h* = π*.universal f h' h*
Finally, we can construct a vertical morphism as is weakly cartesian.
: Hom[ id ] y' (m ^* u')
h** = weak.universal h* h**
Composing and gives the desired factorisation.
: is-cocartesian f f'
cocart .is-cocartesian.universal m h' =
cocart _ ] (π* m _ ∘' h**)
hom[ idr where open Morphisms m h'
Showing that is best understood diagrammatically; both the and cells commute.
.is-cocartesian.commutes m h' =
cocart (π* m _ ∘' h**) ∘' f' ≡˘⟨ yank _ _ _ ⟩
hom[] _ ∘' hom[] (h** ∘' f') ≡⟨ ap (π* m _ ∘'_) (from-pathp (weak.commutes _)) ⟩
π* m _ ∘' π*.universal f h' ≡⟨ π*.commutes f h' ⟩
π* m
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.
.is-cocartesian.unique {u' = u'} {m = m} {h' = h'} m' p =
cocart (symP (π*.commutesp (idr _) m')) ⟩
m' ≡⟨ from-pathp⁻ (π* m u' ∘' id*) ≡⟨ hom[]⟩⟨ ap (π* m u' ∘'_) (weak.unique _ (to-pathp $ π*.unique _ path )) ⟩
hom[] (π* m u' ∘' h**) ∎
hom[] where
open Morphisms m h'
: Hom[ id ] y' (m ^* u')
id* = π*.universalv m'
id*
: π* m u' ∘' hom[ idl _ ] (id* ∘' f') ≡ h'
path =
path (id* ∘' f') ≡⟨ whisker-r _ ⟩
π* m u' ∘' hom[] (π* m u' ∘' id* ∘' f') ≡⟨ cancel _ (ap (m ∘_) (idl _)) (pulll' (idr _) (π*.commutesv m')) ⟩
hom[]
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 ]
: Hom[ f ] x' y'
lifting : is-weak-cocartesian f lifting
weak-cocartesian
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-cocartesian-lift.y' =
weak-co-cartesian-lift→weak-cocartesian-lift wlift .x' wlift
Weak-cartesian-lift.Weak-cocartesian-lift.lifting =
weak-co-cartesian-lift→weak-cocartesian-lift wlift .lifting wlift
Weak-cartesian-lift.Weak-cocartesian-lift.weak-cocartesian =
weak-co-cartesian-lift→weak-cocartesian-lift wlift (Weak-cartesian-lift.weak-cartesian wlift)
weak-co-cartesian→weak-cocartesian
.Weak-cartesian-lift.x' =
weak-cocartesian-lift→weak-co-cartesian-lift wlift .y' wlift
Weak-cocartesian-lift.Weak-cartesian-lift.lifting =
weak-cocartesian-lift→weak-co-cartesian-lift wlift .lifting wlift
Weak-cocartesian-lift.Weak-cartesian-lift.weak-cartesian =
weak-cocartesian-lift→weak-co-cartesian-lift wlift (Weak-cocartesian-lift.weak-cocartesian wlift) weak-cocartesian→weak-co-cartesian
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.
: Type _
Weak-cocartesian-fibration = ∀ {x y} → (f : Hom x y) → (x' : Ob[ x ]) → Weak-cocartesian-lift f x' Weak-cocartesian-fibration
module Weak-cocartesian-fibration (wfib : Weak-cocartesian-fibration) where
module _ {x y} (f : Hom x y) (x' : Ob[ x ]) where
open Weak-cocartesian-lift (wfib f x')
using ()
renaming (y' to _^!_; lifting to ι!)
public
module ι! {x y} {f : Hom x y} {x' : Ob[ x ]} where
open Weak-cocartesian-lift (wfib f x')
hiding (y'; lifting)
public
: ∀ {x y x' x''} → (f : Hom x y)
rebase → Hom[ id ] x' x''
→ Hom[ id ] (f ^! x') (f ^! x'')
=
rebase f vert .universal (hom[ idr _ ] (ι! f _ ∘' vert)) ι!
Weak cocartesian fibrations are dual to weak cartesian fibrations.
weak-op-fibration→weak-opfibration: Weak-cartesian-fibration (ℰ ^total-op)
→ Weak-cocartesian-fibration
weak-opfibration→weak-op-fibration: Weak-cocartesian-fibration
→ Weak-cartesian-fibration (ℰ ^total-op)
As usual, we omit the duality proofs, as they are quite tedious.
=
weak-op-fibration→weak-opfibration wlift f x'
weak-co-cartesian-lift→weak-cocartesian-lift $
wlift f x'
=
weak-opfibration→weak-op-fibration wlift f y'
weak-cocartesian-lift→weak-co-cartesian-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
→ Weak-cocartesian-fibration
.Weak-cocartesian-lift.y' =
cocartesian-lift→weak-cocartesian-lift cocart .y' cocart
Cocartesian-lift.Weak-cocartesian-lift.lifting =
cocartesian-lift→weak-cocartesian-lift cocart .lifting cocart
Cocartesian-lift.Weak-cocartesian-lift.weak-cocartesian =
cocartesian-lift→weak-cocartesian-lift cocart (Cocartesian-lift.cocartesian cocart)
cocartesian→weak-cocartesian
=
opfibration→weak-opfibration opfib f x' (opfib f x') cocartesian-lift→weak-cocartesian-lift
A weak opfibration is an opfibration when weak cocartesian morphisms are closed under composition. This follows via duality.
weak-opfibration→opfibration: 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 $(ℰ ^total-op)
weak-fibration→fibration (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
.
fibration+weak-opfibration→opfibration: Cartesian-fibration ℰ
→ Weak-cocartesian-fibration
→ Cocartesian-fibration
=
fibration+weak-opfibration→opfibration fib wlifts λ f-weak g-weak →
weak-opfibration→opfibration wlifts
cocartesian→weak-cocartesian $
cocartesian-∘(fibration+weak-cocartesian→cocartesian fib f-weak)
(fibration+weak-cocartesian→cocartesian fib g-weak)
fibration+weak-cocartesian-lift→cocartesian-lift: ∀ {x y} {f : Hom x y} {x'}
→ Cartesian-fibration ℰ
→ Weak-cocartesian-lift f x'
→ Cocartesian-lift f x'
{f = f} {x' = x'} fib wcocart =
fibration+weak-cocartesian-lift→cocartesian-lift record
{ lifting = lifting
; cocartesian = fibration+weak-cocartesian→cocartesian fib weak-cocartesian
}
where open Weak-cocartesian-lift wcocart
Weak cocartesian morphisms as left adjoints to base change🔗
Cobase change functors over a map are most naturally1 defined when is a cocartesian fibration, but they can be constructed as soon as admits a family of weak cocartesian lifts.
weak-cocartesian-lift→cobase-change: ∀ {x y}
→ (f : Hom x y)
→ (∀ x' → Weak-cocartesian-lift f x')
→ Functor (Fibre ℰ x) (Fibre ℰ y)
The reason that weak cocartesian lifts suffice is that we only need to consider vertical structure when performing cobase change, so the weaker universal property is enough. This is reflected in the action on morphisms, which is identical to the definition of cobase change for a cocartesian fibration.
{x = x} {y = y} f wcocart = f-cobase-change where
weak-cocartesian-lift→cobase-change module wcocart (x' : Ob[ x ]) where
open Weak-cocartesian-lift (wcocart x')
renaming (y' to f^!_; lifting to ι!)
public
open wcocart
: Functor (Fibre ℰ x) (Fibre ℰ y)
f-cobase-change .Functor.F₀ x' =
f-cobase-change
f^! x'.Functor.F₁ f' =
f-cobase-change _ (hom[ idr _ ] (ι! _ ∘' f')) universal
Functoriality follows from the fact that the universal map is unique, though this is rather tedious to show.
.Functor.F-id =
f-cobase-change _ _ $ cast[] $
sym $ unique _ ≡[]⟨ idl' _ ⟩
id' ∘' ι! _ ≡[]⟨ from-pathp⁻ (symP (idr' _)) ⟩
ι! (ι! _ ∘' id') ∎
hom[] .Functor.F-∘ f' g' =
f-cobase-change _ _ $ cast[] $
sym $ unique (universal _ (hom[ idr _ ] (ι! _ ∘' f')) Fib.∘ universal _ (hom[ idr _ ] (ι! _ ∘' g'))) ∘' ι! _
.pullrf (commutes _ _) ∙[] unwrapr (idr _) ⟩
≡[]⟨ Fib_ (hom[ idr f ] (ι! _ ∘' f')) ∘' (ι! _ ∘' g')
universal _ (commutes _ _) ∙[] unwrapl (idr _) ⟩
≡[]⟨ pulll[] (ι! _ ∘' f') ∘' g'
_ (wrap (idl _)) ∙[] wrap (idr _) ⟩
≡[]⟨ pullr[] (ι! _ ∘' f' Fib.∘ g')
hom[ idr f ] ∎
The existence of cobase change functors also provides an alternative universal property for weak cocartesian lifts when is a cartesian fibration, namely through the existence of left adjoints to each base change functor.
module _ (fib : Cartesian-fibration ℰ) where
open Cat.Displayed.Cartesian.Indexing ℰ fib
open Cartesian-fibration ℰ fib
left-adjoint→weak-cocartesian-lift: ∀ {x y}
→ (f : Hom x y)
→ (f^! : Functor (Fibre ℰ x) (Fibre ℰ y))
→ f^! ⊣ base-change f
→ ∀ x' → Weak-cocartesian-lift f x'
weak-cocartesian-lift→left-adjoint: ∀ {x y}
→ (f : Hom x y)
→ (f^! : ∀ x' → Weak-cocartesian-lift f x')
→ weak-cocartesian-lift→cobase-change f f^! ⊣ base-change f
We start by assuming that base change along each admits a left adjoint and showing that for each the object is the codomain of a cocartesian morphism over This map is obtained as the composite of the unit with the cartesian projection out of this latter object.
{y = y} f f^! f^!⊣f^* x' = f-lift where
left-adjoint→weak-cocartesian-lift module f^! = Functor f^!
open Weak-cocartesian-lift
open _⊣_ f^!⊣f^*
: Hom[ f ] x' (f^!.₀ x')
ι! = hom[ idr _ ] (π* f (f^!.F₀ x') ∘' η x')
ι!
: Weak-cocartesian-lift f x'
f-lift .y' = f^!.₀ x'
f-lift .lifting = ι! f-lift
We can prove that our putative lift is weakly cocartesian via a nice equivalence chase. First, recall that a morphism is weakly cocartesian iff. precomposition induces an equivalence on vertical maps. Moreover, the universal maps into a cartesian lift also assemble into an equivalence, so by 2-out-of-3 it suffices to show that the map taking a vertical to the dashed morphism in the diagram
is an equivalence. However, this map sends each to its left adjunct under the adjunction (up to transports), and assigning adjuncts is an equivalence!
.weak-cocartesian =
f-lift λ {y'} →
precompose-equiv→weak-cocartesian ι! $ (fibration→universal-is-equiv ℰ fib f) $
equiv-cancell (funext (coh y')) (L-adjunct-is-equiv f^!⊣f^*)
subst is-equiv where abstract
coh: ∀ y' (h' : Hom[ id ] (f^!.₀ x') y')
→ hom[ idl _ ] (π*.universal' id-comm (h' ∘' π* f _) ∘' η x')
.universalv (hom[ idl _ ] (h' ∘' ι!))
≡ π*=
coh y' h' .uniquep _ (idl _) (idr _) _ $
from-pathp $ π*.universal' _ (h' ∘' π* f (f^!.₀ x')) ∘' η x' ≡[]⟨ pulll[] _ (π*.commutesp id-comm _) ⟩
π* f y' ∘' π*(h' ∘' π* f (f^!.₀ x')) ∘' η x' ≡[]⟨ (pullr[] (idr _) (wrap (idr _)) ∙[] wrap (idl _)) ⟩
(h' ∘' ι!) ∎ hom[ idl f ]
The converse follows from some more equivalence yoga. First, recall that we can show by exhibiting a natural isomorphism But, by the universal properties of cartesian and cocartesian maps, respectively, these types are both equivalent to maps over
{x = x} {y = y} f wcocart = f-cobase-change-adj where weak-cocartesian-lift→left-adjoint
module wcocart (x' : Ob[ x ]) where
open Weak-cocartesian-lift (wcocart x')
renaming (y' to f^!_; lifting to ι!)
public
open wcocart
open _=>_
open _⊣_
: weak-cocartesian-lift→cobase-change f wcocart ⊣ base-change f
f-cobase-change-adj =
f-cobase-change-adj
hom-iso→adjoints(λ f' → π*.universalv (hom[ idl _ ] (f' ∘' ι! _)))
(∙-is-equiv (weak-cocartesian→precompose-equiv (weak-cocartesian _))
(fibration→universal-is-equiv ℰ fib f))
universalv-natural
All that remains is the naturality condition, which follows from some brute-force applications of the universal property of cartesian maps.
where abstract
universalv-natural: ∀ {x' x'' : Ob[ x ]} {y' y'' : Ob[ y ]}
→ (vy : Hom[ id ] y' y'') (vx : Hom[ id ] x' x'')
→ (f' : Hom[ id ] (f^! x'') y')
→ π*.universal' (idr f) (hom[ idl f ] ((vy Fib.∘ f' Fib.∘ universal x' (hom[ idr _ ] (ι! x'' ∘' vx))) ∘' ι! x'))
.universal' id-comm (vy ∘' π* f y') Fib.∘ π*.universal' (idr f) (hom[ idl _ ] (f' ∘' ι! x'')) Fib.∘ vx
≡ π*=
universalv-natural vy vx f' .uniquep₂ _ _ _ _ _
π*(π*.commutesv _
_
∙[] unwrap .pullrf (Fib.pullrf (commutes _ _)))
∙[] Fib(Fib.pulllf (π*.commutesp id-comm _)
.pulllf (pullr[] _ (π*.commutesv _))
∙[] Fib_ (unwrapl (idl f) ∙[] symP (assoc' _ _ _) ∙[] wrapr (idr f))) ∙[] pullr[]
Note that we can strengthen this result somewhat: every weak cocartesian lift in a fibration is in fact cocartesian, so left adjoints to base change give a family of cocartesian lifts.
module _
{x y} {f : Hom x y}
{f^! : Functor (Fibre ℰ x) (Fibre ℰ y)}
(f^!⊣f^* : f^! ⊣ base-change f)
where
private
module f^! = Cat.Functor.Reasoning f^!
open _⊣_ f^!⊣f^*
: ∀ x' → Cocartesian-lift f x'
left-adjoint→cocartesian-lift =
left-adjoint→cocartesian-lift x'
fibration+weak-cocartesian-lift→cocartesian-lift(left-adjoint→weak-cocartesian-lift f f^! f^!⊣f^* x') fib
Moreover, these choices of lifts are natural!
private
module f (x' : Ob[ x ]) where
open Cocartesian-lift (left-adjoint→cocartesian-lift x')
renaming (y' to ^!_; lifting to ι)
public
left-adjoint→cocartesian-lift-natural: ∀ {x' x''} (h' : Hom[ id ] x' x'')
→ f^!.₁ h' ∘' f.ι x' ≡[ id-comm-sym ] f.ι x'' ∘' h'
The proof is some unenlightening symbol shuffling, so we omit the details.
{x'} {x''} h' =
left-adjoint→cocartesian-lift-natural
cast[] $.₁ h' ∘' hom[] (π* f (f.^! x') ∘' η x')
f^!_ (unwrap (idr _)) ⟩
≡[]⟨ pushr[] (f^!.₁ h' ∘' π* f (f.^! x')) ∘' η x'
.pushlf (symP $ π*.commutesp id-comm _) ⟩
≡[]⟨ Fib(f.^! x'') ∘' π*.universal' id-comm (f^!.₁ h' ∘' π* f (f.^! x')) Fib.∘ η x'
π* f (refl⟩∘'⟨ unit.is-natural _ _ _) ⟩
≡[]˘⟨ (f.^! x'') ∘' (η x'' Fib.∘ h')
π* f .pulllf (wrap (idr _)) ⟩
≡[]⟨ Fib(π* f (f.^! x'') ∘' η x'') ∘' h' ∎ hom[]
We can also characterise the unit and counit of the adjunction in terms of the universal maps of (co)cartesian lifts.
left-adjoint→counit-cocartesian-universal: ∀ {y'} → ε y' ≡ f.universalv _ (π* f y')
left-adjoint→unit-cartesian-universal: ∀ {x'} → η x' ≡ π*.universalv (f.ι x')
These proofs are also mindless symbol shufflling, so we spare the reader the details.
{y'} =
left-adjoint→counit-cocartesian-universal .intror
Fib(f^!.annihilate
(π*.uniquep₂ _ _ _ _ _
(Fib.pulllf (π*.commutesp id-comm _)
(pullr[] _ (unwrapr _ ∙[] π*.commutesv _)
∙[] .commutesp (idl _) _))
∙[] π*(idr' _)))
.extendl (counit.is-natural (id ^* y') y' (π* id y'))
∙ Fib_ _
∙ expandr _ _
∙ reindex
=
left-adjoint→unit-cartesian-universal .uniquev (η _) (wrap (idr _)) π*
left-adjoint→counit-commutesv: ∀ {y'} → ε y' ∘' f.ι (f ^* y') ≡[ idl _ ] π* f y'
= cast[] $
left-adjoint→counit-commutesv _∘'_ left-adjoint→counit-cocartesian-universal refl
ap₂ .commutesv (f ^* _) (π* f _)
∙[] f
left-adjoint→unit-commutesv: ∀ {x'} → π* f (f.^! x') ∘' η x' ≡[ idr _ ] f.ι x'
= cast[] $
left-adjoint→unit-commutesv _∘'_ refl left-adjoint→unit-cartesian-universal
ap₂ .commutesv _ ∙[] π*
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 : Weak-cocartesian-fibration) where
open Weak-cocartesian-fibration wopfib
weak-opfibration→universal-is-equiv: ∀ {x y y' x'}
→ (u : Hom x y)
→ is-equiv (ι!.universal {f = u} {x' = x'} {y'})
{x' = x'} u =
weak-opfibration→universal-is-equiv
is-iso→is-equiv $(λ u' → hom[ idl u ] (u' ∘' ι! u x'))
iso (λ 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 ] (u ^! x') y'
{x' = x'} u =
weak-opfibration→vertical-equiv .universal , 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) (u ^! x')
{y = y} {x' = x'} u = to-natural-iso mi where
weak-opfibration→hom-iso-from open make-natural-iso
: 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' →
mi .unique _ (to-pathp refl)
sym $ ι!.inv∘eta _ = funext λ u' →
mi .commutes _
from-pathp $ ι!.natural _ _ v' = funext λ u' →
mi .unique _ $ to-pathp $
ι!_ _
smashl _ (ap (_∘ u) (idl id)) _ (pullr' _ (ι!.commutes _)) ∙ weave
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 _
to =
vertical-equiv-iso-natural ∀ {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)
→ Weak-cocartesian-fibration
to to-eqv natural =
vertical-equiv→weak-opfibration
weak-op-fibration→weak-opfibration $(ℰ ^total-op) _*₀_ to to-eqv λ f' g' →
vertical-equiv→weak-fibration (reindex _ _ ∙ from-pathp (natural g' f')) to-pathp
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'))
→ 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⁻ $
(Isoⁿ.to (hom-iso _) .is-natural _ _ f') g' happly
module _ (opfib : Cocartesian-fibration) where
open Cat.Displayed.Cocartesian.Indexing ℰ opfib
open Cocartesian-fibration opfib
opfibration→hom-iso-from: ∀ {x y x'} (u : Hom x y)
→ Hom-over-from ℰ u x' ≅ⁿ Hom-from (Fibre ℰ y) (u ^! x')
=
opfibration→hom-iso-from u (opfibration→weak-opfibration opfib) u
weak-opfibration→hom-iso-from
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)
{y = y} {y' = y'} u = to-natural-iso mi where
opfibration→hom-iso-into open make-natural-iso
: make-natural-iso
mi (Hom-over-into ℰ u y')
(Hom-into (Fibre ℰ y) y' F∘ Functor.op (cobase-change u) )
.eta x u' = ι!.universalv u'
mi .inv x v' = hom[ idl u ] (v' ∘' ι! u _)
mi .eta∘inv x = funext λ v' →
mi .uniquev _ (to-pathp refl)
sym $ ι!.inv∘eta x = funext λ u' →
mi (ι!.commutesv _)
from-pathp .natural _ _ v' = funext λ u' →
mi .unique _ $ to-pathp $
ι!_ _
smashl (pullr[] _ (ι!.commutesv _))
∙∙ revive₁ _ _
∙∙ smashr _ (pulll (idl u)) _ (pulll[] _ (ι!.commutesv _))
∙∙ weave _ (idr u)
∙∙ duplicate id-comm
opfibration→hom-iso: ∀ {x y} (u : Hom x y)
→ Hom-over ℰ u ≅ⁿ Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (cobase-change u) F× Id)
{y = y} u = to-natural-iso mi where
opfibration→hom-iso 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)
: make-natural-iso
mi (Hom-over ℰ u)
(Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (cobase-change u) F× Id))
.eta x u' = ι!.universalv u'
mi .inv x v' = hom[ idl u ] (v' ∘' ι! u _)
mi .eta∘inv x = funext λ v' →
mi .uniquev _ (to-pathp refl)
sym $ ι!.inv∘eta x = funext λ u' →
mi (ι!.commutesv _)
from-pathp .natural _ _ (v₁' , v₂') = funext λ u' →
mi .pulll (sym (happly (from-iso.to .is-natural _ _ v₂') u'))
Fibre(happly (into-iso.to .is-natural _ _ v₁') (hom[ idl _ ] (v₂' ∘' u')))
∙∙ sym (into-iso.to .η _) (smashl _ _ ∙ sym assoc[])
∙∙ ap
opfibration→universal-is-equiv: ∀ {x y x' y'}
→ (u : Hom x y)
→ is-equiv (ι!.universalv {f = u} {x' = x'} {y'})
=
opfibration→universal-is-equiv u (opfibration→weak-opfibration opfib) u
weak-opfibration→universal-is-equiv
opfibration→vertical-equiv: ∀ {x y x' y'}
→ (u : Hom x y)
→ Hom[ u ] x' y' ≃ Hom[ id ] (u ^! x') y'
=
opfibration→vertical-equiv u (opfibration→weak-opfibration opfib) u weak-opfibration→vertical-equiv
Note that these functors are only well-behaved if is in fact cocartesian, so this is only a slight generalisation.↩︎