open import 1Lab.Prelude
module Homotopy.Conjugation where

Conjugation of pathsπŸ”—

private variable
  β„“ : Level
  A : Type β„“
  x y z : A
  p q r : x ≑ y

open is-iso

In any type for which we know two points the existence of any identification induces an equivalence between the loop spaces and given by transport in the usual way. However, since we know ahead-of-time what transport in a type of paths computes to, we can take a short-cut and define the equivalence directly: it is given by conjugation with 

opaque
  conj : βˆ€ {β„“} {A : Type β„“} {x y : A} β†’ y ≑ x β†’ y ≑ y β†’ x ≑ x
  conj p q = sym p βˆ™βˆ™ q βˆ™βˆ™ p
opaque
  unfolding conj
  conj-defn : (p : y ≑ x) (q : y ≑ y) β†’ conj p q ≑ sym p βˆ™ q βˆ™ p
  conj-defn p q = double-composite (sym p) q p

  conj-defn' : (p : y ≑ x) (q : y ≑ y) β†’ conj p q ≑ subst (Ξ» x β†’ x ≑ x) p q
  conj-defn' p q = conj-defn p q βˆ™ sym (subst-path-both q p)
opaque
  conj-refl : (l : x ≑ x) β†’ conj refl l ≑ l
  conj-refl l = conj-defn _ _ βˆ™βˆ™ βˆ™-idl _ βˆ™βˆ™ βˆ™-idr _

  conj-βˆ™ : (p : x ≑ y) (q : y ≑ z) (r : x ≑ x)
            β†’ conj q (conj p r) ≑ conj (p βˆ™ q) r
  conj-βˆ™ p q r = transport
    (Ξ» i β†’ conj-defn' q (conj-defn' p r (~ i)) (~ i) ≑ conj-defn' (p βˆ™ q) r (~ i))
    (sym (subst-βˆ™ (Ξ» x β†’ x ≑ x) p q r))
  conj-of-refl : (p : y ≑ x) β†’ conj p refl ≑ refl
  conj-of-refl p = conj-defn _ _ βˆ™βˆ™ ap (sym p βˆ™_) (βˆ™-idl p) βˆ™βˆ™ βˆ™-invl p

  conj-of-βˆ™ : (p : y ≑ x) (q r : y ≑ y) β†’ conj p (q βˆ™ r) ≑ conj p q βˆ™ conj p r
  conj-of-βˆ™ = J (Ξ» x p β†’ βˆ€ q r β†’ conj p (q βˆ™ r) ≑ conj p q βˆ™ conj p r) Ξ» q r β†’
    conj-refl (q βˆ™ r) βˆ™ apβ‚‚ _βˆ™_ (sym (conj-refl q)) (sym (conj-refl r))
opaque
  unfolding conj

  ap-conj
    : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} {x y : A}
    β†’ (f : A β†’ B) (p : y ≑ x) (q : y ≑ y)
    β†’ ap f (conj p q) ≑ conj (ap f p) (ap f q)
  ap-conj f p q = ap-βˆ™βˆ™ f _ _ _
opaque
  conj⁻conj : conj (sym p) (conj p q) ≑ q
  conj⁻conj {p = p} {q = q} =
       ap (conj _) (conj-defn' _ _)
    βˆ™βˆ™ conj-defn' _ _
    βˆ™βˆ™ transport⁻transport (Ξ» i β†’ p i ≑ p i) q
opaque
  pathp→conj
    : {p : y ≑ x} {q₁ : y ≑ y} {qβ‚‚ : x ≑ x}
    β†’ PathP (Ξ» i β†’ p i ≑ p i) q₁ qβ‚‚ β†’ conj p q₁ ≑ qβ‚‚
  pathpβ†’conj p = conj-defn' _ _ βˆ™ from-pathp p
opaque
  conj-commutative : {p q : x ≑ x} β†’ q βˆ™ p ≑ p βˆ™ q β†’ conj p q ≑ q
  conj-commutative Ξ± = conj-defn _ _ βˆ™βˆ™ apβ‚‚ _βˆ™_ refl Ξ± βˆ™βˆ™ βˆ™-cancell _ _
conj-is-iso : (p : y ≑ x) β†’ is-iso (conj p)
conj-is-iso p .from q = conj (sym p) q
conj-is-iso p .rinv q = conj⁻conj
conj-is-iso p .linv q = conj⁻conj
opaque
  conj-is-equiv : (p : y ≑ x) β†’ is-equiv (conj p)
  conj-is-equiv p = is-iso→is-equiv (conj-is-iso p)

module conj {β„“} {A : Type β„“} {x y : A} (p : y ≑ x) = Equiv (conj p , conj-is-equiv p)