Re: [HoTT] Meta-conjecture about MLTT

[Thomas Streicher <stre...@mathematik.tu-darmstadt.de>]

Peter,

I think that doesn't work. Your example is just a presheaf topos and
thus a model of extensional type theory. Interpreting equality on the
universe as diagonal will not identify all isomorphic types.

I am afraid Martin's question is a tricky one. In models of
extensional type theory as we all know isomorphic types typically are
not equal. But Martin asks about the initial model and such questions
are tricky. But, maybe glueing (aka sconing) helps?

Thomas


> As you conjecture, MLTT with equality reflection can???t distinguish between
> isomorphic types.
> 
> Precisely, let MLTT[X] be the extension of MLTT by a single closed base
> type X.
> 
> Suppose \C is a model of MLTT ??? presented as a CwA with appropriate extra
> logical structure ??? and A, B are two isomorphic types in it, over the empty
> context.  So A, B induce two interpretations of MLTT[X] in \C.
> 
> Then there???s a CwA \C^\iso, with the category of isomorphisms in \C, and
> with a type over an iso ??1 <~> ??2 being a pair of types A1, A2 over ??1, ??2
> that correspond under reindexing along the isomorphism.
> 
> Now I claim this carries suitable structure to again model MLTT[X], and
> furthermore (importantly) such that the two projection maps \C^\iso ???> \C
> both preserve all the logical structure.  For most logical type-formers
> (Pi???s, Sigma???s, etc), the structure is by showing that these type-formers
> are provably functorial in isomorphisms.  (This uses the equality
> reflection.)  For the universe(s), this just uses the identity iso on the
> universe(s) of \C.  The base type X, we model by the given isomorphism A
> <~> B.
> 
> So this induces an interpretation of MLTT[X] in \C^\iso, whose two
> projections to \C are the two original interpretations in \C.
> 
> In particular, if P is any type in MLTT[X] ??? i.e. a property of an
> arbitrary type definable in MLTT ??? then its interpretation in \C^\iso is an
> isomorphism P[A] <~> P[B].  I think this is a reasonable positive answer to
> your question?
> 
> I don???t remember anywhere this construction appears in the literature, but
> I???ve always assumed that it has been noted before.  (Actually, I???d be very
> glad to hear a reference if anyone remembers seeing this somewhere, even if
> only in folklore not in print.)  Without identity reflection, it no longer
> works ??? since one doesn???t know that the logical structure in \C respects
> isomorphisms between types ??? but essentially the same approach works once
> one replaces isomorphisms by equivalences.  This is in the work of Chris
> Kapulkin???s and mine that I presented in Bonn in February, which we hope to
> have written up very soon???
> 
> Best,
> ???Peter.
> 
> 
> On Sun, Sep 11, 2016 at 10:47 PM, 'Martin Escardo' via Homotopy Type Theory
> <HomotopyT...@googlegroups.com> wrote:
> 
> > In MLTT with equality reflection, we cannot distinguish isomorphic types.
> >
> > There was some agreement regarding this in previous discussions here in
> > this list in the past (I think).
> >
> > But I don't think we actually saw a proof (have we?). As far as I
> > understand, we only saw that natural attempts to distinguish examples of
> > isomorphic types fail. There was some invokation of realizability models to
> > try to justify this. But I am not (yet) convinced by the arguments I have
> > seen so far.
> >
> > Nevertheless, I am convinced that equality reflection in MLTT cannot be
> > used to distinguish any particular pair of isomorphic types. (Prove me
> > wrong.)
> >
> > The meta-task is to either produce two isomorphic types in an empty
> > context, together with a property that one of them provably has but the
> > other doesn't, or to show that this is impossible.
> >
> > I am strongly inclined to think that this is impossible: that so-called
> > extensional MLTT cannot distinguish isomorphic types.
> >
> > In particular, equality-reflection has nothing whatsoever to do 5with
> > elementwise equality.
> >
> > Of course, what makes this difficult is that MLTT with equality reflection
> > is inconsistent with univalence.
> >
> >
> > Martin
> >
> >
> >
>