Homotopy Type Theory univariate rational expressions > history (Rev #3, changes)

Given a field $F$, the type of univariate rational expression $F(x)$ is the field inductively generated by

• a term $x:F(x)$ representing the indeterminant
• a function $s:F \to F(x)$ representing the function of scalars to constant rational expressions
• a term $c:isField(F(x))$ representing that $F(x)$ is a field.
• a term $h:isFieldHom(s)$ representing that $s:F \to F(x)$ is a field homomorphism?.

A term $a:F(x)$ is a constant univariate rational expression if the fiber of $s$ at $a$ is inhabited

Properties

Composition

Unlike for univariate polynomials, composition is not well defined for univariate rational expressions because the composite of $x^{-1}$ and $0$ does not exist by definition of a field. If a reciprocal of $0$ did exist, then the type $0 = 1$ has a term and the commutative reciprocal ring is trivial and thus by definition no longer a field.

Derivative

For every type $F(x)$, one could define a function called a derivative

such that there are terms

Thus $F(x)$ is a differential algebra?.

Since $R$ is power-associative, there is a term

for monic function $j:\mathbb{Z}_+ \to R[x]$ from the positive integers to $R[x]$.

Since $F$ is an integral domain, there is a term

and since $F$ is a field, there is a term

See also

• field (ring theory)
• univariate polynomial ring
• higher inductive type
• differential algebra?