Email Gateway (Aug 22 2022 at 17:47): Email Gateway (Aug 22 2022 at 17:47):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Is it possible or natural to do homotopy type theory in Isabelle?
Best regards,
Jose M.
Email Gateway (Aug 22 2022 at 17:48):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
According to my personal experience, Isabelle is most comfortable for doing mathematics than Coq, with the only exception of synthetic homotopy theory, where Voevodsky did something revolutionary in UniMath. It would be nice to see synthetic homotopy theory in Isabelle.
Kind Regards,
Jose M.
Last updated: Nov 21 2024 at 12:39 UTC