Email Gateway (Aug 22 2022 at 19:14): Email Gateway (Aug 22 2022 at 19:14):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
If I well-understood Grothendieck's homotopy hypothesis, Isabelle/HoTT can
be modeled in Isabelle/HOL, by representing homotopy types via Kan
complexes (we need to develop the theory of Kan complexes in Isabelle/HOL
in this approach). I may be wrong, I am not an expert in this subject. So,
do not believe me. Here some references:
Mike Shulman (slides):
https://home.sandiego.edu/~shulman/papers/hott-grothendieck.pdf
Kan complexes (definition): https://en.wikipedia.org/wiki/Kan_fibration
Grothendieck's original manuscript (English):
http://www.landsburg.com/grothendieck/EsquisseEng.pdf
Grothendieck's original manuscript (French):
https://webusers.imj-prg.fr/~leila.schneps/grothendieckcircle/EsquisseFr.pdf
John Baez (list of references): http://math.ucr.edu/home/baez/homotopy/
The Grothendieck Song (good to develop the vocabulary):
https://richardelwes.co.uk/2015/01/02/the-grothendieck-song/
Kind Regards,
José M.
Last updated: Nov 21 2024 at 12:39 UTC