## Stream: new members

### Topic: sigma/psigma

#### petercommand (Nov 03 2018 at 15:15):

What's the reason for having types like sigma/psigma, sum/psum at the same time?

#### Kevin Buzzard (Nov 03 2018 at 15:15):

Is it to do with universes?

#### petercommand (Nov 03 2018 at 15:17):

Like, when would I want to use psigma instead of sigma/Exists?

#### Reid Barton (Nov 03 2018 at 15:18):

psigma instead of Exists: because you want to keep the information of what the things are whose existence you claim

#### Reid Barton (Nov 03 2018 at 15:19):

psigma with a Prop is basically the same as subtype, whereas Exists is like nonempty

#### Reid Barton (Nov 03 2018 at 15:20):

psigma instead of sigma: if you want to use a Prop instead of a Type, or you might want either a Prop or a Type

#### Chris Hughes (Nov 03 2018 at 15:20):

The equation compiler uses psigma a lot. | (a : nat) (b : nat) (h : 0 < b) is essentially matching on Σ' a b : ℕ, 0 < b underneath.

#### Reid Barton (Nov 03 2018 at 15:23):

I've found psigma most useful in conjunction with the Σ' binder notation with multiple variables where the eventual "body" is a Prop

#### Mario Carneiro (Nov 03 2018 at 15:26):

isn't that exists?

#### Reid Barton (Nov 03 2018 at 15:26):

like "a pair consisting of an open set U and a function f : U -> R which sends x to 0" = Σ' (u : set α) (hu : is_open u) (f : u → ℝ), f x = 0

#### Chris Hughes (Nov 03 2018 at 15:27):

What's the point of using sigma instead of psigma?

#### Mario Carneiro (Nov 03 2018 at 15:28):

psigma has a difficult target universe

#### Mario Carneiro (Nov 03 2018 at 15:28):

Sort (max u 1) is hard to work with

#### Mario Carneiro (Nov 03 2018 at 15:28):

because it's not algebraic: max u 1 = 1 does not have a unique solution

#### Mario Carneiro (Nov 03 2018 at 15:29):

so lean will often give up on otherwise solvable universe unification problems

#### Mario Carneiro (Nov 03 2018 at 15:30):

where Type u = Sort u+1 has the much easier solution u+1 = 1 -> u = 0

#### Mario Carneiro (Nov 03 2018 at 15:30):

In fact, there are some expressions which do not have any solution, although you might think it does: max u 1 = v+1 has no solution for u

#### Reid Barton (Nov 03 2018 at 15:32):

hmm, that max 1 is coming from Lean bumping up the level of a structure I guess? Is it actually wanted? Why should psigma.{0 0} not be a Prop?

#### Mario Carneiro (Nov 03 2018 at 15:34):

That was deliberate. You can define your own psigma' that lives in Sort (max u v)

#### Mario Carneiro (Nov 03 2018 at 15:34):

but you will find it's not all it's cracked up to be

#### Mario Carneiro (Nov 03 2018 at 15:34):

in particular, it has a recursor like exists

it's not "data"

#### Mario Carneiro (Nov 03 2018 at 15:38):

and if you specialize to u > 0 you get the mystery type, which is neither proof nor data

#### petercommand (Nov 03 2018 at 15:38):

In fact, there are some expressions which do not have any solution, although you might think it does: max u 1 = v+1 has no solution for u

why does max u 1 = v+1 not have any solutions?

#### Mario Carneiro (Nov 03 2018 at 15:39):

because there is no universe expression that gives the solution

#### Reid Barton (Nov 03 2018 at 15:39):

Actually, I can't :)

structure ppsigma {α : Sort u} (β : α → Sort v) : Sort (max u v) := mk :: (fst : α) (snd : β fst)
-- invalid universe polymorphic structure declaration, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')


#### Reid Barton (Nov 03 2018 at 15:39):

But I guess it's because otherwise I would be in the situation you describe.

#### Mario Carneiro (Nov 03 2018 at 15:40):

That's because you used structure, it tried and failed to define the projections

Oh, I see

#### Reid Barton (Nov 03 2018 at 15:41):

Why doesn't singleton elimination help here?
If I manually replace u = v = 0, then I get an eliminator to any sort

#### Mario Carneiro (Nov 03 2018 at 15:42):

@petercommand for each fixed v there is a solution for u, but there is no solution function u(v)

#### Reid Barton (Nov 03 2018 at 15:42):

Just a weird edge case that Lean doesn't support?

#### Mario Carneiro (Nov 03 2018 at 15:42):

because you need one recursor that is polymorphic in u,v

#### Mario Carneiro (Nov 03 2018 at 15:43):

and that recursor will have one extra universe variable depending on whether max u v = 0

#### Mario Carneiro (Nov 03 2018 at 15:43):

there is no way to do that with universe expressions

#### Mario Carneiro (Nov 03 2018 at 15:44):

you could have two recursors, but this breaks parametricity

#### Reid Barton (Nov 03 2018 at 15:45):

I'm trying out different u and v values and in every case I get an eliminator which goes to any sort.
However there is a difference when u = v = 0, which is that the C doesn't take the ppsigma value as an argument then

#### Mario Carneiro (Nov 03 2018 at 15:45):

singleton elimination doesn't help because A and B aren't subsingletons

#### Mario Carneiro (Nov 03 2018 at 15:46):

That's just a convenience thing, the usual recursor is at drec_on

#### Mario Carneiro (Nov 03 2018 at 15:47):

for small eliminating props the dependent and nondependent recursors are interdefinable

#### Reid Barton (Nov 03 2018 at 15:52):

inductive ppsigma00 {α : Sort 0} (β : α → Sort 0) : Sort (max 0 0) | m (fst : α) (snd : β fst) : ppsigma00
#check @ppsigma00.drec_on
│ ppsigma00.drec_on :
│   Π {α : Prop} {β : α → Prop} {C : ppsigma00 β → Sort u_1} (n : ppsigma00 β),
│     (Π (fst : α) (snd : β fst), C _) → C n

inductive ppsigma11 {α : Sort 1} (β : α → Sort 1) : Sort (max 1 1) | m (fst : α) (snd : β fst) : ppsigma11
#check @ppsigma11.rec_on
│ ppsigma11.rec_on :
│   Π {α : Type} {β : α → Type} {C : ppsigma11 β → Sort u_1} (n : ppsigma11 β),
│     (Π (fst : α) (snd : β fst), C (ppsigma11.m fst snd)) → C n


#### Reid Barton (Nov 03 2018 at 15:53):

They look the same to me (especially with set_option pp.proofs true)

#### Reid Barton (Nov 03 2018 at 15:56):

I would maybe believe that the VM can't (easily) implement such a thing, though

#### Reid Barton (Nov 03 2018 at 15:57):

rec_on is an axiom, right? Or one of the related things is?

#### Chris Hughes (Nov 03 2018 at 16:42):

rec_on is rec with the arguments in a different order. rec is an axiom.

#### Kenny Lau (Nov 03 2018 at 16:43):

to be pedantic, it's an axiom schema

#### Chris Hughes (Nov 03 2018 at 16:44):

What's an axiom schema?

#### Kenny Lau (Nov 03 2018 at 16:45):

it isn't one single axiom

#### Kenny Lau (Nov 03 2018 at 16:45):

it's one axiom per inductive type

#### Reid Barton (Nov 03 2018 at 16:45):

Right, I meant [whatever].rec

#### Floris van Doorn (Nov 05 2018 at 13:41):

In fact, there are some expressions which do not have any solution, although you might think it does: max u 1 = v+1 has no solution for u

I'm confused. Lean doesn't know that max (v+1) 1 = v+1?

#### Floris van Doorn (Nov 05 2018 at 13:43):

I presume you misspoke, and meant that there is no solution for v? (I agree with that.)

#### Mario Carneiro (Nov 05 2018 at 13:49):

oh, yes you are right

Last updated: May 15 2021 at 02:11 UTC