Skip to main content

Questions tagged [sigma-type]

Use this tag for questions about using the dependent sum type (Sigma type) in proof assistants.

Filter by
Sorted by
Tagged with
2 votes
0 answers

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 ...
Veky's user avatar
  • 121
6 votes
1 answer

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 ...
Fernando Chu's user avatar
7 votes
2 answers

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 ...
tinlyx's user avatar
  • 2,116