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.