An involution on the standard finite types

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

Created on 2023-02-20.
Last modified on 2023-06-15.

module univalent-combinatorics.involution-standard-finite-types 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.identity-types
open import foundation.involutions

open import univalent-combinatorics.standard-finite-types

Idea

Every standard finite type Fin k has an involution operation given by x ↦ -x - 1, using the group operations on Fin k.

Definition

opposite-Fin : (k : ℕ) → Fin k → Fin k
opposite-Fin k x = pred-Fin k (neg-Fin k x)

Properties

The opposite function on Fin k is an involution

is-involution-opposite-Fin : (k : ℕ) → is-involution (opposite-Fin k)
is-involution-opposite-Fin k x =
  ( ap (pred-Fin k) (neg-pred-Fin k (neg-Fin k x))) ∙
  ( ( is-retraction-pred-Fin k (neg-Fin k (neg-Fin k x))) ∙
    ( neg-neg-Fin k x))

Recent changes