Equivalence relations
We have seen many observational equal types, we can abstract them, ie, for a binary relation $R$ on $A$: $R : A → A → Prop_\mathcal{U}$.
If R is reflexive, symmetric and transitive, then it is an equivalence relation.
Equivalence classes
We can divide $A$ into equivalence classes, ie, for an equivalence relation $R$ on $A$, a subtype $P : A → Prop_\mathcal{U}$ is called an equivalence class if there merely exists $x : A$ such that for all $b : A$ we have $R(a,b) ≃ P(b)$.
$$ is-equiv-class(P) := ∃_{x:A}∀_{b:A} R(x,b) ≃ P(b) $$
We define equivalence class of $x : A$ to be:
$$ [x]_R := R(x, _) $$