The Coq mailing list

[Victor Porton <porton AT narod.ru>]

First, sorry for not 100% on-topic message. I ask about doing informal mathematics (I am writing a book), but I prefer to do it in the same way as if would be done with Coq, because the Coq way of doing mathematics is the best and I want to follow it (maybe in a future I will even rewrite my book in the format of a proof-assistant).

For every sets A and B ("source" and "destination") there exists a set of "funcoids" (for this topic it is irrelevant to define what are funcoids, it's enough to know that for every sets A and B there exists a set of "funcoids") and having funcoid it is possible to obtain its source and destination.

Further study defines composition of reloids f and g provided that the destination of f is equal to the source of g.

Further I define identity funcoid and show that with these definitions funcoids form a category with aforementioned morphism's source, destination, composition and identity.

Let Hom-sets of a category C are denoted as "Hom C A B". (You knowing Coq better than me may write it in Coq terms.)

My question: Should I usually denote the set of funcoids from a set A to a set B like [funcoids_with_given_source_and_destination A B] (three terms) or like [Hom category_of_funcoids A B] (four terms).

That is, should I be explicit that funcoids form a category every time when I mention a funcoid from A to B?

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