Mike Shulman
Mike Shulman
It's a constant source of low-level annoyance to me that Agda doesn't permit using the standard mathematical symbol `=` for propositional equality, and I don't think I'm the only one....
While I'm making wacky rewriting requests (see #5961), I would like to have a version of rewriting that doesn't insist on reasoning modulo _beta_-expansion. Consider for instance: ```agda postulate A...
I think it would be nice to have a version of `--rewriting` that does pure syntactic matching rather than reasoning up to eta-equality. This would mean that ordinary confluence is...
I'm seeing some weird behavior with the current HoTT-Agda library in Agda 2.5.1.1: frequently when I want to compose two complicated paths, Agda is unwilling to parse the path-composition operator...
For Emacs users like myself, it would be nice to have an Emacs mode for elpi. In fact, I haven't been able to find an Emacs mode for any kind...
Apparently our hacks like ``` Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in Type@{i}. ``` can now be replaced with ``` Definition Type2@{i j...
Is it possible to declare something as a "coercion" for purposes of not being printed, but not for purposes of being used when parsing user input? It would be nice...
I know we discussed this a little bit ago, but I don't remember where or what the arguments were. It seems to me that making it a sigT would have...
As discussed at #1155, it would be nice to be able to write something like `x^-1` instead of `- x` for inverses in a multiplicative group (i.e. a group with...
Here's my next iteration of coinductive wild oo-categories. Change # 1: By getting rid of (oo,oo)-categories and considering only (oo,n)-categories for finite n, the proof that equivalences compose becomes much...