The Coq mailing list

[Victor Porton <porton AT narod.ru>]

You may call me a troll again, but it seems for me that I've found a 
deficiency of Coq which should be addressed in future proof assistants. 
(Correct me if there is a way to write this in Coq which I miss.)

Previously I though that this can be expressed with implicit type inference 
in Coq, but my experiments with CoqIDE don't show a way to do this.

Let f in Hom(A;B), g in Hom(B;C) and h in Hom(A;C) for some category.

Let also every Hom(X;Y) is a complete lattice with least element 0.

Consider this formula:

(g o f) /\ h = 0

(where /\ denotes lattice meet).

Intuitively this formula is clear. It expresses an equality for arbitrary 
objects A, B, C.

But when we write it explicitly, we need to add before it:

forall A, B, C, f in Hom(A;B), g in Hom(B;C), h in Hom(A;C).

This is cumbersome as possibly objects for f, g, h can be inferred from the 
formula itself (which intuitively implies that f and g have the same source 
and destination, that the source of h is the same as the source of f etc.) 
and to specify it explicitly is too cumbersome.

At least we would shorten this formula to

forall f, g, h.

But how to denote this? (both in informal mathematics and in formal one)

I've written a book (informal math) where these things are expressed with 
explicit quantification in order not to introduce a non-standard logic which 
allows such expressions without explicit quantifiers. This is bad.

-- 
Victor Porton - http://portonvictor.org