# Conjugation of loops

Content created by Egbert Rijke.

Created on 2023-07-19.

module synthetic-homotopy-theory.conjugation-loops where

Imports
open import foundation.dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels

open import structured-types.pointed-homotopies
open import structured-types.pointed-maps

open import synthetic-homotopy-theory.loop-spaces


## Idea

For any identification p : x ＝ y in a type A there is an conjugation action Ω (A , x) →∗ Ω (A , y) on loop spaces, which is the pointed map given by ω ↦ p⁻¹ωp.

## Definition

### The standard definition of conjugation on loop spaces

module _
{l : Level} {A : UU l}
where

map-conjugation-Ω : {x y : A} (p : x ＝ y) → type-Ω (A , x) → type-Ω (A , y)
map-conjugation-Ω p ω = inv p ∙ (ω ∙ p)

preserves-point-conjugation-Ω :
{x y : A} (p : x ＝ y) → map-conjugation-Ω p refl ＝ refl
preserves-point-conjugation-Ω p = left-inv p

conjugation-Ω : {x y : A} (p : x ＝ y) → Ω (A , x) →∗ Ω (A , y)
pr1 (conjugation-Ω p) = map-conjugation-Ω p
pr2 (conjugation-Ω p) = preserves-point-conjugation-Ω p


### A second definition of conjugation on loop spaces

module _
{l : Level} {A : UU l}
where

conjugation-Ω' : {x y : A} (p : x ＝ y) → Ω (A , x) →∗ Ω (A , y)
conjugation-Ω' refl = id-pointed-map

map-conjugation-Ω' : {x y : A} (p : x ＝ y) → type-Ω (A , x) → type-Ω (A , y)
map-conjugation-Ω' p = map-pointed-map (conjugation-Ω' p)

preserves-point-conjugation-Ω' :
{x y : A} (p : x ＝ y) → map-conjugation-Ω' p refl ＝ refl
preserves-point-conjugation-Ω' p =
preserves-point-pointed-map (conjugation-Ω' p)


## Properties

### The two definitions of conjugation on loop spaces are pointed homotopic

module _
{l : Level} {A : UU l}
where

htpy-compute-conjugation-Ω :
{x y : A} (p : x ＝ y) → map-conjugation-Ω p ~ map-conjugation-Ω' p
htpy-compute-conjugation-Ω refl ω = right-unit

coherence-point-compute-conjugation-Ω :
{x y : A} (p : x ＝ y) →
coherence-point-unpointed-htpy-pointed-Π
( conjugation-Ω p)
( conjugation-Ω' p)
( htpy-compute-conjugation-Ω p)
coherence-point-compute-conjugation-Ω refl = refl

compute-conjugation-Ω :
{x y : A} (p : x ＝ y) → conjugation-Ω p ~∗ conjugation-Ω' p
pr1 (compute-conjugation-Ω p) = htpy-compute-conjugation-Ω p
pr2 (compute-conjugation-Ω p) = coherence-point-compute-conjugation-Ω p