Transposing identifications along involutions

Content created by Egbert Rijke and Louis Wasserman.

Created on 2026-05-05.
Last modified on 2026-05-05.

module foundation.transposition-identifications-along-involutions where
Imports 
open import foundation.involutions
open import foundation.universe-levels

open import foundation-core.identity-types

Idea

If f : A → A is an involution, then we have an equivalence

  f x ＝ y ≃ x = f y

for every x y : A.

Definitions

Transposing identifications along involutions

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

  eq-transpose-involution :
    {x y : A} → x ＝ f y → f x ＝ y
  eq-transpose-involution refl = H _

  eq-transpose-involution' :
    {x y : A} → f x ＝ y → x ＝ f y
  eq-transpose-involution' refl = inv (H _)

Recent changes