Skip to main content
4 votes

Non-trivial examples of dependent sum ($\Sigma$-types) in Lean?

I would like to warn you that dependent product type is usually used for the dependent function type, while the dependent version of the product type is referred to as the dependent sum type. ...
ice1000's user avatar
  • 6,256
1 vote

What are the typechecking differences between records and iterated sigma types in Agda?

There is no typechecking difference because Sigma types are records in Agda. So generally, Sigma types represent a subset of the options one has for declaring record types (eta or no, inductive or no, ...
Joey Eremondi's user avatar
1 vote

Non-trivial examples of dependent sum ($\Sigma$-types) in Lean?

Here an example from group theory: Consider a family of groups Π (i : ι), G i (which is using the Pi-type to say that for every index ...
Joachim Breitner's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible