Formalizing basic category theory in Coq

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 le

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

StackExchange Computer Science Q#42589, answer score: 4