在构造微积分中的"反射"事物？

Question

在语言,如Agda,Idris或Haskell用类型扩展,有一种=像以下类型排序

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

a :~: b意味着a和b是一样的.

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

Answer 1

a :~: bCoC 的标准教会编码是:

(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