基于Coq 8.10.2定义参数化函数为态射的欧氏空间范畴报错求助

首先咱们得明确范畴论里态射复合的核心类型约束——范畴的compose必须满足：

compose : ∀ A B C, hom B C → hom A B → hom A C

而你定义的hom A B是forall {P:SuperEuc}, Euc (dim P) -> Euc (dim A) -> Euc (dim B)，这意味着hom A C的类型是forall {P:SuperEuc}, Euc (dim P) -> Euc (dim A) -> Euc (dim C)。关键点在这里：每个态射都是“对任意参数空间P”的函数，所以复合后的态射也必须是一个单一的函数，接受同一个P的实例，同时给前后两个态射使用。

你之前的compose写法里试图给I用P、给J用Q，这就违背了hom的类型要求——复合后的结果需要能接受任意单个P，而不是两个不同的参数空间。这就是为什么Coq报错说类型不匹配：你的写法返回的是依赖两个参数P和Q的结果，但范畴要求compose的结果必须是只依赖单个P的函数。

修正后的代码 #

我们需要调整compose的定义，让I和J共享同一个参数P。具体来说，对于任意给定的P，拿到它的实例p:Euc (dim P)，先通过I得到Euc (dim A) -> Euc (dim B)的函数，再通过J得到Euc (dim B) -> Euc (dim C)的函数，最后把这两个函数复合起来：

Require Import Coq.Reals.Reals.
Require Import Category.Theory.

Inductive Euc:nat -> Type:=
|RO : Euc 0
|Rn : forall n:nat, R -> Euc n -> Euc (S n).

Record SuperEuc := { dim : nat; }.

Program Instance Para : Category := {
  obj := SuperEuc;
  hom := fun A B:SuperEuc => forall {P:SuperEuc}, Euc (dim P) -> Euc (dim A) -> Euc (dim B);
  compose := fun A B C (J : hom B C) (I : hom A B) {P:SuperEuc} (p:Euc (dim P)) (a:Euc (dim A)) =>
    J p (I p a);
  identity := fun A {P:SuperEuc} (p:Euc (dim P)) (a:Euc (dim A)) => a;
}.

为什么这样可行？ #

• 修正后的compose返回的正好是hom A C类型：它接受任意P，然后把I和J都作用在同一个p上，复合得到从A到C的函数。
• 我们还补充了identity态射的定义——这是范畴必须的单位元，它对任意P和a，直接返回a，符合单位态射的要求。

接下来你需要用Next Obligation来证明范畴的公理（结合律和单位元律），Coq的Program机制会帮你生成这些义务，你只需要完成证明即可。

内容的提问来源于stack exchange，提问作者Daisuke Sugawara