Парное равенство в agda

У меня есть следующий код, который я хочу доказать:

data Pair (A : Set) (B : A → Set) : Set where
  pair : (a : A) → (B a) → Pair A B

pairEq : (A : Set) → (B : A → Set) → (a : A) → (b₁ b₂ : B a) → (pair {A} {B} a b₁ ≡ pair {A} {B} a b₂) → b₁ ≡ b₂
pairEq A B a b₁ b₂ refl = {!!}

Как я могу доказать, что это агда? ввод refl приводит к ошибке. Как я могу это обойти?


agda
person Konstantin Solomatov    schedule 13.05.2014    source источник
comment
Люди, почему вы это отрицаете?   -  person Konstantin Solomatov    schedule 13.05.2014

Ответы (1)


arrow_upward
0
arrow_downward

Сам сделал:

data Pair (A : Set) (B : A → Set) : Set where
  pair : (a : A) → (B a) → Pair A B

pairEq : (A : Set) → (B : A → Set) → (a : A) → (b₁ b₂ : B a) → (pair {A} {B} a b₁ ≡ pair {A} {B} a b₂) → b₁ ≡ b₂
pairEq A B a .b b refl = refl
person Konstantin Solomatov    schedule 13.05.2014