Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
* [HoTT] Papers on constructive simplicial homotopy theory
@ 2019-07-15 10:18 Nicola Gambino
  2019-07-17 17:56 ` Michael Shulman
  0 siblings, 1 reply; 5+ messages in thread
From: Nicola Gambino @ 2019-07-15 10:18 UTC (permalink / raw)
  To: Homotopy Type Theory, constructivenews

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

Dear all,

Readers of this list may be interested in the following series of papers:

[1] S. Henry, Weak model categories in classical and constructive mathematics,

https://arxiv.org/abs/1807.02650<https://arxiv.org/abs/1905.06281>

[2] S. Henry, A constructive account of the Kan-Quillen model structure and of Kan's Ex∞ functor,

  https://arxiv.org/abs/1905.06160

[3] N. Gambino, C. Sattler, K. Szumiło, The constructive Kan-Quillen model structure: two new proofs

https://arxiv.org/abs/1907.05394

[4] N. Gambino, S. Henry, Towards a constructive simplicial model of Univalent Foundations

https://arxiv.org/abs/1905.06281

Apologies for cross-posting.

With best regards,
Nicola

==
Dr Nicola Gambino
Associate Professor in Pure Mathematics
School of Mathematics, University of Leeds
http://www1.maths.leeds.ac.uk/~pmtng/




-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D3003278-EEC5-46A0-A07A-AD260A830DB2%40leeds.ac.uk.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 5+ messages in thread

* Re: [HoTT] Papers on constructive simplicial homotopy theory
  2019-07-15 10:18 [HoTT] Papers on constructive simplicial homotopy theory Nicola Gambino
@ 2019-07-17 17:56 ` Michael Shulman
  2019-07-18  7:55   ` Nicola Gambino
  0 siblings, 1 reply; 5+ messages in thread
From: Michael Shulman @ 2019-07-17 17:56 UTC (permalink / raw)
  To: Homotopy Type Theory

Thanks for collecting all those links together, Nicola!

One of the aspects of this theory that I find especially interesting
is the observation that many uses of AC in classical model category
theory can be avoided by working with "fibration structures" and
requiring all factorization and lifting "properties" to be instead
given by functions.  Of course a similar perspective is present in the
notions of algebraic model category (and algebraic weak factorization
system) that have recently been playing a bigger role even in
classical homotopy theory, so it's interesting that the natural
constructive approach is also to work with structure rather than
properties, even in the "non-algebraic" case when the structure isn't
at all "coherent".

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
HoTT?



On Mon, Jul 15, 2019 at 3:18 AM Nicola Gambino <N.Gambino@leeds.ac.uk> wrote:
>
> Dear all,
>
> Readers of this list may be interested in the following series of papers:
>
> [1] S. Henry, Weak model categories in classical and constructive mathematics,
>
> https://arxiv.org/abs/1807.02650
>
> [2] S. Henry, A constructive account of the Kan-Quillen model structure and of Kan's Ex∞ functor,
>
>   https://arxiv.org/abs/1905.06160
>
> [3] N. Gambino, C. Sattler, K. Szumiło, The constructive Kan-Quillen model structure: two new proofs
>
> https://arxiv.org/abs/1907.05394
>
> [4] N. Gambino, S. Henry, Towards a constructive simplicial model of Univalent Foundations
>
> https://arxiv.org/abs/1905.06281
>
> Apologies for cross-posting.
>
> With best regards,
> Nicola
>
> ==
> Dr Nicola Gambino
> Associate Professor in Pure Mathematics
> School of Mathematics, University of Leeds
> http://www1.maths.leeds.ac.uk/~pmtng/
>
>
>
>
> --
> 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.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D3003278-EEC5-46A0-A07A-AD260A830DB2%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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQzEtgcx15UZrpos%2Bch8TCKsnQSotvpK5oEVO2EVD160eQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 5+ messages in thread

* Re: [HoTT] Papers on constructive simplicial homotopy theory
  2019-07-17 17:56 ` Michael Shulman
@ 2019-07-18  7:55   ` Nicola Gambino
  2019-07-18  8:15     ` Bas Spitters
  2019-07-18 12:21     ` Michael Shulman
  0 siblings, 2 replies; 5+ messages in thread
From: Nicola Gambino @ 2019-07-18  7:55 UTC (permalink / raw)
  To: Michael Shulman; +Cc: Homotopy Type Theory

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

Dear Mike,

On 17 Jul 2019, at 18:56, Michael Shulman <shulman@sandiego.edu<mailto:shulman@sandiego.edu>> 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
HoTT?

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,
Nicola

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
http://www1.maths.leeds.ac.uk/~pmtng/




-- 
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.
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.

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

^ permalink raw reply	[flat|nested] 5+ messages in thread

* Re: [HoTT] Papers on constructive simplicial homotopy theory
  2019-07-18  7:55   ` Nicola Gambino
@ 2019-07-18  8:15     ` Bas Spitters
  2019-07-18 12:21     ` Michael Shulman
  1 sibling, 0 replies; 5+ messages in thread
From: Bas Spitters @ 2019-07-18  8:15 UTC (permalink / raw)
  To: Nicola Gambino; +Cc: Michael Shulman, Homotopy Type Theory

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)
www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/
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 <shulman@sandiego.edu> 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
> HoTT?
>
>
> 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,
> Nicola
>
> 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
> http://www1.maths.leeds.ac.uk/~pmtng/
>
>
>
>
> --
> 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.
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
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.

^ permalink raw reply	[flat|nested] 5+ messages in thread

* Re: [HoTT] Papers on constructive simplicial homotopy theory
  2019-07-18  7:55   ` Nicola Gambino
  2019-07-18  8:15     ` Bas Spitters
@ 2019-07-18 12:21     ` Michael Shulman
  1 sibling, 0 replies; 5+ messages in thread
From: Michael Shulman @ 2019-07-18 12:21 UTC (permalink / raw)
  To: Nicola Gambino; +Cc: Homotopy Type Theory

For something that ought to work in the internal language of a
category with finite limits, like the first paper on weak model
categories, it should technically suffice to have Sigma- and Id-types
with UIP (since those are a version of that internal language).  If we
wanted to internalize more of the abusive external statements like "f
is an acyclic fibration if it has right lifting for every
cofibration", it should be enough to add Pi-types and a universe.

To enhance this to the internal language of an elementary
(predicative) 1-topos with NNO or an analogue of CZF, coproducts,
propositional truncations, pushouts, and a natural numbers type should
be enough.  I'm very curious to hear where propositional truncations
and pushouts are used (if ever), since in so many places the "for all
x, exists y" is actually an untruncated Sigma.  Certainly pushouts
appear in the small object argument, but I wonder whether those
pushouts could be implemented with coproducts in the case when they
are pushouts of cofibrations that are sufficiently "complemented
inclusions" (the pushout of A -> X along a complemented inclusion A ->
A+B is just X+B).

On Thu, Jul 18, 2019 at 12:55 AM Nicola Gambino <N.Gambino@leeds.ac.uk> wrote:
>
> Dear Mike,
>
> On 17 Jul 2019, at 18:56, Michael Shulman <shulman@sandiego.edu> 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
> HoTT?
>
>
> 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,
> Nicola
>
> 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
> http://www1.maths.leeds.ac.uk/~pmtng/
>
>
>
>
> --
> 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.
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQySjeDQXj_wWt9m1oQbAJj0%2BDn-NQ0yBX__DO1N3NBC_g%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 5+ messages in thread

end of thread, back to index

Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-07-15 10:18 [HoTT] Papers on constructive simplicial homotopy theory Nicola Gambino
2019-07-17 17:56 ` Michael Shulman
2019-07-18  7:55   ` Nicola Gambino
2019-07-18  8:15     ` Bas Spitters
2019-07-18 12:21     ` Michael Shulman

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox