Yet another characterization of univalence

Yet another characterization of univalence

[Martín Hötzel Escardó]

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

Re: [HoTT] Yet another characterization of univalence

[y]

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

Re: [HoTT] Yet another characterization of univalence

[Martín Hötzel Escardó]

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

Re: [HoTT] Yet another characterization of univalence

[Martín Hötzel Escardó]

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

Re: [HoTT] Yet another characterization of univalence

[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

Re: [HoTT] Yet another characterization of univalence

[Evan Cavallo]

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

Re: [HoTT] Yet another characterization of univalence

[Evan Cavallo]

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

Re: [HoTT] Yet another characterization of univalence

[Martín Hötzel Escardó]

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

Re: [HoTT] Yet another characterization of univalence

[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

Re: [HoTT] Yet another characterization of univalence

[Martín Hötzel Escardó]

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

Re: [HoTT] Yet another characterization of univalence

[Martín Hötzel Escardó]

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

Re: [HoTT] Yet another characterization of univalence

[Martín Hötzel Escardó]

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

Re: [HoTT] Yet another characterization of univalence

[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

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.

Re: [HoTT] Yet another characterization of univalence

[Martín Hötzel Escardó]

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

Re: [HoTT] Yet another characterization of univalence

[Martín Hötzel Escardó]

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

Re: [HoTT] Yet another characterization of univalence

[Martín Hötzel Escardó]

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