搞乱范畴论

Question

动机：我正在尝试研究范畴论，同时对我在任何教科书中找到的想法进行 Coq 形式化。为了使这种形式化尽可能简单，我想我应该用它们的标识箭头来标识对象，这样一个类别就可以简化为一组（class，类型）箭头 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 的机会。

问题：我的第一个 objective 是创建一个 'Category'，它尽可能类似于类别 Set。在集合论框架中，我可能会考虑三元组 (a,b,f) 的 class，其中 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).

然后我继续在 Arrow 上定义构图：

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 会让我陷入某种 Russel 悖论，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 的元素的相等性概念，使得适用于 [=21] 的关联性和恒等性证明=] 休息。有两种解决方案：

在理论中采用额外的公理，以便所需的属性仍然通过。在上面的例子中，你需要证明无关性：

proof_irrelevance : forall (P : Prop) (p q : P), p = q.
更改类别公理，使恒等式在特定于该类别的某些等价关系之前有效，而不是普通的 Coq 等式。这种做法是遵循here，例如

搞乱范畴论

Messing around with category theory

coq

category-theory