LINEAR TYPES

The type constructor defines linear types in cohesive type theory, ensuring resources are used exactly once. Linear types model structures like vector spaces, linear maps, or quantum states, with applications in quantum computing and categorical semantics.

In Urs, operates on types in graded universes from , with applications in quantum systems , tensor products , and braided monoidal structures .

Formation

(Linear Type Formation). The constructor forms linear types over a base type in a graded universe.

def Linear (i : Nat) (g : Grade) (A : U i g) : U i g

Introduction

(Linear Type Constructors). Terms of are introduced via linear maps and tensor products, ensuring linearity constraints.

def lin-map (i : Nat) (g : Grade) (A B : U i g) (lA : Linear i g A) (lB : Linear i g B) : U i g
def lin-tensor (i : Nat) (g : Grade) (A B : U i g) (lA : Linear i g A) (lB : Linear i g B) : Linear i g (A ⊗ B)

Elimination

(Linear Type Eliminator). The eliminator for maps linear types to properties in .

def linear_ind (i : Nat) (g : Grade) (A : U i g)
    (phi : (Linear i g A) -> U_0)
    (h : Π (l : Linear i g A), phi l)
  : Π (l : Linear i g A), phi l

Theorems

(Linearity Constraint). Linear types enforce that resources are used exactly once, preventing cloning.

def no-cloning (i : Nat) (g : Grade) (A : U i g) (l : Linear i g A)
  : ¬ (lin-map i g A (A ⊗ A) l (l ⊗ l))

(Linear Quantum States). For , models quantum states with linear constraints.

def linear-qubit (i : Nat) (g : Grade) (C H : U_0)
  : U i g
 := Linear i g (Qubit C H)

(Linear Tensor Associativity). The tensor product of linear types is associative, aligning with .

def lin-tensor-assoc (i : Nat) (g : Grade) (A B C : U i g)
  : (lin-tensor i g A B) ⊗ (lin-tensor i g B C) = lin-tensor i g A (lin-tensor i g B C)