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 
> <javascript:>> 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?
>