haskell - `Refl` 构造微积分中的东西？

Question

在诸如 Agda 之类的语言中, Idris , 或 Haskell使用类型扩展，有一个 =类型如下

data a :~: b where
  Refl :: a :~: a

a :~: b表示 a和 b是相同的。

可以在 calculus of constructions 中定义这样的类型吗？或 Morte (这是基于构造演算的编程语言)？

Answer 1

a :~: b 的标准 Church 编码在 CoC 中是:

(a :~: b) =
   forall (P :: * -> * -> *).
      (forall c :: *. P c c) ->
      P a b

Refl存在

Refl a :: a :~: a
Refl a =
   \ (P :: * -> * -> *)
     (h :: forall (c::*). P c c) ->
     h a

以上表述了类型之间的相等性。对于术语之间的相等性， :~:关系必须有一个额外的参数 t :: * , 其中 a b :: t .

((:~:) t a b) = 
   forall (P :: t -> t -> *).
      (forall c :: t. P c c) ->
      P a b

Refl t a :: (:~:) t a a
Refl t a =
   \ (P :: t -> t -> *)
     (h :: forall (c :: t). P c c) ->
     h a