Resolve "Add `Eq`"

Closes #63 (closed)

This MR implements an intensional equality à la MLTT, The aim is to extend this definition once Proof-irrelevance is added, by transforming this equality into an intensional equality à la CCobs (https://hal.archives-ouvertes.fr/hal-03857705v1). The observational equality can be added as a "drop-in" replacement, as in:

-Eq and Refl will still be axiomatised

-Eq_rec will be encodable through the new cast and transport constructors.