Mike Shulman

Since Id doesn't reduce to the first component of ap, it should have all the same computation rules as the latter (as should the other pieces of IdU: tr, lift,...

- [x] sym(sym(x)) = x - [ ] sym(ap_ap(x)) = ap_ap(sym(x)) - [ ] sym(refl_refl) = refl_refl (special case of the previous) - [ ] braid equation: sym(ap_sym(sym(x))) = ap_sym(sym(ap_sym(x)))...

Compute sym on all types

1

- [ ] Unit type - [ ] Sigma-types - [ ] Pi-types - [ ] Copy-types - [ ] The universe - [ ] Sum-types - [ ] Natural...

Speed things up

1

Why does having imported Pi.Transport.Lift make Pi.Transport.Ulift slow? Why does having imported Pi.Transport make Arrow.Transport slow?

We have a separate type of integers to make things easier for our summer 2022 exercises. - [x] encode-decode, decidable equality, sethood - [ ] ap and refl on the...

- [x] encode-decode, decidable equality, sethood - [ ] ap and refl on the constructors - [ ] ap-ind - [ ] refl-ind - [ ] tr - [ ]...

It would be really nice if Agda had a `Reserved Notation` feature like Coq, but I suppose that's impossible given its architecture.

- [ ] ap-case - [ ] refl-case - [ ] tr - [ ] lift - [ ] utr and ulift

de Bruijn index out of scope when rewriting

3

I'm sorry that this example is so long; I wasn't able to remove any parts of it and still reproduce the error. ```agda {-# OPTIONS --type-in-type --rewriting #-} infix 10...

Internal error rewriting with holes

2

While trying to adapt the rest of my code to the restriction of #5996, I ran into another internal error. ```agda {-# OPTIONS --type-in-type --rewriting #-} infix 10 _≡_ infixl...