A puzzle about "univalent equality"

A puzzle about "univalent equality"

[Andrew Polonsky]

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

Hi,

There is a common understanding that the "right" concept of equality in 
Martin-Lof type theory is not the intensional identity type, but is a 
different notion of equality, which is extensional.  The adjunction of the 
univalence axiom to standard MLTT makes the identity type behave like this 
"intended" equality --- but it breaks the computational edifice of type 
theory.

More precisely, this "Hott book" approach only nails down the concept of 
equality with respect to its *logical properties* --- the things you can 
prove about it.  But not its actual computational behavior.

Since computational behavior can often be "seen" on the logical level, I am 
trying to get a better understanding of the sense in which this "Hott book" 
equality type is really (in)complete.  How would a "truly computational" 
equality type be different from it?  (Other than satisfying canonicity, 
etc.)

One precise example is that, for the "right" notion of equality, the 
equivalences characterizing path types of standard type constructors proved 
in Chapter 2 of the book could perhaps hold definitionally.  (The theorems 
proved there are thus "seeing" these equalities on the logical level.)

I tried to look for a more interesting example, and came up with the 
following puzzle.

f, g : Bool -> Bool -> Bool
f x y = if x then y else ff
g x y = if y then x else ff

e : f = g
e = FE(...)  [using UA to get Function Extensionality]

Phi : Bool -> Type
Phi tt = Bool
Phi ff = Unit

Psi : (Bool->Bool->Bool)->Type
Psi = \u. (u tt tt) x (u tt ff) x (u ff tt) x (u ff ff)

X : Psi f
X = (tt,*,*,*)

Y : Psi g
Y = subst Psi e X

QUESTION.
Can we prove, in "book Hott", that "proj1 Y = tt" is inhabited?

Cheers!
Andrew

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

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

[Michael Shulman]

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

I assume that in the definition of Psi you meant to write "Phi (u tt
tt)" and so on, since "u tt tt" is not a type, and otherwise Phi
wouldn't be used anywhere.  With this modification the answer is yes;
see attached code.

On Mon, Sep 5, 2016 at 9:54 AM, Andrew Polonsky
<andrew....@gmail.com> wrote:
> Hi,
>
> There is a common understanding that the "right" concept of equality in
> Martin-Lof type theory is not the intensional identity type, but is a
> different notion of equality, which is extensional.  The adjunction of the
> univalence axiom to standard MLTT makes the identity type behave like this
> "intended" equality --- but it breaks the computational edifice of type
> theory.
>
> More precisely, this "Hott book" approach only nails down the concept of
> equality with respect to its *logical properties* --- the things you can
> prove about it.  But not its actual computational behavior.
>
> Since computational behavior can often be "seen" on the logical level, I am
> trying to get a better understanding of the sense in which this "Hott book"
> equality type is really (in)complete.  How would a "truly computational"
> equality type be different from it?  (Other than satisfying canonicity,
> etc.)
>
> One precise example is that, for the "right" notion of equality, the
> equivalences characterizing path types of standard type constructors proved
> in Chapter 2 of the book could perhaps hold definitionally.  (The theorems
> proved there are thus "seeing" these equalities on the logical level.)
>
> I tried to look for a more interesting example, and came up with the
> following puzzle.
>
> f, g : Bool -> Bool -> Bool
> f x y = if x then y else ff
> g x y = if y then x else ff
>
> e : f = g
> e = FE(...)  [using UA to get Function Extensionality]
>
> Phi : Bool -> Type
> Phi tt = Bool
> Phi ff = Unit
>
> Psi : (Bool->Bool->Bool)->Type
> Psi = \u. (u tt tt) x (u tt ff) x (u ff tt) x (u ff ff)
>
> X : Psi f
> X = (tt,*,*,*)
>
> Y : Psi g
> Y = subst Psi e X
>
> QUESTION.
> Can we prove, in "book Hott", that "proj1 Y = tt" is inhabited?
>
> Cheers!
> Andrew
>
> --
> 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.
> For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Puzzle.v --]
[-- Type: text/x-verilog, Size: 963 bytes --]

Require Import HoTT FunextAxiom.

Definition f : Bool -> Bool -> Bool :=
  fun x y => if x then y else false.

Definition g : Bool -> Bool -> Bool :=
  fun x y => if y then x else false.

Definition e : f = g.
  apply path_forall; intros x; apply path_forall; intros y.
  destruct x, y; reflexivity.
Defined.

Definition Phi : Bool -> Type :=
  fun x => match x with true => Bool | false => Unit end.

Definition Psi : (Bool->Bool->Bool)->Type :=
  fun u => Phi (u true true) * Phi (u true false) * Phi (u false true) * Phi (u false false).

Definition X : Psi f := (true,tt,tt,tt).

Definition Y : Psi g := transport Psi e X.

(* Binary products in Coq associate to the left *)
Definition puzzle : fst (fst (fst Y)) = true.
Proof.
  unfold Y, X, Psi.
  rewrite !transport_prod; cbn.
  rewrite transport_compose.
  rewrite (ap_compose (fun u => u true) (fun v => v true) e).
  rewrite !ap_apply_l.
  unfold e.
  rewrite !ap10_path_forall.
  reflexivity.
Defined.

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

[Dan Licata]

yes, see https://github.com/dlicata335/hott-agda/blob/master/misc/Andrew.agda

Using the notation 

e1 : (x : Bool) → (f True x) == (g True x)
e1 True = id
e1 False = id

eh : (x : _) → f x == g x
eh True = λ≃ e1
eh False = λ≃ (λ { True → id ; False → id })

e : f == g
e = λ≃ eh

the steps are

goal : fst Y == True
goal = fst Y                                                                              ≃〈 ... 〉 
       transport (λ u → Phi (u True True)) e (fst X)                       ≃〈 ... 〉 
       transport Phi (ap (λ u → u True True) e) (fst X)                    ≃〈 ... 〉 
       transport Phi (ap (λ f₁ → f₁ True) (ap (λ f₁ → f₁ True) e)) (fst X) ≃〈 ... 〉 
       transport Phi (ap (λ f₁ → f₁ True) (λ≃ e1)) (fst X)                 ≃〈 ... 〉 
       True ∎

I would be very surprised if there was something like this that was not provable in "book HoTT”.  

-Dan

> On Sep 5, 2016, at 12:54 PM, Andrew Polonsky <andrew....@gmail.com> wrote:
> 
> Hi,
> 
> There is a common understanding that the "right" concept of equality in Martin-Lof type theory is not the intensional identity type, but is a different notion of equality, which is extensional.  The adjunction of the univalence axiom to standard MLTT makes the identity type behave like this "intended" equality --- but it breaks the computational edifice of type theory.
> 
> More precisely, this "Hott book" approach only nails down the concept of equality with respect to its *logical properties* --- the things you can prove about it.  But not its actual computational behavior.
> 
> Since computational behavior can often be "seen" on the logical level, I am trying to get a better understanding of the sense in which this "Hott book" equality type is really (in)complete.  How would a "truly computational" equality type be different from it?  (Other than satisfying canonicity, etc.)
> 
> One precise example is that, for the "right" notion of equality, the equivalences characterizing path types of standard type constructors proved in Chapter 2 of the book could perhaps hold definitionally.  (The theorems proved there are thus "seeing" these equalities on the logical level.)
> 
> I tried to look for a more interesting example, and came up with the following puzzle.
> 
> f, g : Bool -> Bool -> Bool
> f x y = if x then y else ff
> g x y = if y then x else ff
> 
> e : f = g
> e = FE(...)  [using UA to get Function Extensionality]
> 
> Phi : Bool -> Type
> Phi tt = Bool
> Phi ff = Unit
> 
> Psi : (Bool->Bool->Bool)->Type
> Psi = \u. (u tt tt) x (u tt ff) x (u ff tt) x (u ff ff)
> 
> X : Psi f
> X = (tt,*,*,*)
> 
> Y : Psi g
> Y = subst Psi e X
> 
> QUESTION.
> Can we prove, in "book Hott", that "proj1 Y = tt" is inhabited?
> 
> Cheers!
> Andrew
> 
> -- 
> 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.
> For more options, visit https://groups.google.com/d/optout.

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

[Andrew Polonsky]

Thanks, Mike and Dan.  And congratulations on giving essentially
identical solutions at essentially identical times, in two different
languages!

> I would be very surprised if there was something like this that was not provable in "book HoTT”.

I believe there can't be, either.  But maybe this "belief" is really a
matter of definition, in that the equalities which are "supposed to"
hold, are precisely those which can be derived in book HoTT.

What I find subtle in the above example is that it apparently cannot
be done with the "pre-HoTT" FunExt axiom; you need to use the stronger
formulation, that the canonical map (f=g -> f==g) is an equivalence,
to make the transports compute.

Cheers,
Andrew

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

[Michael Shulman]

Although, as Voevodsky showed, weak funext implies strong funext.

On Tue, Sep 6, 2016 at 12:30 AM, Andrew Polonsky
<andrew....@gmail.com> wrote:
> Thanks, Mike and Dan.  And congratulations on giving essentially
> identical solutions at essentially identical times, in two different
> languages!
>
>> I would be very surprised if there was something like this that was not provable in "book HoTT”.
>
> I believe there can't be, either.  But maybe this "belief" is really a
> matter of definition, in that the equalities which are "supposed to"
> hold, are precisely those which can be derived in book HoTT.
>
> What I find subtle in the above example is that it apparently cannot
> be done with the "pre-HoTT" FunExt axiom; you need to use the stronger
> formulation, that the canonical map (f=g -> f==g) is an equivalence,
> to make the transports compute.
>
> Cheers,
> Andrew
>
> --
> 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.
> For more options, visit https://groups.google.com/d/optout.

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

[Dan Licata]

and the issue only comes up if you don’t have K, which would equate (ap (λ u → u True True) e) and Refl

-Dan

> On Sep 6, 2016, at 8:32 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> Although, as Voevodsky showed, weak funext implies strong funext.
> 
> On Tue, Sep 6, 2016 at 12:30 AM, Andrew Polonsky
> <andrew....@gmail.com> wrote:
>> Thanks, Mike and Dan.  And congratulations on giving essentially
>> identical solutions at essentially identical times, in two different
>> languages!
>> 
>>> I would be very surprised if there was something like this that was not provable in "book HoTT”.
>> 
>> I believe there can't be, either.  But maybe this "belief" is really a
>> matter of definition, in that the equalities which are "supposed to"
>> hold, are precisely those which can be derived in book HoTT.
>> 
>> What I find subtle in the above example is that it apparently cannot
>> be done with the "pre-HoTT" FunExt axiom; you need to use the stronger
>> formulation, that the canonical map (f=g -> f==g) is an equivalence,
>> to make the transports compute.
>> 
>> Cheers,
>> Andrew
>> 
>> --
>> 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.
>> 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.
> For more options, visit https://groups.google.com/d/optout.

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

[Peter LeFanu Lumsdaine]

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

On Tue, Sep 6, 2016 at 2:32 PM, Michael Shulman <shu...@sandiego.edu>
wrote:

> Although, as Voevodsky showed, weak funext implies strong funext.


Just to clarify, though, this *doesn’t*  mean that Andews’ original goal
“proj1 Y = tt” is necesarily inhabited, if the funext witness used early in
his development is taken just from weak funext.

The proof “weak funext implies strong funext” shows that given some witness
funext0 of weak funext (i.e. funext0 : (forall X Y f g, f == g -> f = g)),
then you can construct some new witness funext1, which additionally is a
(two-sided) inverse for the canonical map the other way (“ap10” in the
current HoTT library).  (I blogged the details here:
https://homotopytypetheory.org/2011/12/19/strong-funext-from-weak/)

But it *doesn’t* show that the original witness funext0 is an inverse for
ap10, and indeed the proof points to how this may fail: funext0 might
conjugate paths by some family of non-trivial loops in the codomain type.
Andrew’s original goal “proj1 Y = tt” depends on the witness used earlier
for funext — so if that witness happens to conjugate paths Bool –> Bool in
Type by the non-trivial auto-equivalence of Bool, then one could have proj1
Y = ff.

–p.



> On Tue, Sep 6, 2016 at 12:30 AM, Andrew Polonsky
> <andrew....@gmail.com> wrote:
> > Thanks, Mike and Dan.  And congratulations on giving essentially
> > identical solutions at essentially identical times, in two different
> > languages!
> >
> >> I would be very surprised if there was something like this that was not
> provable in "book HoTT”.
> >
> > I believe there can't be, either.  But maybe this "belief" is really a
> > matter of definition, in that the equalities which are "supposed to"
> > hold, are precisely those which can be derived in book HoTT.
> >
> > What I find subtle in the above example is that it apparently cannot
> > be done with the "pre-HoTT" FunExt axiom; you need to use the stronger
> > formulation, that the canonical map (f=g -> f==g) is an equivalence,
> > to make the transports compute.
> >
> > Cheers,
> > Andrew
> >
> > --
> > 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.
> > 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.
> For more options, visit https://groups.google.com/d/optout.
>

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

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

[Andrew Polonsky]

These are all good points.  I now have an exhaustive answer to my
motivating question.

Thanks,
Andrew

On Tue, Sep 6, 2016 at 2:57 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> On Tue, Sep 6, 2016 at 2:32 PM, Michael Shulman <shu...@sandiego.edu>
> wrote:
>>
>> Although, as Voevodsky showed, weak funext implies strong funext.
>
>
> Just to clarify, though, this *doesn’t*  mean that Andews’ original goal
> “proj1 Y = tt” is necesarily inhabited, if the funext witness used early in
> his development is taken just from weak funext.
>
> The proof “weak funext implies strong funext” shows that given some witness
> funext0 of weak funext (i.e. funext0 : (forall X Y f g, f == g -> f = g)),
> then you can construct some new witness funext1, which additionally is a
> (two-sided) inverse for the canonical map the other way (“ap10” in the
> current HoTT library).  (I blogged the details here:
> https://homotopytypetheory.org/2011/12/19/strong-funext-from-weak/)
>
> But it *doesn’t* show that the original witness funext0 is an inverse for
> ap10, and indeed the proof points to how this may fail: funext0 might
> conjugate paths by some family of non-trivial loops in the codomain type.
> Andrew’s original goal “proj1 Y = tt” depends on the witness used earlier
> for funext — so if that witness happens to conjugate paths Bool –> Bool in
> Type by the non-trivial auto-equivalence of Bool, then one could have proj1
> Y = ff.
>
> –p.
>
>
>>
>> On Tue, Sep 6, 2016 at 12:30 AM, Andrew Polonsky
>> <andrew....@gmail.com> wrote:
>> > Thanks, Mike and Dan.  And congratulations on giving essentially
>> > identical solutions at essentially identical times, in two different
>> > languages!
>> >
>> >> I would be very surprised if there was something like this that was not
>> >> provable in "book HoTT”.
>> >
>> > I believe there can't be, either.  But maybe this "belief" is really a
>> > matter of definition, in that the equalities which are "supposed to"
>> > hold, are precisely those which can be derived in book HoTT.
>> >
>> > What I find subtle in the above example is that it apparently cannot
>> > be done with the "pre-HoTT" FunExt axiom; you need to use the stronger
>> > formulation, that the canonical map (f=g -> f==g) is an equivalence,
>> > to make the transports compute.
>> >
>> > Cheers,
>> > Andrew
>> >
>> > --
>> > 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.
>> > 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.
>> For more options, visit https://groups.google.com/d/optout.
>
>

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

[Martin Escardo]

I've been asking myself a similar question for some time now, and
perhaps it is the time to share it, although I was waiting to have a
more precise formulation, which I still don't. (So fill free to improve
my question or to say why it can't be answered.)

The nature of the type Id U X Y, in MLTT, is under-specified by the
(intensional) MLTT "axioms".

Maybe isProp(Id U X Y). This is the K-axiom (for the universe U).

Maybe Id U X Y is canonically equivalent to the type X~Y of
equivalences. This is the univalence axiom (for the universe U).

Maybe ... many more interesting things are possible? What else is
consistent beyond K and univalence, and possibly interesting?

Some people like the K-axiom for U because ... (let them fill the answer).

We like the univalence axiom for U because, "magically", it makes Id
behave as we think equality should behave (equality of groups should be
group isomorphism, for instance, and it is, under univalence).

But ... can we avoid the magical aspect?

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?

At the moment, univalence is "experimentally" interesting/compelling: it
gives function extensionality, it gives propositional extensionality, it
gives that the fundamental group of the circle HIT is Z, it gives that
equality of categories is categorical equivalence, and much more.

But can we "ultimately" justify it as the "intrinsically mathematically
appealing" determination of Id U X Y, before we consider the interesting
experimental consequences?

Martin



On 06/09/16 14:44, Andrew Polonsky wrote:
> These are all good points.  I now have an exhaustive answer to my
> motivating question.
>
> Thanks,
> Andrew
>
> On Tue, Sep 6, 2016 at 2:57 PM, Peter LeFanu Lumsdaine
> <p.l.lu...@gmail.com> wrote:
>> On Tue, Sep 6, 2016 at 2:32 PM, Michael Shulman <shu...@sandiego.edu>
>> wrote:
>>>
>>> Although, as Voevodsky showed, weak funext implies strong funext.
>>
>>
>> Just to clarify, though, this *doesn’t*  mean that Andews’ original goal
>> “proj1 Y = tt” is necesarily inhabited, if the funext witness used early in
>> his development is taken just from weak funext.
>>
>> The proof “weak funext implies strong funext” shows that given some witness
>> funext0 of weak funext (i.e. funext0 : (forall X Y f g, f == g -> f = g)),
>> then you can construct some new witness funext1, which additionally is a
>> (two-sided) inverse for the canonical map the other way (“ap10” in the
>> current HoTT library).  (I blogged the details here:
>> https://homotopytypetheory.org/2011/12/19/strong-funext-from-weak/)
>>
>> But it *doesn’t* show that the original witness funext0 is an inverse for
>> ap10, and indeed the proof points to how this may fail: funext0 might
>> conjugate paths by some family of non-trivial loops in the codomain type.
>> Andrew’s original goal “proj1 Y = tt” depends on the witness used earlier
>> for funext — so if that witness happens to conjugate paths Bool –> Bool in
>> Type by the non-trivial auto-equivalence of Bool, then one could have proj1
>> Y = ff.
>>
>> –p.
>>
>>
>>>
>>> On Tue, Sep 6, 2016 at 12:30 AM, Andrew Polonsky
>>> <andrew....@gmail.com> wrote:
>>>> Thanks, Mike and Dan.  And congratulations on giving essentially
>>>> identical solutions at essentially identical times, in two different
>>>> languages!
>>>>
>>>>> I would be very surprised if there was something like this that was not
>>>>> provable in "book HoTT”.
>>>>
>>>> I believe there can't be, either.  But maybe this "belief" is really a
>>>> matter of definition, in that the equalities which are "supposed to"
>>>> hold, are precisely those which can be derived in book HoTT.
>>>>
>>>> What I find subtle in the above example is that it apparently cannot
>>>> be done with the "pre-HoTT" FunExt axiom; you need to use the stronger
>>>> formulation, that the canonical map (f=g -> f==g) is an equivalence,
>>>> to make the transports compute.
>>>>
>>>> Cheers,
>>>> Andrew
>>>>
>>>> --
>>>> 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.
>>>> 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.
>>> For more options, visit https://groups.google.com/d/optout.
>>
>>
>

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

[Matt Oliveri]

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

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.

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

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

[Michael Shulman]

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

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

[Jason Gross]

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

> 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.

On Wed, Sep 7, 2016, 9:15 PM Michael Shulman <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> 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.
> > 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.
> For more options, visit https://groups.google.com/d/optout.
>

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

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

[Martin Escardo]

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.

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

[Matt Oliveri]

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

True, the language does not provide this structure. But that doesn't mean 
it isn't in the model. Is there a problem interpreting ITT as all 
Zermelo-style sets, with identity as a subsingletons for equality?

On Thursday, September 8, 2016 at 12:15:13 AM UTC-4, Michael Shulman 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 
> <javascript:>> 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.
>

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

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

[Michael Shulman]

Type theory does have set-theoretic models, of course.  But that
doesn't provide a notion of equality that makes sense *inside* MLTT,
compelling or otherwise.

On Wed, Sep 7, 2016 at 11:34 PM, Matt Oliveri <atm...@gmail.com> wrote:
> True, the language does not provide this structure. But that doesn't mean it
> isn't in the model. Is there a problem interpreting ITT as all Zermelo-style
> sets, with identity as a subsingletons for equality?
>
> On Thursday, September 8, 2016 at 12:15:13 AM UTC-4, Michael Shulman 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> 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.
> For more options, visit https://groups.google.com/d/optout.

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

[Martin Escardo]

On 08/09/16 07:45, Michael Shulman wrote:
> Type theory does have set-theoretic models, of course.  But that
> doesn't provide a notion of equality that makes sense *inside* MLTT,
> compelling or otherwise.


Exactly: elementwise equality can't even be formulated internally.

However, there is one situation in which elementwise equality can both
be formulated and is the equality we get.

For a type X define its powerset to be

  PX := X->Prop.

For A:PX write x \in A (like in topos type theory) to mean A(x).

Then (A=B) = (forall x:X, x \in A <-> x \in B).

In topos type theory we get this because both function extensionality
and propositional extensionality hold.

In HoTT we get this because these two extensionality properties are a
particular case of univalence.

In MLTT with equality reflection, you don't get this, because although
you get function extensionality, you don't get propositional
extensionality. So equality reflection is not doing the job of capturing
elementwise equality in the powerset. But univalence is.

Martin

> 
> On Wed, Sep 7, 2016 at 11:34 PM, Matt Oliveri <atm...@gmail.com> wrote:
>> True, the language does not provide this structure. But that doesn't mean it
>> isn't in the model. Is there a problem interpreting ITT as all Zermelo-style
>> sets, with identity as a subsingletons for equality?
>>
>> On Thursday, September 8, 2016 at 12:15:13 AM UTC-4, Michael Shulman 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> 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.
>> For more options, visit https://groups.google.com/d/optout.
> 

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

[Thomas Streicher]

Intensional type theory is consistent with extensional type theory
which can be interpreted in any  locally cartesian category. Equality
is there interpreted via diagonals (in slice categories). This does
not at all assume quantification over an untyped universe.

Adding K to ITT is an attempt to approach ETT and keeping type
checking decidable.

Most of the known models of type theory are models of extensional type
theory. This collection contains all lcc's and all toposes. I have no
problem to recall these...

Models of ITT but not of ETT and not validating Univalence were
constructed in my Habilitation Thesis and more recently in the Thesis
of Tamara von Glehn.

Thomas

Re: A puzzle about "univalent equality"

[Robin Adams]

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

Very interesting thread.  I'd like to add an observation: in cubical type 
theory, the terms X and Y are definitionally. equal.

Proof: Let us use s == t to denote that s and t are the same expression, 
and s = t for definitional equality.

Let e0 be the term such that x : Bool, y : Bool, i : I |- e0 : Path Bool (f 
x y) (g x y), so that e is the result of applying functional extensionality 
to e0, that is

e == <i> \ x y . e0

Note that

e0[x := tt, y := tt] = Bool
e0[x := tt, y := ff] = Unit
e0[x := ff, y := tt] = Unit
e0[x := ff, y := ff] = Unit

Then we have

Y == comp^i (psi (e i)) [] X
   = comp^i (phi (e i tt tt) x phi(e i tt ff) x phi(e i ff tt) x phi(e i ff 
ff)) [] X
   = comp^i (Bool x Unit x Unit x Unit) [] X
   = < comp^i Bool [] tt , comp^i Unit [] *, comp^i Unit [] *, comp^i Unit 
[] * > (computation rule for comp with Sigma)
   = < tt, *, *, * >  (computation rule for comp with Bool and Unit)
   == X

Note that this only works because X is a canonical object; it doesn't hold 
for an arbitrary term of type Psi f.  (Because we don't, in general, have 
that comp maps 1_A to 1_A up to definitional equality; that is, we don't 
have comp^i A [] t = t where i does not occur free in A.)

--
Robin

On Monday, 5 September 2016 18:54:14 UTC+2, Andrew Polonsky wrote:
>
> Hi,
>
> There is a common understanding that the "right" concept of equality in 
> Martin-Lof type theory is not the intensional identity type, but is a 
> different notion of equality, which is extensional.  The adjunction of the 
> univalence axiom to standard MLTT makes the identity type behave like this 
> "intended" equality --- but it breaks the computational edifice of type 
> theory.
>
> More precisely, this "Hott book" approach only nails down the concept of 
> equality with respect to its *logical properties* --- the things you can 
> prove about it.  But not its actual computational behavior.
>
> Since computational behavior can often be "seen" on the logical level, I 
> am trying to get a better understanding of the sense in which this "Hott 
> book" equality type is really (in)complete.  How would a "truly 
> computational" equality type be different from it?  (Other than satisfying 
> canonicity, etc.)
>
> One precise example is that, for the "right" notion of equality, the 
> equivalences characterizing path types of standard type constructors proved 
> in Chapter 2 of the book could perhaps hold definitionally.  (The theorems 
> proved there are thus "seeing" these equalities on the logical level.)
>
> I tried to look for a more interesting example, and came up with the 
> following puzzle.
>
> f, g : Bool -> Bool -> Bool
> f x y = if x then y else ff
> g x y = if y then x else ff
>
> e : f = g
> e = FE(...)  [using UA to get Function Extensionality]
>
> Phi : Bool -> Type
> Phi tt = Bool
> Phi ff = Unit
>
> Psi : (Bool->Bool->Bool)->Type
> Psi = \u. (u tt tt) x (u tt ff) x (u ff tt) x (u ff ff)
>
> X : Psi f
> X = (tt,*,*,*)
>
> Y : Psi g
> Y = subst Psi e X
>
> QUESTION.
> Can we prove, in "book Hott", that "proj1 Y = tt" is inhabited?
>
> Cheers!
> Andrew
>

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