Inductive types in Prop -- a comment in TPIL4

Stream: new members

[Kevin Cheung]

In Ch. 7 of TPIL4, the following example is given:

namespace Hid
inductive False : Prop

inductive True : Prop where
  | intro : True

inductive And (a b : Prop) : Prop where
  | intro : a → b → And a b

inductive Or (a b : Prop) : Prop where
  | inl : a → Or a b
  | inr : b → Or a b

end Hid

There is the following comment after this example: "Roughly speaking, what characterizes inductive types in Prop is that one can only eliminate to other types in Prop."

However, when I checked types of the recursors, only the one for Or has motive that maps to Prop; everything else maps to sort u:

#check Hid.False.rec -- Hid.False.rec.{u} (motive : False → Sort u) (t : False) : motive t
#check Hid.True.rec -- Hid.True.rec.{u} {motive : True → Sort u} (intro : motive True.intro) (t : True) : motive t
#check Hid.And.rec -- Hid.And.rec.{u} {a b : Prop} {motive : And a b → Sort u} (intro : (a_1 : a) → (a_2 : b) → motive ⋯) (t : And a b) : motive t
#check Hid.Or.rec -- Hid.Or.rec {a b : Prop} {motive : Or a b → Prop} (inl : ∀ (a_1 : a), motive ⋯) (inr : ∀ (a_1 : b), motive ⋯) (t : Or a b) : motive t

How does one reconcile these observations with the comment?

Also, what is ⋯ in motive ⋯?

Help greatly appreciated.

[Joachim Breitner]

Kevin Cheung said:

Also, what is ⋯ in motive ⋯?

This is an elision of proof terms, use set_option pp.proofs true to see them.

[Joachim Breitner]

There is an exception to the rule that Prop can only eliminate into Prop for Props with no computational value. The rule, according to “The Type Theory of Lean” is

2. The type family has at most one constructor, and all the non-recursive arguments to the constructor are either propositions or directly appear in the output type. This is called subsingleton (SS) elimination, and is relevant for the definition of equality as a large eliminating proposition.

[Kevin Cheung]

Thanks. I'm wondering if TPIL should add a footnote about this?

BTW, is "large eliminating proposition" a technical term? I can't quite make sense of it.

[Sebastian Ullrich]

Large elimination means exactly what you observed, eliminating into a higher universe than the type lives in

[Kevin Cheung]

I see. I guess I need to spend some time reading The type theory of Lean.