From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 18 Dec 2017 03:55:35 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <11CC10D7-7853-48E7-88BD-42A8EFD47998@exmail.nottingham.ac.uk> <20171212120233.GA32661@mathematik.tu-darmstadt.de> <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk> <20171215170011.GA22027@mathematik.tu-darmstadt.de> <20171217102151.GA16619@mathematik.tu-darmstadt.de> Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_6632_2054263458.1513598136049" ------=_Part_6632_2054263458.1513598136049 Content-Type: multipart/alternative; boundary="----=_Part_6633_392402252.1513598136049" ------=_Part_6633_392402252.1513598136049 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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 > 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? > ------=_Part_6633_392402252.1513598136049 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Oh right. Static propositions alone doesn't seem to gu= arantee a quasitopos either.

I thought HITs make sense with static p= rops. 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 t= o me, except that I don't know whether a
static universe of props without unique choice *actually* gives a
quasitopos. =C2=A0It gives you a class of subobjects that have a classi= fer,
which looks kind of like a quasitopos, but can we prove that they are
actually the strong/regular monos as in a quasitopos? =C2=A0And 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 u= sing 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 b= e consistent
> as an additional primitive, or you can ensure in some other way th= at 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&= #39;t already
> propositions, but they all correspond to a proposition stating tha= t 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-de= pendent
> 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 sys= tem, along
> with unique choice or equivalent. (To say nothing of whether that&= #39;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-irrelev= ance still doesn't
> come up.
>
> But if it is, you should at least have typal proof-irrelevance. (T= hat is,
> stated using equality types.)
>
> In that case, with equality reflection, you automatically get judg= mental
> 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?
------=_Part_6633_392402252.1513598136049-- ------=_Part_6632_2054263458.1513598136049--