Re: [HoTT] Papers on constructive simplicial homotopy theory

[Michael Shulman <shulman@sandiego.edu>]

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.