How to get the unique term is a type of "cardinal 1"

Stream: maths

[Joël Riou]

Is there a better proof for this (e.g. without using choice):

import logic.unique

noncomputable def unique_of_existence_and_uniqueness {X : Type*}
  (existence : ∃ (x : X), true) (uniqueness : ∀ (x y : X), x=y) : unique X :=
let h : nonempty X := exists_true_iff_nonempty.mp existence in
{ default := h.some,
  uniq := λ x, uniqueness x h.some, }

[Adam Topaz]

One way to do this is using docs#nonempty and docs#subsingleton . I'm not sure if we have a unique instance given both nonempty and subsingleton

[Adam Topaz]

I don't think you can avoid choice

[Yakov Pechersky]

import logic.unique

variables {X : Type*}

noncomputable def unique_of_existence_and_uniqueness
  (existence : ∃ (x : X), true) (uniqueness : ∀ (x y : X), x=y) : unique X :=
by letI : subsingleton X := ⟨uniqueness⟩; exact unique_of_subsingleton existence.some

[Yakov Pechersky]

You can't avoid choice, you can't get data (and unique is data) from the existensial proposition.

[Eric Rodriguez]

you definitely can't avoid choice, what if my type is {x : R // x is chaitin's constant}

[Kevin Buzzard]

This is a difference between set theory and type theory. In ZFC you wouldn't need choice.

[Kevin Buzzard]

In Lean it's very clear when you need it -- it is the only route from the Prop universe to the Type universe

[Yakov Pechersky]

Computable, using a computable existensial:

import logic.unique

variables {X : Type*}

def unique_of_existence_and_uniqueness
  (existence : trunc X) (uniqueness : ∀ (x y : X), x=y) : unique X :=
by letI : subsingleton X := ⟨uniqueness⟩; exact unique_of_subsingleton (existence.lift id uniqueness)

[Yakov Pechersky]

trunc X is quot (λ _ _, true) of X. So a term of trunc X is equal to any other term of trunc X.

[Yakov Pechersky]

And since lean quotients are computable, we can "lift" the data out of trunc X, the x : X that is wrapped in the quotient, and provide it as the data-witness to unique, and this is legal because we have a proof that all x y : X are equal.

[Yakov Pechersky]

So it didn't matter if it was x : X "inside" the trunc X or y : X inside.

[Joël Riou]

Thanks for your answers! Then, similarly, if we have R : set (X × Y) such that (∀ (x : X), ∃ (y : Y), ⟨x,y⟩ ∈ R) ∧ (∀ xy xy', xy ∈ R → xy' ∈ R → xy.1 = xy.1 → xy.2 = xy.2), then we cannot define a term of type X → Y without using choice. That is indeed a big difference between ZF(C) and type theory!

For my particular case, I am afraid the computable existensial trick will not work :-(

[Yakov Pechersky]

Can I ask, why do you need to it to be computable? If you want computable functions, you probably wouldn't be working with set X anyway, since set can be arbitrarily large, infinite, uncountable, etc

[Yakov Pechersky]

Did you construct such a set, or do you want to just prove things about it?

[Yakov Pechersky]

You can for sure prove that this set.nonempty R as long as [nonempty X].

[Joël Riou]

My question was a minimal working example based on the situation I was in while working in the simplex category. I do not need computability or anything: I was only unsatisfied that choice had to be used!