[HoTT] the weak infinite groupoid in Simple Type Theory

["José Manuel Rodriguez Caballero" <josephcmac@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1274 bytes --]

  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.

[-- Attachment #2: Type: text/html, Size: 1903 bytes --]