Равенство между путями - PullRequest
Новая
       42

Равенство между путями

0 голосов
/ 06 ноября 2018

Используя библиотеку cubical-demo, я подумал, что следующее будет тривиально доказать: 

{-# OPTIONS --cubical #-}
open import Cubical.PathPrelude

foo : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → trans refl p ≡ p
foo p = ?

Но, увы, это не имеет решающего значения: попытка использовать refl не удалась с 

primComp (λ _ → ;A) (~ i ∨ i) (λ { i₁ (i = i0) → ;x ; i₁ (i = i1) → p i₁ }) (refl i)
!= p i 
of type ;A

и я не знаю с чего начать.

Ответы [ 2 ]

0 голосов
/ 07 ноября 2018

На основании ответа Сайзана Я посмотрел доказательства в cubical-demo и перенес его в новую библиотеку cubical. Я могу видеть, как это работает (например, я вижу, что значение данного пути равно x на всех трех обозначенных ребрах), но я пока не вижу, как бы я нашел подобное доказательство для аналогичного ситуация: 

{-# OPTIONS --cubical #-}
module _ where

open import Cubical.Core.Prelude

refl-compPath : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → compPath refl p ≡ p
refl-compPath {x = x} p i j = hcomp {φ = ~ j ∨ j ∨ i}
  (λ { k (j = i0) → x
     ; k (j = i1) → p k
     ; k (i = i1) → p (k ∧ j)
     })
  x
0 голосов
/ 06 ноября 2018

Нет, к сожалению, мы теряем некоторые определения определений при использовании Path, потому что мы не знаем, как сохранить систему в слиянии, если бы мы добавили эти сокращения.

Вместо этого тип Id имеет обычные правила сокращения.

https://github.com/Saizan/cubical-demo/blob/master/src/Cubical/Id.agda

В случае леммы, которую вы хотите доказать о trans, вы можете найти доказательство в

https://github.com/Saizan/cubical-demo/blob/master/src/Cubical/Lemmas.agda

Кстати, кубическая демоверсия выросла органически, и мы начинаем заново с надеждой на более чистую настройку (хотя и с различными примитивами) на

https://github.com/agda/cubical

cubical имеет лучший Id модуль, например:

https://github.com/agda/cubical/blob/master/Cubical/Core/Id.agda

...