## Stream: general

### Topic: set.indefinite_description

#### Kenny Lau (Dec 04 2018 at 22:27):

Is it possible to fill in this sorry?

universes u
protected def set.indefinite_description {α : Type u}
{p : set α  Prop} (h :  s, p s) : { s : set α // p s} := sorry

#### Reid Barton (Dec 04 2018 at 22:36):

I guess you mean without adding noncomputable? Interesting question

#### Mario Carneiro (Dec 05 2018 at 00:04):

yes

universes u
protected def set.indefinite_description {α : Type u}
{p : set α  Prop} (h :  s, p s) : { s : set α // p s} :=
{x : α | x  classical.some h}, classical.some_spec h

#### Mario Carneiro (Dec 05 2018 at 00:04):

I've mentioned before about "trivially computable" types, which includes subtypes of functions returning Prop

#### Mario Carneiro (Dec 05 2018 at 00:05):

Any term of such a type can be made computable with appropriate wrapping

#### Mario Carneiro (Dec 05 2018 at 00:06):

If you meant "without axioms", then no it's not possible, it would imply the axiom of choice

#### Mario Carneiro (Dec 05 2018 at 00:12):

However there is an interesting construction here for definite description with no axioms (well extensionality)

import data.set.basic

universes u
protected def set.definite_description {α : Type u}
{p : set α  Prop} (h : ∃! s, p s) : { s : set α // p s} :=
{x : α |  s, x  s  p s   y, p y  y = s},
let s, ps, al := h in
have s = {x : α |  s, x  s  p s   y, p y  y = s},
from set.ext \$ λ x, ⟨λ xs, ⟨_, xs, ps, al,
λ s', xs', ps', al', (al' _ ps).symm  xs',
this  ps

#### Kenny Lau (Dec 05 2018 at 00:25):

@Mario Carneiro so... we can have a "computable" basis?

#### Mario Carneiro (Dec 05 2018 at 00:25):

"computable" but not computable

#### Mario Carneiro (Dec 05 2018 at 00:26):

when I revisited bases recently, we discussed changing the definition of a basis from a set to a family over a type. In that case it wouldn't be computationally irrelevant

Last updated: May 14 2021 at 04:22 UTC