# Involutions

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Elisabeth Stenholm and Eléonore Mangel.

Created on 2022-03-05.

module foundation.involutions where

Imports
open import foundation.automorphisms
open import foundation.dependent-pair-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopy-algebra
open import foundation.homotopy-induction
open import foundation.structure-identity-principle
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.torsorial-type-families
open import foundation-core.truncated-types
open import foundation-core.truncation-levels

open import structured-types.pointed-types


## Idea

An involution on a type A is a map f : A → A such that (f ∘ f) ~ id.

## Definition

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

is-involution : (A → A) → UU l
is-involution f = (f ∘ f) ~ id

is-involution-aut : Aut A → UU l
is-involution-aut e = is-involution (map-equiv e)


### The type of involutions on A

involution : {l : Level} → UU l → UU l
involution A = Σ (A → A) is-involution

module _
{l : Level} {A : UU l} (f : involution A)
where

map-involution : A → A
map-involution = pr1 f

is-involution-map-involution : is-involution map-involution
is-involution-map-involution = pr2 f


## Properties

### Involutions are equivalences

is-equiv-is-involution :
{l : Level} {A : UU l} {f : A → A} → is-involution f → is-equiv f
is-equiv-is-involution {f = f} is-involution-f =
is-equiv-is-invertible f is-involution-f is-involution-f

is-equiv-map-involution :
{l : Level} {A : UU l} (f : involution A) → is-equiv (map-involution f)
is-equiv-map-involution = is-equiv-is-involution ∘ is-involution-map-involution

equiv-is-involution :
{l : Level} {A : UU l} {f : A → A} → is-involution f → A ≃ A
pr1 (equiv-is-involution {f = f} is-involution-f) = f
pr2 (equiv-is-involution is-involution-f) =
is-equiv-is-involution is-involution-f

equiv-involution :
{l : Level} {A : UU l} → involution A → A ≃ A
equiv-involution f =
equiv-is-involution {f = map-involution f} (is-involution-map-involution f)


### Involutions are their own inverse

htpy-own-inverse-is-involution :
{l : Level} {A : UU l} {f : Aut A} →
is-involution-aut f → map-inv-equiv f ~ map-equiv f
htpy-own-inverse-is-involution {f = f} is-involution-f x =
is-injective-equiv f
( htpy-eq-equiv (right-inverse-law-equiv f) x ∙
inv (is-involution-f x))

own-inverse-is-involution :
{l : Level} {A : UU l} {f : Aut A} →
is-involution-aut f → inv-equiv f ＝ f
own-inverse-is-involution {f = f} =
eq-htpy-equiv ∘ htpy-own-inverse-is-involution {f = f}


### Characterizing equality of involutions

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

coherence-htpy-involution :
(s t : involution A) → map-involution s ~ map-involution t → UU l
coherence-htpy-involution s t H =
( is-involution-map-involution s) ~
( horizontal-concat-htpy H H ∙h is-involution-map-involution t)

htpy-involution : (s t : involution A) → UU l
htpy-involution s t =
Σ ( map-involution s ~ map-involution t)
( coherence-htpy-involution s t)

refl-htpy-involution : (s : involution A) → htpy-involution s s
pr1 (refl-htpy-involution s) = refl-htpy
pr2 (refl-htpy-involution s) = refl-htpy

htpy-eq-involution : (s t : involution A) → s ＝ t → htpy-involution s t
htpy-eq-involution s .s refl = refl-htpy-involution s

is-torsorial-htpy-involution :
(s : involution A) → is-torsorial (htpy-involution s)
is-torsorial-htpy-involution s =
is-torsorial-Eq-structure
( is-torsorial-htpy (map-involution s))
( map-involution s , refl-htpy)
( is-torsorial-htpy (is-involution-map-involution s))

is-equiv-htpy-eq-involution :
(s t : involution A) → is-equiv (htpy-eq-involution s t)
is-equiv-htpy-eq-involution s =
fundamental-theorem-id
( is-torsorial-htpy-involution s)
( htpy-eq-involution s)

extensionality-involution :
(s t : involution A) → (s ＝ t) ≃ (htpy-involution s t)
pr1 (extensionality-involution s t) = htpy-eq-involution s t
pr2 (extensionality-involution s t) = is-equiv-htpy-eq-involution s t

eq-htpy-involution : (s t : involution A) → htpy-involution s t → s ＝ t
eq-htpy-involution s t = map-inv-equiv (extensionality-involution s t)


### If A is k-truncated then the type of involutions is k-truncated

is-trunc-is-involution :
{l : Level} (k : 𝕋) {A : UU l} →
is-trunc (succ-𝕋 k) A → (f : A → A) → is-trunc k (is-involution f)
is-trunc-is-involution k is-trunc-A f =
is-trunc-Π k λ x → is-trunc-A (f (f x)) x

is-involution-Truncated-Type :
{l : Level} (k : 𝕋) {A : UU l} →
is-trunc (succ-𝕋 k) A → (A → A) → Truncated-Type l k
pr1 (is-involution-Truncated-Type k is-trunc-A f) = is-involution f
pr2 (is-involution-Truncated-Type k is-trunc-A f) =
is-trunc-is-involution k is-trunc-A f

is-trunc-involution :
{l : Level} (k : 𝕋) {A : UU l} →
is-trunc k A → is-trunc k (involution A)
is-trunc-involution k is-trunc-A =
is-trunc-Σ
( is-trunc-function-type k is-trunc-A)
( is-trunc-is-involution k (is-trunc-succ-is-trunc k is-trunc-A))

involution-Truncated-Type :
{l : Level} (k : 𝕋) → Truncated-Type l k → Truncated-Type l k
pr1 (involution-Truncated-Type k (A , is-trunc-A)) = involution A
pr2 (involution-Truncated-Type k (A , is-trunc-A)) =
is-trunc-involution k is-trunc-A


### Involutions on dependent function types

involution-Π-involution-fam :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
((x : A) → involution (B x)) → involution ((x : A) → B x)
pr1 (involution-Π-involution-fam i) f x =
map-involution (i x) (f x)
pr2 (involution-Π-involution-fam i) f =
eq-htpy (λ x → is-involution-map-involution (i x) (f x))


### Coherence of involutions

module _
{l : Level} {A : UU l} {f : A → A} (H : is-involution f)
where

coherence-is-involution : UU l
coherence-is-involution = f ·l H ~ H ·r f


## Examples

### The identity function is an involution

is-involution-id :
{l : Level} {A : UU l} → is-involution (id {A = A})
is-involution-id = refl-htpy

id-involution :
{l : Level} {A : UU l} → involution A
pr1 id-involution = id
pr2 id-involution = is-involution-id

involution-Pointed-Type :
{l : Level} (A : UU l) → Pointed-Type l
pr1 (involution-Pointed-Type A) = involution A
pr2 (involution-Pointed-Type A) = id-involution