# Homotopy Type Theory Clifford algebra > history (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

## Defintion

Given a

commutative ring $R$, a $R$-pre-Clifford algebra is an $R$-algebra $A$ with a canonical injection $\iota: R \to A$ and a quadratic form $q:A \to R$ such that

$\prod_{a:A} a \cdot a = \iota(q(a))$

A $R$-pre-Clifford algebra homomorphism between two $R$-pre-Clifford algebras $A$ and $B$ is an $R$-algebra homomorphism $f:A \to B$ such that the quadratic form is preserved

$\prod_{a:A} q_A(a) = q_B(f(a))$

The $R$-Clifford algebra $Cl(R, q)$ is the initial object in the category of $R$-pre-Clifford algebras and $R$-pre-Clifford algebra homomorphisms.

Suppose an $n$-dimensional $R$-Clifford algebra $A$ has a basis vector function $e:U(n) \to A$, where

$U(n) \coloneqq \sum_{i:\mathbb{N}} i \lt n$

is the type of natural numbers less than $n$, such that for all $i:U(n)$, $q(e_i) = 1$. Then $q$ is the standard diagonal form and $A$ is usually written as $Cl_n(R)$.