代码之家  ›  专栏  ›  技术社区  ›  Cactus

一价公理是内射的吗?

homotopy-type-theory cubical-type-theory agda
  •  1
  • Cactus  · 技术社区  · 6 年前

    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

    我怀疑上面的说法应该成立,因为在 the HoTT book

    f F 产生一条路 p : A ≡ A .

    如果 p refl A ,然后(再次按单价) F 将等于 同一函数 A

    2 回复  |  直到 6 年前
        1
  •  1
  •   András Kovács    6 年前

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

        2
  •  1
  •   Cactus    6 年前

    使 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 .

    推荐文章
    关于   移动版
    代码之家 - 一站式码农服务社区
    沪ICP备11025650号