\import{set.tex}
\import{set/partition.tex}
\import{relation.tex}
\import{order/quasiorder.tex}


\subsection{Equivalences}

% Sometimes also called "restricted equivalence".
\begin{abbreviation}\label{partialequivalence}
    $E$ is a partial equivalence iff
    $E$ is transitive and symmetric.
\end{abbreviation}

\begin{proposition}\label{partialequivalence_is_quasireflexive}
    Let $E$ be a partial equivalence.
    Then $E$ is quasireflexive.
\end{proposition}
\begin{proof}
    Follows by \cref{quasireflexive,symmetric,transitive}.
\end{proof}

\begin{abbreviation}\label{equivalence}
    $E$ is an equivalence iff
    $E$ is a symmetric quasiorder.
\end{abbreviation}

\begin{abbreviation}\label{equivalence_on}
    $E$ is an equivalence on $A$ iff
    $E$ is a symmetric quasiorder on $A$.
\end{abbreviation}

\begin{proposition}\label{inters_of_family_of_equivalences_is_equivalence}
    Let $F$ be a family of relations.
    Suppose every element of $F$ is an equivalence.
    Then $\inters{F}$ is an equivalence.
\end{proposition}
\begin{proof}
    $\inters{F}$ is quasireflexive by \cref{quasireflexive,inters_destr,inters_iff_forall}.
    $\inters{F}$ is symmetric by \cref{symmetric,inters_iff_forall,inters_destr}.
    $\inters{F}$ is transitive by \cref{transitive,inters_iff_forall,inters_destr}.
\end{proof}

\begin{proposition}\label{inters_of_family_of_equivalences_on_a_set_is_equivalence_on_that_set}
    Let $F$ be an inhabited family of relations.
    Suppose every element of $F$ is an equivalence on $A$.
    Then $\inters{F}$ is an equivalence on $A$.
\end{proposition}
\begin{proof}
    $\inters{F}$ is reflexive on $A$ by \cref{inters_of_family_of_reflexive_relations_is_reflexive}.
    $\inters{F}$ is symmetric.
    $\inters{F}$ is transitive.
\end{proof}
% NOTE: the union of a family of equivalence relations is not necessarily an
% equivalence relation because a binary union of transitive relations is not
% necessarily transitive.


\subsubsection{Equivalence classes}

\begin{abbreviation}\label{equiv_class}
    $\equivalenceClass{E}{a} = \downward{E}{a}$.
\end{abbreviation}

\begin{abbreviation}\label{equivclass_abbr}
    The $E$-equivalence class of $a$ is $\equivalenceClass{E}{a}$.
\end{abbreviation}

\begin{proposition}\label{equivclasses_inhabited}
    Let $E$ be an equivalence.
    Let $a\in \fld{E}$.
    Then $a\in\equivalenceClass{E}{a}$.
\end{proposition}
\begin{proof}
    $a\mathrel{E} a$ by \cref{reflexive_on,quasireflexive_implies_reflexive_on_fld}.
\end{proof}

\begin{proposition}\label{equivclasses_inhabited_equivalenceon}
    Let $E$ be an equivalence on $A$.
    Let $a\in A$.
    Then $a\in\equivalenceClass{E}{a}$.
\end{proposition}
\begin{proof}
    $a\mathrel{E} a$ by \cref{reflexive_on}.
\end{proof}

\begin{proposition}\label{equiv_implies_equivanlence_classes_eq}
    Let $E$ be an equivalence on $A$.
    Let $a, b\in A$.
    Suppose $a\mathrel{E} b$.
    Then $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$.
\end{proposition}
\begin{proof}
    We have for all $c\in\equivalenceClass{E}{a}$
        we have $c\in\equivalenceClass{E}{b}$
        by \cref{downward_closure_iff,transitive}.
    We have for all $c\in\equivalenceClass{E}{b}$
        we have $c\in\equivalenceClass{E}{a}$
        by \cref{downward_closure_iff,symmetric,transitive}.
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{equivclasses_eq_implies_equiv}
    Let $E$ be an equivalence on $A$.
    Let $a, b\in A$.
    Suppose $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$.
    Then $a\mathrel{E} b$.
\end{proposition}
\begin{proof}
    $a\in\equivalenceClass{E}{a}$ by \cref{equivclasses_inhabited_equivalenceon}.
    Thus $a\in\equivalenceClass{E}{b}$.
    Follows by \cref{downward_closure_iff}.
\end{proof}

\begin{proposition}\label{equiv_iff_equivclasses_eq}
    Let $E$ be an equivalence on $A$.
    Let $a, b\in A$.
    Then $a\mathrel{E} b$ iff $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$.
\end{proposition}
\begin{proof}
    Follows by \cref{equiv_implies_equivanlence_classes_eq,equivclasses_eq_implies_equiv}.
\end{proof}

\begin{proposition}\label{equivclasses_diseq_implies_disjoint}
    Let $E$ be a partial equivalence.
    Suppose $\equivalenceClass{E}{a}\neq \equivalenceClass{E}{b}$.
    Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$.
\end{proposition}
\begin{proof}
    Show there exists no $c$ such that
        $c\in\equivalenceClass{E}{a}$ and
        $c\in\equivalenceClass{E}{b}$.
    \begin{subproof}
        Assume there exists a set $c$ such that
            $c\in\equivalenceClass{E}{a}$ and
            $c\in\equivalenceClass{E}{b}$.
        Take $c$ such that $c\in\equivalenceClass{E}{a}$ and
            $c\in\equivalenceClass{E}{b}$ by assumption.
        We have $c\mathrel{E}a$ and $c\mathrel{E}b$
            by \cref{downward_closure_iff}.
        Thus $a\mathrel{E}c$ and $b\mathrel{E}c$ by \cref{symmetric}.
        Thus $a\mathrel{E}b$ and $b\mathrel{E}a$ by \cref{transitive}.
        Hence $\equivalenceClass{E}{a}\subseteq\equivalenceClass{E}{b}$
            by \cref{downward_closure_iff,transitive_downward_subseteq}.
        We have $\equivalenceClass{E}{b}\subseteq\equivalenceClass{E}{a}$
            by \cref{downward_closure_iff,transitive_downward_subseteq}.
        Thus $\equivalenceClass{E}{a}=\equivalenceClass{E}{b}$
            by \cref{subseteq_antisymmetric}.
        Contradiction by assumption.
    \end{subproof}
    Follows by \cref{disjoint}.
\end{proof}

\begin{corollary}\label{equivalence_equivclasses_diseq_implies_disjoint}
    Let $E$ be an equivalence.
    Suppose $\equivalenceClass{E}{a}\neq \equivalenceClass{E}{b}$.
    Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$.
\end{corollary}
\begin{proof}
    Follows by \cref{equivclasses_diseq_implies_disjoint}.
\end{proof}

\begin{corollary}\label{equivalenceon_equivclasses_diseq_implies_disjoint}
    Let $E$ be an equivalence on $A$.
    Suppose $\equivalenceClass{E}{a}\neq \equivalenceClass{E}{b}$.
    Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$.
\end{corollary}
\begin{proof}
    Follows by \cref{equivclasses_diseq_implies_disjoint}.
\end{proof}


\subsubsection{Quotients}

\begin{definition}\label{quotient}
    $\quotient{A}{E} = \{\equivalenceClass{E}{a}\mid a\in A\}$.
\end{definition}

%\begin{definition}\label{equivalenceclasses}
%    $\equivalenceClasses{E} = \{\equivalenceClass{E}{a}\mid a\in\dom{E}\}$.
%\end{definition}

\begin{proposition}\label{quotient_emptyset}
    $\quotient{\emptyset}{\emptyset} = \emptyset$.
\end{proposition}
\begin{proof}
    We have for all $C\in\quotient{\emptyset}{\emptyset}$
        we have $C\in\emptyset$ by \cref{quotient,emptyset}.
    We have for all $C\in\emptyset$
        we have $C\in\quotient{\emptyset}{\emptyset}$ by \cref{emptyset}.
    Follows by set extensionality.
\end{proof}


\begin{proposition}\label{quotient_elems_disjoint}
    Let $E$ be an equivalence on $A$.
    Suppose $B,C\in\quotient{A}{E}$ and $B\neq C$.
    Then $B$ is disjoint from $C$.
\end{proposition}
\begin{proof}
    Take $b$ such that $b\in A$ and $B = \equivalenceClass{E}{b}$ by \cref{quotient}.
    Take $c$ such that $c\in A$ and $C = \equivalenceClass{E}{c}$ by \cref{quotient}.
    Then $B$ is disjoint from $C$ by \cref{equivalenceon_equivclasses_diseq_implies_disjoint}.
\end{proof}

\begin{proposition}\label{quotient_elems_inhabited}
    Let $E$ be an equivalence on $A$.
    Suppose $C\in\quotient{A}{E}$.
    Then $C$ is inhabited.
\end{proposition}
\begin{proof}
    Take $a$ such that $a\in A$ and $C = \equivalenceClass{E}{a}$ by \cref{quotient}.
    Then $a\in \equivalenceClass{E}{a}$ by \cref{equivclasses_inhabited_equivalenceon}.
    $C$ is inhabited by \cref{quotient,equivclasses_inhabited}.
\end{proof}

\begin{proposition}\label{quotient_elems_type}
    Let $E$ be an equivalence on $A$.
    Suppose $a\in C\in\quotient{A}{E}$.
    Then $a\in A$.
\end{proposition}
\begin{proof}
    Take $b$ such that $b\in A$ and $C = \equivalenceClass{E}{b}$
        by \cref{quotient}.
    Then $a\mathrel{E} b$.
    Thus $a\in A$ by \cref{times_tuple_elim,subseteq}.
\end{proof}


\begin{corollary}\label{quotient_notni_emptyset}
    Let $E$ be an equivalence on $A$.
    $\emptyset\notin\quotient{A}{E}$.
\end{corollary}
\begin{proof}
    Follows by \cref{quotient_elems_inhabited,emptyset}.
\end{proof}

\begin{proposition}\label{quotient_partition}
    Let $E$ be an equivalence on $A$.
    $\quotient{A}{E}$ is a partition.
\end{proposition}
\begin{proof}
    $\emptyset\notin\quotient{A}{E}$ by \cref{quotient_notni_emptyset}.
    For all $B, C\in \quotient{A}{E}$ such that $B\neq C$
        we have $B$ is disjoint from $C$ by \cref{quotient_elems_disjoint}.
    Follows by \cref{partition}.
\end{proof}

\begin{proposition}\label{quotient_partition_of}
    Let $E$ be an equivalence on $A$.
    $\quotient{A}{E}$ is a partition of $A$.
\end{proposition}
\begin{proof}
    We have for all $a\in\unions{(\quotient{A}{E})}$
        we have $a\in A$ by \cref{unions_iff,quotient_elems_type}.
    We have for all $a\in A$
        we have $a\in\unions{(\quotient{A}{E})}$
        by \cref{unions_iff,quotient,equivclasses_inhabited_equivalenceon}.
    Thus $\unions{(\quotient{A}{E})} = A$ by set extensionality.
    Follows by \cref{quotient_partition}.
\end{proof}



\begin{definition}\label{equivalence_from_partition}
    $\equivfrompartition{P}{A} = \{(a, b)\mid a\in A, b\in A\mid \exists C\in P.\ a, b\in C\}$.
\end{definition}

\begin{proposition}\label{equivalence_from_partition_intro}
    Let $P$ be a partition of $A$.
    Let $a,b\in A$.
    Suppose $a,b\in C\in P$.
    Then $a\mathrel{\equivfrompartition{P}{A}} b$.
\end{proposition}
\begin{proof}
    Follows by \cref{equivalence_from_partition}.
\end{proof}

\begin{proposition}\label{equivalence_from_partition_reflexive}
    Let $P$ be a partition of $A$.
    $\equivfrompartition{P}{A}$ is reflexive on $A$.
\end{proposition}
\begin{proof}
    Follows by \cref{reflexive_on,equivalence_from_partition_intro,partition,unions_iff}.
\end{proof}

\begin{proposition}\label{equivalence_from_partition_symmetric}
    Let $P$ be a partition.
    $\equivfrompartition{P}{A}$ is symmetric.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

\begin{proposition}\label{equivalence_from_partition_transitive}
    Let $P$ be a partition.
    $\equivfrompartition{P}{A}$ is transitive.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

\begin{proposition}\label{equivalence_from_partition_is_equivalence}
    Let $P$ be a partition of $A$.
    $\equivfrompartition{P}{A}$ is an equivalence on $A$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

\begin{proposition}\label{equivalence_from_quotient}
    Let $E$ be an equivalence on $A$.
    Then $\equivfrompartition{\quotient{A}{E}}{A} = E$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

\begin{proposition}\label{partition_eq_quotient_by_equivalence_from_partition}
    Let $P$ be a partition of $A$.
    Then $\quotient{A}{\equivfrompartition{P}{A}} = P$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}