Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Hott?

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

view this post on Zulip 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: Apr 25 2024 at 20:15 UTC