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: Feb 06 2023 at 05:03 UTC