Конечные мультимножества как хит в кубической Агде - PullRequest
Новая
       99

Конечные мультимножества как хит в кубической Агде

2 голосов
/ 29 сентября 2019

В стандартной библиотеке Cubical Agda есть конечные мультимножества , элегантные определения которых я воспроизвожу ниже: 

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude

infixr 20 _∷_

data FMSet (A : Set) : Set where
  []    : FMSet A
  _∷_   : (x : A) → (xs : FMSet A) → FMSet A
  comm  : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  trunc : isSet (FMSet A)

_++_ : ∀ {A : Set} -> FMSet A → FMSet A → FMSet A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
comm x y xs i ++ ys = comm x y (xs ++ ys) i
trunc xs1 xs2 p q i j ++ ys =
  trunc (xs1 ++ ys) (xs2 ++ ys) (cong (_++ ys) p) (cong (_++ ys) q) i j

Для доказательства того, что [] является правонейтральным элементом, используютсяабстрактная лемма FMSetElimProp.f, которую я не понимаю.Поэтому я пытаюсь сделать прямое доказательство, но я застрял.Вот мои попытки: 

unitr-++ : ∀ {A : Set} (ys : FMSet A) → ys ++ [] ≡ ys
unitr-++ [] = refl
unitr-++ (y ∷ ys) = cong ((y ∷_)) (unitr-++ ys)
unitr-++ (comm x y xs i) = cong₂ {!comm x y!} (unitr-++ xs) refl
unitr-++ (trunc xs1 xs2 p q i j) = {!!}

Я на правильном пути?Как я могу закончить это доказательство?

...