小编Pat*_*ens的帖子

如何在 Cubical Agda 中证明两件事不相等？（v2.6.1，Cubical 回购版本acabbd9）

具体来说，以下是作为更高归纳类型的整数：

{-# OPTIONS --safe --warning=error --cubical --without-K #-}\n\nopen import Cubical.Core.Everything\nopen import Cubical.Foundations.Prelude\n\nmodule Integers where\n\ndata False : Set where\n\ndata \xe2\x84\x95 : Set where\n  zero : \xe2\x84\x95\n  succ : \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\x95\n\n{-# BUILTIN NATURAL \xe2\x84\x95 #-}\n\ndata \xe2\x84\xa4 : Set where\n  pos : \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\xa4\n  neg : \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\xa4\n  congZero : pos 0 \xe2\x89\xa1 neg 0\n

很容易表现出一些相当奇怪的等式，因为这里的“等式”实际上意味着一些与我们在非立方世界中习惯的东西不太一样的东西：

oddThing2 : pos 0 \xe2\x89\xa1 congZero i1\noddThing2 = congZero\n

我在https://github.com/Saizan/cubical-demo/blob/b112c292ded61b02fa32a1b65cac77314a1e9698/examples/Cubical/Examples/CTT/Data/Nat.agda发现了一个相当令人讨厌的证明，证明后继者非零：

TL;DR：在 Agda 中，给定a : A和proof : A == B，我可以获得一个元素a : B吗？

在我不断尝试学习 Agda 的过程中，我创建了以下Prime : nat -> Set数据类型，它见证了自然的原始性。

Prime zero = False
Prime (succ zero) = False
Prime (succ (succ n)) = forall {i : nat} -> divides i p -> i <N p -> zero <N i -> i == (succ zero)
  where
    p = succ (succ n)

这里：

• False 是没有构造函数的数据类型；
• divides a b是一种数据类型，包含k对以下事实的见证a * k = …