351   \begin{proposition}[Function Quotient]\label{funquot}

   351   \begin{proposition}[Function Quotient]\label{funquot}

   352   @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2" 

   352   @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2" 

   353       and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}

   353       and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}

   354   \end{proposition}

   354   \end{proposition}

   355 

   355 

   356   \noindent

   360   \noindent

   357   We will heavily rely on this part of Homeier's work including an extension 

   361   We will heavily rely on this part of Homeier's work including an extension 

   358   to deal with compositions of equivalence relations defined as follows

   362   to deal with compositions of equivalence relations defined as follows

   359 

   363 

   360   \begin{definition}[Composition of Relations]

   364   \begin{definition}[Composition of Relations]

   367   \noindent

   371   \noindent

   368   Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for

   372   Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for

   369   the composition of any two quotients in not true (it is not even typable in

   373   the composition of any two quotients in not true (it is not even typable in

   370   the HOL type system). However, we can prove useful instances for compatible

   374   the HOL type system). However, we can prove useful instances for compatible

   371   containers. We will show such example in Section \ref{sec:resp}.

   375   containers. We will show such example in Section \ref{sec:resp}.

   372 

   377 

   373 *}

   378 *}

   374 

   379 

   375 section {* Quotient Types and Quotient Definitions\label{sec:type} *}

   380 section {* Quotient Types and Quotient Definitions\label{sec:type} *}

   376 

   381