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

[Michael Shulman <shu...@sandiego.edu>]

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?
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.