English
There is a natural equivalence between the type Unique (Unique α) and Unique α. Specifically, Unique (Unique α) ≃ Unique α, with the forward map sending a unique structure to its default element and the backward map constructing a unique structure from a given element.
Русский
Существует естественная эквивалентность между типами Unique (Unique α) и Unique α: Unique (Unique α) ≃ Unique α, где отображение вперёд отправляет уникальную структуру в её значение по умолчанию, а обратное строит уникальную структуру из данного элемента.
LaTeX
$$$Unique\\,(Unique\\,\\alpha)\\ \\simeq\\ Unique\\,\\alpha.$$$
Lean4
/-- `Unique (Unique α)` is equivalent to `Unique α`. -/
def uniqueUniqueEquiv : Unique (Unique α) ≃ Unique α :=
equivOfSubsingletonOfSubsingleton (fun h => h.default) fun h =>
{ default := h, uniq := fun _ => Subsingleton.elim _ _ }
