Encodable types #
This file defines encodable (constructively countable) types as a typeclass.
This is used to provide explicit encode/decode functions from and to
ℕ, with the information that
those functions are inverses of each other.
The difference with
denumerable is that finite types are encodable. For infinite types,
Main declarations #
encodable α: States that there exists an explicit encoding function
encode : α → ℕwith a partial inverse
decode : ℕ → option α.
decode₂: Version of
decodethat is equal to
noneoutside of the range of
encode. Useful as we do not require this in the definition of
ulower α: Any encodable type has an equivalent type living in the lowest universe, namely a subtype of
ulower αfinds it.
Implementation notes #
The point of asking for an explicit partial inverse
decode : ℕ → option α to
encode : α → ℕ is
to make the range of
encode decidable even when the finiteness of
α is not.
- encode : α → ℕ
- decode : ℕ → option α
- encodek : ∀ (a : α), encodable.decode α (encodable.encode a) = some a
Constructively countable type. Made from an explicit injection
encode : α → ℕ and a partial
decode : ℕ → option α. Note that finite types are countable. See
denumerable if you
wish to enforce infiniteness.
An encodable type has decidable equality. Not set as an instance because this is usually not the best way to infer decidability.
α is encodable and there is an injection
f : β → α, then
β is encodable as well.
α is encodable and
f : β → α is invertible, then
β is encodable as well.
α is encodable, then so is
Failsafe variant of
decode₂ α n returns the preimage of
encode if it
exists, and returns
none if it doesn't. This requirement could be imposed directly on
is not to help make the definition easier to use.
An encodable type is equivalent to the range of its encoding function.
Explicit decoding function for the sum of two encodable types.
Explicit decoding function for
Explicit decoding function for a decidable subtype of an encodable type
A decidable subtype of an encodable type is encodable.
Constructive choice function for a decidable subtype of an encodable type.
directed r function
f : α → β defined on an encodable inhabited type,
construct a noncomputable sequence such that
r (f (x n)) (f (x (n + 1)))
r (f a) (f (x (encode a + 1)).
The quotient of an encodable space by a decidable equivalence relation is encodable.