Why is PProd never in Prop?

Stream: new members

[Timo Carlin-Burns]

Why does docs#PProd have sort Sort (max (max u 1) v) instead of Sort (max u v)? It seems like PProd.{0, 0} could be equivalent to And without causing any inconsistency.

variable (P Q : Prop)

#check PProd P Q -- Type
#check P ∧ Q -- Prop

[Eric Wieser]

Note that if you write

structure PPProd (α : Sort u) (β : Sort v) : Sort (max u v) where
  fst : α
  snd : β

you get the error

invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
  max u v

[Eric Wieser]

(lean 3 gives the same error)

[Eric Wieser]

I was hoping this would work, but it doesn't (filed as lean4#3310):

set_option bootstrap.inductiveCheckResultingUniverse false in
structure PPProd.{u,v} (α : Sort u) (β : Sort v) : Sort (max u v) where
  fst : α
  snd : β