# Homotopy Type Theory Heyting skewfield > history (Rev #1)

## Definition

A Heyting skewfield is a Heyting reciprocal ring $(A, +, -, 0, \cdot, 1, #)$ with a term $p: 0 # 1$.