/
Fibrewise.lagda.md
93 lines (78 loc) · 2.67 KB
/
Fibrewise.lagda.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
---
description: |
We establish a correspondence between "fibrewise equivalences" and
equivalences of total spaces (Σ-types).
---
<!--
```agda
open import 1Lab.HLevel.Closure
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type
```
-->
```agda
module 1Lab.Equiv.Fibrewise where
```
# Fibrewise equivalences
In HoTT, a type family `P : A → Type` can be seen as a [_fibration_]
with total space `Σ P`, with the fibration being the projection
`fst`{.Agda}. Because of this, a function with type `(X : _) → P x → Q
x` can be referred as a _fibrewise map_.
[_fibration_]: https://ncatlab.org/nlab/show/fibration
A function like this can be lifted to a function on total spaces:
<!--
```
private variable
ℓ : Level
A B : Type ℓ
P Q : A → Type ℓ
```
-->
```agda
total : ((x : A) → P x → Q x)
→ Σ A P → Σ A Q
total f (x , y) = x , f x y
```
Furthermore, the fibres of `total f` correspond to fibres of f, in the
following manner:
```agda
total-fibres : {f : (x : A) → P x → Q x} {x : A} {v : Q x}
→ Iso (fibre (f x) v) (fibre (total f) (x , v))
total-fibres {A = A} {P = P} {Q = Q} {f = f} {x = x} {v = v} = the-iso where
open is-iso
to : {x : A} {v : Q x} → fibre (f x) v → fibre (total f) (x , v)
to (v' , p) = (_ , v') , λ i → _ , p i
from : {x : A} {v : Q x} → fibre (total f) (x , v) → fibre (f x) v
from ((x , v) , p) = transport (λ i → fibre (f (p i .fst)) (p i .snd)) (v , refl)
the-iso : {x : A} {v : Q x} → Iso (fibre (f x) v) (fibre (total f) (x , v))
the-iso .fst = to
the-iso .snd .is-iso.inv = from
the-iso .snd .is-iso.rinv ((x , v) , p) =
J (λ { _ p → to (from ((x , v) , p)) ≡ ((x , v) , p) })
(ap to (J-refl {A = Σ A Q} (λ { (x , v) _ → fibre (f x) v } ) (v , refl)))
p
the-iso .snd .is-iso.linv (v , p) =
J (λ { _ p → from (to (v , p)) ≡ (v , p) })
(J-refl {A = Σ A Q} (λ { (x , v) _ → fibre (f x) v } ) (v , refl))
p
```
From this, we immediately get that a fibrewise transformation is an
equivalence iff. it induces an equivalence of total spaces by `total`.
```agda
total→equiv : {f : (x : A) → P x → Q x}
→ is-equiv (total f)
→ {x : A} → is-equiv (f x)
total→equiv eqv {x} .is-eqv y =
iso→is-hlevel 0 (total-fibres .snd .is-iso.inv)
(is-iso.inverse (total-fibres .snd))
(eqv .is-eqv (x , y))
equiv→total : {f : (x : A) → P x → Q x}
→ ({x : A} → is-equiv (f x))
→ is-equiv (total f)
equiv→total always-eqv .is-eqv y =
iso→is-hlevel 0
(total-fibres .fst)
(total-fibres .snd)
(always-eqv .is-eqv (y .snd))
```