Как я могу доказать, что тип действителен в Agda?

Question

Я пытаюсь сделать доказательства по зависимым функциям, и я сталкиваюсь с загадкой.

Итак, скажем, у нас есть теорема F-равно

f-equal : ∀ {A B} {f : A → B} {x y : A} → x ≡ y → f x ≡ f y
f-equal refl = refl

Я пытаюсь доказать более общее представление о сохранении равенства над зависимыми функциями и столкнуться с проблемой. А именно, тип

Π-equal : ∀ {A} {B : A → Set} {f : {a : A} → B a} {x y : A} →
            x ≡ y → f x ≡ f y

делает компилятор несчастным, потому что он не может понять, что fx и fy одного типа. Кажется, это должно быть исправимо. Это?

нота; используемое отношение эквивалентности определяется так:

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

Answer 1

Вы можете явно изменить тип f x:

Π-equal : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
        -> (p : x ≡ y) -> P.subst B p (f x) ≡ f y
Π-equal refl = refl

Или же

Π-equal'T : ∀ {α β} {A : Set α} {B : A -> Set β} -> ((x : A) -> B x) -> (x y : A) -> x ≡ y -> Set β
Π-equal'T f x y p with f x | f y
...| fx | fy rewrite p = fx ≡ fy

Π-equal' : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
        -> (p : x ≡ y) -> Π-equal'T f x y p
Π-equal' refl = refl

Или вы можете использовать гетерогенное равенство:

Π-equal'' : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
          -> x ≡ y -> f x ≅ f y
Π-equal'' refl = refl

subst функция также может быть полезна, вот ее тип (C-c C-d P.subst в Emacs):

{a p : .Agda.Primitive.Level} {A : Set a} (P : A → Set p)
      {x y : A} →
      x ≡ y → P x → P y

Импорт используется:

open import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.HeterogeneousEquality as H

Кстати, ваш f-equal является cong в стандартной библиотеке.

Answer 2

Это может быть обработано гетерогенным равенством, которое может быть импортировано из Relation.Binary.HeterogeneousEquality:

data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set ℓ where
   refl : x ≅ x

Интуитивно понятно равенство свидетельствует о равенстве вовлеченных типов, а также о равенстве ценностей.

Можно найти аналоги для функций для стандартного равенства (subst, trans, congи т. д.) в модуле. Также вы можете конвертировать туда и обратно стандарт и хет. использование равенства ≅-to-≡ а также ≡-to-≅, но только когда типы на сторонах наглядно равны.

Обратите внимание, что синтаксис "переписать" нельзя использовать с het. равенство.

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

Π-equal : 
  ∀ {A : Set} {B : A → Set}{f : ∀ a → B a}{x y : A} → (p : x ≡ y) → subst B p (f x) ≡ f y
Π-equal refl = refl

Этот подход фактически эквивалентен гет. равенство, но я нахожу это. с равенством намного легче работать.