Types with a unique term #
In this file we define a typeclass Unique
,
which expresses that a type has a unique term.
In other words, a type that is Inhabited
and a Subsingleton
.
Main declaration #
Unique
: a typeclass that expresses that a type has a unique term.
Main statements #
Unique.mk'
: an inhabited subsingleton type isUnique
. This can not be an instance because it would lead to loops in typeclass inference.Function.Surjective.unique
: if the domain of a surjective function isUnique
, then its codomain isUnique
as well.Function.Injective.subsingleton
: if the codomain of an injective function isSubsingleton
, then its domain isSubsingleton
as well.Function.Injective.unique
: if the codomain of an injective function isSubsingleton
and its domain isInhabited
, then its domain isUnique
.
Implementation details #
The typeclass Unique α
is implemented as a type,
rather than a Prop
-valued predicate,
for good definitional properties of the default term.
Unique α
expresses that α
is a type with a unique term default
.
This is implemented as a type, rather than a Prop
-valued predicate,
for good definitional properties of the default term.
Instances
Given an explicit a : α
with Subsingleton α
, we can construct
a Unique α
instance. This is a def because the typeclass search cannot
arbitrarily invent the a : α
term. Nevertheless, these instances are all
equivalent by Unique.Subsingleton.unique
.
See note [reducible non-instances].
Equations
- uniqueOfSubsingleton a = { default := a, uniq := ⋯ }
Instances For
Equations
- PUnit.unique = { default := PUnit.unit, uniq := PUnit.unique.proof_1 }
Every provable proposition is unique, as all proofs are equal.
Equations
- uniqueProp h = { default := h, uniq := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Construct Unique
from Inhabited
and Subsingleton
. Making this an instance would create
a loop in the class inheritance graph.
Equations
- Unique.mk' α = { toInhabited := h₁, uniq := ⋯ }
Instances For
There is a unique function on an empty domain.
Equations
- Pi.uniqueOfIsEmpty β = { default := fun (a : α) => isEmptyElim a, uniq := ⋯ }
If the codomain of an injective function is a subsingleton, then the domain is a subsingleton as well.
If the domain of a surjective function is a subsingleton, then the codomain is a subsingleton as well.
If the domain of a surjective function is a singleton, then the codomain is a singleton as well.
Equations
Instances For
If α
is inhabited and admits an injective map to a subsingleton type, then α
is Unique
.
Equations
- hf.unique = Unique.mk' α
Instances For
If a constant function is surjective, then the codomain is a singleton.
Equations
Instances For
Given one value over a unique, we get a dependent function.
Equations
- uniqueElim x i = ⋯.mpr x
Instances For
Option α
is a Subsingleton
if and only if α
is empty.
Equations
- Option.instUniqueOfIsEmpty = Unique.mk' (Option α)
Equations
- Unique.subtypeEq y = { default := ⟨y, ⋯⟩, uniq := ⋯ }
Equations
- Unique.subtypeEq' y = { default := ⟨y, ⋯⟩, uniq := ⋯ }