module 1Lab.Equiv.HalfAdjoint whereAdjoint equivalences🔗
An adjoint equivalence is an isomorphism where the homotopies ( satisfy the triangle identities, thus witnessing and 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.
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
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
and
we can take the values provided by is-iso. However, if we want
to satisfy the triangle identities, we can not in general take
We can, however, alter it like thus:
ε' : (y : B) → f (g y) ≡ y
ε' y = sym (ε (f (g y))) ∙ ap f (η (g y)) ∙ ε yDrawn as a diagram, the path above factors like:
There is a great deal of redundancy in this definition, given that and have the same boundary! The point is that while the definition of is entirely opaque to us, is written in such a way that we can use properties of paths to make the and cancel:
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) ≡⟨ ∙-cancell (ε (f (g (f x)))) (ap f (η x)) ⟩
ap f (η x) ∎The notion of half-adjoint equivalence is a
useful stepping stone in writing a more comprehensible proof that isomorphisms are equivalences. 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 fibres, which will be used in proving
that half adjoint equivalences are equivalences.
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))The proof of this is not very enlightening, but it’s included here (rather than being completely invisible) for completeness:
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¡ (∙-idl _) ⟩
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'Then, given an element we can construct a fibre of of and, using the above characterisation of paths, prove that this fibre is a centre of contraction:
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 , ε yThe fibre is given by which we can prove identical to another using a very boring calculation:
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-∙ 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 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
and naturality of
lets us “push it past
”
to get something we can cancel:
ap (f ∘ g) (sym p) ∙ ap (f ∘ g) p ∙ ε y ≡⟨ ∙-assoc _ _ _ ⟩
⌜ ap (f ∘ g) (sym p) ∙ ap (f ∘ g) p ⌝ ∙ ε y ≡˘⟨ ap¡ (ap-∙ (f ∘ g) (sym p) p) ⟩
ap (f ∘ g) ⌜ sym p ∙ p ⌝ ∙ ε y ≡⟨ ap! (∙-invr _) ⟩
ap (f ∘ g) refl ∙ ε y ≡⟨⟩
refl ∙ ε y ≡⟨ ∙-idl (ε y) ⟩
ε y ∎Putting these together, we get an alternative definition of is-iso→is-equiv:
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_ = 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