# An involution on the standard finite types

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

Created on 2023-02-20.

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