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