Use this tag for questions about using the dependent sum type (Sigma type) in proof assistants.
Sigma types are usually referred to as the dependent sum type or dependent pair type. The name "dependent product type" is ambiguous with the name of pi types.
|
created |
2 years, 5 months ago |
|
viewed |
3 times |
|
active |
2 years, 5 months ago |
|
editors |
1 |
