Re: [HoTT] A puzzle about "univalent equality"

[Martin Escardo <escardo...@googlemail.com>]

On 08/09/16 07:06, Jason Gross wrote:
>> Can we stare at the type (Id U X Y)
>> objectively, mathematically, say
>> within intensional MLTT, where it was
>> introduced, and, internally in
>> MLTT, ponder what it can be, and identify the
>> only "compelling" thing it
>> can be as the type of equivalences X~Y,
>> where "compelling" is a notion
>> remote from univalence?
> 
> I am not sure what you mean by internally, but the way I usually
> motivate univalence is: we can ask "which equalities (Id U X Y) are
> provable in MLTT?"  The answer is: "only when X and Y are definitionally
> equal."  We can ask: "when can we prove that (Id U X Y) is absurd?"  The
> answer turns out to be: "exactly when X and Y are provably not
> isomorphic."  (The proof that this is the most general answer is the
> proof that univalence is consistent.)  So it seems natural to ask about
> the two extremes.  On the one hand, the converse of the strictest
> equality we can have is the equality reflection rule.  On the other
> extreme, the inverse of the weakest equality rule is logically
> equivalent to univalence. 

Ok, I would regard this as an external, experimental motivation. I use
a similar one (and so do other people): (intensional or extensional)
MLTT cannot distinguish isomorphic types by exhibiting a property that
one (provably) has but not the other. For intensional MLTT the proof
is the consistency of univalence. For extensional MLTT this can be
proved via realizability models (we discussed this in this list, I
think). So this is a weak justification for univalence, because
extensional MLTT already has this meta-theoretical property, but is
not consistent with univalence. In any case, this is a meta-level
statement, and I was looking more something internal.

Because I am looking for something internal, equality reflection
doesn't qualify (as it cannot be taken as a hypothesis, as it is not a
type but a rule).

The K axiom does qualify as something that one can hypothesize
internally, as does univalence.

In November last year, I observed in this list thatI, in MLTT, we can
construct a map

  E: {X Y : U} -> (X->Y) -> U

and a (recursively defined) equivalence

  Phi: {X Y : U} -> X=Y -> Sigma(f:X->Y).E(f).

Because this is in intensional MLTT, it is also a theorem/construction
of extensional MLTT, with equality-reflection present but not used.

We have that E(f) -> isEquiv(f). The K axiom (which holds in the
presence of equality reflection) is of course equivalent to saying
that the only E-map X->X is the identity. In the other extreme,
univalence is the converse implication E(f) <- isEquiv(f), saying that
all equivalences X->Y are E-maps.

But can we "locate" univalence among the space of possibilities for E
other than saying that it is one of the two extreme possibilities?

Martin


> 
> On Wed, Sep 7, 2016, 9:15 PM Michael Shulman <shu...@sandiego.edu
> <mailto:shu...@sandiego.edu>> wrote:
> 
>     Does "Zermelo-style set-theoretic equality" even make sense in MLTT?
>     Types don't have the global membership structure that Zermelo-sets do.
> 
>     On Wed, Sep 7, 2016 at 4:18 PM, Matt Oliveri <atm...@gmail.com
>     <mailto:atm...@gmail.com>> wrote:
>     > On Tuesday, September 6, 2016 at 6:14:24 PM UTC-4, Martin Hotzel
>     Escardo
>     > wrote:
>     >>
>     >> Some people like the K-axiom for U because ... (let them fill the
>     answer).
>     >
>     >
>     > It allows you to interpret (within type theory) the types of ITT +
>     K as
>     > types of U, and their elements as the corresponding elements.
>     (Conjecture?)
>     > Whereas without K, we don't know how to interpret ITT types as
>     types of U.
>     > In other words, K is a simple way to give ITT reflection.
>     >
>     >> Can we stare at the type (Id U X Y) objectively, mathematically, say
>     >> within intensional MLTT, where it was introduced, and, internally in
>     >> MLTT, ponder what it can be, and identify the only "compelling"
>     thing it
>     >> can be as the type of equivalences X~Y, where "compelling" is a
>     notion
>     >> remote from univalence?
>     >
>     >
>     > How does Zermelo-style set-theoretic equality get ruled out as a
>     potential
>     > "compelling" meaning for identity? Of course, there's a potential
>     argument
>     > about what "compelling" ought to be getting at. You seem to not
>     consider
>     > set-theoretic equality compelling, which I can play along with.
>     >
>     > --
>     > 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:HomotopyTypeTheo...@googlegroups.com>.
>     > For more options, visit https://groups.google.com/d/optout.
> 
>     --
>     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:HomotopyTypeTheo...@googlegroups.com>.
>     For more options, visit https://groups.google.com/d/optout.
> 
> -- 
> 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.