-
Notifications
You must be signed in to change notification settings - Fork 63
/
HalfAdjoint.lagda.md
217 lines (189 loc) · 8.85 KB
/
HalfAdjoint.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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
---
description: |
We formalise the theory of _half-adjoint equivalences_, another
well-behaved alternative to the notion of isomorphism. Then, we use
half-adjoint equivalences as a stepping stone to show that
isomorphisms are equivalences.
---
```agda
{-# OPTIONS -vtc.def.fun:10 #-}
open import 1Lab.Reflection.Marker
open import 1Lab.HLevel.Retracts
open import 1Lab.Path.Groupoid
open import 1Lab.Equiv.Biinv
open import 1Lab.Type.Sigma
open import 1Lab.Univalence
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type
module 1Lab.Equiv.HalfAdjoint where
```
# Adjoint Equivalences
An **adjoint equivalence** is an [isomorphism] $(f, g, \eta,
\varepsilon)$ where the [homotopies] ($\eta$, $\varepsilon$) satisfy the
[triangle identities], thus witnessing $f$ and $g$ as [adjoint
functors]. In Homotopy Type Theory, we can use a _half_ adjoint
equivalence - satisfying only _one_ of the triangle identities - as a
[good notion of equivalence].
[isomorphism]: 1Lab.Equiv.html#isomorphisms-from-equivalences
[homotopies]: 1Lab.Path.html#π-types
[triangle identities]: https://ncatlab.org/nlab/show/triangle+identities
[adjoint functors]: https://ncatlab.org/nlab/show/adjoint+functor
[good notion of equivalence]: 1Lab.Equiv.html#equivalences
```agda
is-half-adjoint-equiv : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂} (f : A → B) → Type _
is-half-adjoint-equiv {A = A} {B = B} f =
Σ[ g ∈ (B → A) ]
Σ[ η ∈ ((x : A) → g (f x) ≡ x) ]
Σ[ ε ∈ ((y : B) → f (g y) ≡ y) ]
((x : A) → ap f (η x) ≡ ε (f x))
```
The argument is an adaptation of a standard result of both category
theory and homotopy theory - where we can "improve" an equivalence of
categories into an adjoint equivalence, or a homotopy equivalence into a
strong homotopy equivalence (Vogt's lemma). In HoTT, we show this
synthetically for equivalences between $\infty$-groupoids.
```agda
is-iso→is-half-adjoint-equiv
: ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂} {f : A → B}
→ is-iso f → is-half-adjoint-equiv f
is-iso→is-half-adjoint-equiv {A = A} {B} {f} iiso =
g , η , ε' , λ x → sym (zig x)
where
open is-iso iiso renaming (inv to g ; linv to η ; rinv to ε)
```
For $g$ and $\eta$, we can take the values provided by `is-iso`{.Agda}.
However, if we want $(\eta, \varepsilon)$ to satisfy the triangle
identities, we can not in general take $\varepsilon' = \varepsilon$. We
can, however, alter it like thus:
```agda
ε' : (y : B) → f (g y) ≡ y
ε' y = sym (ε (f (g y))) ∙ ap f (η (g y)) ∙ ε y
```
Drawn as a diagram, the path above factors like:
~~~{.quiver}
\[\begin{tikzcd}
{f(g(y))} && y \\
{f(g(f(g(y))))} && {f(g(y))}
\arrow["{\id{sym}\ (\varepsilon(f(g(y))))}"', from=1-1, to=2-1]
\arrow["{\id{ap}\ f\ (\eta(g(y)))}"', from=2-1, to=2-3]
\arrow["{\varepsilon \ y}"', from=2-3, to=1-3]
\arrow["{\varepsilon'\ y}", dashed, from=1-1, to=1-3]
\end{tikzcd}\]
~~~
There is a great deal of redundancy in this definition, given that
$\varepsilon y$ and $\varepsilon' y$ have the same boundary! The point
is that while the definition of $\varepsilon$ is entirely opaque to us,
$\varepsilon'$ is written in such a way that we can use properties of
paths to make the $\id{sym}\ (\varepsilon ...)$ and $\varepsilon$
cancel:
```agda
zig : (x : A) → ε' (f x) ≡ ap f (η x)
zig x =
ε' (f x) ≡⟨⟩
sym (ε (f (g (f x)))) ∙ ap f ⌜ (η (g (f x))) ⌝ ∙ ε (f x) ≡⟨ ap (λ e → sym (ε _) ∙ ap f e ∙ ε _) (homotopy-invert η) ⟩
sym (ε (f (g (f x)))) ∙ ⌜ ap (f ∘ g ∘ f) (η x) ∙ ε (f x) ⌝ ≡˘⟨ ap¡ (homotopy-natural ε _) ⟩
sym (ε (f (g (f x)))) ∙ ε (f (g (f x))) ∙ ap f (η x) ≡⟨ ∙-cancel-l (ε (f (g (f x)))) (ap f (η x)) ⟩
ap f (η x) ∎
```
The notion of `half-adjoint equivalence`{.Agda ident=is-half-adjoint-equiv} is a useful
stepping stone in writing a more comprehensible proof that `isomorphisms
are equivalences`{.Agda ident=Iso→Equiv}. Since this result is
fundamental, the proof we actually use is written with efficiency of
computation in mind - hence, cubically. The proof here is intended to be
more educational.
First, we give an equivalent characterisation of paths in
`fibre`{.Agda}s, which will be used in proving that `half adjoint
equivalences are equivalences`{.Agda ident=is-half-adjoint-equiv→is-equiv}.
```agda
fibre-paths : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂} {f : A → B} {y : B}
→ {f1 f2 : fibre f y}
→ (f1 ≡ f2)
≃ (Σ[ γ ∈ f1 .fst ≡ f2 .fst ] (ap f γ ∙ f2 .snd ≡ f1 .snd))
```
<details>
<summary>The proof of this is not very enlightening, but it's included
here (rather than being completely invisible) for
completeness:</summary>
```
fibre-paths {f = f} {y} {f1} {f2} =
Path (fibre f y) f1 f2 ≃⟨ Iso→Equiv Σ-path-iso e⁻¹ ⟩
(Σ[ γ ∈ f1 .fst ≡ f2 .fst ] (subst (λ x₁ → f x₁ ≡ _) γ (f1 .snd) ≡ f2 .snd)) ≃⟨ Σ-ap-snd (λ x → path→equiv (lemma x)) ⟩
(Σ[ γ ∈ f1 .fst ≡ f2 .fst ] (ap f γ ∙ f2 .snd ≡ f1 .snd)) ≃∎
where
helper : (p' : f (f1 .fst) ≡ y)
→ (subst (λ x → f x ≡ y) refl (f1 .snd) ≡ p')
≡ (ap f refl ∙ p' ≡ f1 .snd)
helper p' =
subst (λ x → f x ≡ y) refl (f1 .snd) ≡ p' ≡⟨ ap₂ _≡_ (transport-refl _) refl ⟩
(f1 .snd) ≡ p' ≡⟨ Iso→Path (sym , iso sym (λ x → refl) (λ x → refl)) ⟩
⌜ p' ⌝ ≡ f1 .snd ≡˘⟨ ap¡ (∙-id-l _) ⟩
refl ∙ p' ≡ f1 .snd ≡⟨⟩
ap f refl ∙ p' ≡ f1 .snd ∎
lemma : ∀ {x'} {p'} → (γ : f1 .fst ≡ x')
→ (subst (λ x → f x ≡ _) γ (f1 .snd) ≡ p')
≡ (ap f γ ∙ p' ≡ f1 .snd)
lemma {x'} {p'} p =
J (λ x' γ → ∀ p' → (subst (λ x → f x ≡ _) γ (f1 .snd) ≡ p')
≡ (ap f γ ∙ p' ≡ f1 .snd))
helper p p'
```
</details>
Then, given an element $y : B$, we can construct a fibre of of $f$, and,
using the above characterisation of paths, prove that this fibre is a
centre of contraction:
```agda
is-half-adjoint-equiv→is-equiv
: ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂} {f : A → B}
→ is-half-adjoint-equiv f → is-equiv f
is-half-adjoint-equiv→is-equiv {A = A} {B} {f} (g , η , ε , zig) .is-eqv y = contr fib contract where
fib : fibre f y
fib = g y , ε y
```
The fibre is given by $(g(y), ε(y))$, which we can prove identical to
another $(x, p)$ using a very boring calculation:
```agda
contract : (fib₂ : fibre f y) → fib ≡ fib₂
contract (x , p) = (fibre-paths e⁻¹) .fst (x≡gy , path) where
x≡gy = ap g (sym p) ∙ η x
path : ap f (ap g (sym p) ∙ η x) ∙ p ≡ ε y
path =
ap f (ap g (sym p) ∙ η x) ∙ p ≡⟨ ap₂ _∙_ (ap-comp-path f (ap g (sym p)) (η x)) refl ∙ sym (∙-assoc _ _ _) ⟩
ap (λ x → f (g x)) (sym p) ∙ ⌜ ap f (η x) ⌝ ∙ p ≡⟨ ap! (zig _) ⟩ -- by the triangle identity
ap (f ∘ g) (sym p) ∙ ⌜ ε (f x) ∙ p ⌝ ≡⟨ ap! (homotopy-natural ε p) ⟩ -- by naturality of ε
```
The calculation of `path`{.Agda} factors as a bunch of boring
adjustments to paths using the groupoid structure of types, and the two
interesting steps above: The triangle identity says that
$\id{ap}(f)(\eta x) = \varepsilon(f x)$, and naturality of
$\varepsilon$ lets us "push it past $p$" to get something we can cancel:
```agda
ap (f ∘ g) (sym p) ∙ ap (f ∘ g) p ∙ ε y ≡⟨ ∙-assoc _ _ _ ⟩
⌜ ap (f ∘ g) (sym p) ∙ ap (f ∘ g) p ⌝ ∙ ε y ≡˘⟨ ap¡ (ap-comp-path (f ∘ g) (sym p) p) ⟩
ap (f ∘ g) ⌜ sym p ∙ p ⌝ ∙ ε y ≡⟨ ap! (∙-inv-r _) ⟩
ap (f ∘ g) refl ∙ ε y ≡⟨⟩
refl ∙ ε y ≡⟨ ∙-id-l (ε y) ⟩
ε y ∎
```
Putting these together, we get an alternative definition of
`is-iso→is-equiv`{.Agda}:
```agda
is-iso→is-equiv'
: ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂} {f : A → B}
→ is-iso f → is-equiv f
is-iso→is-equiv' = is-half-adjoint-equiv→is-equiv ∘ is-iso→is-half-adjoint-equiv
```
<!--
```agda
_ = is-iso→is-equiv
is-equiv→is-half-adjoint-equiv
: ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂} {f : A → B}
→ is-equiv f → is-half-adjoint-equiv f
is-equiv→is-half-adjoint-equiv {f = f} eqv =
equiv→inverse eqv
, equiv→unit eqv
, equiv→counit eqv
, equiv→zig eqv
```
-->