Symmetric elements of involutive types

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

Created on 2023-02-09.
Last modified on 2025-10-31.

module structured-types.symmetric-elements-involutive-types where
Imports 
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

Recent changes