问题标签 [injective-function]

说我有一个Inductive类型

但我真正想要的是“认同” b——c也就是说，我希望能够将它们视为编写同一事物的两种不同方式——并且能够将一种重写为另一种。

我可以把它作为一个公理来介绍：

但这显然是不合理的：

有没有其他方法可以做到这一点，或者类似的东西？我怀疑答案是否定的，因为它与Inductive构造函数的内射相矛盾。

当前的解决方法

我有关系

然后让我定义一个命题是否是关于它的明确定义的。

但这是不愉快的。这意味着，对于我自己的归纳定义命题，我需要添加一个额外的构造函数，equiv_foo以便能够证明明确定义的属性。（我怀疑仅仅为某个命题断言上述属性是不合理的。）

我能不能告诉 Coq“这个东西，以及使用它构建的任何东西，可能不是单射的”？

我有一组属性A= {a1, a2, ...an}和一组集群C = {c1, c2, ... ck}，我有一组对应关系COR，它们是A x C和的子集|COR|<< A x C。这是一组对应的样本

COR = {(a1, c1), (a1, c2), (a2, c1), (a3, c3), (a4, c4)}

现在，我想生成这样的所有子集，COR使得子集中的每一对都代表一个从 setA到 set的单射函数C。让我们称每个这样的子集为一个映射，那么来自上述集合的有效映射COR将是有趣的
m1 = {(a1, c1), (a3, c3), (a4, c4)}，m2 = {(a1, c2), (a2, c1), (a3, c3), (a4, c4)}
m1因为添加任何剩余的元素 from要么违反函数的定义，要么违反作为单射函数的COR条件m1. 例如，如果我们将对添加(a1,c2)到m1,m1将不再是一个函数，如果我们添加(a2,c1)到m1，它将不再是单射函数。因此，我对一些可用于生成所有此类映射的代码片段或算法感兴趣。这是我迄今为止在 python import collections import itertools 中尝试过的

正如预期的那样，代码会产生m2但不是m1因为m1不会从itertools.product. 有人可以指导我吗？我还想要一些关于性能的指导，因为实际的集合会比COR这里使用的集合大，并且可能包含更多冲突的集合。

所以就像标题说的那样，我需要帮助尝试将点从二维平面映射到数轴，这样每个点都与一个唯一的正整数相关联。换句话说，我需要一个函数 f:ZxZ->Z+ 并且我需要 f 是单射的。此外，我需要在合理的时间内运行。

所以我认为这样做的方式基本上只是计算点，从 (1,1) 开始并向外螺旋。

下面我写了一些 python 代码来做这件事（i，j）

我很确定这可行，但正如您所见，它是一个相当庞大的功能。我正在想办法简化这种“螺旋计数”逻辑。或者，如果有另一种更易于编码的计数方法也可以使用。

假设我有一个渲染功能：

我需要证明这个说法：

如果rasterize w h t1 = rasterize w h t2那么t1 ≡ t2

换句话说，如果 t1 和 t2 在相同宽度和高度的情况下呈现相同的值，那么它们是相等的。

我不知道在 agda 中怎么说，我想出了以下内容：

但我怀疑这不是我的意思，通过谷歌搜索我认为我需要定义一个比较渲染值的运算符？还涉及某种 sigma 类型？

如果我有一个单射类型族和类型等价证明，我怎样才能得到参数等价的证明？

我能想出的最好的 uses unsafeCoerce，这对我来说似乎是合理的，因为 TypeFamily 是单射的，但是......函数本身不会检查TypeFamily 是否是单射的，所以，这可能是一个来源错误。我也可能是错的，即使这也不是安全使用unsafeCoerce.