Yet another characterization of univalence

[Martín Hötzel Escardó]

Consider the identity type former Id of the type X:U in the universe U:

    Id : X -> (X -> U).

I've known for some years that this is an embedding of the type X into the type (X->U). This means that the fibers of Id are propositions, or, equivalently, that the maps ap Id  : x = y -> Id x = Id y are equivalences for all x,y:X.

This depends on univalence. I've just realized that this is actually *equivalent* to univalence. Has anybody noticed this before?

Martin

[y]

Can you elaborate on why it is true? Also as this statement is similar to Yoneda's lemma, do we have something like 

For a type X : U and B : X -> U, Id (X -> U) (Id X x) B is equivalent to B x?

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

[Martín Hötzel Escardó]

On 20/11/17 03:54, y wrote:

> Can you elaborate on why it is true? 

I am writing this in Agda to be absolutely sure of all the

details. But this is going slowly because lack of time. When It is

done I will give you a link and also a proof in English prose.

> Also as this statement is similar

> to Yoneda's lemma, do we have something like

> Also as this statement is similar  to Yoneda's lemma, do we have

> something like

> For a type X : U and B : X -> U, Id (X -> U) (Id X x) B is equivalent to 

> B x?

As I said privately to you, yes. This follows from one of the Yoneda

Lemmas, namely that if Sigma B is contractible then the recursively

defined map

  Pi(y : Y), Id x y -> B y is an equivalence

for every x : X and b : B x (and conversely).

The Id-fiber of B is Sigma(x : X), Id x = B.

If (x:X, p : Id x = B) is in the fiber, then

   ap Sigma p : Sigma(Id x) = Sigma B,

and hence, being equal to a contractible type, Sigma B is

contractible.

This doesn't use univalence or function extensionality.

Next you have to use the contractibility of Sigma B to show that the

Id-fiber of B is contractible. It is this step which uses the (above

form of the) Yoneda Lemma and univalence, so show that this fiber is

equivalence to Sigma B (being a retract suffices, but we do in fact

get an equivalence automatically: it is laborious to check the

retraction condition; the section condition, which is not nedeed, is

much easier).

With this you get that Id is an embedding.

That from this (for all types) you get univalence is subtler, and I

want to check everything before I sketch an argument in public. But I

didn't want to do this if somebody told me, in response to the message

below, that this has been already done, but nobody did.

Martin

[Martín Hötzel Escardó]

On Friday, 24 November 2017 12:21:58 UTC, Martín Hötzel Escardó wrote:

On 20/11/17 03:54, y wrote:

> Can you elaborate on why it is true? 

Actually, my argument was fundamentally flawed, because this is not provable.

If univalence holds, then Id : X -> (X -> U) is an embedding.

But If the K axiom holds, then again Id : X -> (X -> U) is an embedding.

And hence there is no hope to deduce univalence from the fact that Id_X is an embedding for every X:U.

(And, as a side remark, I can't see how to prove that Id_X is an embedding without using K or univalence.)

Martin

[Martín Hötzel Escardó]

You asked a question privately, but I choose to answer it here.

On Monday, 20 November 2017 03:54:55 UTC, Yuhao Huang wrote:

Can you elaborate on why it is true? Also as this statement is similar to Yoneda's lemma, do we have something like 

For a type X : U and A : X -> U, Id (X -> U) (Id X x) A is equivalent to A x?

We have

 A x ≃ Nat (Id x) A           (yoneda)

     = Π(y:Y), Id x y → A y  (definition)

     ≃ Π(y:Y), Id x y ≃ A y (because Σ A is contractible (Yoneda corollary))

     ≃ Π(y:Y), Id x y ≡ A y (by univalence)

     ≃ Id x ≡ A y           (by extensionality)

Martin

 

[Martín Hötzel Escardó]

Of course the last line is Id x ≡ A (without the y). Copy-and-paste-and-don't-modify properly phenomenon. 

On Friday, 24 November 2017 23:12:03 UTC, Martín Hötzel Escardó wrote:

 A x ≃ Nat (Id x) A           (yoneda)

     = Π(y:Y), Id x y → A y  (definition)

     ≃ Π(y:Y), Id x y ≃ A y (because Σ A is contractible (Yoneda corollary))

     ≃ Π(y:Y), Id x y ≡ A y (by univalence)

     ≃ Id x ≡ A y           (by extensionality)

Lat line should have been 

         ≃ Id x ≡ A

 

Martin

 

[Andrej Bauer]

> If univalence holds, then Id : X -> (X -> U) is an embedding.
>
> But If the K axiom holds, then again Id : X -> (X -> U) is an embedding.
>
> And hence there is no hope to deduce univalence from the fact that Id_X is
> an embedding for every X:U.
>
> (And, as a side remark, I can't see how to prove that Id_X is an embedding
> without using K or univalence.)

So you've invented a new axiom?

Escardo's axiom: Id : X → (X → U) is an embedding.

(We could call it Martin's axiom to create lots of confusion.)

With kind regards,

Andrej

[Evan Cavallo]

Maybe this is interesting: assuming funext, if the canonical map Id A B -> A ≃ B is an embedding for all A,B, then Martin's axiom holds. Since Id x y is always equivalent to (Π(z:X), Id x z ≃ Id y z), showing that it is equivalent to Id (Id x) (Id y) can be reduced to showing that the map Id (Id x) (Id y) -> (Π(z:X), Id x z ≃ Id y z) is an embedding.

Id A B -> A ≃ B is an embedding both if univalence holds and if axiom K holds.

Evan

[Evan Cavallo]

Can you show the converse?

I don't think so (or at least, I don't see how it could be done).

Evan

2017-11-29 17:12 GMT-05:00 Martín Hötzel Escardó <m.es...@cs.bham.ac.uk>:

On 29/11/17 21:12, Evan Cavallo wrote:

Maybe this is interesting: assuming funext, if the canonical map Id A B -> A ≃ B is an embedding for all A,B, then Martin's axiom holds. Since Id x y is always equivalent to (Π(z:X), Id x z ≃ Id y z), showing that it is equivalent to Id (Id x) (Id y) can be reduced to showing that the map Id (Id x) (Id y) -> (Π(z:X), Id x z ≃ Id y z) is an embedding.

Id A B -> A ≃ B is an embedding both if univalence holds and if axiom K holds.

I like it. You say that (assuming funext) if idtoeq : (A B : U) -> A = B -> A ≃ B is a natural embedding (rather than an equivalence as the univalence axiom demands) then Id_X : X -> (X -> U) is an embedding for all X:U.

Can you show the converse?

Martin

Evan

2017-11-28 4:40 GMT-05:00 Andrej Bauer <andrej...@andrej.com <mailto:andrej...@andrej.com>>:

    > If univalence holds, then Id : X -> (X -> U) is an embedding.
    >
    > But If the K axiom holds, then again Id : X -> (X -> U) is an embedding.
    >
    > And hence there is no hope to deduce univalence from the fact that Id_X is
    > an embedding for every X:U.
    >
    > (And, as a side remark, I can't see how to prove that Id_X is an embedding
    > without using K or univalence.)

    So you've invented a new axiom?

       Escardo's axiom: Id : X → (X → U) is an embedding.

    (We could call it Martin's axiom to create lots of confusion.)

    With kind regards,

    Andrej

    --
    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+unsubscribe@googlegroups.com
    <mailto:HomotopyTypeTheory%2Bunsubs...@googlegroups.com>.

    For more options, visit https://groups.google.com/d/optout

    <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+unsubscribe@googlegroups.com <mailto:HomotopyTypeTheory+unsubsc...@googlegroups.com>.

For more options, visit https://groups.google.com/d/optout.

--
http://www.cs.bham.ac.uk/~mhe

[Martín Hötzel Escardó]

On Wednesday, 29 November 2017 21:13:27 UTC, E Cavallo wrote:

Maybe this is interesting: assuming funext, if the canonical map Id A B -> A ≃ B is an embedding for all A,B, then Martin's axiom holds. Since Id x y is always equivalent to (Π(z:X), Id x z ≃ Id y z), showing that it is equivalent to Id (Id x) (Id y) can be reduced to showing that the map Id (Id x) (Id y) -> (Π(z:X), Id x z ≃ Id y z) is an embedding.

Id A B -> A ≃ B is an embedding both if univalence holds and if axiom K holds.

I like it. You say that (assuming funext) if idtoeq : (A B : U) -> A = B 
-> A ≃ B is a natural embedding (rather than a natural equivalence as the 
univalence axiom demands) then Id_X : X -> (X -> U) is an embedding for 
all X:U.

It is natural to ask whether the converse holds (particularly given my original wrong claim recorded in the subject of this thread). Do you think it does?

Martin

[Martin Escardo]

On 29/11/17 21:12, Evan Cavallo wrote:

> Maybe this is interesting: assuming funext, if the canonical map Id A B
> -> A ≃ B is an embedding for all A,B, then Martin's axiom holds. Since
> Id x y is always equivalent to (Π(z:X), Id x z ≃ Id y z), showing that
> it is equivalent to Id (Id x) (Id y) can be reduced to showing that the
> map Id (Id x) (Id y) -> (Π(z:X), Id x z ≃ Id y z) is an embedding.
>
> Id A B -> A ≃ B is an embedding both if univalence holds and if axiom K
> holds.

OK. Here is a further weakening of the hypotheses. It suffices to have
funext (again) and that the map

idtofun{B}{C} : A=B → (A→B)

is left-cancellable (that is, idtofun p = idtofun q → p=q).

Univalence gives that this is an embedding, which is stronger than
saying that it is left-cancellable. And also K gives that this is an
embedding, as Evan said.


Here is the proof that these assumptions suffice.

To show that Id : X→(X→U) is an embedding, let A : X→U.

It suffices to show that the type T := Σ(x:X), Id x = A is a
proposition.

To this end, it is in turn enough to show that T → isProp T.

So let (x₀:X, p₀: Id x = A) : T.

Then ap Σ p₀ : Σ(Id x₀) = Σ A, where Σ{X} : (X→U)→U.

Because the type Σ(Id x₀) of paths from x₀ is contractible, so is the
type Σ A by transport.

For x:X arbitrary, we have maps

Id x = A
(1) → (happly)
Π(y:X), Id x y = A x
(2) → (induced by idtofun)
Π(y:X), Id x y → A x
(3) → (evaluate at x and idpath x)
A x

If funext holds, then the map (1) is left-cancellable because it is an
equivalence.

The map idtofun : Id x y = A x → (A x y → A x) is left-cancellable by
assumption. The induced map (2) is then also left-cancellable assuming
funext.

The map (3) is an equivalence assuming funext, and hence
left-cancellable.

Left-cancellable maps are closed under composition, and hence we get
a left-cancellable map

f x : Id x = A → A x

But then also the map

g : (Σ(x:X), Id x A) → Σ A

defined by g(x,p) = (x, f x p) is left-cancellable (easy to check, in
the general form that if f i : B i → C i is a family of left
cancellable maps then the map (i,b) ↦ (i,f i b) : Σ B → Σ C is
left-cancellable).

But for any left-cancellable map into a proposition, its domain is a
proposition. Hence (Σ(x:X), Id x A) is a proposition because Σ A,
being contractible, is a proposition.

This concludes the proof that T → isProp T and hence that Id is an
embedding.

Martin

[Martín Hötzel Escardó]

On Wednesday, 29 November 2017 21:13:27 UTC, E Cavallo wrote:

Maybe this is interesting: assuming funext, if the canonical map Id A B -> A ≃ B is an embedding for all A,B, then Martin's axiom holds. Since Id x y is always equivalent to (Π(z:X), Id x z ≃ Id y z), showing that it is equivalent to Id (Id x) (Id y) can be reduced to showing that the map Id (Id x) (Id y) -> (Π(z:X), Id x z ≃ Id y z) is an embedding.

Id A B -> A ≃ B is an embedding both if univalence holds and if axiom K holds.

 OK. Here is a further weakening of the hypotheses. It suffices to have

funext (again) and that the map

    idtofun{B}{C} : A=B → (A→B)

is left-cancellable (that is, idtofun p = idtofun q → p=q).

Univalence gives that this is an embedding, which is stronger than

saying that it is left-cancellable. And also K gives that this is an

embedding.

This concludes the proof that T → isProp T and hence that Id is an

embedding.

Martin

[Martín Hötzel Escardó]

On Friday, 1 December 2017 14:53:25 UTC, Martín Hötzel Escardó wrote:

 OK. Here is a further weakening of the hypotheses. It suffices to have

funext (again) and that the map

    idtofun{B}{C} : A=B → (A→B)

is left-cancellable (that is, idtofun p = idtofun q → p=q).

Univalence gives that this is an embedding, which is stronger than

saying that it is left-cancellable. And also K gives that this is an

embedding.

I've written this down here in Agda :  http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html

(updating a 2015 development)

  * This is self-contained (doesn't use any library).

  * A main feature is that instead of J (or pattern maching on refl), this uses the Yoneda machinery everywhere instead (regretably with just one exception (I'd be grateful for suggestions of how to get rid of this use of J)).

A syntactical novelty is a new notation for universes in Agda closer to the notation in the HoTT book for informal mathematics in type theory. This could be further improved by making it built-in in Agda (as explained in the imported NonStandardUniverseNotation.lagda), but probably it is good enough without any modification to Agda.

Martin

  

[Martín Hötzel Escardó]

I am interested in the fact that Id_X : X → (X → U) is an embedding

(in the sense of univalent mathematics), because it gives this:

  The injective types are precisely the retracts of exponential powers

  of universes, where an exponential power of a type D is a type of

  the form A → D for some type A.

Injectivity is defined as (functional) data rather than property

(using Σ rather than ∃).

A type D is called injective if for any embedding j:X→Y, every

function f:X→D extends to a map f':Y→D along j.

This injectivity result depends crucially on univalence (even though

the fact that Id_X is an embedding depends on much weaker hypotheses,

as we've found out in this thread).

It is also crucial that we say that j is an embedding (its fibers are

propositions) rather than merely that j is left-cancellable.

The following elaborates on this, with more comments and more

technical results rendered in Agda.

http://www.cs.bham.ac.uk/~mhe/agda-new/InjectiveTypes.html

We don't postulate anything in this development. Any axiom (UA, K, or

FunExt) is used explicitly as an assumption whenever needed.

The reason I came across injective types was my interest in searchable

and omniscient types. (In a previous research life, I had already come

across injective topological spaces when working on domain theory in

the sense of Dana Scott, and what we do here is partly inherited from

that.) This is also reported in this development: 

http://www.cs.bham.ac.uk/~mhe/agda-new/index.html

Some of this was reported in the past in this list. But there are new 

things, in particular regarding injectivity.

Martin.

[Gershom B]

On December 18, 2017 at 5:58:22 PM, Martín Hötzel Escardó

(escardo...@gmail.com) wrote:
> >
> A type D is called injective if for any embedding j:X→Y, every
> function f:X→D extends to a map f':Y→D along j.
>

Here is a question: given a local operator (Lawvere-Tierny topology)
j, an object D is a sheaf if for any j-dense subobject X >-> Y, every
function f : X -> D extends to a map f’ : Y -> D. Is there a way in
which we can view injective types as sheafs in some appropriate sense?

Regards,
Gershom

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

[Martín Hötzel Escardó]

On Tuesday, 19 December 2017 03:36:51 UTC, Gershom B wrote:
On December 18, 2017 at 5:58:22 PM, Martín Hötzel Escardó 
(escardo...@gmail.com) wrote: 
> > 
> > A type D is called injective if for any embedding j:X→Y, every 
> > function f:X→D extends to a map f':Y→D along j. 
> 

> Here is a question: given a local operator (Lawvere-Tierny topology) 
> j, an object D is a sheaf if for any j-dense subobject X >-> Y, every 
> function f : X -> D extends to a map f’ : Y -> D. Is there a way in 
> which we can view injective types as sheafs in some appropriate sense? 


I don't think so, because we don't have the required uniqueness
of the sheaf condition here.

In general, if a type D is injective, many extensions of any
f:X→D along an embedding j:X→Y exist.

In the file
http://www.cs.bham.ac.uk/~mhe/agda-new/InjectiveTypes.html, 
two canonical extensions are shown to exist, a minimal one f\j
using Σ, and a maximal f/j one using Π. 

In fact they are left and right Kan extensions, in the sense that we
have equivalences

 Nat f (g ∘ j) ≃ Nat f∖j  g

and

 Nat g f/j ≃ Nat (g ∘ j) f

of natural transformations involving the "presheaves" g : Y → U and
f\j, f/j : X → U.

Although these two extensions are canonical in the above sense, they are not unique.

Martin