单价公理是内射的吗？

Question

单价公理是否可逆（模路径）？是否可以证明，使用Agda's Cubical library，证明如下：

open import Cubical.Core.Glue

uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} → 
  ua f ≡ ua g → equivFun f ≡ equivFun g

我怀疑上面应该成立，因为在[=20=的例子3.19]中，有一个证明步骤，其中两个等价之间的等价用于证明它们功能之间的等价：

[...] so f is an equivalence. Hence, by univalence, f gives rise to a path p : A ≡ A.

If p were equal to refl A, then (again by univalence) f would equal the identity function of A.

Answer 1

当然，ua是等价的，所以它是单射的。在 HoTT 书中，ua 的倒数是 idtoeqv，所以通过同余 idtoeqv (ua f) ≡ idtoeqv (ua g) 然后通过倒数 f ≡ g。我不熟悉 cubical Agda prelude 的内容，但这应该是可以证明的，因为它直接来自单价陈述。

Answer 2

把写成代码，我们可以证明一般等价函数的单射性：

equivInj : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (f : A ≃ B) → 
  ∀ x x′ → equivFun f x ≡ equivFun f x′ → x ≡ x′
equivInj f x x′ p = cong fst $ begin
  x , refl                   ≡⟨ sym (equivCtrPath f (equivFun f x) (x , refl)) ⟩
  equivCtr f (equivFun f x)  ≡⟨ equivCtrPath f (equivFun f x) (x′ , p) ⟩
  x′ , p ∎

然后给出

univalence : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)

我们得到

uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} → ua f ≡ ua g → equivFun f ≡ equivFun g
uaInj {f = f} {g = g} = cong equivFun ∘ equivInj (invEquiv univalence) f g

唯一的问题是 Cubical 库中的 univalence is not readily available。希望很快就能解决这个问题。

更新：针对上述问题单，proof of univalence is now available in the Cubical library。

单价公理是内射的吗？

Is the univalence axiom injective?

agda

cubical-type-theory

homotopy-type-theory