{-# 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,Ξ·,Ξ΅)(f, g, \eta, \varepsilon) where the homotopies (Ξ·\eta, Ξ΅\varepsilon) satisfy the triangle identities, thus witnessing ff and gg 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 ∞\infty-groupoids.

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 gg and Ξ·\eta, we can take the values provided by is-iso. 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:

    Ξ΅' : (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:

There is a great deal of redundancy in this definition, given that Ξ΅y\varepsilon y and Ξ΅β€²y\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 symΒ (Ξ΅...)\id{sym}\ (\varepsilon ...) and Ξ΅\varepsilon 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)  β‰‘βŸ¨ βˆ™-cancel-l (Ξ΅ (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Β‘ (βˆ™-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'

Then, given an element y:By : B, we can construct a fibre of of ff, 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 , Ξ΅ y

The fibre is given by (g(y),Ξ΅(y))(g(y), Ξ΅(y)), which we can prove identical to another (x,p)(x, p) 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-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 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 ap(f)(Ξ·x)=Ξ΅(fx)\id{ap}(f)(\eta x) = \varepsilon(f x), and naturality of Ξ΅\varepsilon lets us β€œpush it past pp” 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-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:

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