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.

class Unique (α : Sort u) extends Inhabited α : Sort (max 1 u)

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.

• default : α
• uniq : ∀ (a : α), a = default

  In a Unique type, every term is equal to the default element (from Inhabited).

theorem Unique.ext {α : Sort u} {x y : Unique α} (default : default = default) : x = y

theorem unique_iff_exists_unique (α : Sort u) : Nonempty (Unique α) ↔ ∃! x : α, True

theorem unique_subtype_iff_exists_unique {α : Sort u_1} (p : α → Prop) : Nonempty (Unique (Subtype p)) ↔ ∃! a : α, p a

@[reducible, inline]

abbrev uniqueOfSubsingleton {α : Sort u_1} [Subsingleton α] (a : α) : Unique α

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 := ⋯ }

instance PUnit.unique : Unique PUnit.{u}

Equations

• PUnit.unique = { default := PUnit.unit, uniq := PUnit.unique.proof_1 }

@[simp]

theorem PUnit.default_eq_unit : default = PUnit.unit

def uniqueProp {p : Prop} (h : p) : Unique p

Every provable proposition is unique, as all proofs are equal.

Equations

• uniqueProp h = { default := h, uniq := ⋯ }

instance instUniqueTrue : Unique True

Equations

• instUniqueTrue = uniqueProp trivial

@[instance 100]

instance Unique.instInhabited {α : Sort u_1} [Unique α] : Inhabited α

Equations

• Unique.instInhabited = inst.toInhabited

theorem Unique.eq_default {α : Sort u_1} [Unique α] (a : α) : a = default

theorem Unique.default_eq {α : Sort u_1} [Unique α] (a : α) : default = a

@[instance 100]

instance Unique.instSubsingleton {α : Sort u_1} [Unique α] : Subsingleton α

Equations

• ⋯ = ⋯

theorem Unique.forall_iff {α : Sort u_1} [Unique α] {p : α → Prop} : (∀ (a : α), p a) ↔ p default

theorem Unique.exists_iff {α : Sort u_1} [Unique α] {p : α → Prop} : Exists p ↔ p default

theorem Unique.subsingleton_unique' {α : Sort u_1} (h₁ h₂ : Unique α) : h₁ = h₂

instance Unique.subsingleton_unique {α : Sort u_1} : Subsingleton (Unique α)

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev Unique.mk' (α : Sort u) [h₁ : Inhabited α] [Subsingleton α] : Unique α

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 := ⋯ }

theorem nonempty_unique (α : Sort u) [Subsingleton α] [Nonempty α] : Nonempty (Unique α)

theorem unique_iff_subsingleton_and_nonempty (α : Sort u) : Nonempty (Unique α) ↔ Subsingleton α ∧ Nonempty α

@[simp]

theorem Pi.default_def {α : Sort u_1} {β : α → Sort v} [(a : α) → Inhabited (β a)] : default = fun (a : α) => default

theorem Pi.default_apply {α : Sort u_1} {β : α → Sort v} [(a : α) → Inhabited (β a)] (a : α) : default a = default

instance Pi.unique {α : Sort u_1} {β : α → Sort v} [(a : α) → Unique (β a)] : Unique ((a : α) → β a)

Equations

• Pi.unique = { toInhabited := Pi.instInhabited, uniq := ⋯ }

instance Pi.uniqueOfIsEmpty {α : Sort u_1} [IsEmpty α] (β : α → Sort v) : Unique ((a : α) → β a)

There is a unique function on an empty domain.

Equations

• Pi.uniqueOfIsEmpty β = { default := fun (a : α) => isEmptyElim a, uniq := ⋯ }

theorem eq_const_of_subsingleton {α : Sort u_1} {β : Sort u_2} [Subsingleton α] (f : α → β) (a : α) : f = Function.const α (f a)

theorem eq_const_of_unique {α : Sort u_1} {β : Sort u_2} [Unique α] (f : α → β) : f = Function.const α (f default)

theorem heq_const_of_unique {α : Sort u_1} [Unique α] {β : α → Sort v} (f : (a : α) → β a) : HEq f (Function.const α (f default))

theorem Function.Injective.subsingleton {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Injective f) [Subsingleton β] : Subsingleton α

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

theorem Function.Surjective.subsingleton {α : Sort u_1} {β : Sort u_2} {f : α → β} [Subsingleton α] (hf : Function.Surjective f) : Subsingleton β

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

def Function.Surjective.unique {β : Sort u_2} {α : Sort u} (f : α → β) (hf : Function.Surjective f) [Unique α] : Unique β

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

Equations

• Function.Surjective.unique f hf = Unique.mk' β

def Function.Injective.unique {α : Sort u_1} {β : Sort u_2} {f : α → β} [Inhabited α] [Subsingleton β] (hf : Function.Injective f) : Unique α

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

Equations

• hf.unique = Unique.mk' α

def Function.Surjective.uniqueOfSurjectiveConst (α : Type u_3) {β : Type u_4} (b : β) (h : Function.Surjective (Function.const α b)) : Unique β

If a constant function is surjective, then the codomain is a singleton.

Equations

• Function.Surjective.uniqueOfSurjectiveConst α b h = uniqueOfSubsingleton b

def uniqueElim {ι : Sort u_2} {α : ι → Sort u_3} [Unique ι] (x : α default) (i : ι) : α i

Given one value over a unique, we get a dependent function.

Equations

• uniqueElim x i = ⋯.mpr x

@[simp]

theorem uniqueElim_default {ι : Sort u_2} {α : ι → Sort u_3} {x✝ : Unique ι} (x : α default) : uniqueElim x default = x

@[simp]

theorem uniqueElim_const {ι : Sort u_2} {β : Sort u_4} {x✝ : Unique ι} (x : β) (i : ι) : uniqueElim x i = x

theorem Unique.bijective {A : Sort u_2} {B : Sort u_3} [Unique A] [Unique B] {f : A → B} : Function.Bijective f

theorem Option.subsingleton_iff_isEmpty {α : Type u} : Subsingleton (Option α) ↔ IsEmpty α

Option α is a Subsingleton if and only if α is empty.

instance Option.instUniqueOfIsEmpty {α : Type u_2} [IsEmpty α] : Unique (Option α)

Equations

• Option.instUniqueOfIsEmpty = Unique.mk' (Option α)

instance Unique.subtypeEq {α : Sort u_1} (y : α) : Unique { x : α // x = y }

Equations

• Unique.subtypeEq y = { default := ⟨y, ⋯⟩, uniq := ⋯ }

instance Unique.subtypeEq' {α : Sort u_1} (y : α) : Unique { x : α // y = x }

Equations

• Unique.subtypeEq' y = { default := ⟨y, ⋯⟩, uniq := ⋯ }

instance Fin.instUnique : Unique (Fin 1)

Equations

• Fin.instUnique = { toInhabited := Fin.instInhabited, uniq := Fin.instUnique.proof_2 }