Re: [HoTT] Yet another characterization of univalence

[Evan Cavallo <evanc...@gmail.com>]

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