Stream: Coq workshop 2020

Topic: [S3] A Decision Procedure for Equivalence Relations


view this post on Zulip 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".

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2020 at 13:06):

The talk will start in 5 minutes.

view this post on Zulip 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

view this post on Zulip 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: Dec 07 2023 at 14:02 UTC