coq - 与范畴论打交道

Question

动机:我正在尝试研究范畴论，同时为我在所遵循的任何教科书中发现的想法创建 Coq 形式化。为了使这种形式化尽可能简单，我认为应该用其标识箭头来标识对象，因此可以将类别简化为具有源映射的一组(类，类型)箭头 X s:X->X、目标映射 t:X->X 和组合映射 product : X -> X -> option X这是为 t f = s g 定义的部分映射。显然，结构(X,s,t,product)应该遵循各种属性。为了清楚起见，我在下面详细说明了我选择的形式化，但我认为没有必要遵循它来阅读我的问题:

Record Category {A:Type} : Type := category
    {   source : A -> A
    ;   target : A -> A
    ;   product: A -> A -> option A
    ;   proof_of_ss : forall f:A, source (source f) = source f    
    ;   proof_of_ts : forall f:A, target (source f) = source f
    ;   proof_of_tt : forall f:A, target (target f) = target f
    ;   proof_of_st : forall f:A, source (target f) = target f
    ;   proof_of_dom: forall f g:A, target f = source g <-> product f g <> None
    ;   proof_of_src: forall f g h:A, product f g = Some h -> source h = source f
    ;   proof_of_tgt: forall f g h:A, product f g = Some h -> target h = target g
    ;   proof_of_idl: forall a f:A, 
            a = source a -> 
            a = target a -> 
            a = source f -> 
            product a f = Some f
    ;   proof_of_idr: forall a f:A,
            a = source a -> 
            a = target a -> 
            a = target f -> 
            product f a = Some f
    ;   proof_of_asc: 
            forall f g h fg gh:A, 
            product f g = Some fg -> 
            product g h = Some gh -> 
            product fg h = product f gh
    }
    .

我不知道这有多实用以及它会带我走多远。我认为这是一个同时学习范畴论和 Coq 的机会。

问题:我的第一个目标是创建一个尽可能类似于类别Set的“类别”。在集合论框架中，我可能会考虑三元组 (a,b,f) 类，其中 f 是具有域 a 的映射并范围 b 的子集。考虑到这一点，我尝试了:

Record Arrow : Type := arrow
    {   dom  : Type
    ;   cod  : Type
    ;   arr  : dom -> cod
    }
    .

因此，Arrow 成为我的基本类型，我可以在其上尝试构建类别结构。我开始将 Type 嵌入到 Arrow 中:

Definition id (a : Type) : Arrow := arrow a a (fun x => x).

它允许我定义源和目标映射:

Definition domain (f:Arrow) : Arrow := id (dom f).
Definition codomain (f:Arrow) : Arrow := id (cod f). 

然后我继续在箭头上定义组合:

Definition compose (f g: Arrow) : option Arrow :=
    match f with
        | arrow a b f' => 
            match g with
                | arrow b' c g' =>
                    match b with 
                        | b'    => Some (arrow a c (fun x => (g' (f' x))))
                        | _     => None
                    end
            end
    end.

但是，此代码是非法的，因为我收到错误:

The term "f' x" has type "b" while it is expected to have type "b'".

问题:我有一种感觉，我不会逃脱这个惩罚，我天真地使用 Type 会让我陷入某种罗素悖论，而 Coq 不会让我做。但是，为了以防万一，有没有办法在 Arrow 上定义 compose ？

Answer 1

由于理论的建设性性质，您的编码在普通 Coq 中不起作用:不可能比较两个集合是否相等。如果你绝对想遵循这种方法，Daniel 的评论勾画了一个解决方案:你需要假设一个强大的经典原理，以便能够检查两个箭头的端点是否匹配，然后操纵一个等式证明以使 Coq 接受该定义。

另一种方法是为箭头和对象设置单独的类型，并使用类型依赖关系来表达箭头端点的兼容性要求。这个定义只需要三个公理，并且大大简化了类别的构造:

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Record category : Type := Category {
  obj   : Type;
  hom   : obj -> obj -> Type;
  id    : forall {X}, hom X X;
  comp  : forall X Y Z, hom X Y -> hom Y Z -> hom X Z;
  (* Axioms *)
  idL   : forall X Y (f : hom X Y), comp id f = f;
  idR   : forall X Y (f : hom X Y), comp f id = f;
  assoc : forall X Y Z W 
                 (f : hom X Y) (g : hom Y Z) (h : hom Z W),
            comp f (comp g h) = comp (comp f g) h
}.

我们现在可以定义集合的类别并要求 Coq 自动为我们证明公理。

Require Import Coq.Program.Tactics.

Program Definition Sets : category := {|
  obj := Type;
  hom X Y := X -> Y;
  id X := fun x => x;
  comp X Y Z f g := fun x => g (f x)
|}.

(这不会导致任何循环悖论，因为 Coq 的宇宙机制:Coq 知道此定义中使用的 Type 实际上比用于定义 category 的要小。)

由于 Coq 理论缺乏外延性，这种编码有时会很不方便，因为它阻止了某些公理的成立。例如，考虑群的类别，其中态射是与群运算进行交换的函数。这些态射的合理定义如下(假设有某种类型group代表群，*表示乘法，1表示中性元素)。

Record group_morphism (X Y : group) : Type := {
  mor   : X -> Y;
  mor_1 : mor 1 = 1;
  mor_m : forall x1 x2, mor (x1 * x2) = mor x1 * mor x2
}.

问题是属性 mor_1和mor_m干扰 group_morphism 元素的平等概念，证明适用于 Sets 的关联性和恒等性休息。解决办法有两种:

1. 在理论中采用额外的公理，以便仍然满足所需的属性。在上面的示例中，您需要证明无关性:

   proof_irrelevance : forall (P : Prop) (p q : P), p = q。

2. 更改类别公理，以便恒等式在特定于该类别的某种等价关系上有效，而不是简单的 Coq 等式。此方法遵循here例如。