Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Matt Oliveri <atm...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1781 bytes --]

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

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.

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

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.

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.

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. This does not necessarily mean that proofs are 
computationally irrelevant. With unique choice, they cannot be, or else you 
lose canonicity.

All OK?

[-- Attachment #1.2: Type: text/html, Size: 1908 bytes --]