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

[Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>]

[-- Attachment #1: Type: text/plain, Size: 4781 bytes --]

Hi Matt,

Yes, this is what I wanted to say. To put it in a different way: in Type Theory we can approximate Omega by HProp. And indeed, every subobject of 1 is represented as an element of HProp. There are 2 mismatches: HProp is large but Omega is small (this corresponds to impredicativity or resizing). The other is propositional extensionality which is an instance of univalence.

We can view topoi as a first approximation of HoTT. When we replace a subobject classifier by an object classifier, that is classifying all maps and not just propositions we obtain univalent universes. However, two provisos are necessary: 1. we cannot classify all maps otherwise we end up with a system with Type : Type and 2. we have to move to an (omega,1)-category because univalence is forced upon us as an equality and this doesn’t work if all types are sets. That is a higher predicative topos fixes the historic shortcomings of topos theory.

By moving to a predicative setting we give up the encodings of colimits (e.g. coequalizers) using the subobject classifier. Indeed, this is just the impredicative encoding of quotient types. Instead we need to explictly add them but we can do this in a way which goes beyond topos theory (even in the propositional setting) namely as QITs (propositional) or HITs (in the higher case).

Thorsten


From: <homotopyt...@googlegroups.com<mailto:homotopyt...@googlegroups.com>> on behalf of Matt Oliveri <atm...@gmail.com<mailto:atm...@gmail.com>>
Date: Thursday, 21 December 2017 at 00:42
To: Homotopy Type Theory <homotopyt...@googlegroups.com<mailto:homotopyt...@googlegroups.com>>
Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

Hi Thorsten and Thomas,

It still looks to me like you're talking about different things and having a misunderstanding.
By "propositional extensionality", Thorsten seems to mean the special case of univalence that applies to hprops. (Which he's simply calling propositions.) But it sounds like Thomas is counting "propositional extensionality" as a separate principle from univalence, for a type of static props. I think the system Thorsten has in mind presents a (pre)topos as a univalent type system, where hprops are used *instead of* a type of static props.

But maybe not, and I'm misunderstanding.

On Wednesday, December 20, 2017 at 6:41:14 AM UTC-5, Thomas Streicher wrote:
Hi Thorsten,

> we have already established that my argument was incorrect (for the
> reasons you state) and I was misinformed about the behaviour of
> Lean.

I know, I just wanted to spot where the problem precisely is.

> >Another gap in Thorsten's argument is the following. Though Single(a) and
> >Single(a') are isomorphic in order to conclude that they are propositionally
> >equal they would have to be elements of a univalent universe BUT I don't see
> >where such a universe should come from in the general topos case!

> I don???t understand this point. In a type theoretic implementation of a topos Single(a) and Single(a???) would be propositionally equal due to propositional extensionality. The only additional assumption I need to make is that the universe of proposition is strict, e.g. we have that El(A -> B) is definitionally equal to  EL(A) -> El(B). This seems to be quite natural from the point of type theory where universes are usually strict and moreover this is true in any univalent category giving rise to a topos.

Well, Single(a) and Single(a') were propsitionally equal if they were
elements of a univalent universe U but where should this come from if
you start from an elementary topos in a univalent metatheory.

Thomas

--
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<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.


[-- Attachment #2: Type: text/html, Size: 6579 bytes --]