BOSONIC MODALITY

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

In Urs, operates on types in graded universes from , with applications in bosonic quantum fields and supergeometry .

Formation

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

def bosonic (i : Nat) (g : Grade) (A : U i g) : U i 0
(* Bosonic modality *)

Introduction

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

(* Applied via bosonic i g A *)
(* Bosonic modality introduction *)

Elimination

(Bosonic Modality Elimination). The eliminator for maps bosonic types to properties in .

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

Theorems

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

def bosonic_idem (i : Nat) (g : Grade) (A : U i g) : (bosonic i 0 (bosonic i g A)) = (bosonic i g A)
(* Idempotence: bosonic (bosonic A) = bosonic A *)

(Bosonic Qubits). For , models bosonic quantum states.

def bosonic_qubit (i : Nat) (g : Grade) (C H : U_0) : U i 0 := bosonic i g (Qubit C H)
(* Bosonic qubits: bosonic Qubit(C, H) *)