5
$\begingroup$

There are essentially two ways to impose extentionality on a type theory (I know, it is not very fashionable to impose extentionality these days, but please, bear with me) you can either have a "propositional extentionality axiom" like UIP (uniqueness of identity proof) which says that every two inhabitant of Id(x,y) are propositionally equals, or a "reflexion rules" which says that if you have an inhabitant $a:Id(x,y)$ then $x=y$ and $a=r(x)$. (and if you do it for all types you might not even it to ask that $a=r(x)$)

One expect that the two are equivalent in some precise sens: clearly the reflexion principle implies UIP, so if you can prove something using UIP you can also prove it using the reflection principle, but the converse is a bit harder and one only expect that if we are able to proves that x=y using the reflection principle then one can prove that there is an inhabitant of Id(x,y) using UIP.

I assume it can be formalized by somehow quotienting types & terms using the equivalence relation defined by $\exists v \in Id(x,y)$ but I would be interested to see it done concretely.

So I would be interested by any references making some cases of this into rigorous theorem (for various kind of type theory). If it exists I'm also interested in situation where you only impose UIP/Reflection on some types and not on all types.

(and I don't really care about the specific form of the axioms used to impose extentionality other than the distinction between definitional and propositional)

$\endgroup$
3
$\begingroup$

Martin Hofmann proves in his thesis (theorem 3.2.5) that whenever we have a type $\Gamma \vdash A$ in intensional type theory (ITT) and a term $|\Gamma| \vdash a : |A|$ in ETT there is a term $\Gamma \vdash a' : A$ such that $|\Gamma| \vdash |a'| \equiv a : |A|$. In particular, this implies that whenever some statement is provable in ETT it is also provable in ITT.

This is related to the question that I'm working on, so let me discuss it if you don't mind. Hofmann's theorem implies that ITT and ETT are equivalent in some precise sense. We can define a notion of weak equivalences between type theories (of course, we need to define a category of type theories first) either as a map with some syntactic properties similar to the one described above or as a map that induces (Quillen) equivalence of categories of models (these definitions are equivalent). There are many natural examples of weak equivalences between type theories. This is a work in progress and will be a part of my thesis.

$\endgroup$
  • $\begingroup$ That reference sound perfect, I'll look at it immediately. also What you are working sound interesting ! I assume you are familiar with it, but just in case: do you know the recent work (arxiv.org/abs/1610.00037) of Peter Lumsdaine and Chris Kapulkin which do something which sound a little bit like what you say. I also defined a very similar weak model structure in my own work essentially simultaneously, but we had different motivation and the one of Peter and Chris is a lot closer to syntaxe and type theory. $\endgroup$ – Simon Henry Nov 28 '17 at 19:20
  • 1
    $\begingroup$ Yes, Peter, Chris, and I (independently) work on similar questions with the same motivation, but with different approaches. I also have a construction of almost the same model structure (the difference is that it is a full model structure, but the type theory is slightly unusual, it's closer to the cubical TT). $\endgroup$ – Valery Isaev Nov 28 '17 at 19:47
  • $\begingroup$ Ok, nice. I'll wait to see your thesis then. My version (arxiv.org/abs/1609.04622) is more categorical: it is a "weak model structure" on the category of "category with cofibrations together with a class of equivalences" ("pre-brown categories" in some sense) a bit like the work of Karol Szumilo but in practice a lot more similar to the one constructed by Peter and Chris. But I don't get a semi-model structure: it is "semi" on both side. But my motivation were very different: I was actually interested in constructing and comparing the model structures that these objects generates... $\endgroup$ – Simon Henry Nov 28 '17 at 22:22

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.