rec only to Prop?

Stream: new members

[Chris M]

I have the code

universe u

inductive ind1 : Sort u
| const1 : ind1
| const2 : ind1 → ind1 → ind1

#check @ind1.rec

And this last check gives me

ind1.rec :
  ∀ {C : ind1 → Prop},
    C ind1.const1 → (∀ (a a_1 : ind1), C a → C a_1 → C (ind1.const2 a a_1)) → ∀ (n : ind1), C n

This is strange, because shouldn't C have the type C:ind1 \to Sort v or something like this? This is at least what the reference manual says.

[Chris B]

I think this is large elimination vs. small elimination (into Prop). You need to meet certain conditions in order to get large elimination. This one's small because it's in Sort u. If you change it to Type u, the motive will be (C : ind1 -> Sort l)

[Chris B]

You can also get large elimination with an instance of subsingleton.

[Chris B]

There are some other rules for getting a large eliminating inductive prop, it's like zero or one constructors, and all of the arguments have to be params/indices or props themselves ala false/eq.

[Chris B]

IIRC the motivation is that with proof irrelevance and large eliminating prop you can do something like

def x : ind1.{0} := ind1.const1
def y : ind1.{0} := ind1.const2 x x
-- by proof_irrel
lemma x_eq_y : x = y := rfl

inductive color
| black : color
| white : color

def pick_color : ind1 -> color
| const1 := black
| const2 := white

def black_eq_white : black = white := congr_arg pick_color x_eq_y

[Chris M]

What does the .{0} in ind1.{0} mean?

[Chris B]

@Chris M It's a way of explicitly passing the universe variable. In this case putting it in Sort 0/Prop.

#check ind1 -- ind1 : Sort u_1
universe x
#check ind1.{x} -- ind1 : Sort x
#check ind1.{0} -- ind1 : Prop