Zulip Chat Archive

Stream: new members

Topic: Question regarding sigma type signature


view this post on Zulip Rajiv (Dec 12 2020 at 12:42):

In Theorem Proving in Lean, Section 7.2, https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#constructors-with-arguments , there is an example for defining sigma types.

universes u v

inductive sigma₁ {α : Type u} (β : α  Type v)
| dpair : Π a : α, β a  sigma₁

#check @sigma₁

#check @sigma₁.dpair

The type signature for sigma₁.dpair is shown as follows.

sigma₁.dpair : Π {α : Type u_1} {β : α  Type u_2} (a : α), β a  sigma₁ β

I was wondering why dpair is generating term of type sigma₁ β and not sigma₁ α β?

view this post on Zulip Mario Carneiro (Dec 12 2020 at 12:44):

the alpha is implicit

view this post on Zulip Mario Carneiro (Dec 12 2020 at 12:44):

because it was written {α : Type u}

view this post on Zulip Rajiv (Dec 12 2020 at 12:45):

Thanks Mario. Now I see it.


Last updated: May 14 2021 at 21:11 UTC