From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sun, 17 Dec 2017 23:41:49 -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_6212_1769680893.1513582909266" ------=_Part_6212_1769680893.1513582909266 Content-Type: multipart/alternative; boundary="----=_Part_6213_339429842.1513582909267" ------=_Part_6213_339429842.1513582909267 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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_6213_339429842.1513582909267 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Hello. I'd like to see if I have the situation straigh= t:

For presenting a topos as a type system, there are expected to be= (at least) two styles: having a type of "static" propositions, o= r using hprops.

With hprops, you can prove unique choice, so it'= s always topos-like (pretopos?).

With static props, you can't pr= ove 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.
<= br>If you don't necessarily have unique choice or equivalent, you'r= e dealing with a quasitopos, which is a more general thing.

With sta= tic props and unique choice, subsingletons generally aren't already pro= positions, but they all correspond to a proposition stating that the subsin= gleton is inhabited. Unique choice obtains the element of a subsingleton kn= own to be inhabited.

The usual way to present a topos as a type syst= em 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 equiv= alent. (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 judgm= ental proof-irrelevance. This does not necessarily mean that proofs are com= putationally irrelevant. With unique choice, they cannot be, or else you lo= se canonicity.

All OK?
------=_Part_6213_339429842.1513582909267-- ------=_Part_6212_1769680893.1513582909266--