Iterating involutions

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-05-06.
Last modified on 2023-10-16.

module foundation.iterating-involutions where
Imports 
open import elementary-number-theory.modular-arithmetic-standard-finite-types
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.involutions
open import foundation.iterating-functions
open import foundation.universe-levels

open import foundation-core.coproduct-types
open import foundation-core.identity-types

open import univalent-combinatorics.standard-finite-types

Definition

Iterating involutions

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

  iterate-involution :
    (n : ℕ) (x : X) → iterate n f x ＝ iterate (nat-Fin 2 (mod-two-ℕ n)) f x
  iterate-involution zero-ℕ x = refl
  iterate-involution (succ-ℕ n) x =
    ap f (iterate-involution n x) ∙ (cases-iterate-involution (mod-two-ℕ n))
    where
    cases-iterate-involution :
      (k : Fin 2) →
      f (iterate (nat-Fin 2 k) f x) ＝ iterate (nat-Fin 2 (succ-Fin 2 k)) f x
    cases-iterate-involution (inl (inr _)) = refl
    cases-iterate-involution (inr _) = P x

Recent changes