Questions tagged [sigma-type]
Use this tag for questions about using the dependent sum type (Sigma type) in proof assistants.
3
questions
2
votes
0
answers
102
views
An unexpectedly hard question about type equality (of sigma types)
Suppose you have A: Type and P Q: A -> Prop such that {x : A | P x} = {x : A | Q x}. Can ...
- 121
6
votes
1
answer
101
views
What are the typechecking differences between records and iterated sigma types in Agda?
If we have univalence at hand, the records and iterated sigma versions of some type will be equal. Still, there may be some important typechecking-related differences.
For example, it seems that one ...
- 161
7
votes
2
answers
742
views
Non-trivial examples of dependent sum ($\Sigma$-types) in Lean?
I am trying to understand the concept of dependent sum types ($\Sigma$ types) using concrete examples. The example given in Theorem Proving in Lean 4 seems to be a degenerate case rendering the ...
- 2,220