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

[Matt Oliveri <atm...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2021 bytes --]

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
>

[-- Attachment #1.2: Type: text/html, Size: 2296 bytes --]