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).
@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: Dec 07 2023 at 14:02 UTC