Zulip Chat Archive

Stream: new members

Topic: function type


Holly Liu (Aug 21 2021 at 15:35):

what's the difference between functions of type Π and of type λ?

Eric Rodriguez (Aug 21 2021 at 15:36):

Π declares a function type, λ introduces it to prove things. Π is , and λ is intros, basically

Eric Rodriguez (Aug 21 2021 at 15:37):

for example: def id' : Π α : Type*, Type* := λ α, α

Johan Commelin (Aug 21 2021 at 15:39):

In other words, a term of shape λ _, _ has a type of shape Π _, _.

Holly Liu (Aug 21 2021 at 16:10):

ok, thanks

Kevin Buzzard (Aug 21 2021 at 19:21):

Pi A, B is how the computer scientists write Hom(A,B) and lambda is how they write \mapsto


Last updated: Dec 20 2023 at 11:08 UTC