From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 18 Dec 2017 12:08:14 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <1a2c4994-6b09-4a57-be5e-1fe0a7495e28@googlegroups.com> 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_3792_48485523.1513627695152" ------=_Part_3792_48485523.1513627695152 Content-Type: multipart/alternative; boundary="----=_Part_3793_1552826101.1513627695153" ------=_Part_3793_1552826101.1513627695153 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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 > 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 > 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_3793_1552826101.1513627695153 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Well that's true. For some reason, I was thinking equa= lity would still be an ordinary type, but I guess that would be silly.
<= br>So what do you require, for HITs to "make sense", with equalit= y being a static prop family? That they can provide finite colimits? Don= 9;t they do this, analogously to homotopy colimits in HoTT?

On Monda= y, 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> w= rote:
> 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 o= f
> 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 whe= ther a
>> static universe of props without unique choice *actually* give= s a
>> quasitopos. =C2=A0It gives you a class of subobjects that have= a classifer,
>> which looks kind of like a quasitopos, but can we prove that t= hey are
>> actually the strong/regular monos as in a quasitopos? =C2=A0An= d 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...@g= mail.com> wrote:
>> > Hello. I'd like to see if I have the situation straig= ht:
>> >
>> > For presenting a topos as a type system, there are expect= ed to be (at
>> > least)
>> > two styles: having a type of "static" propositi= ons, or using hprops.
>> >
>> > With hprops, you can prove unique choice, so it's alw= ays 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 oth= er way that you
>> > have a subobject classifier.
>> >
>> > If you don't necessarily have unique choice or equiva= lent, you're
>> > dealing
>> > with a quasitopos, which is a more general thing.
>> >
>> > With static props and unique choice, subsingletons genera= lly aren't
>> > already
>> > propositions, but they all correspond to a proposition st= ating that the
>> > subsingleton is inhabited. Unique choice obtains the elem= ent 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 h= props, so
>> > static
>> > props is the way. Proofs will not be objects, so proof-ir= relevance
>> > 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 whet= her 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 proo= f-irrelevance still
>> > doesn't
>> > come up.
>> >
>> > But if it is, you should at least have typal proof-irrele= vance. (That
>> > is,
>> > stated using equality types.)
>> >
>> > In that case, with equality reflection, you automatically= get judgmental
>> > proof-irrelevance. This does not necessarily mean that pr= oofs are
>> > computationally irrelevant. With unique choice, they cann= ot be, or else
>> > you
>> > lose canonicity.
>> >
>> > All OK?
------=_Part_3793_1552826101.1513627695153-- ------=_Part_3792_48485523.1513627695152--