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