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 .inv  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)