This is the topic to ask questions on the talk "A Decision Procedure for Equivalence Relations".
The talk will start in 5 minutes.
Nice result! Does it extend to dependent equalities (assuming UIP), like the one in lean: https://arxiv.org/abs/1701.04391
Shameless plug: At 19:00 today we have a completely general algorithm in cubical type theory (agda).
https://hott-uf.github.io/2020/
https://hott-uf.github.io/2020/HoTTUF_2020_paper_16.pdf
@Bas It does not (yet). We are already trying to provide help for old school formalization efforts using setoids. I have seen your talk on the program and plan to attend!
Last updated: Jun 01 2023 at 11:01 UTC