7
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ Just to quickly answer the extra question, a coercion is a device that allows one type to be treated in some way as another type, this gives a good example. I haven't seen that exact syntax before though, so it must be a "special" type of coercion (probably a trivial one, i.e. anything can be an Ob)? $\endgroup$ – Luke Mathieson May 15 '15 at 11:39
  • $\begingroup$ See also coq.inria.fr/refman/Reference-Manual021.html (though that may just muddy the waters) $\endgroup$ – Luke Mathieson May 15 '15 at 11:41
  • $\begingroup$ Just as a side note, you should know that dependent types are very available in coq, and they happen to capture exactly this notion of fiber product! A natural way to write this would be to have mor depend on s and t, e.g. mor: forall s t : ob, Type. $\endgroup$ – cody May 15 '15 at 13:49
  • $\begingroup$ @cody Aren't this the first approach (that I don't want)? The symbol $s$ and $t$ should not stand for objects but for function source and target. Imagine graphs instead of categories: the first approach defines a graph as a set of vertices and for each (sorted) couple a set of edges, while the second approach defines a graph as two sets V and E (V for the vertices, E for all the egdes) with two applications $s,t \colon E \rightrightarrows V$ designating the source and target of each edge. $\endgroup$ – Pece May 15 '15 at 13:56
  • $\begingroup$ Oh right I'm sorry, I missed your first point. It seems though, that you are arguing against the very point you are trying to make: that "internal" definitions are more natural, but as you are observing, it's harder to write them down... $\endgroup$ – cody May 15 '15 at 13:58
4
$\begingroup$

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

$\endgroup$
  • $\begingroup$ You may also need to add a proof irrelevance hypothesis: surely the result of composing f and g should not depend on the proof e that t(f)=s(g)... $\endgroup$ – gallais May 18 '15 at 17:01
  • $\begingroup$ I guess, though that problem shouldn't come up in most contexts where there is only one proof of t(f) = s(g) lying around (e.g. if equality on objects is decidable). $\endgroup$ – cody May 18 '15 at 19:00
0
$\begingroup$

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          
  }.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.