yep I had without detailed study, checked tutorial of Coq to understand about. (i mean just checked the tutorial for 30 min or so) and understood briefly whats this system is about. (had not learnt in detail but just checked some tutorial some features of) 

imho then i decided its not required initially in evaluation of category diagrams (for 0.1 version) not that we cant utilize this tool to check some axiomatics etc, I just think its better if i write the inferencing deductive system of category diagrams (not mine would be better(possibly worser, but imho learning Coq would take alot time. I mean a day or so, it just creates ADD or ADHD. plus I dont want to transcribe deductive functions to a thirdparty tool if possible  since then functions would be dependent to an extra dependency.  Not just the required learning effort is the issue, its that then we have to write some transcriptions etc which effort of seemed kind of as not trivial task. Imho writing own deductive system axiomatics is kind of better approach initially for 0.1 version.  But I also liked Coq library's approach and axiomatics capabilities. But seems as alot effort to integrate to project (for e.g. 0.1 version )

-----------------------------------------------------------------------------------------------------------------------------

yep so there we are, again NLP studies of project.

this time POS tags to diagrams conversion. 

But we need to add temporality to the definition sets. hmm. I think I would for that apply some method I saw. and build some iniital basic axiomatics also based on. 

Currently task is to define the ontology information embedding and also POS tags diagrams  etc.