logic.unique

# 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 is unique. 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 is unique, then its codomain is unique as well.

• function.injective.subsingleton: if the codomain of an injective function is subsingleton, then its domain is subsingleton as well.

• function.injective.unique: if the codomain of an injective function is subsingleton and its domain is inhabited, then its domain is unique.

## Implementation details

The typeclass unique α is implemented as a type, rather than a Prop-valued predicate, for good definitional properties of the default term.

@[ext, class]
structure unique (α : Sort u) :
Sort (max 1 u)
• to_inhabited :
• uniq : ∀ (a : α), a =

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
theorem unique.ext_iff {α : Sort u} (x y : unique α) :
x = y

theorem unique.ext {α : Sort u} (x y : unique α) (h : x.to_inhabited = y.to_inhabited) :
x = y

@[instance]

Equations
theorem fin.eq_zero (n : fin 1) :
n = 0

@[instance]
def fin.inhabited {n : } :

Equations
@[simp]
theorem fin.default_eq_zero (n : ) :

@[instance]
def fin.unique  :

Equations
@[instance]
def unique.inhabited {α : Sort u} [unique α] :

Equations
theorem unique.eq_default {α : Sort u} [unique α] (a : α) :
a =

theorem unique.default_eq {α : Sort u} [unique α] (a : α) :
= a

@[instance]
def unique.subsingleton {α : Sort u} [unique α] :

theorem unique.forall_iff {α : Sort u} [unique α] {p : α → Prop} :
(∀ (a : α), p a) p (default α)

theorem unique.exists_iff {α : Sort u} [unique α] {p : α → Prop} :
p (default α)

@[ext]
theorem unique.subsingleton_unique' {α : Sort u} (h₁ h₂ : unique α) :
h₁ = h₂

@[instance]
def unique.subsingleton_unique {α : Sort u} :

def unique.mk' (α : Sort u) [h₁ : inhabited α] [subsingleton α] :

Construct unique from inhabited and subsingleton. Making this an instance would create a loop in the class inheritance graph.

Equations
@[simp]
theorem pi.default_def {α : Sort u} {β : α → Sort v} [Π (a : α), inhabited (β a)] :
default (Π (a : α), β a) = λ (a : α), default (β a)

theorem pi.default_apply {α : Sort u} {β : α → Sort v} [Π (a : α), inhabited (β a)] (a : α) :
default (Π (a : α), β a) a = default (β a)

@[instance]
def pi.unique {α : Sort u} {β : α → Sort v} [Π (a : α), unique (β a)] :
unique (Π (a : α), β a)

Equations
def pi.unique_of_empty {α : Sort u} (h : α → false) (β : α → Sort v) :
unique (Π (a : α), β a)

There is a unique function on an empty domain.

Equations
def function.surjective.unique {α : Sort u} {β : Sort v} {f : α → β} (hf : function.surjective f) [unique α] :

If the domain of a surjective function is a singleton, then the codomain is a singleton as well.

Equations
theorem function.injective.subsingleton {α : Sort u} {β : Sort v} {f : α → β} (hf : function.injective f) [subsingleton β] :

If the codomain of an injective function is a subsingleton, then the domain is a subsingleton as well.

def function.injective.unique {α : Sort u} {β : Sort v} {f : α → β} [inhabited α] [subsingleton β] (hf : function.injective f) :

If α is inhabited and admits an injective map to a subsingleton type, then α is unique.

Equations