A puzzle about "univalent equality"

[Andrew Polonsky]

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

[Michael Shulman]

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.

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

[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

[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

[Michael Shulman]

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

[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

[Peter LeFanu Lumsdaine]

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 HomotopyTypeTheory+unsub...@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 HomotopyTypeTheory+unsub...@googlegroups.com.

[Andrew Polonsky]

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

Thanks,
Andrew

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

[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

[Matt Oliveri]

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.

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

[Jason Gross]

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

[Matt Oliveri]

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?

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

[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

[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

> <mailto:HomotopyTypeTheory%2Bunsu...@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:HomotopyTypeTheory%2Bunsu...@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>.

[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

[Robin Adams]

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