From: Bas Spitters <firstname.lastname@example.org>
To: Nicola Gambino <N.Gambino@leeds.ac.uk>
Cc: Michael Shulman <email@example.com>,
Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Papers on constructive simplicial homotopy theory
Date: Thu, 18 Jul 2019 10:15:55 +0200 [thread overview]
Message-ID: <CAOoPQuS3E+dK8FPigSd+6KDtk9bCnfrwLsbKBR_93h3WBL7jag@mail.gmail.com> (raw)
In our work on GCTT we used the internal DTT/DPL of a topos.
https://arxiv.org/abs/1611.09263 (sec 4)
There's a convenient presentation of this in the work of Phao (appendix 1)
and the elephant D4.3,4.4.
It may not give you everything that you need, but it may be a start.
On Thu, Jul 18, 2019 at 9:55 AM Nicola Gambino <N.Gambino@leeds.ac.uk> wrote:
> Dear Mike,
> On 17 Jul 2019, at 18:56, Michael Shulman <firstname.lastname@example.org> wrote:
> Most of these papers describe the situation with phrases like "we are
> working in the internal language of a category with finite limits" or
> an elementary topos with NNO, or in CZF, and by an "abuse of language"
> we interpret "for all x there exists a y" as referring to the giving
> of a function assigning a y to each x. But wouldn't it be more
> precise and less abusive to just work in dependent type theory with
> Sigma and Id types, and sometimes Pi and Nat, and use the untruncated
> propositions-as-types logic where "for all x there exists a y"
> literally means Pi(x) Sigma(y) and therefore (by the "type-theoretic
> principle of non-choice") automatically induces a function assigning a
> y to each x? That would also allow asking and answering the question
> of how much UIP is required -- do these model structures exist in
> Thank you for your email.
> Your suggestion of working in a dependent type theory is interesting. I am not sure what kind of dependent type theory would be sufficient to develop these papers and what would be the best approach to the formalization (e.g. via sets-as-hsets or via sets-as-setoids).
> Regarding the dependent type theory, apart from basic rules, I guess one would need:
> - some extensionality,
> - propositional truncations,
> - pushouts,
> - some inductive types (for the instances of the small object argument)
> - at least one universe (cf. quantification over all Kan complexes).
> One could then keep track explicitly of which existential quantifies are to be left untruncated and which ones can be truncated, and then see if everything can be done in HoTT.
> Is this the kind of thing you had in mind?
> Another approach to avoiding the abuse of language, suggested by Andre’ Joyal, is to develop a theory of “split” weak factorisation systems, i.e. weak factorisation systems in which one has a given choice of fillers, and work with them. This would be a variant of the theory of algebraic weak factorisation systems. We are working on that.
> With best wishes,
> PS The first link in my email was incorrect. Simon Henry’s paper "Weak model categories in classical and constructive mathematics” is available at https://arxiv.org/abs/1807.02650.
> Dr Nicola Gambino
> Associate Professor in Pure Mathematics
> School of Mathematics, University of Leeds
> 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 HomotopyTypeTheoryemail@example.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D49A1FEA-4CE1-448F-97A8-46065AF9E7B6%40leeds.ac.uk.
> 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 HomotopyTypeTheoryfirstname.lastname@example.org.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuS3E%2BdK8FPigSd%2B6KDtk9bCnfrwLsbKBR_93h3WBL7jag%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.
next prev parent reply other threads:[~2019-07-18 8:16 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-07-15 10:18 Nicola Gambino
2019-07-17 17:56 ` Michael Shulman
2019-07-18 7:55 ` Nicola Gambino
2019-07-18 8:15 ` Bas Spitters [this message]
2019-07-18 12:21 ` Michael Shulman
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:
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
* 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).