Definition of Respects.
--- a/Quotient-Paper/Paper.thy Tue Jun 15 09:22:38 2010 +0200
+++ b/Quotient-Paper/Paper.thy Tue Jun 15 10:08:12 2010 +0200
@@ -353,6 +353,10 @@
and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
\end{proposition}
+ \begin{definition}[Respects]
+ An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}.
+ \end{definition}
+
\noindent
We will heavily rely on this part of Homeier's work including an extension
to deal with compositions of equivalence relations defined as follows
@@ -370,6 +374,7 @@
the HOL type system). However, we can prove useful instances for compatible
containers. We will show such example in Section \ref{sec:resp}.
+
*}
section {* Quotient Types and Quotient Definitions\label{sec:type} *}