GRADED UNIVERSES

The type represents a graded universe indexed by a monoid , where encodes a level () and parity (: = bosonic, = fermionic). Graded universes support type hierarchies with cumulativity, graded tensor products, and coherence rules, used in supergeometry (e.g., bosonic/fermionic types), quantum systems (e.g., graded qubits), and cohesive type theory.

In Urs, is a type indexed by , with operations like lifting, product formation, and graded tensor products, extending standard universe hierarchies to include parity, building on .

Formation

(Grading Monoid). The grading monoid is defined as , with operation and neutral element , encoding level and parity.

(Graded Universe Formation). The universe is a type indexed by , containing types of grade . A shorthand notation is used for .

def 𝒢 : Type := ℕ × ℤ/2ℤ  -- Levels (ℕ) and parity (ℤ/2ℤ: 𝟎 = Bose, 𝟏 = Fermi)
def ⊕ (α β : 𝒢) : 𝒢 := (fst α + fst β, (snd α + snd β) mod 2)
def 𝟘 : 𝒢 := (0, 0)  -- Neutral: level 0, bosonic
def U (α : 𝒢) : Type := Universe α  -- Universe formation
def Grade : Set := {0, 1}  -- 0 for bosonic, 1 for fermionic
def U (i : Nat) (g : Grade) : Type := U (i, g)
def U₀ (g : Grade) : U (>1, g) := U (0, g)
def U₀₀ : Type := U (0, 0)  -- Bosonic level 0
def U₁₀ : Type := U (>1, 0)  -- Bosonic level 1
def U₀₁ : Type := U (0, 1)  -- Fermionic level 0

Introduction

(Graded Universe Coherence Rules). Graded universes support coherence rules for lifting, product formation, and substitution, ensuring type-theoretic consistency.

def lift (α β : 𝒢) (δ : 𝒢) (e : U α) : β = α ⊕ δ → U β := λ eq : β = α ⊕ δ, transport (λ x : 𝒢, U x) eq e  -- Universe lifting
def univ-type (α : 𝒢) : U (α ⊕ (>1, 0)) := lift α (α ⊕ (>1, 0)) (>1, 0) (U α) refl  -- Type-in-type formation
def cumul (α β : 𝒢) (A : U α) (δ : 𝒢) : β = α ⊕ δ → U β := lift α β δ A  -- Cumulativity
def prod-rule (α β : \mathcal{G}) (A : U α) (B : A → U β) : U (α ⊕ β) := Π (x : A), B x  -- Product formation
def subst-rule (α β : \mathcal{G}) (A : U α) (B : A → U β) (t : A) : U β := B t  -- Substitution coherence
def shift (α δ : \mathcal{G}) (A : U α) : U (α ⊕ δ) := lift α (α ⊕ δ) δ A refl  -- Grade shift
(* Graded universe coherence rules *)

(Graded Tensor Introduction). Graded tensor products combine types with matching levels, combining parities.

def tensor (i : Nat) (g₁ g₂ : Grade) (A : U i g₁) (B : U i g₂) : U i (g₁ + g₂ mod 2) := A ⊗ B
def pair-tensor (i : Nat) (g₁ g₂ : Grade) (A : U i g₁) (B : U i g₂) (a : A) (b : B) : tensor i g₁ g₂ A B := a ⊗ b
(* Graded tensor product introduction *)

Elimination

(Graded Tensor Eliminators). Eliminators for graded tensor products project to their components.

def proj-tensor₁ (i : Nat) (g₁ g₂ : Grade) (A : U i g₁) (B : U i g₂) (p : A ⊗ B) : A := p.1
def proj-tensor₂ (i : Nat) (g₁ g₂ : Grade) (A : U i g₁) (B : U i g₂) (p : A ⊗ B) : B := p.2
(* Projections for graded tensor products *)

Theorems

(Monoid Properties). The grading monoid satisfies associativity and identity laws.

def assoc (α β γ : 𝒢) : (α ⊕ β) ⊕ γ = α ⊕ (β ⊕ γ) := refl  -- Associativity
def ident-left (α : 𝒢) : α ⊕ 𝟘 = α := refl  -- Left identity
def ident-right (α : 𝒢) : 𝟘 ⊕ α = α := refl  -- Right identity
(* Monoid properties *)

(Graded Tensor Product Properties). Graded tensor products satisfy graded commutativity and computation rules, reflecting supergeometry principles.

def tensor-comm (i : Nat) (g₁ g₂ : Grade) (A : U i g₁) (B : U i g₂) (a : A) (b : B)
  : Path (A ⊗ B) (a ⊗ b) ((-1)^(g₁ * g₂) * (b ⊗ a))
 := idp (A ⊗ B) (a ⊗ b)  -- Graded commutativity: a ⊗ b = (-1)^(g₁ g₂) (b ⊗ a)
def tensor-β₁ (i : Nat) (g₁ g₂ : Grade) (A : U i g₁) (B : U i g₂) (a : A) (b : B)
  : Path A (proj-tensor₁ i g₁ g₂ A B (a ⊗ b)) a := idp A a
(* Graded tensor product properties *)

(Tensor Associativity). Graded tensor products are associative, aligning with supergeometry and \texttt{tensor.pug}.

def tensor-assoc (i : Nat) (g₁ g₂ g₃ : Grade) (A : U i g₁) (B : U i g₂) (C : U i g₃)
  : Path (U i (g₁ + (g₂ + g₃) mod 2)) ((A ⊗ B) ⊗ C) (A ⊗ (B ⊗ C))
 := idp _ _  -- Associativity: (A ⊗ B) ⊗ C = A ⊗ (B ⊗ C)
(* Tensor associativity *)

(Test Cases). Examples illustrate bosonic and fermionic tensor products, applicable to quantum systems like \texttt{qubit.pug}.

def test-bosonic-tensor (A B : U 0 0) (a : A) (b : B)
  : tensor 0 0 0 A B := pair-tensor 0 0 0 A B a b
def test-bosonic-comm (A B : U 0 0) (a : A) (b : B)
  : Path (A ⊗ B) (a ⊗ b) (b ⊗ a) := tensor-comm 0 0 0 A B a b  -- 0 * 0 = 0, so 1
def test-fermionic-tensor (A B : U 0 1) (a : A) (b : B)
  : tensor 0 1 1 A B := pair-tensor 0 1 1 A B a b
def test-fermionic-comm (A B : U 0 1) (a : A) (b : B)
  : Path (A ⊗ B) (a ⊗ b) (- (b ⊗ a)) := tensor-comm 0 1 1 A B a b  -- 1 * 1 = 1, so -1
(* Test cases for bosonic and fermionic tensors *)