\subsection{Riegs of Propositions}
\subsubsection{The rieg of truth values}
\begin{example}[Rieg of truth values]\label{ExampleRiegOfTruthValues}
    The set of truth values $\2 = \{\bot, \top\}$ has a natural rieg structure, as $(\2, \bot, \top, \lor, \land, \leftarrow)$. This is isomorphic to the overflow rieg with threshold $2$.
\end{example}

\begin{example}[Powerset]
For any set $X$, its powerset $\Po{X}$ has a rieg structure with $(\Po{X}, \emptyset, X, \cup,\cap, \leftarrow)$, where $A\leftarrow B$ is defined to be $A\cup B^{\co}$. More generally, every Heyting algebra\footnote{or CCC} is a rieg. \memo{Then, there is a free construction of \dq{associated Heyting algebras}}

When $X=\emptyset$, its powerset rieg is the trivial rieg. When $X$ is a singleton, its power rieg is the rieg of truth values.
\end{example}

% \subsection*{Relation to Heyting algebras}
\subsubsection{Heyting algebras are riegs}
A Heyting algebra is not just related but is a rieg satisfying additional equations. 
\begin{proposition}
    Every Heyting algebra $(H,0,1,\lor,\land, \leftarrow)$ is a rieg.
\end{proposition}

\begin{proposition}
    A rieg $A$ is a Heyting algebra, if and only if it satisfies the following additional equations:
    \begin{itemize}
        % \item $x\ti x=x$
        % \item $1+1=1$ %$x+x = x$
        \item $x^x =1$
        \item $x(y+1)=x$ %$$xy+y=y$
        \item $x^{y+1}=x$ %$y y^x = y$
        % \item $(x+y)y=y$
        \item $x y^x = xy$
        
    \end{itemize}
\end{proposition}

\begin{corollary}
 The category of Heyting algebras $\HeyAlg$ is a reflective full subcategory of the category of riegs $\Rieg$.
     \[
        \begin{tikzcd}
        \HeyAlg \ar[r, shift right, hookrightarrow]&\Rieg \ar[l, shift right]
        \end{tikzcd}
    \]
\end{corollary}
The construction of the left adjoint is the usual one: quotient by new equations. For example, the associated Heyting algebra of $\N$ is the Heyting algebra of truth values $\{\bot, \top\}.$\footnote{This particular example is a trivial case, since a left adjoint preserves colimits.}

The relation between Heyting algebras and riegs is not an addition of structures, but an addition of properties. In this respect, it is closer to the relationship between abelian groups and groups rather than to the relationship between rings and groups.

\memo{Full sub. Birkhoff's theorem}
\memo{Is it Malcev?}

\newpage
\subsubsection{Associated Heyting algebra of a rieg}
\memo{Sheaf topos over a top.sp.}

\memo{Or, more generally, how about a topos?}