は、以下微積分の「Refl」は何ですか？そのような<code>Agda</code>、<code>Idris</code>、またはタイプ拡張子<code>Haskell</code>などの言語で
data a :~: b where
Refl :: a :~: a
a :~: b等の=型ソートがあるaとbが同じであることを意味します。
このようなタイプは、calculus of constructionsまたはMorte（計算の計算に基づくプログラミング言語）で定義できますか？
のCoCでa :~: bの標準教会エンコーディングは次のとおり
(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
興味深い。他の言語でもできるように、 '0：〜：1'から矛盾を引き出すことは可能ですか？ （真実ではなく '（）'を返し、偽ではなく 'Void'を返す等価関数を作るだけです） – PyRulez
（これは他のGADTにも簡単に一般化する方法を見ています。） – PyRulez
@PyRulezはい。教会の数字では、 '0 f x = x'と' 1 f x = f x'（モジュロ型引数の追加）です。これを使うと、 '0（const True）False = False'と' 1（const True）False = True'を持つことができます。 <->（y（const True）False） 'とすると、' False <-> True'と証明できます。 – chi
すべての帰納的型はCoCでコード化することができますが、関連する依存性除去原則はありません（非依存性排除が利用可能です）。 （また、 'a：〜：b'は型ですが、' Refl'は値です）。 – chi
構造の微積はラムダキューブの "トップ"です。ハスケル、アグダ、イドリスはCoCの「下」です。したがって、CoCはより表現力があるという単純な事実のために可能であるべきです。 – Bakuriu
@Bakuriu実際、Agda/Coqは、CoCには欠けている依存型除去型の帰納的型を許可しているので、CoCを超えています。 Agdaはまた、Streicherの公理Kを証明している。これは、CoCまたはCoq（別名CiC）では利用できない同じ平等a = bの2つの証明「p、q」が等しい（「p = q」）必要があることを暗示する。 – chi