Один текст всё никак не созревал, но тема формализации ТК была задета в переписке славного ontolog-forum.
И 06.07.14 написал я 2 Pat Phayes:
"Pat,
category theory is just 2-sorts theory like this
Sorts: ob {- objects-}, ar {- arrows-}.
Functions: dom ar:ob, cod ar:ob, one ob:ar, comp ar ar:ar infix "∘".
And axioms:
dom(g∘f)=dom(f). cod(g∘f)=cod(g).
h∘(g∘f)=(h∘g)∘f.
dom(one(b))=b. cod(one(b))=b.
one(b)∘f=f. g∘one(b)=g.
And we should keep in mind that comp is partial with predicate of definability - Defined(x∘y) =def dom(x)=cod(y).
Alex"
Задержку же вызывала необходимость точно формализовать предикат области определённости частичной функции, т.е. понять как их ввести в YAFOLL и как с ними работать. По идее они дают возможность для некоторых(?) термов с их участием вывести и для терма предикат области определённости.
Henson Graves в тот же день ответил очень интересно (см.).
И вот что я ему накатал 07.07.14:
"Henson,
I just have 2-sorted Goldblatt's description in TOPOI. The categorial analysis of logic. 1979.
I like idea that set theory is may be over reduced to one prime predicate symbol ∈. Maybe it's like a Scheffer stroke for propositional calculus:-)
In this case category should replace algebraic system as a model for theory?
When we work with a partial function it is necessary to supply a predicate for an area where it's defined. For ex. for x/y it's y<>0. This is just a pre-condition to calculate term "x/y" value without abort. And if we have an arbitrary term with partial functions we should derive pre-condition for it.
Is this what you keep as "decidable well-formedness conditions for operations"?
Alex"