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<= br style=3D"caret-color: rgb(0, 0, 0); font-family: LucidaGrande; font-size= : 12px; font-style: normal; font-variant-caps: normal; font-weight: normal;= letter-spacing: normal; text-align: start; text-indent: 0px; text-transfor= m: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width:= 0px; text-decoration: none;" class=3D""> an elementary topos with NNO, or in CZF, and by an "abuse of language&qu= ot;
we interpret "for all x there exists a y" as referring to the givin= g
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?

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 dev= elop 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 o= ne 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).&n= bsp;

One could then keep track explicitly of which existential quantifies a= re 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= =E2=80=99 Joyal, is to develop a theory of =E2=80=9Csplit=E2=80=9D weak fac= torisation systems, i.e. weak factorisation systems in which one has a give= n choice of fillers, and work with them. This would be a variant of the theory of algebraic weak factorisation systems. We are work= ing on that.

With best wishes,
Nicola

PS The first link in my email was incorrect. Simon Henry=E2=80=99s pap= er "Weak model categories in cl= assical and constructive mathematics=E2=80=9D is available at <= a href=3D"https://arxiv.org/abs/1807.02650" class=3D"">https://arxiv.org/ab= s/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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/m= sgid/HomotopyTypeTheory/D49A1FEA-4CE1-448F-97A8-46065AF9E7B6%40leeds.ac.uk<= /a>.
For more options, visit