Инъективна ли аксиома однолистности?

Question

Является ли аксиома однолистности обратимой (по модулю путей)? Можно ли доказать, используя Кубическая библиотека Агды , чтобы доказать следующее:

open import Cubical.Core.Glue

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

Я подозреваю, что вышеупомянутое должно иметь место, потому что в примере 3.19 из книги HoTT , есть шаг в доказательстве, где эквивалентность между двумя эквивалентностями используется для доказательства эквивалентности между их функциями:

[...] так что f является эквивалентность. Следовательно, по однолистности f дает начало пути p : A ≡ A.

Если бы p было равно refl A, то (опять же по однолистности) f было бы равно тождественная функция A.

Answer 1

Чтобы вставить ответ Андраса в код, мы можем доказать инъективность функций эквивалентности в целом:

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 .

Answer 2

Конечно, ua - эквивалентность, поэтому она инъективна.В книге HoTT обратное значение ua равно idtoeqv, поэтому по конгруэнтности idtoeqv (ua f) ≡ idtoeqv (ua g), а затем по инверсиям f ≡ g.Я не знаком с содержанием кубической прелюдии Агды, но это должно быть доказуемо, поскольку это следует непосредственно из утверждения об однолистности.