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

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

# Contents

## Definition

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

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

An antiderivative is a term of the above type.