Skip to content

Commit

Permalink
refactor: banish wrapper records from weak (co)cartesian fibrations
Browse files Browse the repository at this point in the history 
I also removed some bad 'is-' prefixes
  • Loading branch information
@TOTBWF
TOTBWF committed Feb 8, 2025
1 parent 632648a commit ced3fa3
Show file tree
Hide file tree
Showing 3 changed files with 125 additions and 145 deletions.
176 changes: 76 additions & 100 deletions src/Cat/Displayed/Cartesian/Weak.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
```

<!--
```agda
module _ {x y} (f : Hom x y) (y' : Ob[ y ]) where
open Weak-cartesian-lift (wfib f y')
using ()
renaming (x' to _^*_; lifting to π*)
public

module weak-lift {x y} (f : Hom x y) (y' : Ob[ y ]) =
Weak-cartesian-lift (weak-lift f y')
module π* {x y} {f : Hom x y} {y' : Ob[ y ]} where
open Weak-cartesian-lift (wfib f y')
hiding (x'; lifting)
public
```
-->

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
Expand All @@ -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.
Expand All @@ -250,7 +262,7 @@ cartesian-lift→weak-cartesian-lift

fibration→weak-fibration
: Cartesian-fibration
→ is-weak-cartesian-fibration
→ Weak-cartesian-fibration
```

<details>
Expand All @@ -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')
```
</details>
Expand All @@ -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
Expand All @@ -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:
Expand Down Expand Up @@ -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')
```

<details>
Expand All @@ -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' ∎
```
</details>

Expand All @@ -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') ∎
```
</details>

Expand All @@ -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
```

Expand All @@ -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'
```
Expand All @@ -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
Expand All @@ -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
```

Expand All @@ -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
Expand All @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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₀)
Expand Down
Loading

0 comments on commit ced3fa3

Please sign in to comment.