Symmetric elements of involutive types

module structured-types.symmetric-elements-involutive-types where

open import foundation.universe-levels

open import structured-types.involutive-types

open import univalent-combinatorics.2-element-types

Idea

Symmetric elements of involutive types are fixed points of the involution. In other words, the type of symmetric elements of an involutive type A is defined to be

  (X : 2-Element-Type lzero) → A X

Definition

symmetric-element-Involutive-Type :
  {l : Level} (A : Involutive-Type l) → UU (lsuc lzero ⊔ l)
symmetric-element-Involutive-Type A = (X : 2-Element-Type lzero) → A X