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

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

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

Well that's true. For some reason, I was thinking equality would still be 
an ordinary type, but I guess that would be silly.

So what do you require, for HITs to "make sense", with equality being a 
static prop family? That they can provide finite colimits? Don't they do 
this, analogously to homotopy colimits in HoTT?

On Monday, December 18, 2017 at 11:25:22 AM UTC-5, Michael Shulman wrote:
>
> HITs involve equality, so if equality is a static prop, then it is 
> involved. 
>
> On Mon, Dec 18, 2017 at 3:55 AM, Matt Oliveri <atm...@gmail.com 
> <javascript:>> wrote: 
> > Oh right. Static propositions alone doesn't seem to guarantee a 
> quasitopos 
> > either. 
> > 
> > I thought HITs make sense with static props. After all, the type of 
> > propositions isn't even involved, formally. 
> > 
> > On Monday, December 18, 2017 at 5:00:51 AM UTC-5, Michael Shulman wrote: 
> >> 
> >> That seems about right to me, except that I don't know whether a 
> >> static universe of props without unique choice *actually* gives a 
> >> quasitopos.  It gives you a class of subobjects that have a classifer, 
> >> which looks kind of like a quasitopos, but can we prove that they are 
> >> actually the strong/regular monos as in a quasitopos?  And a 
> >> quasitopos also has finite colimits; do HITs make sense with a static 
> >> Prop? 
> >> 
> >> On Sun, Dec 17, 2017 at 11:41 PM, Matt Oliveri <atm...@gmail.com> 
> wrote: 
> >> > 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: 4786 bytes --]