Involutive types

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

Created on 2023-02-09.
Last modified on 2023-03-13.

module structured-types.involutive-types where
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.universe-levels

open import univalent-combinatorics.2-element-types


Involutive types are types equipped with a ℤ/2-action. In other words, involutive types are type families over 2-Element-Type lzero.

Similarly, an involutive structure on a type X consists of a type family Y over 2-Element-Type lzero equipped with an equivalence X ≃ Y (Fin 2).


Involutive types

Involutive-Type : (l : Level)  UU (lsuc l)
Involutive-Type l = 2-Element-Type lzero  UU l

module _
  {l : Level} (X : Involutive-Type l)

  type-Involutive-Type : UU l
  type-Involutive-Type = X (standard-2-Element-Type lzero)

Involutive structure on a type

involutive-structure :
  {l1 : Level} (l2 : Level) (X : UU l1)  UU (l1  lsuc l2)
involutive-structure l2 X =
  Σ (Involutive-Type l2)  Y  X  type-Involutive-Type Y)

Recent changes