-Type is the sort of sets equipped with the Id equality (i.e. an intensional,
-not quotiented set). We will avoid using Leibnitz equality Id,
-thus we will explicitly equip a set with an equality when needed.
-We will call this structure `setoid`. Note that we will
-attach the infix = symbol only to the equality of a setoid,
+Type is the sort of sets equipped with the `Id `equality (i.e. an intensional,
+not quotiented set). We will avoid using `Id` (Leibnitz equality),
+thus we will explicitly equip a set with an equivalence relation when needed.
+We will call this structure a _setoid_. Note that we will
+attach the infix `=` symbol only to the equality of a setoid,