Recently a user of Isabelle provided his version of HoTT here: https://github.com/jaycech3n/Isabelle-HoTT

  A brief description from the author: 

Joshua:
This logic implements intensional Martin-Löf type theory with univalent cumulative Russell-style universes, and is 
polymorphic.

This version of HoTT involves some axiomatization in addition to univalence, e.g., Sum.thy and Prod.thy.

  HoTT is traditionally developed in CiC, whereas UniMath is traditionally developed in the Martin-Löf type theory (as part of CiC in Coq). As a user of Isabelle/HOL, interested in homotopy type theory, I would like to know the topological interpretation, as a weak infinite groupoid, of Simple Type Theory (the type theory behind Isabelle/HOL) and how it becomes isomorphic to HoTT by means of the axiomatization (maybe there is some topological intuition related to this transformation, cutting and pasting).

Thank you in advance,
José M.


--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.