1

单价公理是可逆的（模路径）吗？是否可以使用Agda 的 Cubical 库来证明以下内容：

open import Cubical.Core.Glue

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

我怀疑上述内容应该成立，因为在HoTT book的示例 3.19 中，证明中有一个步骤使用两个等价之间的等价来证明它们的功能之间的等价：

[...]f等价物也是如此。因此，通过一元性，f产生了一条路径p : A ≡ A。

如果p等于refl A，那么（再次通过单价）f将等于 的恒等函数A。

4

2 回答 2

1

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

于 2018-11-14T15:11:42.097 回答
1

要将András 的答案放入代码中，我们可以证明一般等价函数的单射性：

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中并不容易获得。Cubical希望这很快就会得到解决。

更新：针对上述错误票，库中现在提供了单价证明Cubical。

于 2018-11-16T13:24:26.107 回答