[parent not found: <204e382a-efcf-cb13-006f-47fdbadd99a5@cs.bham.ac.uk>]
* Re: [HoTT] Yet another characterization of univalence
[not found] ` <204e382a-efcf-cb13-006f-47fdbadd99a5@cs.bham.ac.uk>
@ 2017-11-29 22:15 ` Evan Cavallo
0 siblings, 0 replies; 16+ messages in thread
From: Evan Cavallo @ 2017-11-29 22:15 UTC (permalink / raw)
To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 2681 bytes --]
>
> 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 HomotopyTypeThe...@googlegroups.com
>> <mailto:HomotopyTypeTheo...@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 HomotopyTypeThe...@googlegroups.com <mailto:
>> HomotopyTypeThe...@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout.
>>
>
> --
> http://www.cs.bham.ac.uk/~mhe
>
[-- Attachment #2: Type: text/html, Size: 4667 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-11-29 21:12 ` Evan Cavallo
[not found] ` <204e382a-efcf-cb13-006f-47fdbadd99a5@cs.bham.ac.uk>
@ 2017-11-29 22:16 ` Martín Hötzel Escardó
2017-12-01 14:49 ` Martin Escardo
2017-12-01 14:53 ` Martín Hötzel Escardó
3 siblings, 0 replies; 16+ messages in thread
From: Martín Hötzel Escardó @ 2017-11-29 22:16 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 2021 bytes --]
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
> Evan
>
> 2017-11-28 4:40 GMT-05:00 Andrej Bauer <andr...@andrej.com <javascript:>
> >:
>
>> > 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 HomotopyTypeThe...@googlegroups.com <javascript:>.
>> For more options, visit https://groups.google.com/d/optout.
>>
>
>
[-- Attachment #1.2: Type: text/html, Size: 3389 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-11-29 21:12 ` Evan Cavallo
[not found] ` <204e382a-efcf-cb13-006f-47fdbadd99a5@cs.bham.ac.uk>
2017-11-29 22:16 ` Martín Hötzel Escardó
@ 2017-12-01 14:49 ` Martin Escardo
2017-12-01 14:53 ` Martín Hötzel Escardó
3 siblings, 0 replies; 16+ messages in thread
From: Martin Escardo @ 2017-12-01 14:49 UTC (permalink / raw)
To: Homotopy Type Theory
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
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-11-29 21:12 ` Evan Cavallo
` (2 preceding siblings ...)
2017-12-01 14:49 ` Martin Escardo
@ 2017-12-01 14:53 ` Martín Hötzel Escardó
2017-12-09 0:27 ` Martín Hötzel Escardó
3 siblings, 1 reply; 16+ messages in thread
From: Martín Hötzel Escardó @ 2017-12-01 14:53 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 2683 bytes --]
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.
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
[-- Attachment #1.2: Type: text/html, Size: 3694 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-12-01 14:53 ` Martín Hötzel Escardó
@ 2017-12-09 0:27 ` Martín Hötzel Escardó
2017-12-18 22:58 ` Martín Hötzel Escardó
0 siblings, 1 reply; 16+ messages in thread
From: Martín Hötzel Escardó @ 2017-12-09 0:27 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 1242 bytes --]
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
[-- Attachment #1.2: Type: text/html, Size: 1663 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-12-09 0:27 ` Martín Hötzel Escardó
@ 2017-12-18 22:58 ` Martín Hötzel Escardó
2017-12-19 3:36 ` Gershom B
0 siblings, 1 reply; 16+ messages in thread
From: Martín Hötzel Escardó @ 2017-12-18 22:58 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 3052 bytes --]
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.
On Saturday, 9 December 2017 00:27:16 UTC, Martín Hötzel Escardó wrote:
>
> 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
>
>
>
[-- Attachment #1.2: Type: text/html, Size: 4520 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-12-18 22:58 ` Martín Hötzel Escardó
@ 2017-12-19 3:36 ` Gershom B
2017-12-20 20:46 ` Martín Hötzel Escardó
0 siblings, 1 reply; 16+ messages in thread
From: Gershom B @ 2017-12-19 3:36 UTC (permalink / raw)
To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory
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
On Mon, Dec 18, 2017 at 5:58 PM, Martín Hötzel Escardó
<escardo...@gmail.com> wrote:
> 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.
>
>
> On Saturday, 9 December 2017 00:27:16 UTC, Martín Hötzel Escardó wrote:
>>
>> 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
>>
>>
>
> --
> 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.
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-12-19 3:36 ` Gershom B
@ 2017-12-20 20:46 ` Martín Hötzel Escardó
0 siblings, 0 replies; 16+ messages in thread
From: Martín Hötzel Escardó @ 2017-12-20 20:46 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 1349 bytes --]
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ó
(escar...@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
[-- Attachment #1.2: Type: text/html, Size: 1610 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread