* Yet another characterization of univalence
@ 2017-11-17 23:53 Martín Hötzel Escardó
2017-11-20 3:54 ` [HoTT] " y
0 siblings, 1 reply; 16+ messages in thread
From: Martín Hötzel Escardó @ 2017-11-17 23:53 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 475 bytes --]
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
[-- Attachment #1.2: Type: text/html, Size: 624 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-11-17 23:53 Yet another characterization of univalence Martín Hötzel Escardó
@ 2017-11-20 3:54 ` y
2017-11-24 12:21 ` Martín Hötzel Escardó
2017-11-24 23:12 ` Martín Hötzel Escardó
0 siblings, 2 replies; 16+ messages in thread
From: y @ 2017-11-20 3:54 UTC (permalink / raw)
To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 1111 bytes --]
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?
On Fri, Nov 17, 2017 at 3:53 PM, Martín Hötzel Escardó <
escardo...@gmail.com> wrote:
> 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
>
> --
> 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: 1844 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-11-20 3:54 ` [HoTT] " y
@ 2017-11-24 12:21 ` Martín Hötzel Escardó
2017-11-24 19:11 ` Martín Hötzel Escardó
2017-11-24 23:12 ` Martín Hötzel Escardó
1 sibling, 1 reply; 16+ messages in thread
From: Martín Hötzel Escardó @ 2017-11-24 12:21 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 1756 bytes --]
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
[-- Attachment #1.2: Type: text/html, Size: 2403 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-11-24 12:21 ` Martín Hötzel Escardó
@ 2017-11-24 19:11 ` Martín Hötzel Escardó
2017-11-28 9:40 ` Andrej Bauer
0 siblings, 1 reply; 16+ messages in thread
From: Martín Hötzel Escardó @ 2017-11-24 19:11 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 2438 bytes --]
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
> 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
>
>
[-- Attachment #1.2: Type: text/html, Size: 3426 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-11-20 3:54 ` [HoTT] " y
2017-11-24 12:21 ` Martín Hötzel Escardó
@ 2017-11-24 23:12 ` Martín Hötzel Escardó
2017-11-24 23:28 ` Martín Hötzel Escardó
1 sibling, 1 reply; 16+ messages in thread
From: Martín Hötzel Escardó @ 2017-11-24 23:12 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 651 bytes --]
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
[-- Attachment #1.2: Type: text/html, Size: 1044 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-11-24 23:12 ` Martín Hötzel Escardó
@ 2017-11-24 23:28 ` Martín Hötzel Escardó
0 siblings, 0 replies; 16+ messages in thread
From: Martín Hötzel Escardó @ 2017-11-24 23:28 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 571 bytes --]
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
>
>
>
[-- Attachment #1.2: Type: text/html, Size: 1080 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-11-24 19:11 ` Martín Hötzel Escardó
@ 2017-11-28 9:40 ` Andrej Bauer
2017-11-29 21:12 ` Evan Cavallo
0 siblings, 1 reply; 16+ messages in thread
From: Andrej Bauer @ 2017-11-28 9:40 UTC (permalink / raw)
To: Homotopy Type Theory
> 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
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Yet another characterization of univalence
2017-11-28 9:40 ` Andrej Bauer
@ 2017-11-29 21:12 ` Evan Cavallo
[not found] ` <204e382a-efcf-cb13-006f-47fdbadd99a5@cs.bham.ac.uk>
` (3 more replies)
0 siblings, 4 replies; 16+ messages in thread
From: Evan Cavallo @ 2017-11-29 21:12 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 1442 bytes --]
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
2017-11-28 4:40 GMT-05:00 Andrej Bauer <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.
> For more options, visit https://groups.google.com/d/optout.
>
[-- Attachment #1.2: Type: text/html, Size: 2134 bytes --]
[-- Attachment #2: IdEmbedding.agda --]
[-- Type: application/octet-stream, Size: 6258 bytes --]
{-# OPTIONS --without-K --rewriting #-}
open import HoTT
module IdEmbedding where
is-embedding : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) → Type (lmax i j)
is-embedding f = ∀ b → is-prop (hfiber f b)
equiv-is-embedding : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) → is-equiv f → is-embedding f
equiv-is-embedding f f-eq b = contr-is-prop (equiv-is-contr-map f-eq b)
embedding-ap-is-equiv : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
→ is-embedding f
→ ∀ a₁ a₂ → is-equiv (ap f :> (a₁ == a₂ → f a₁ == f a₂))
embedding-ap-is-equiv f f-em a₁ a₂ = is-eq
(ap f)
(λ q → fst= (prop-has-all-paths {{f-em (f a₂)}} (a₁ , q) (a₂ , idp)))
(λ q → ∘-ap f fst _ ∙ ! (↓-app=cst-out' $ apd snd (prop-has-all-paths {{f-em (f a₂)}} (a₁ , q) (a₂ , idp))))
(λ p → ap fst= (prop-has-all-paths {{=-preserves-level (f-em (f a₂))}} _ _) ∙ fst=-β p (↓-app=cst-in' idp))
ap-equiv-is-embedding : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
→ (∀ a₁ a₂ → is-equiv (ap f :> (a₁ == a₂ → f a₁ == f a₂)))
→ is-embedding f
ap-equiv-is-embedding f eq-ap b = all-paths-is-prop $ (λ {(a₁ , p₁) (a₂ , p₂) →
pair= (is-equiv.g (eq-ap a₁ a₂) (p₁ ∙ ! p₂))
(↓-app=cst-in $ lemma p₁ p₂ ∙ ! (ap (λ r → r ∙ p₂) (is-equiv.f-g (eq-ap a₁ a₂) (p₁ ∙ ! p₂))))})
where
lemma : ∀ {i} {A : Type i} {a₁ a₂ a₃ : A} (p : a₁ == a₂) (q : a₃ == a₂)
→ p == (p ∙ ! q) ∙ q
lemma idp idp = idp
_∘emb_ : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} {g : B → C} {f : A → B}
→ is-embedding g → is-embedding f → is-embedding (g ∘ f)
_∘emb_ {g = g} {f = f} g-em f-em = ap-equiv-is-embedding (g ∘ f) $ λ a₁ a₂ →
transport is-equiv
(λ= (∘-ap g f))
(embedding-ap-is-equiv g g-em (f a₁) (f a₂) ∘ise embedding-ap-is-equiv f f-em a₁ a₂)
ap-hfiber : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A → B) (g : B → C)
(b : B) → hfiber f b → hfiber (g ∘ f) (g b)
ap-hfiber f g b (a , p) = (a , ap g p)
ap-hfiber-embedding-is-equiv : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A → B) (g : B → C)
→ is-embedding g
→ ∀ b → is-equiv (ap-hfiber f g b)
ap-hfiber-embedding-is-equiv {A = A} f g g-em b = is-eq
(ap-hfiber f g b)
(λ {(a , q) → a , <– e q})
(λ {(a , q) → pair= idp (<–-inv-r e q)})
(λ {(a , p) → pair= idp (<–-inv-l e p)})
where
e : ∀ {b₁ b₂} → (b₁ == b₂) ≃ (g b₁ == g b₂)
e {b₁} {b₂} = (ap g , embedding-ap-is-equiv g g-em b₁ b₂)
equiv-lift : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A → B) (g : B → C)
→ is-equiv (g ∘ f) → is-embedding g → is-equiv f
equiv-lift f g gf-eq g-em = contr-map-is-equiv $ λ b →
equiv-preserves-level ((_ , ap-hfiber-embedding-is-equiv f g g-em b)⁻¹) {{equiv-is-contr-map gf-eq (g b)}}
米田 : ∀ {i} {A : Type i} {a₁ a₂ : A} → a₁ == a₂ → (∀ a → Path a₂ a ≃ Path a₁ a)
米田 p a = pre∙-equiv p
米田-is-equiv : ∀ {i} {A : Type i} {a₁ a₂ : A} → is-equiv (米田 {a₁ = a₁} {a₂ = a₂})
米田-is-equiv = is-eq 米田 g 米田-g g-米田
where
g : ∀ {i} {A : Type i} {a₁ a₂ : A} → (∀ a → Path a₂ a ≃ Path a₁ a) → a₁ == a₂
g {a₂ = a₂} e = –> (e a₂) idp
米田-g : ∀ {i} {A : Type i} {a₁ a₂ : A} (e : ∀ a → Path a₂ a ≃ Path a₁ a) → 米田 (g e) == e
米田-g e = λ= $ λ a → pair= (λ= $ naturality e) prop-has-all-paths-↓
where
naturality : ∀ {i} {A : Type i} {a₁ a₂ : A} (e : ∀ a → Path a₂ a ≃ Path a₁ a)
{a : A} (p : a₂ == a) → –> (e a₂) idp ∙ p == –> (e a) p
naturality e idp = ∙-unit-r _
g-米田 : ∀ {i} {A : Type i} {a₁ a₂ : A} (p : a₁ == a₂) → g (米田 p) == p
g-米田 idp = idp
apply : ∀ {i} {A : Type i} {a₁ a₂ : A} → Path a₁ == Path a₂ → (∀ a → Path a₁ a ≃ Path a₂ a)
apply α a = coe-equiv (app= α a)
Thm₁ : ∀ {i} {A : Type i}
→ ((a₁ a₂ : A) → is-embedding (apply {a₁ = a₁} {a₂ = a₂}))
→ is-embedding (Path {A = A})
Thm₁ apply-em = ap-equiv-is-embedding _ $ λ a₁ a₂ →
equiv-lift (ap Path) !
(equiv-lift (! ∘ ap Path) apply (transport is-equiv (! $ λ= triangle) 米田-is-equiv) (apply-em a₂ a₁))
(equiv-is-embedding ! (snd !-equiv))
where
triangle : ∀ {i} {A : Type i} {a₁ a₂ : A} (p : a₁ == a₂) → apply (! (ap Path p)) == 米田 p
triangle idp = λ= $ (λ _ → pair= idp $ prop-has-all-paths _ _)
post∘-is-equiv' : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} (h : ∀ a → B a → C a)
→ (∀ a → is-equiv (h a))
→ is-equiv (λ (k : Π A B) a → h a (k a))
post∘-is-equiv' h e = is-eq
(λ k a → h a (k a))
(λ k a → is-equiv.g (e a) (k a))
(λ k → λ= (λ a → is-equiv.f-g (e a) (k a)))
(λ k → λ= (λ a → is-equiv.g-f (e a) (k a)))
post∘-is-embedding : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} (g : ∀ a → B a → C a)
→ (∀ a → is-embedding (g a))
→ is-embedding {A = Π A B} (λ f a → g a (f a))
post∘-is-embedding {A = A} {B = B} g g-em = ap-equiv-is-embedding _ $ λ f₁ f₂ →
let
lemma₁ : is-equiv (λ (p : (a : A) → f₁ a == f₂ a) (a : A) → ap (g a) (p a))
lemma₁ = (post∘-is-equiv' (λ a → ap (g a)) (λ a → embedding-ap-is-equiv (g a) (g-em a) (f₁ a) (f₂ a)))
in
transport is-equiv
(λ= $ lemma₂ f₁ f₂)
(snd (app=-equiv ⁻¹) ∘ise lemma₁ ∘ise snd app=-equiv)
where
lemma₂ : (f₁ f₂ : Π A B) (p : f₁ == f₂) → <– app=-equiv (λ a → ap (g a) (app= p a)) == ap (λ f a → g a (f a)) p
lemma₂ f₁ ._ idp = <–-inv-l app=-equiv idp
Thm₂ : ∀ {i}
→ ((A B : Type i) → is-embedding (coe-equiv :> (A == B → A ≃ B)))
→ ((A : Type i) → is-embedding (Path {A = A}))
Thm₂ coe-equiv-em A = Thm₁ $ λ a₁ a₂ →
post∘-is-embedding (λ a αa → coe-equiv αa) (λ a → coe-equiv-em (Path a₁ a) (Path a₂ a))
∘emb
(equiv-is-embedding app= (snd (app=-equiv)))
^ permalink raw reply [flat|nested] 16+ messages in thread
* 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
end of thread, other threads:[~2017-12-20 20:46 UTC | newest]
Thread overview: 16+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-11-17 23:53 Yet another characterization of univalence Martín Hötzel Escardó
2017-11-20 3:54 ` [HoTT] " y
2017-11-24 12:21 ` Martín Hötzel Escardó
2017-11-24 19:11 ` Martín Hötzel Escardó
2017-11-28 9:40 ` Andrej Bauer
2017-11-29 21:12 ` Evan Cavallo
[not found] ` <204e382a-efcf-cb13-006f-47fdbadd99a5@cs.bham.ac.uk>
2017-11-29 22:15 ` Evan Cavallo
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ó
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
2017-12-20 20:46 ` Martín Hötzel Escardó
2017-11-24 23:12 ` Martín Hötzel Escardó
2017-11-24 23:28 ` Martín Hötzel Escardó
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).