Zulip Chat Archive

Stream: new members

Topic: Question regarding sigma type signature

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₁ α β?

Mario Carneiro (Dec 12 2020 at 12:44):

the alpha is implicit

Mario Carneiro (Dec 12 2020 at 12:44):

because it was written {α : Type u}

Rajiv (Dec 12 2020 at 12:45):

Thanks Mario. Now I see it.

Last updated: Dec 20 2023 at 11:08 UTC