如何在Agda中证明某种类型有效？

我正在尝试对依赖函数进行证明,而且我遇到了障碍.

所以我们假设我们有一个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

user3237465.. 6

您可以明确更改以下类型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在标准库.