Add Pi types for iterative sets#1306

Open

flgrubm wants to merge 11 commits into

agda:masterfrom

flgrubm:iterative-sets-pi

Commits on Apr 29, 2026

Add (non-terminating) Pi type codes for iterative sets
flgrubm
committed
Rename `overline` to `index` and `tilde` to `elements` (to reflect upstream change)
flgrubm
committed
Add illegal whitespace to fail check and prevent CI from running non-terminating code
flgrubm
committed

Commits on May 12, 2026

Improve performance of UnorderedPair – now compiles fast without `--lossy-unification`
flgrubm
committed
Improve legibility of ordered pairs – still doesn't compile without `--lossy-unification` [skip ci]
flgrubm
committed

Commits on May 16, 2026

Commits on May 17, 2026