Definition talk:Morphisms-Only Metacategory

I derived this correct set of axioms for MO metacategories today; of course, their justification hinges on the two theorems in the also see section. When these theorems (and the corresponding ones for categories themselves (which I'd rather take implicit)) are up, category theory is finally founded in PredCalc and so endowed with as rigorous a basis as set theory has. This is a major achievement IMHO and I have not seen it done in any of the texts I have encountered on the subject. --Lord_Farin (talk) 19:56, 18 September 2012 (UTC)

Hm, I have to check still that it is implied that $\operatorname{dom} u = u = \operatorname{cod} u$. Give me some time. --Lord_Farin (talk) 19:59, 18 September 2012 (UTC)

Impressive. --prime mover (talk) 21:09, 18 September 2012 (UTC)

Thanks; I had to impose said equalities, though. One of them would suffice but this would make it harder to demonstrate duality theorems later on. --Lord_Farin (talk) 21:50, 18 September 2012 (UTC)

I discovered that I could replace axioms 4 and 5 with the much simpler fourth axiom now in place; all the other properties imposed before now follow easily. Earlier I attempted to follow MacLane but he doesn't use the dom and cod operators; allowing these yielded this relatively simple axiomatisation. --Lord_Farin (talk) 11:06, 21 September 2012 (UTC)