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

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

## Definition

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

$isConstant(a) \coloneqq \Vert fiber(s, a) \Vert$

## 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

$\frac{\partial}{\partial x}: F(x) \to F(x)$

such that there are terms

$\lambda:\prod_{a:F(x)} \prod_{b:F(x)} isConstant(a) \times isConstant(b) \times \prod_{p:F(x)} \prod_{q:F(x)} \frac{\partial}{\partial x}(a \cdot p + b \cdot q) = a \cdot \frac{\partial}{\partial x}(p) + b \cdot \frac{\partial}{\partial t}(q)$
$\pi: \prod_{p:F(x)} \prod_{q:F(x)} \frac{\partial}{\partial x}(p \cdot q) = p \cdot \frac{\partial}{\partial x}(q) + \frac{\partial}{\partial x}(p) \cdot q$
$\iota: \frac{\partial}{\partial x}(x) = 1$

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

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

$\alpha: \prod_{n:\mathbb{Z}_+} \left(\frac{\partial}{\partial x}(x^{n+1}) = j(n + 1) \cdot x^{n} \right)$

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

$\zeta: \prod_{a:R} isConstant(a) \times \left(\frac{\partial}{\partial x}a = 0\right)$

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

$\delta: \prod_{p:F(x)} \prod_{q:F(x)} (q # 0) \times \left(\frac{\partial}{\partial x}\left(\frac{p}{q}\right) = \frac{\partial}{\partial x}(p) \cdot \frac{1}{q} - \frac{\partial}{\partial x}(q) \cdot \frac{p}{q^2} \right)$