\chapter{Equality}
\section{Eq}\label{febh}Let $\alpha$ be a type.
\begin{definition}\label{def:fgbh}
We define $\mname{eq}$ to be ${\uniddcgcg x y : {\alpha} .  {\unicdcdadad Q : {{\alpha}\unicdbdjdcd{{\alpha}\unicdbdjdcd{o}}} .  {{{{Q}~{x}}~{y}}\unicdbdjdcd{{{Q}~{y}}~{x}}}}}$ of type ${{\alpha}\unicdbdjdcd{{\alpha}\unicdbdjdcd{o}}}$.
\end{definition}
Since Proofgold has no polymorphism, there is
no single object corresponding to $\mname{eq}$.
Instead there is a constructor ${\mname{Eq}}$
that takes a type argument and is always expanded away 
using the definition above
as part of normalization.

\begin{definition}\label{def:ogfgbh}
We define $\mname{neq}$ to be ${\uniddcgcg x y : {\alpha} .  {\preoh{{{{\mname{eq}}~{x}}~{y}}}}}$ of type ${{\alpha}\unicdbdjdcd{{\alpha}\unicdbdjdcd{o}}}$.
\end{definition}
Again, there is no single object in Proofgold corresponding to
$\mname{neq}$. Instead it is represented by its definition which
is then expanded away as part of normalization.

\section{Notation for Equality} % Eq
{\bf{Notation.}} We use $\infnd$ as an infix operator  corresponding to applying term ${\mname{eq}}$.
{\bf{Notation.}} We use $\infmdod$ as an infix operator  corresponding to applying term ${\mname{neq}}$.
\section{Functional Extensionality}\label{gefe}Let $ \alpha \beta $ be types.
\begin{axiom}\label{ax:ggfhogdgpffgiheh} ${\unicdcdadad f g : {{\alpha}\unicdbdjdcd{\beta}} .  {{({\unicdcdadad x : {\alpha} .  {{{f}~{x}}={{g}~{x}}}})}\unicdbdjdcd{{f}={g}}}}$.
\end{axiom}
Functional extensionality is built in as part of the proof term
data structure in Proofgold, so this proposition has no counterpart
as a proposition published in the chain.

