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

Question

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

Так скажем, у нас есть теорема п равных

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 

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

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

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 

BTW, ваш 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 

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