Théo Zimmermann (Jun 24 2020 at 11:19): Théo Zimmermann (Jun 24 2020 at 11:19):This is the topic to ask questions on the talk "A Decision Procedure for Equivalence Relations".
Emilio Jesús Gallego Arias (Jul 05 2020 at 13:06):The talk will start in 5 minutes.
Bas Spitters (Jul 05 2020 at 13:16):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
Pierre Corbineau (Jul 05 2020 at 13:37):@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