problem-set/algebra/category.theory/p12.desc created : 07/05/89 revised : 07/19/89 Natural Language Description: Lemma 12: cod(dom(x)) = dom(x). Versions : p12.ver1 : uses UR resolution, with axioms from B.Mitchell, "Theory of Categories", Chapter 1. created : from Mitchell, "Theory of Categories", Ch. 1. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : 07/05/89. p12.ver2 : in Quaife's axiom system, this is an axiom. p12.ver3 : Scott axioms, using UR resolution. created : from Scott, "Identity & Existence in Intuitionist Logic" [1978]. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : no proof.