Zulip Chat Archive

Stream: new members

Topic: interchangeable representation of theorems


Matt Yan (Feb 07 2022 at 07:51):

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=0a=0 a + b = 0 \rightarrow a = 0 . What is the type in the first case?

Kevin Buzzard (Feb 07 2022 at 07:54):

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 (Feb 07 2022 at 07:54):

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 (Feb 07 2022 at 07:54):

Yeah, I did it all by hand

Kevin Buzzard (Feb 07 2022 at 07:55):

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

Kevin Buzzard (Feb 07 2022 at 07:57):

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 (Feb 07 2022 at 07:57):

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 (Feb 07 2022 at 07:57):

This is lean

Kevin Buzzard (Feb 07 2022 at 07:57):

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

Matt Yan (Feb 07 2022 at 08:00):

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 (Feb 07 2022 at 08:03):

I did

Kevin Buzzard (Feb 07 2022 at 08:03):

But I didn't read any more after that

Patrick Massot (Feb 07 2022 at 08:05):

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

Patrick Massot (Feb 07 2022 at 08:06):

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

Matt Yan (Feb 07 2022 at 08:10):

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


Last updated: Dec 20 2023 at 11:08 UTC