TENSOR PRODUCT TYPE

The type models the tensor product of types , forming a new type that combines their structures bilinearly, used in quantum systems, smooth geometry, and stable homotopy theory.

In Urs, is a type-forming operation in , supporting constructions like multi-qubit states , sheaf products , and homotopical compositions .

Formation

(-Formation). The type is a type in , formed for each , representing their tensor product.

def Tensor (X Y : U_0) : U_0

Introduction

(-Introduction). Terms of type are introduced via the constructor, forming bilinear pairs from and .

def tensor (X Y : U_0) (x : X) (y : Y) : X ⊗ Y

Elimination

(-Elimination). The eliminator for maps tensor products to properties in , analyzing their bilinear structure.

def tensor_ind (X Y : U_0) (beta : (X ⊗ Y) -> U_0)
    (h : Π (z : X ⊗ Y), beta z)
  : Π (z : X ⊗ Y), beta z

Theorems

(Associativity). For , the tensor product is associative up to isomorphism.

def tensor_assoc (X Y Z : U_0)
  : Path ((X ⊗ Y) ⊗ Z) (X ⊗ (Y ⊗ Z))

(Tensor for Qubits). Qubits and form composite systems via tensor products.

def tensor_qubit (C H_1 H_2 : U_0)
  : Qubit C H_1 -> Qubit C H_2 -> Qubit C (H_1 ⊗ H_2)

(Tensor for Smooth Sets). For , forms a smooth set, preserving sheaf structure.

def tensor_smthset (X Y : SmthSet)
  : SheafStr (X ⊗ Y) ℝ^m