Dependent sum with Prop

Stream: general

[Harrison Grodin]

I'm trying to write a list merging function which, given two lists and an included proof that each is nondecreasing, produces a result list and a proof that it's also nondecreasing. While I think I have some idea of how to tackle it implementation-wise, I can't seem to get the types to line up (especially wrt pi/sigma vs. forall/exists). Here's a sketch of my current setup (with a bit of pseudocode in the merge type itself):

inductive nondecreasing : list ℕ → Prop
| nil    : nondecreasing []
| single : Π {x : ℕ}, nondecreasing [x]
| zip    : Π {x y : ℕ} {xs : list ℕ}, x ≤ y → nondecreasing (y :: xs) → nondecreasing (x :: y :: xs)

def merge : Π (x y : Σ l, nondecreasing l), Σ l' : list ℕ, nondecreasing (list.append x.l y.l) l' := sorry

Is there any way I can make this (or something like it) work?

[Harrison Grodin]

The main issue with this approach, afaict, is the distinction between Prop and Type ?:

has type
  list ℕ → Prop : Type
but is expected to have type
  list ℕ → Type ? : Type (?+1)

[Harrison Grodin]

If I use a Σ, it complains about Prop being invalid, but if I use a ∃, I'm unable to unpack the actual list itself... I think this is due to the special casing on Prop?

[Harrison Grodin]

(Apologies if this is a silly question - seems like it could be...)

[Mario Carneiro]

Use Σ'

[Mario Carneiro]

or {l | nondecreasing l}

[Harrison Grodin]

Oh, that's perfect! Thanks.