The Coq mailing list

[Pablo Alberto Armelin <pablo AT dcs.qmw.ac.uk>]

Hello

I'm trying to define types for objects and arrows for categories, with 
the property that associativity is built-in to the datatype. What I've 
got at the moment is this:

        Reset Initial.

        Implicit Arguments On.

        Axiom obj:Set.

        Inductive arr: obj-> obj-> Set := 
                  id: (x:obj)(arr x x)
                | ar: (x,y,z:obj)(arr y z)->(arr x z).

Up to here everything seems to be fine. The intuition behind this is
that arrows will be lists of objects, and will have the tipe fixed by
the first and last object in the list. I can do this:

        Variables P,Q:obj.
        Definition idQ := (id Q).
        Definition f := (ar P idQ).

Now I need to define composition. I tried many different ways, and
I'll present the two closest I managed:

        Fixpoint comp [x,y,z:obj;f:(arr x y)]:(arr y z) -> (arr x z):=
                 [g:(arr y z)] Cases f g of
                  (id m) _  => g
                | _  (id m) => f
                | (ar w a b h) j => (ar w (comp h j)) end.

Produces the error:

        Error: In environment
        comp : (x,y,z:obj)(arr x y)->(arr y z)->(arr x z)
        [ ... snip ...]
        j := (ar _ _) : (arr _ _)
        The term j has type (arr _ _) while it is expected to have type
         (arr b ?66)

which I think happens because of the (comp h j) part. But I don't
understand why it doesn't work out the type by itself.

Another try was:

     Definition comp [x,y,z:obj]:= 
        Fix aux {aux/1:(arr x y)->(arr y z)->(arr x z) :=
                [f:(arr x y);g:(arr y z)]
                  Cases f g of
                  (id m) _  => g
                | _  (id m) => f
                | (ar w a b h) j => (ar w (aux h j)) end}.

which produces a similar error but saying:

        The term h0 has type (arr a b) while it is expected to have type
         (arr x y)

I understand this is the case because the type inferred for aux is
actually (arr x y), so it's not polimorphic inside the definition.

Any help/suggestion will be appreciated. Thanks. 

-- 
 __________________________________    w&&&, 
(         Pablo  Armelin           )  o/o %& 
|       
pablo AT dcs.qmw.ac.uk
        |  <_  ?& 
| http://www.dcs.qmw.ac.uk/~pablo/  ;>  7  ;&,
(__________________________________)   `-' `&