Simple type theory also has topological / homotopical models, but less
of the structure is visible to them. If you think of the types as
topological spaces up to homeomorphism, then you get something
approaching "synthetic topology", where the "predicates" can be
(depending on the rules) either injective continuous functions or
subspace embeddings. (Note that this approach is incompatible with
classical logic, which I believe is built into Isabelle/HOL.) If you
think of the types as spaces up to homotopy, then you get sort of a
truncated version of HoTT, where the predicates are unions of
connected components, and in which probably not very much that's
actually homotopical can be said without dependent types.
On Fri, Sep 28, 2018 at 1:28 PM José Manuel Rodriguez Caballero
<
josephcmac@gmail.com> wrote:
Dear Mike,
Thank you for the elucidation with respect to my confusions concerning type theory and proof assistants. I use Isabelle/HOL in a practical way in order to formalize my own mathematical results in number theory and language theory, but I am a beginner with respect to the theory behind proof assistants.
I watched some lectures of Voevodsky using topological reasoning in homotopy type theory, e.g., talking about the homotopy fiber and drawing some pictures. I like the topological language, because I am mathematician rather than computer scientist. So, it would be wonderful for me to use topological language and maybe topological intuition when I am programming in Isabelle/HOL (simple type theory). But I am not sure if this is possible.
Kind Regards,
Jose M.
El vie., 28 sept. 2018 a las 15:21, Michael Shulman (<shulman@sandiego.edu>) escribió:
It sounds like there are several misconceptions here.
Firstly, many different type theories are used in the subject of
homotopy type theory, but CiC is not really one of them. In addition
to inductive types, CiC is distinguished by a primitive impredicative
universe of propositions, whereas (almost?) all work in HoTT instead
defines the "propositions" to be the homotopy (-1)-types. Coq is a
proof assistant that implements CiC, and Coq is also often used to
formalize HoTT -- but only by ignoring the universe Prop (indeed, we
had to get the Coq developers to implement a special flag for HoTT to
*enable* us to ignore Prop). So even though HoTT is often formalized
in Coq, I think it's misleading to say that CiC is so used. UniMath
is a particular library which formalizes a particular approach to HoTT
in Coq, using roughly only the MLTT core plus univalence; other
libraries for Coq in HoTT also use inductive types and axioms for
HITs.
Secondly, I expect you probably know this even better than I do, but
Isabelle (or Isabelle/Pure) is distinct from Isabelle/HOL:
Isabelle/Pure is a "logical framework" in which one can specify and
work with many different object theories, of which HOL is only one.
It appears that Josh's development is such a theory, so rather than
"HoTT in Isabelle/HOL" it is "HoTT in Isabelle/Pure", or one might say
"Isabelle/HoTT" -- it's not really related at all to Isabelle/HOL
except that they are both formalized in the same logical framework.
Finally, specifying HoTT inside of a logical framework does not make
the logical framework "isomorphic" to HoTT (I'm not even sure what
that would mean), nor does it directly give a topological or
higher-groupoidal interpretation of the framework. In particular,
Josh's Isabelle encoding of HoTT is (like the earlier encoding
Isabelle/CTT of an extensional dependent type theory,
https://isabelle.in.tum.de/dist/library/CTT/index.html) what some
LF-theorists call "synthetic"
(https://ncatlab.org/nlab/show/logical+framework#Synthetic), which
means that it is an encoding of the *untyped syntax* together with the
typing judgments. So I think it is not very different, from a
semantic perspective, from formulating the syntax of HoTT inside, say,
ZFC; in particular it doesn't imply any relationship between the
semantics of the object-language and the meta-language. (The
advantage of a logical framework like Isabelle/Pure over ZFC for this
purpose is the availability of higher-order abstract syntax to
represent variable binding.)
If one uses a logical framework "analytically" instead
(https://ncatlab.org/nlab/show/logical+framework#Analytic), then there
can be a closer connection between the semantics of the framework and
the object language. However, I believe that such an encoding of a
*dependent* type theory is only possible in a framework that is also
dependently typed, unlike Isabelle.
I hope this helps answer your questions; if I misunderstood what you
were asking, please ask again!
Mike
On Thu, Sep 27, 2018 at 10:59 PM José Manuel Rodriguez Caballero
<josephcmac@gmail.com> wrote:
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.
--
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.
--
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.