% problem-set/algebra/category.theory/p4.ver2.clauses % created : 07/10/89 % revised : 07/19/89 % description: % % Theorem 4: If x and y are epimorphisms, then xy is. % [Notice order of composition: xy indicates y(x()) ]. % representation: % % declare_predicate(2,=). % declare_function(2,star). % declare_functions(1,[dom,cod]). % % x = y : usual classical equality % star(x,y) : x composed with y % dom(x) : the object which is the domain of x % cod(x) : the object which is the codomain of x % equality axiom (all x (x = x)). % category theory axioms (all x (cod(dom(x)) = dom(x))). (all x (dom(cod(x)) = cod(x))). (all x (star(dom(x),x) = x)). (all x (star(x,cod(x)) = x)). (all x all y ((cod(x) = dom(y)) -> (dom(star(x,y)) = dom(x)))). (all x all y ((cod(x) = dom(y)) -> (cod(star(x,y)) = cod(y)))). (all x all y all z (((cod(x) = dom(y)) & (cod(y) = dom(z))) -> (star(x,star(y,z)) = star(star(x,y),z)))). % hypothesis of denial (all x all y all z ((cod(a) != dom(x)) | (star(a,x) != y) | (cod(a) != dom(z)) | (star(a,z) != y) | (x = z))). (all x all y all z ((cod(b) != dom(x)) | (star(b,x) != y) | (cod(b) != dom(z)) | (star(b,z) != y) | (x = z))). % denial of Theorem 4 (cod(a) = dom(b)). (cod(star(a,b)) = dom(h)). (cod(star(a,b)) = dom(g)). (star(star(a,b),h) = star(star(a,b),g)). (h != g).