一价公理是内射的吗?

当然 ua 行动单位 是 idtoeqv ,所以同余 idtoeqv (ua f) ≡ idtoeqv (ua g) f ≡ g . 我不熟悉立体阿格达前奏曲的内容,但这应该是可以证明的,因为它直接从一价声明。

使 András's answer 在代码中,我们通常可以证明等价函数的内射性:

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

唯一的问题是, univalence is not readily available Cubical 图书馆。希望很快就能解决。

更新 proof of univalence is now available in the Cubical library .