equal
deleted
inserted
replaced
692 the properties of \emph{respectfulness} and \emph{preservation}. We have |
692 the properties of \emph{respectfulness} and \emph{preservation}. We have |
693 to slightly extend Homeier's definitions in order to deal with quotient |
693 to slightly extend Homeier's definitions in order to deal with quotient |
694 compositions. |
694 compositions. |
695 |
695 |
696 To formally define what respectfulness is, we have to first define |
696 To formally define what respectfulness is, we have to first define |
697 the notion of \emph{aggregate equivalence relations} using the function @{text REL}: |
697 the notion of \emph{aggregate equivalence relations} using the function @{text "REL(\<sigma>, \<tau>)"} |
|
698 The idea behind this function is to simultaneously descend into the raw types |
|
699 @{text \<sigma>} and quotient types @{text \<tau>}, and generate the appropriate |
|
700 quotient equivalence relations in places where the types differ and equalities |
|
701 elsewhere. |
698 |
702 |
699 \begin{center} |
703 \begin{center} |
700 \hfill |
704 \hfill |
701 \begin{tabular}{rcl} |
705 \begin{tabular}{rcl} |
702 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ |
706 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ |