%  problem-set/algebra/category.theory/p2.ver2.clauses
%  created : 07/10/89
%  revised : 07/19/89

% description: 
%
% Theorem 2: If x and y are monomorphisms and xy is well-defined, 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

(cod(a) = dom(b)).
(all x all y all z ((cod(x) != dom(a)) | (star(x,a) != y) | (cod(z) != dom(b)) 
	| (star(z,a) != y) | (x = z))).
(all x all y all z ((cod(x) != dom(a)) | (star(x,b) != y) | (cod(z) != dom(b)) 
	| (star(z,b) != y) | (x = z))).
(cod(h) = dom(star(a,b))).
(cod(g) = dom(star(a,b))).

% denial of Theorem 2

(star(h,star(a,b)) = star(g,star(a,b)) ).
(h != g).