Definition of Category and internal category in coq

user_16769486 0
Viewed 105

I have a two-part question. Goal: I want to define the notion of a category internal to a given category.

  1. I came up with the following simple code, that however produces an inexplicable error message, namely:

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. How to "internalize" this definition? Specifically, I want to define a category internal to the above specified type Category. This means a type "internal category" such that the objects are categories, i.e. belong to the above type Category and the arrows are morphisms of the type Category. All of this assuming the relevant pullbacks exist. If this is not clear, please refer to https://ncatlab.org/nlab/show/internal+category My guess is that the best way to pull this off is to define the internal category as a Module inheriting from the above specified type Category. The aim is to ultimately get a hierarchy of structures internal to an "ambient category". So I ultimately want to go beyond just defining a category internal to another category, but other structures as well. Any pointers are appreciated.
coq category-theory
2 Answers

You are not using Agda, so _o_ does not define an infix notation. Also, you cannot have a filed named 1 either. Again, you would have to rely on the notation system.

The following is accepted.

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

Then you can use notations for composition and the unit:

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 *)
user_12759750

Since Théo already provided a great answer to your first question, I'll focus on the second one. In principle, you can define the concept of internal category simply by translating the textbook definition in Coq. We would begin by defining what it means for something to be a pullback:

Record is_pullback {C : Category} 
  {X Y Z : Ob C} (f : Hom C X Z) (g : Hom C Y Z) (P : Ob C) := {
  proj1 : Hom C P X;
  proj2 : Hom C P Y;
  pair : forall W (a : Hom C W X) (b : Hom C W Y),
    f \o a = g \o b -> Hom C W P;
  (* ... plus axioms saying that pairing and projections are
     inverses of each other *)
}.

Then, we would define a category with pullbacks as a category with a choice of pullbacks:

Record PBCategory := {
  Cat :> Category;
  pb : forall X Y Z (f : Hom C X Z) (g : Hom C Y Z), Ob Cat;
  pb_is_pb : forall X Y Z f g, is_pullback f g (pb X Y Z f g);
}.

(The :> is a coercion declaration. It tells Coq that every category with pullbacks can be coerced into a category via Cat.)

Finally, we would write down the definition of an internal category:

Record IntCategory (C : PBCategory) := {
  ArrOb : Ob C;
  ObOb  : Ob C;
  source : Hom C ArrOb ObOb;
  dest : Hom C ArrOb ObOb;
  comp : Hom C (pb _ _ _ _ source dest) ArrOb;
  (* + axioms *)
}.

At this point, however, I believe that we would hit a wall. Writing down the axioms for an internal category in diagrammatic language is too cumbersome. For instance, when phrasing the associativity axiom, we would have to explicitly reason about the isomorphism

(ArrOb x_ObOb ArrOb) x_ObOb ArrOb ~ ArrOb x_ObOb (ArrOb x_ObOb ArrOb)

which is almost always ignored in a textbook presentation. Alas, it is not possible to define an internal category as a particular instance or extension of your Category type.

It might be possible to circumvent this issue by working with indexed categories instead of an internal category, since every internal category gives rise to an indexed category via the Yoneda embedding. That is, we would formalize what it means for something to be a functor of type C^op -> Cat, and then we could define an internal category as being a representable indexed category. This might simplify the definition, but I am not it would be that much easier to work with...

Edit

Here is a potential encoding, though I don't know if this would suit your application or not: https://x80.org/collacoq/urunebifup.coq. The idea is to express composition not as an arrow whose domain is a pullback, but rather as an operation on arrows (more-or-less like what you would get with the Yoneda embedding).

user_16337700
Related