From: <homotop...@googlegroups.com> on behalf of Matt Oliveri <at...@gmail.com>
Date: Monday, 18 December 2017 at 07:41
To: Homotopy Type Theory <homotop...@googlegroups.com>
Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

 

Hello. I'd like to see if I have the situation straight:

For presenting a topos as a type system, there are expected to be (at least) two styles: having a type of "static" propositions, or using hprops.

With hprops, you can prove unique choice, so it's always topos-like (pretopos?).

 

Yes, indeed. The remaining issue is the question of impredicativity. If you want to stay predicative you may want to add quotients or QITs. Interestingly it seems that QITs are more expressive then quotients (which can be encoded impredicatively).

With static props, you can't prove unique choice, but it may be consistent as an additional primitive, or you can ensure in some other way that you have a subobject classifier.

 

Yes, indeed. However, adding postulates to Type Theory is just a stop gap measure because you still don’t have a computational interpretation. While we have a computational interpretation for most of HoTT, namely cubical type theory ala Coquand et al, one might hope that there is a simpler way to deal with the set level fragment of HoTT.

If you don't necessarily have unique choice or equivalent, you're dealing with a quasitopos, which is a more general thing.

 

Basically you reflect some subobjects but not all. I don’t yet understand how the definition of a quasitops relates to static universes of propositios.

With static props and unique choice, subsingletons generally aren't already propositions, but they all correspond to a proposition stating that the subsingleton is inhabited. Unique choice obtains the element of a subsingleton known to be inhabited.

The usual way to present a topos as a type system is with a non-dependent type system like IHOL. This will not be able to express hprops, so static props is the way. Proofs will not be objects, so proof-irrelevance doesn't come up.

 

Indeed or to put it the other way: set level HoTT is a novel way to present a topos. And as I said above, QITs are an interesting extension which in some instances avoids appealing to the axiom of choice.

The static props approach can also be used in a dependent type system, along with unique choice or equivalent. (To say nothing of whether that's a natural kind of system.)

In a dependent type system, a type of static props may or may not be a universe.

 

What do you mean by “is a universe” here?

If it's not, proofs still aren't objects and proof-irrelevance still doesn't come up.

But if it is, you should at least have typal proof-irrelevance. (That is, stated using equality types.)

In that case, with equality reflection, you automatically get judgmental proof-irrelevance.

 

For equality but not for propositions in general.

 

This does not necessarily mean that proofs are computationally irrelevant.

 

Now I am confused: what is the difference between judgmental and computational irrelevance?

 

With unique choice, they cannot be, or else you lose canonicity.

Since I didn’t understand the previous sentences I am not sure about this conclusion. It sounds right, though.

 

Thorsten

All OK?