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 -&gt; ob -&gt; Type ;
    compose : forall x y z : ob,
                mor x y -&gt; mor y z -&gt; 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 -&gt; ob ;
    t : mor -&gt; ob ;
    compose : mor -&gt; mor -&gt; option mor ;
    i : ob -&gt; mor ;

    adequacy : forall f g : mor, 
                 (exists h, (compose f g) = (some h)) -&gt; (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 :&gt; 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?
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...