Proper sigma types #6

New issue

Open

opened 2024-12-05 19:23:06 -08:00 by wball · 1 comment

wball commented

2024-12-05 19:23:06 -08:00

Owner

This would greatly simplify impredicative code involving and and exists, as well as make it possible to use in the predicative universes. Syntax sugar for records could be built on top of sigma types as well, which would be nice. Supporting eta equality as well would get rid of the axiom definite_description in peano.pg, which would be very nice.

This would greatly simplify impredicative code involving `and` and `exists`, as well as make it possible to use in the predicative universes. Syntax sugar for records could be built on top of sigma types as well, which would be nice. Supporting eta equality as well would get rid of the axiom `definite_description` in `peano.pg`, which would be very nice.

wball referenced this issue

2024-12-05 19:24:47 -08:00

Proper sum types #7

wball referenced this issue

2024-12-05 19:26:26 -08:00

Full on inductive definitions #8

wball added the

core

label 2024-12-05 19:45:22 -08:00

wball commented

2025-01-24 01:05:41 -08:00

Author

Owner

Working on products in its own branch. Currently support non-dependent products with a very temporary placeholder syntax as of 2c1f193d77. One very nice consequence of natively supporting products rather than relying on the impredicative definition of products that I didn't realize is that we get type inference on calls to previous and_elim_{l,r} and and_intro almost for free.

Remaining TODOs:

Finalize syntax/improve parser
Support dependent products (sums? this notation/terminology is kind of stupid)
Update treesitter
Allow × and , to appear in sections (π₁ and π₂ would be impossible to curry without further inference)

Working on products in its own branch. Currently support non-dependent products with a very temporary placeholder syntax as of 2c1f193d77. One very nice consequence of natively supporting products rather than relying on the impredicative definition of products that I didn't realize is that we get `type inference` on calls to previous `and_elim_{l,r}` and `and_intro` almost for free. Remaining TODOs: - [ ] Finalize syntax/improve parser - [ ] Support dependent products (sums? this notation/terminology is kind of stupid) - [ ] Update treesitter - [ ] Allow `×` and `,` to appear in sections (`π₁` and `π₂` would be impossible to curry without further inference)