Formalizing basic category theory in Coq

Question

I'm a total beginner in Coq and I'm trying to implement some category theory stuff as an exercise.

I surfed a little among git repos of the many avaible such implementations (HoTT, Awodey's Coq companion, etc.) it seems that every single project implements something like that

Record Category : Type :=
  mkCategory{
    ob : Type ;
    mor : ob -> ob -> Type ;
    compose : forall x y z : ob,
                mor x y -> mor y z -> mor x z ;
    identity : forall x, mor x x ;
    (* ... axioms ... *)
  }.

It is kind of natural, considering most definition of categories in modern book. However, I feel that it would be easier to implement it internally (if not mistaken, it was the common definition at Grothendieck's time) :

Definition. A category is the data of

• a set/class $\rm Ob$ of objects,
• a set/class $\rm Mor$ of morphisms,
• functions $s,t \colon {\rm Mor} \to {\rm Ob}$, and $i \colon {\rm Ob} \to {\rm Mor}$ ($s$ stands for source, $t$ for target, and $i$ for identity)
• a function $\circ \colon {\rm Mor} \times_{s,t} {\rm Mor} \to {\rm Mor}$ whose domain is the fiber product of $${\rm Mor} \stackrel s \to {\rm Ob} \stackrel t \leftarrow {\rm Mor}$$

satisfying some axioms...

The advantage of such a definition is that it generalizes directly by replacing "set/class" by "objects of some category" and "functions" by "morphisms of this category", leading to the concept of internal category. (Then you can talk of topological/differential categories, or categories inside a topos, etc.)

My problem is to formalize the fiber product in Coq. My first attemp would be to do something like

Record Category : Type :=
  mkCategory{
    ob : Type ;
    mor : Type ;
    s : mor -> ob ;
    t : mor -> ob ;
    compose : mor -> mor -> option mor ;
    i : ob -> mor ;

    adequacy : forall f g : mor, 
                 (exists h, (compose f g) = (some h)) -> (t f = s g) ;
    (* ... axioms ... *)
  }.

But I feel that could lead to some curbersome later code. For example, chained compositions would be difficult to read.

Is there a project with an implementation based on the internal definition? Is there a quick way to define the fiber product I need in Coq?

Edit. By the way, I see a lot of

Ob :> Type

rather of

Ob : Type

What is the meaning of the extra ">"? From the doc, it seems it is some kind of coercion. What exactly does this mean?

Answer 1

A natural way to write down what you want is to restrict the type of composition to only the "composable" morphisms:

$$ \mathrm{compose}:\forall f\ g: \mathrm{mor}, t(f) = s(g)\rightarrow \mathrm{mor}$$

adding, of course, the conditions: $$ s(\mathrm{compose}\ f\ g\ e)=s(f)$$ $$ t(\mathrm{compose}\ f\ g\ e)=t(g)$$

This works, as it now only allows composing functions that are provably composable. This roughly corresponds to the fibered product in category theory you were mentioning.

However is somewhat awkward as it adds proof obligations to every application of compose, which can quickly become unmanageable (even expressing associativity is hard!). Also it somewhat precludes adding the notation $\circ=\mathrm{compose}$, since compose takes 3 arguments.

This is a somewhat common problem in type theory, which results from the fundamental tension of having partial functions in a total language.

Another, less elegant solution, is to define composition to be everywhere defined: $$ \mathrm{compose} :\mathrm{mor}\rightarrow\mathrm{mor}\rightarrow\mathrm{mor}$$ and guard every theorem involving composition with well-definedness conditions:

$$\mathrm{assoc}:\forall f g h:\mathrm{mor}, t(f)=s(g)\wedge t(g)=s(h)\Rightarrow\\ \mathrm{compose}\ f\ (\mathrm{compose}\ g\ h) = \mathrm{compose}\ (\mathrm{compose}\ f\ g)\ h $$ This essentially means:

compose is defined everywhere, but the definition is only meaningful if applied to composable morphisms.

This approach also has drawbacks, mostly the gargantuan quantity of proof obligations that follow every application of the basic axioms.

I'm afraid you have to choose your poison in this case, or come up with a clever way to do better...

Answer 2

After some struggling, I think the best way to do what I want is to actually encode the fiber product of type through its universal property.

It goes along that kind of lines:

Class FiberProduct (A B C : Type) (f : A -> C) (g : B -> C) : Type :=
  {
    FiberProductCarrier : Type ;
    FiberProductProj_1 : FiberProductCarrier -> A ;
    FiberProductProj_2 : FiberProductCarrier -> B ;
    FiberProductCommutativity :
      forall x : FiberProductCarrier,
        f (FiberProductProj_1 x) = g (FiberProductProj_2 x) ;
    FiberProductUniversalExistence :
      forall X : Type, forall (p_1 : X -> A) (p_2 : X -> B),
        (forall x : X, f (p_1 x) = g (p_2 x)) ->
        (exists h : X -> FiberProductCarrier,
           (forall x : X, FiberProductProj_1 (h x) = p_1 x
                          /\ FiberProductProj_2 (h x) = p_2 x)) ;
    FiberProductUniversalUniqueness :
      forall X : Type, forall (p_1 : X -> A) (p_2 : X -> B),
        (forall x : X, f (p_1 x) = g (p_2 x)) ->
        (forall k l : X -> FiberProductCarrier,
           (forall x : X, FiberProductProj_1 (k x) = p_1 x
                          /\ FiberProductProj_2 (k x) = p_2 x
                          /\ FiberProductProj_1 (l x) = p_1 x
                          /\ FiberProductProj_2 (l x) = p_2 x)
           -> k = l)
  }.

Then the internal version of the notion of category is given by:

Class InternalCategory : Type :=
  {
    ob : Type ;
    mor : Type ;
    s : mor -> ob ;
    t : mor -> ob ;
    i : ob -> mor ;
    comp_domain : FiberProduct mor mor ob s t ;
    comp : FiberProductCarrier  -> mor  ;
    (* axioms *)
    asso :
      forall fg_h f_gh : FiberProductCarrier,
        (exists fg gh : FiberProductCarrier,
           FiberProductProj_1 fg_h = comp fg /\
           FiberProductProj_2 f_gh = comp gh /\
           FiberProductProj_1 fg = FiberProductProj_1 f_gh /\
           FiberProductProj_2 fg = FiberProductProj_1 gh /\
           FiberProductProj_2 gh = FiberProductProj_2 fg_h) ->
        (comp fg_h = comp f_gh) ;
    id_right :
      forall fid : FiberProductCarrier,
      forall f : mor,
        (FiberProductProj_1 fid = f) ->
        (exists x : ob, FiberProductProj_2 fid = i x) ->
        (comp fid = f) ;
    id_left :
      forall idf : FiberProductCarrier,
      forall f : mor,
        (FiberProductProj_2 idf = f) ->
        (exists x : ob, FiberProductProj_1 idf = i x) ->
        (comp idf = f) ;
    id_s :
      forall x, s (i x) = x ;
    id_t :
      forall x, t (i x) = x          
  }.