coq - coq中类别和内部类别的定义

Question

我有一个分为两部分的问题。目标:我想定义给定类别内部类别的概念。

1. 我想出了以下简单的代码，但是却产生了一条莫名其妙的错误消息，即:

File "./Category.v", line 5, characters 4-5:Syntax error: '}' expected after [record_fields] (in [constructor_list_or_record_decl]).

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 }.

1. 如何“内化”这个定义？具体来说，我想在上面指定的类型类别中定义一个内部类别。这意味着一个类型“内部范畴”使得对象是范畴，即属于上面的类型 Category 并且箭头是类型 Category 的态射。所有这一切都假设存在相关回调。不清楚的可以引用https://ncatlab.org/nlab/show/internal+category我的猜测是，实现这一目标的最佳方法是将内部类别定义为继承自上述指定类型类别的模块。目的是最终获得“环境类别”内部结构的层次结构。所以我最终想要超越仅仅定义另一个类别内部的类别，但也包括其他结构。感谢任何指点。

Answer 1

你没有使用 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 *)