module Homotopy.Conjugation where
Conjugation of paths🔗
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
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)
conj-refl : (l : x ≡ x) → conj refl l ≡ l conj-refl l = ∙-idr l conj-∙ : (p : x ≡ y) (q : y ≡ z) (r : x ≡ x) → conj q (conj p r) ≡ conj (p ∙ q) r conj-∙ p q r = ∙∙-stack
conj-of-refl : (p : y ≡ x) → conj p refl ≡ refl conj-of-refl p i j = hcomp (i ∨ ∂ j) λ where k (k = i0) → p k k (i = i1) → p k k (j = i0) → p k k (j = i1) → p k conj-of-∙ : (p : y ≡ x) (q r : y ≡ y) → conj p (q ∙ r) ≡ conj p q ∙ conj p r conj-of-∙ p q r = sym ∙∙-chain
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 square→conj : {p : y ≡ x} {q₁ : y ≡ y} {q₂ : x ≡ x} → Square p q₁ q₂ p → conj p q₁ ≡ q₂ square→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