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

Created on 2022-03-05.
Last modified on 2024-04-17.

module foundation.involutions where
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


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


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

  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)

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

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


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}

  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-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 =
      ( 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-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)

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


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

Recent changes