interchangeable representation of theorems

Stream: new members

[Matt Yan]

world 8 level 11 and 12 gives different representation of almost the same theorems. I understand the second one but not the first. From a HoTT perspective, if I understand correctly, every theorem is an inhabited type. With the second representation (add_right_eq_zero), the type of the theorem is $a + b = 0 \rightarrow a = 0$. What is the type in the first case?

[Kevin Buzzard]

The same (modulo the switch from a to b) -- it makes no difference to the type whether you put arguments before or after the colon

[Matt Yan]

I think it's just unrigorous typesetting in the theorems column...becuase if I go to level 11, I can see the expected version image.png

[Kevin Buzzard]

Yeah, I did it all by hand

[Kevin Buzzard]

The actual type is Pi a : nat, Pi b : nat, Pi a + b = 0, a = 0.

[Kevin Buzzard]

That is, you can move the a and b after the colon too (and indeed this is what you'll see if you just type end in NNG (dropping you back into term mode) and then try things like #check @add_right_eq_zero

[Matt Yan]

Kevin Buzzard said:

The actual type is Pi a : nat, Pi b : nat, Pi a + b = 0, a = 0.

I see you lied when you said you were clueless in HoTT :wink:

[Kevin Buzzard]

This is lean

[Kevin Buzzard]

Lean has pi types. I don't know anything about univalence

[Matt Yan]

ahhh you should read the first chapter of the HoTT book! The pi types are covered 30 pages in and it doesn't need any univalence theorem. Actually they seem quite alike to how they are represented in Lean so you are probablly all good :smile:

[Kevin Buzzard]

I did

[Kevin Buzzard]

But I didn't read any more after that

[Patrick Massot]

Matt, I think you call HoTT anything which is dependent type theory. This is why people are confused.

[Patrick Massot]

The same confusion would be present if you start calling "local class field theory" anything involving any kind of algebraic structure.

[Matt Yan]

Patrick Massot said:

Matt, I think you call HoTT anything which is dependent type theory. This is why people are confused.

sorry I just learned the dependent types and was too excited to see a Pi