# Homotopy Type Theory antiderivative > history (Rev #5, changes)

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

# Contents

## Definition

Given a sequentially Cauchy complete Archimedean ordered field $\mathbb{R}$ and a function $f:\mathbb{R} \to \mathbb{R}$, the type of antiderivatives of $f$ is the fiber of the Newton-Leibniz operator at $f$:

$antiderivatives(f) \coloneqq \sum_{g:D^1(\mathbb{R}, \mathbb{R})} \tilde{D}(g) = f$

An antiderivative is a term of the above type.