Subsingleton elimination on non-props without choice

Stream: Type theory

[Nir Paz]

For a proposition inductive type to have large elimination it needs to "clearly" have at most 1 instance, clearly basically meaning that all of its arguments are propositions, which are guaranteed to be subsingletons by lean's type theory. It's also not difficult to fill these 2 sorries by splitting to the case that α is empty and the case it is not, proving large elimination for subsingletons that are not propositions:

import Mathlib

noncomputable section

variable (α : Type*) (h : Subsingleton α)

inductive Foo : Prop where
  | c : α → Foo

#check Foo.rec
  -- ∀ {α : Type} {motive : Foo α → Prop}, (∀ (a : α), motive (Foo.c a)) → ∀ (t : Foo α), motive t

def Foo.betterRec {motive : Foo α → Sort*} : (∀ a : α, motive (Foo.c a)) → ∀ t, motive t :=
  sorry

theorem Foo.prop {motive : Foo α → Sort*} (f : ∀ a : α, motive (Foo.c a)) (a : α) :
    Foo.betterRec α f (Foo.c a) = f a :=
  sorry

But splitting into cases uses the axiom of choice (via LEM), and I'm trying to figure out if this is true without it as well. I think it isn't but I can't show that it implies any form of choice.

[Nir Paz]

I assume that if this is true without choice then so is every similar large elimination with subsingletones, so I'm talking about the general "scheme" and not just Foo.

[Chris Hughes]

Your type Foo is basically Nonempty. With the subsingleton instance, Foo.betterRec is basically what people call Unique Choice. It will never be computable in Lean because Lean forgets proofs. If we use betterRec to try to just return the unique element of α we will be recovering the data used to prove Foo which will have been forgotten by Lean.

So the answer to your question is that no, it's not provable in Lean without choice, although it only requires Unique Choice which is weaker but will still not allow computation.

Type theorists do have notions of computable Unique Choice, but these also won't be computable unless I only use contructive principles to prove Nonempty.