An Optional Prop

Stream: new members

[Mark Fischer]

Here is a small example where I've been trying to work out what the error is telling me.

def t := (x : ℕ) → Option (x > 5)

The error I'm seeing says:

argument
  x > 5
has type
  Prop : Type
but is expected to have type
  Type ?u.202 : Type (?u.202 + 1)

I think that this wants a Type when I gave it a Sort? Though isn't Type i just sugar for Sort (i - 1)?

I do get that what this is doing is strange. t is what? ... a predicate for perhaps a proof? I'm assuming impredicative Prop might be the reason this isn't allowed, but I'm still having trouble parsing the error.

[Arthur Adjedj]

Option expects an argument that lives in Type, and doesn't take in predicates (things that live in Prop). Type u is sugar for Sort (u+1), not Sort (u-1).

[Arthur Adjedj]

In order to do this, you could either define your own optional type which would live in Prop, i.e use:

def OptionP (P : Prop) := P ∨ True

Another way you could to it would be to use a universe lift PLift, your type would then be Option (PLift (x > 5)) instead of Option (x > 5).

[Mark Fischer]

Ah yes. That makes sense

[Mark Fischer]

PLift's implementation is so simple - which makes sense. Very cool.

[Mark Fischer]

I suppose my follow up question is whether there's a deeper reason behind why Option isn't implemented for Prop as well?

Playing around with the following seems to work

inductive Option' α where
  | none : Option' α
  | some (val : α) : Option' α

The universe polymorphic type is like:

inductive Option' (α : Sort u) : Sort (max 1 u)

[Joachim Breitner]

Is

def OptionP (P : Prop) := P ∨ True

really useful? It’s equivalent to True no matter what P is:

example : OptionP P = True := or_true _

[Mario Carneiro]

yeah, you want ⊕' there instead

[Mario Carneiro]

@Treq the max 1 u universe tends to generate harder universe unification problems because it is not injective, compared to u+1 which is what Option has. That's why we have PSum and PSigma as more general versions of Sum and Sigma which allow any sort, but don't use them by default

[Mario Carneiro]

A ⊕' B is notation for PSum A B

[Mark Fischer]

Ah, okay! Good to know :)