Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: "José Manuel Rodriguez Caballero" <josephcmac@gmail.com>
To: HomotopyTypeTheory@googlegroups.com
Cc: Joshua Chen <joshua.chen@uni-bonn.de>
Subject: Re: [HoTT] the weak infinite groupoid in Simple Type Theory
Date: Mon, 1 Oct 2018 19:14:52 -0400	[thread overview]
Message-ID: <CAA8xVUg-X1=2P56wwnasqmEP_aYE55vBq+_aNYmBKtmNinzYrQ@mail.gmail.com> (raw)
In-Reply-To: <6535A055-1DC4-42AD-A0EB-37B1D523ECA1@cmu.edu>

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

>
> Mike wrote:
> 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.


Indeed, I think that the lemma

lemma card_permutations:
  assumes "card S = n"
    and "finite S"
  shows "card {p. p permutes S} = fact n"

in HOL/Library/Permutations.thy

is a truncation of the following theorem due to Voevodsky

Theorem weqfromweqstntostn ( n : nat ) : ( (⟦n⟧) ≃ (⟦n⟧) ) ≃ ⟦factorial n⟧.

which can be found here:
https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/StandardFiniteSets.v

By the way, I do not know if the project of developing combinatorics from
homotopy type theory, started by Voevodsky, continues today or if it
stopped.

Kind Regards,
José M.


El lun., 1 oct. 2018 a las 10:53, Steve Awodey (<awodey@cmu.edu>) escribió:

> of course, there are also topological models of simple type theory resp.
> HOL, and extensional MLTT, which are then not homotopical.
> See e.g.:
>
> https://arxiv.org/abs/math/9707206
>
> Steve
>
> On Oct 1, 2018, at 10:43 AM, Michael Shulman <shulman@sandiego.edu> wrote:
>
> 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.
>
>
>

-- 
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: 11243 bytes --]

  reply	other threads:[~2018-10-01 23:15 UTC|newest]

Thread overview: 12+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2018-09-27 13:10 [HoTT] Characteristic Classes for Types Juan Ospina
2018-09-28  0:38 ` [HoTT] " Ali Caglayan
2018-09-28  1:00   ` Juan Ospina
2018-09-28  1:04   ` Juan Ospina
2018-09-28  2:51   ` Michael Shulman
2018-09-28  5:59 ` [HoTT] the weak infinite groupoid in Simple Type Theory José Manuel Rodriguez Caballero
2018-09-28 19:21   ` Michael Shulman
2018-09-28 20:27     ` José Manuel Rodriguez Caballero
2018-10-01 14:43       ` Michael Shulman
2018-10-01 14:53         ` Steve Awodey
2018-10-01 23:14           ` José Manuel Rodriguez Caballero [this message]
2018-10-02 16:20             ` Michael Shulman

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CAA8xVUg-X1=2P56wwnasqmEP_aYE55vBq+_aNYmBKtmNinzYrQ@mail.gmail.com' \
    --to=josephcmac@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=joshua.chen@uni-bonn.de \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).