coq中Category和内部类别的定义
我有一个由两部分组成的问题。目标：我想定义给定类别内部的类别概念。
- 我想出了以下简单的代码，但是会产生一个莫名其妙的错误消息，即：
Record Category :=
{ Ob : Type;
Hom : Ob -> Ob -> Type;
_o_ : forall {a b c}, Hom b c -> Hom a b -> Hom a c;
1 : forall {x}, Hom x x;
Assoc : forall a b c d (f : Hom c d) (g : Hom b c) (h : Hom a b),
f o (g o h) = (f o g) o h;
LeftId : forall a b (f : Hom a b), 1 o f = f;
RightId : forall a b (f : Hom a b), f o 1 = f;
Truncated : forall a b (f g : Hom a b) (p q : f = g), p = q }.
- 如何“内化”这个定义？具体来说，我想在上面指定的类型类别内部定义一个类别。这意味着一个“内部类别”类型，对象是类别，即属于上述类别类别，箭头是类别类别的态射。所有这些都假设存在相关回调。如果不清楚，请参考https://ncatlab.org/nlab/show/internal+category
我猜想解决这个问题的最好方法是将内部类别定义为从上述指定类型继承的模块类别。目的是最终获得“环境类别”内部结构的层次结构。所以我最终想要超越仅仅定义另一个类别内部的类别，以及其他结构。
回答
您没有使用 Agda，因此_o_没有定义中缀表示法。此外，您也不能有一个名为的文件1。同样，您将不得不依赖符号系统。
接受以下内容。
Record Category := {
Ob : Type ;
Hom : Ob -> Ob -> Type ;
comp : forall {a b c}, Hom b c -> Hom a b -> Hom a c ;
id : forall {x}, Hom x x ;
Assoc :
forall a b c d (f : Hom c d) (g : Hom b c) (h : Hom a b),
comp f (comp g h) = comp (comp f g) h ;
LeftId : forall a b (f : Hom a b), comp id f = f ;
RightId : forall a b (f : Hom a b), comp f id = f ;
Truncated : forall a b (f g : Hom a b) (p q : f = g), p = q
}.
然后您可以使用符号表示组合和单位：
Arguments comp {_ _ _ _} _ _.
Notation "f ? g" := (comp f g) (at level 20).
Arguments id {_ _}.
Notation "1" := (id).
Check Assoc.
(* Assoc
: forall (c : Category) (a b c0 d : Ob c) (f : Hom c c0 d)
(g : Hom c b c0) (h : Hom c a b), f ? (g ? h) = (f ? g) ? h *)
Check LeftId.
(* LeftId
: forall (c : Category) (a b : Ob c) (f : Hom c a b), 1 ? f = f *)