Ideally, a codec should link to a formalisation of the corresponding theorem; if there is none yet, any flexible description of the theorem should be used instead. The description should subsume both isomorphism/canonicity and representation in simpler (database) types.
Ideally, a codec should link to a formalisation of the corresponding theorem; if there is none yet, any flexible description of the theorem should be used instead. The description should subsume both isomorphism/canonicity and representation in simpler (database) types.