FERMIONIC MODALITY

The modality in cohesive type theory projects a type to fermionic parity (). For a type , forces the type to be fermionic, used in supergeometry and quantum physics.

In Urs, operates on types in graded universes from , with applications in fermionic quantum fields and braid group delooping .

Formation

(Fermionic Modality Formation). The modality is a type operator on graded universes, mapping to fermionic parity.

def fermionic (i : Nat) (g : Grade) (A : U i g) : U i 1

Introduction

(Fermionic Modality Introduction). The modality is applied to a type , producing with fermionic parity.

Elimination

(Fermionic Modality Elimination). The eliminator for maps fermionic types to properties in .

def fermionic_ind (i : Nat) (g : Grade) (A : U i g)
    (phi : (fermionic i g A) -> U_0)
    (h : Π (a : fermionic i g A), phi a)
  : Π (a : fermionic i g A), phi a

Theorems

(Idempotence of Fermionic). The modality is idempotent, as it always projects to fermionic parity.

def fermionic_idem (i : Nat) (g : Grade) (A : U i g)
  : (fermionic i 1 (fermionic i g A)) = (fermionic i g A)

(Fermionic Qubits). For , models fermionic quantum states.

def fermionic_qubit (i : Nat) (g : Grade) (C H : U_0) : U i 1
 := fermionic i g (Qubit C H)

(Fermionic and Braid Delooping). The modality relates to braid group delooping in .

def fermionic_braid (i : Nat) (g : Grade) (n : Nat) : U i 1
 := fermionic i g (Braid n ℝ^2)