\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{CAT001-0.ax} Category theory axioms






$\mbox{defined}(x,y) \ \Rightarrow \ x\cdot y{=}x\circ y\qquad\mbox{cnf}(\mbox{closure\_of\_composition},\mbox{axiom})$

$x\cdot y{=}z \ \Rightarrow \ \mbox{defined}(x,y)\qquad\mbox{cnf}(\mbox{associative\_property}_1,\mbox{axiom})$

$( x\cdot y{=}\mbox{xy}\mbox{ and }\mbox{defined}(\mbox{xy},z) ) \ \Rightarrow \ \mbox{defined}(y,z)\qquad\mbox{cnf}(\mbox{associative\_property}_2,\mbox{axiom})$

$( x\cdot y{=}\mbox{xy}\mbox{ and }y\cdot z{=}\mbox{yz}\mbox{ and }\mbox{defined}(\mbox{xy},z) ) \ \Rightarrow \ \mbox{defined}(x,\mbox{yz})\qquad\mbox{cnf}(\mbox{category\_theory\_axiom}_1,\mbox{axiom})$

$( x\cdot y{=}\mbox{xy}\mbox{ and }\mbox{xy}\cdot z{=}\mbox{xyz}\mbox{ and }y\cdot z{=}\mbox{yz} ) \ \Rightarrow \ x\cdot \mbox{yz}{=}\mbox{xyz}\qquad\mbox{cnf}(\mbox{category\_theory\_axiom}_2,\mbox{axiom})$

$( y\cdot z{=}\mbox{yz}\mbox{ and }\mbox{defined}(x,\mbox{yz}) ) \ \Rightarrow \ \mbox{defined}(x,y)\qquad\mbox{cnf}(\mbox{category\_theory\_axiom}_3,\mbox{axiom})$

$( y\cdot z{=}\mbox{yz}\mbox{ and }x\cdot y{=}\mbox{xy}\mbox{ and }\mbox{defined}(x,\mbox{yz}) ) \ \Rightarrow \ \mbox{defined}(\mbox{xy},z)\qquad\mbox{cnf}(\mbox{category\_theory\_axiom}_4,\mbox{axiom})$

$( y\cdot z{=}\mbox{yz}\mbox{ and }x\cdot \mbox{yz}{=}\mbox{xyz}\mbox{ and }x\cdot y{=}\mbox{xy} ) \ \Rightarrow \ \mbox{xy}\cdot z{=}\mbox{xyz}\qquad\mbox{cnf}(\mbox{category\_theory\_axiom}_5,\mbox{axiom})$

$( \mbox{defined}(x,y)\mbox{ and }\mbox{defined}(y,z)\mbox{ and }\mbox{identity\_map}(y) ) \ \Rightarrow \ \mbox{defined}(x,z)\qquad\mbox{cnf}(\mbox{category\_theory\_axiom}_6,\mbox{axiom})$

$\mbox{identity\_map}(1_{\text{dom}(x)})\qquad\mbox{cnf}(\mbox{domain\_is\_an\_identity\_map},\mbox{axiom})$

$\mbox{identity\_map}(1_{\text{cod}(x)})\qquad\mbox{cnf}(\mbox{codomain\_is\_an\_identity\_map},\mbox{axiom})$

$\mbox{defined}(x,1_{\text{dom}(x)})\qquad\mbox{cnf}(\mbox{mapping\_from\_x\_to\_its\_domain},\mbox{axiom})$

$\mbox{defined}(1_{\text{cod}(x)},x)\qquad\mbox{cnf}(\mbox{mapping\_from\_codomain\_of\_x\_to\_x},\mbox{axiom})$

$x\cdot 1_{\text{dom}(x)}{=}x\qquad\mbox{cnf}(\mbox{product\_on\_domain},\mbox{axiom})$

$1_{\text{cod}(x)}\cdot x{=}x\qquad\mbox{cnf}(\mbox{product\_on\_codomain},\mbox{axiom})$

$( \mbox{defined}(x,y)\mbox{ and }\mbox{identity\_map}(x) ) \ \Rightarrow \ x\cdot y{=}y\qquad\mbox{cnf}(\mbox{identity}_1,\mbox{axiom})$

$( \mbox{defined}(x,y)\mbox{ and }\mbox{identity\_map}(y) ) \ \Rightarrow \ x\cdot y{=}x\qquad\mbox{cnf}(\mbox{identity}_2,\mbox{axiom})$

$( x\cdot y{=}z\mbox{ and }x\cdot y{=}w ) \ \Rightarrow \ z = w\qquad\mbox{cnf}(\mbox{composition\_is\_well\_defined},\mbox{axiom})$

\medskip\textbf{CAT002-0.ax} Category theory (equality) axioms






$1_{\text{cod}(1_{\text{dom}(x)})} = 1_{\text{dom}(x)}\qquad\mbox{cnf}(\mbox{codomain\_of\_domain\_is\_domain},\mbox{axiom})$

$1_{\text{dom}(1_{\text{cod}(x)})} = 1_{\text{cod}(x)}\qquad\mbox{cnf}(\mbox{domain\_of\_codomain\_is\_codomain},\mbox{axiom})$

$1_{\text{dom}(x)}\circ x = x\qquad\mbox{cnf}(\mbox{domain\_composition},\mbox{axiom})$

$x\circ 1_{\text{cod}(x)} = x\qquad\mbox{cnf}(\mbox{codomain\_composition},\mbox{axiom})$

$1_{\text{cod}(x)} = 1_{\text{dom}(y)} \ \Rightarrow \ 1_{\text{dom}(x\circ y)} = 1_{\text{dom}(x)}\qquad\mbox{cnf}(\mbox{codomain\_domain}_1,\mbox{axiom})$

$1_{\text{cod}(x)} = 1_{\text{dom}(y)} \ \Rightarrow \ 1_{\text{cod}(x\circ y)} = 1_{\text{cod}(y)}\qquad\mbox{cnf}(\mbox{codomain\_domain}_2,\mbox{axiom})$

$( 1_{\text{cod}(x)} = 1_{\text{dom}(y)}\mbox{ and }1_{\text{cod}(y)} = 1_{\text{dom}(z)} ) \ \Rightarrow \ x\circ ( y\circ z ) = ( x\circ y )\circ z\qquad\mbox{cnf}(\mbox{star\_property},\mbox{axiom})$

\medskip\textbf{CAT004-0.ax} Category theory axioms






$\mbox{equivalent}(x,y) \ \Rightarrow \ \mbox{there\_exists}(x)\qquad\mbox{cnf}(\mbox{equivalence\_implies\_existence}_1,\mbox{axiom})$

$\mbox{equivalent}(x,y) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{equivalence\_implies\_existence}_2,\mbox{axiom})$

$( \mbox{there\_exists}(x)\mbox{ and }x = y ) \ \Rightarrow \ \mbox{equivalent}(x,y)\qquad\mbox{cnf}(\mbox{existence\_and\_equality\_implies\_equivalence}_1,\mbox{axiom})$

$\mbox{there\_exists}(1_{\text{dom}(x)}) \ \Rightarrow \ \mbox{there\_exists}(x)\qquad\mbox{cnf}(\mbox{domain\_has\_elements},\mbox{axiom})$

$\mbox{there\_exists}(1_{\text{cod}(x)}) \ \Rightarrow \ \mbox{there\_exists}(x)\qquad\mbox{cnf}(\mbox{codomain\_has\_elements},\mbox{axiom})$

$\mbox{there\_exists}(x\circ y) \ \Rightarrow \ \mbox{there\_exists}(1_{\text{dom}(x)})\qquad\mbox{cnf}(\mbox{composition\_implies\_domain},\mbox{axiom})$

$\mbox{there\_exists}(x\circ y) \ \Rightarrow \ 1_{\text{dom}(x)} = 1_{\text{cod}(y)}\qquad\mbox{cnf}(\mbox{domain\_codomain\_composition}_1,\mbox{axiom})$

$( \mbox{there\_exists}(1_{\text{dom}(x)})\mbox{ and }1_{\text{dom}(x)} = 1_{\text{cod}(y)} ) \ \Rightarrow \ \mbox{there\_exists}(x\circ y)\qquad\mbox{cnf}(\mbox{domain\_codomain\_composition}_2,\mbox{axiom})$

$x\circ ( y\circ z ) = ( x\circ y )\circ z\qquad\mbox{cnf}(\mbox{associativity\_of\_compose},\mbox{axiom})$

$x\circ 1_{\text{dom}(x)} = x\qquad\mbox{cnf}(\mbox{compose\_domain},\mbox{axiom})$

$1_{\text{cod}(x)}\circ x = x\qquad\mbox{cnf}(\mbox{compose\_codomain},\mbox{axiom})$

\medskip\textbf{CAT003-0.ax} Category theory axioms






$\mbox{equivalent}(x,y) \ \Rightarrow \ \mbox{there\_exists}(x)\qquad\mbox{cnf}(\mbox{equivalence\_implies\_existence}_1,\mbox{axiom})$

$\mbox{equivalent}(x,y) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{equivalence\_implies\_existence}_2,\mbox{axiom})$

$( \mbox{there\_exists}(x)\mbox{ and }x = y ) \ \Rightarrow \ \mbox{equivalent}(x,y)\qquad\mbox{cnf}(\mbox{existence\_and\_equality\_implies\_equivalence}_1,\mbox{axiom})$

$\mbox{there\_exists}(1_{\text{dom}(x)}) \ \Rightarrow \ \mbox{there\_exists}(x)\qquad\mbox{cnf}(\mbox{domain\_has\_elements},\mbox{axiom})$

$\mbox{there\_exists}(1_{\text{cod}(x)}) \ \Rightarrow \ \mbox{there\_exists}(x)\qquad\mbox{cnf}(\mbox{codomain\_has\_elements},\mbox{axiom})$

$\mbox{there\_exists}(x\circ y) \ \Rightarrow \ \mbox{there\_exists}(1_{\text{dom}(x)})\qquad\mbox{cnf}(\mbox{composition\_implies\_domain},\mbox{axiom})$

$\mbox{there\_exists}(x\circ y) \ \Rightarrow \ 1_{\text{dom}(x)} = 1_{\text{cod}(y)}\qquad\mbox{cnf}(\mbox{domain\_codomain\_composition}_1,\mbox{axiom})$

$( \mbox{there\_exists}(1_{\text{dom}(x)})\mbox{ and }1_{\text{dom}(x)} = 1_{\text{cod}(y)} ) \ \Rightarrow \ \mbox{there\_exists}(x\circ y)\qquad\mbox{cnf}(\mbox{domain\_codomain\_composition}_2,\mbox{axiom})$

$x\circ ( y\circ z ) = ( x\circ y )\circ z\qquad\mbox{cnf}(\mbox{associativity\_of\_compose},\mbox{axiom})$

$x\circ 1_{\text{dom}(x)} = x\qquad\mbox{cnf}(\mbox{compose\_domain},\mbox{axiom})$

$1_{\text{cod}(x)}\circ x = x\qquad\mbox{cnf}(\mbox{compose\_codomain},\mbox{axiom})$

$\mbox{equivalent}(x,y) \ \Rightarrow \ \mbox{there\_exists}(y)\qquad\mbox{cnf}(\mbox{equivalence\_implies\_existence}_3,\mbox{axiom})$

$( \mbox{there\_exists}(x)\mbox{ and }\mbox{there\_exists}(y)\mbox{ and }x = y ) \ \Rightarrow \ \mbox{equivalent}(x,y)\qquad\mbox{cnf}(\mbox{existence\_and\_equality\_implies\_equivalence}_2,\mbox{axiom})$

$\mbox{there\_exists}(x\circ y) \ \Rightarrow \ \mbox{there\_exists}(1_{\text{cod}(x)})\qquad\mbox{cnf}(\mbox{composition\_implies\_codomain},\mbox{axiom})$

$\mbox{there\_exists}(f_1(x,y))\mbox{ or }x = y\qquad\mbox{cnf}(\mbox{indiscernibles}_1,\mbox{axiom})$

$x = f_1(x,y)\mbox{ or }y = f_1(x,y)\mbox{ or }x = y\qquad\mbox{cnf}(\mbox{indiscernibles}_2,\mbox{axiom})$

$( x = f_1(x,y)\mbox{ and }y = f_1(x,y) ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{indiscernibles}_3,\mbox{axiom})$

\medskip\textbf{CAT019-5.p} Axiom of Indiscernibles

[all z (x=z $<$$\to$ y=z)] $\to$ x=y.




$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(c)\qquad\mbox{cnf}(\mbox{assume\_c\_exists},\mbox{hypothesis})$

$( \mbox{there\_exists}(z)\mbox{ and }a = z ) \ \Rightarrow \ b = z\qquad\mbox{cnf}(\mbox{equality\_of\_a\_and\_b}_1,\mbox{hypothesis})$

$( \mbox{there\_exists}(z)\mbox{ and }b = z ) \ \Rightarrow \ a = z\qquad\mbox{cnf}(\mbox{equality\_of\_a\_and\_b}_2,\mbox{hypothesis})$

$a\ne b\qquad\mbox{cnf}(\mbox{prove\_a\_equals\_b},\mbox{negated\_conjecture})$

\medskip\textbf{CAT012-4.p} codomain(domain(x)) = domain(x)






$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(1_{\text{dom}(a)})\qquad\mbox{cnf}(\mbox{assume\_domain\_exists},\mbox{hypothesis})$

$1_{\text{cod}(1_{\text{dom}(a)})}\ne 1_{\text{dom}(a)}\qquad\mbox{cnf}(\mbox{prove\_codomain\_of\_domain\_is\_domain},\mbox{negated\_conjecture})$

\medskip\textbf{CAT013-4.p} domain(codomain(x)) = codomain(x)






$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(1_{\text{cod}(a)})\qquad\mbox{cnf}(\mbox{assume\_codomain\_exists},\mbox{hypothesis})$

$1_{\text{dom}(1_{\text{cod}(a)})}\ne 1_{\text{cod}(a)}\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_codomain\_is\_codomain},\mbox{negated\_conjecture})$

\medskip\textbf{CAT019-1.p} Axiom of Indiscernibles

[all z (x=z $<$$\to$ y=z)] $\to$ x=y.




$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$c_2 = z \ \Rightarrow \ c_1 = z\qquad\mbox{cnf}(\mbox{equality\_to\_c1\_and\_c2}_1,\mbox{hypothesis})$

$c_1 = z \ \Rightarrow \ c_2 = z\qquad\mbox{cnf}(\mbox{equality\_to\_c1\_and\_c2}_2,\mbox{hypothesis})$

$c_2\ne c_1\qquad\mbox{cnf}(\mbox{prove\_c1\_equals\_c}_2,\mbox{negated\_conjecture})$

\medskip\textbf{CAT002-2.p} X and Y monomorphisms, XY well-defined =$>$ XY monomorphism

If x and y are monomorphisms and xy is well-defined then
 xy is a monomorphism.




$\mbox{include}(\mbox{'Axioms/CAT002-0.ax'})$

$1_{\text{cod}(a)} = 1_{\text{dom}(b)}\qquad\mbox{cnf}(\mbox{codomain\_of\_a\_equals\_domain\_of\_b},\mbox{hypothesis})$

$( 1_{\text{cod}(x)} = 1_{\text{dom}(a)}\mbox{ and }x\circ a = y\mbox{ and }1_{\text{cod}(z)} = 1_{\text{dom}(b)}\mbox{ and }z\circ a = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{monomorphism}_1,\mbox{hypothesis})$

$( 1_{\text{cod}(x)} = 1_{\text{dom}(a)}\mbox{ and }x\circ b = y\mbox{ and }1_{\text{cod}(z)} = 1_{\text{dom}(b)}\mbox{ and }z\circ b = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{monomorphism}_2,\mbox{hypothesis})$

$1_{\text{cod}(h)} = 1_{\text{dom}(a\circ b)}\qquad\mbox{cnf}(\mbox{codomain\_of\_h\_equals\_domain\_of\_ab},\mbox{hypothesis})$

$1_{\text{cod}(g)} = 1_{\text{dom}(a\circ b)}\qquad\mbox{cnf}(\mbox{codomain\_of\_g\_equals\_domain\_of\_ab},\mbox{hypothesis})$

$h\circ ( a\circ b ) = g\circ ( a\circ b )\qquad\mbox{cnf}(\mbox{h\_ab\_equals\_g\_ab},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT013-1.p} domain(codomain(x)) = codomain(x)






$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$1_{\text{dom}(1_{\text{cod}(a)})}\ne 1_{\text{cod}(a)}\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_codomain\_is\_codomain},\mbox{negated\_conjecture})$

\medskip\textbf{CAT006-1.p} Codomain is the unique left identity

codomain(x) is the unique identity j such that jx is defined.




$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$\mbox{defined}(h,a)\qquad\mbox{cnf}(\mbox{ha\_defined},\mbox{hypothesis})$

$\mbox{identity\_map}(h)\qquad\mbox{cnf}(\mbox{h\_is\_the\_identity\_map},\mbox{hypothesis})$

$1_{\text{cod}(a)}\ne h\qquad\mbox{cnf}(\mbox{prove\_codomain\_of\_a\_is\_h},\mbox{negated\_conjecture})$

\medskip\textbf{CAT007-1.p} If domain(x) = codomain(y) then xy is defined






$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$1_{\text{dom}(a)} = 1_{\text{cod}(b)}\qquad\mbox{cnf}(\mbox{domain\_of\_a\_equals\_codomain\_of\_b},\mbox{hypothesis})$

$\neg\,\mbox{defined}(a,b)\qquad\mbox{cnf}(\mbox{prove\_ab\_is\_defined},\mbox{negated\_conjecture})$

\medskip\textbf{CAT005-4.p} Domain is the unique right identity

domain(x) is the unique identity i such that xi is defined.




$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(a\circ d)\qquad\mbox{cnf}(\mbox{ad\_exists},\mbox{hypothesis})$

$\mbox{there\_exists}(x\circ d) \ \Rightarrow \ x\circ d = x\qquad\mbox{cnf}(\mbox{xd\_equals\_x},\mbox{hypothesis})$

$\mbox{there\_exists}(d\circ y) \ \Rightarrow \ d\circ y = y\qquad\mbox{cnf}(\mbox{dy\_equals\_y},\mbox{hypothesis})$

$1_{\text{dom}(a)}\ne d\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_a\_is\_d},\mbox{negated\_conjecture})$

\medskip\textbf{CAT014-4.p} codomain(codomain(x)) = codomain(x)






$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(1_{\text{cod}(a)})\qquad\mbox{cnf}(\mbox{assume\_codomain\_exists},\mbox{hypothesis})$

$1_{\text{cod}(1_{\text{cod}(a)})}\ne 1_{\text{cod}(a)}\qquad\mbox{cnf}(\mbox{prove\_codomain\_is\_idempotent},\mbox{negated\_conjecture})$

\medskip\textbf{CAT009-1.p} If xy is defined, then domain(xy) = domain(y)






$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$\mbox{defined}(b,a)\qquad\mbox{cnf}(\mbox{ba\_defined},\mbox{hypothesis})$

$1_{\text{dom}(b\circ a)}\ne 1_{\text{dom}(a)}\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_ba\_equals\_domain\_of\_a},\mbox{negated\_conjecture})$

\medskip\textbf{CAT014-3.p} codomain(codomain(x)) = codomain(x)






$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(1_{\text{cod}(a)})\qquad\mbox{cnf}(\mbox{assume\_codomain\_exists},\mbox{hypothesis})$

$1_{\text{cod}(1_{\text{cod}(a)})}\ne 1_{\text{cod}(a)}\qquad\mbox{cnf}(\mbox{prove\_codomain\_is\_idempotent},\mbox{negated\_conjecture})$

\medskip\textbf{CAT015-3.p} Prove something exists

Can anything be proven to exist, directly from the axioms?
 Using all the kinds of resolution steps possible, no.




$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$x = y\mbox{ or }\mbox{there\_exists}(x)\mbox{ or }\mbox{there\_exists}(y)\qquad\mbox{cnf}(\mbox{equal\_things\_exist},\mbox{axiom})$

$\neg\,\mbox{there\_exists}(x)\qquad\mbox{cnf}(\mbox{prove\_something\_exists},\mbox{negated\_conjecture})$

\medskip\textbf{CAT002-1.p} X and Y monomorphisms, XY well-defined =$>$ XY monomorphism

If x and y are monomorphisms and xy is well-defined then
 xy is a monomorphism.




$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$( a\cdot x{=}w\mbox{ and }a\cdot y{=}w ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{cancellation\_for\_product}_1,\mbox{hypothesis})$

$( b\cdot x{=}w\mbox{ and }b\cdot y{=}w ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{cancellation\_for\_product}_2,\mbox{hypothesis})$

$a\cdot b{=}c\qquad\mbox{cnf}(\mbox{ab\_equals\_c},\mbox{hypothesis})$

$c\cdot h{=}d\qquad\mbox{cnf}(\mbox{ch\_equals\_d},\mbox{hypothesis})$

$c\cdot g{=}d\qquad\mbox{cnf}(\mbox{cg\_equals\_d},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT010-1.p} If xy is defined, then codomain(xy) = codomain(x)






$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$\mbox{defined}(b,a)\qquad\mbox{cnf}(\mbox{ba\_defined},\mbox{hypothesis})$

$1_{\text{cod}(b\circ a)}\ne 1_{\text{cod}(b)}\qquad\mbox{cnf}(\mbox{prove\_codomain\_of\_ba\_equals\_codomain\_of\_b},\mbox{negated\_conjecture})$

\medskip\textbf{CAT003-4.p} XY epimorphism =$>$ X epimorphism

If xy is an epimorphism, then x is an epimorphism.




$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$( x\circ ( a\circ b ) = y\mbox{ and }z\circ ( a\circ b ) = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{epimorphism},\mbox{hypothesis})$

$\mbox{there\_exists}(h)\qquad\mbox{cnf}(\mbox{assume\_h\_exists},\mbox{hypothesis})$

$h\circ a = g\circ a\qquad\mbox{cnf}(\mbox{ha\_equals\_ga},\mbox{hypothesis})$

$g\ne h\qquad\mbox{cnf}(\mbox{prove\_g\_equals\_h},\mbox{negated\_conjecture})$

\medskip\textbf{CAT018-4.p} If xy and yz exist, then so does x(yz)






$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$\mbox{there\_exists}(b\circ c)\qquad\mbox{cnf}(\mbox{assume\_bc\_exists},\mbox{hypothesis})$

$\neg\,\mbox{there\_exists}(a\circ ( b\circ c ))\qquad\mbox{cnf}(\mbox{prove\_a\_bc\_exists},\mbox{negated\_conjecture})$

\medskip\textbf{CAT011-1.p} domain(domain(x)) = domain(x)






$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$1_{\text{dom}(1_{\text{dom}(a)})}\ne 1_{\text{dom}(a)}\qquad\mbox{cnf}(\mbox{prove\_domain\_is\_idempotent},\mbox{negated\_conjecture})$

\medskip\textbf{CAT005-3.p} Domain is the unique right identity

domain(x) is the unique identity i such that xi is defined.




$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(a\circ d)\qquad\mbox{cnf}(\mbox{ad\_exists},\mbox{hypothesis})$

$\mbox{there\_exists}(x\circ d) \ \Rightarrow \ x\circ d = x\qquad\mbox{cnf}(\mbox{xd\_equals\_x},\mbox{hypothesis})$

$\mbox{there\_exists}(d\circ y) \ \Rightarrow \ d\circ y = y\qquad\mbox{cnf}(\mbox{dy\_equals\_y},\mbox{hypothesis})$

$1_{\text{dom}(a)}\ne d\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_a\_is\_d},\mbox{negated\_conjecture})$

\medskip\textbf{CAT018-3.p} If xy and yz exist, then so does x(yz)






$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$\mbox{there\_exists}(b\circ c)\qquad\mbox{cnf}(\mbox{assume\_bc\_exists},\mbox{hypothesis})$

$\neg\,\mbox{there\_exists}(a\circ ( b\circ c ))\qquad\mbox{cnf}(\mbox{prove\_a\_bc\_exists},\mbox{negated\_conjecture})$

\medskip\textbf{CAT020-4.p} Category theory axioms






$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

\medskip\textbf{CAT004-1.p} X and Y epimorphisms, XY well-defined =$>$ XY epimorphism

If x and y are epimorphisms and xy is well-defined, then
 xy is an epimorphism.




$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$( x\cdot a{=}w\mbox{ and }y\cdot a{=}w ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{cancellation\_for\_product}_1,\mbox{hypothesis})$

$( x\cdot b{=}w\mbox{ and }y\cdot b{=}w ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{cancellation\_for\_product}_2,\mbox{hypothesis})$

$a\cdot b{=}c\qquad\mbox{cnf}(\mbox{ab\_equals\_c},\mbox{hypothesis})$

$h\cdot c{=}d\qquad\mbox{cnf}(\mbox{hc\_equals\_d},\mbox{hypothesis})$

$g\cdot c{=}d\qquad\mbox{cnf}(\mbox{gc\_equals\_d},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT038$\wedge$1.p} Swapping function

The proposition can be interpreted in concrete categories and
 asserts the existence of a certain arrow.




$a{:}\;\mbox{\$i}\qquad\mbox{thf}(a,\mbox{type})$

$b{:}\;\mbox{\$i}\qquad\mbox{thf}(b,\mbox{type})$

$\exists f{:}\;\mbox{\$i}\to \mbox{\$i}{:}\;( ( f@ a ) = b\mbox{ and }( f@ b ) = a )\qquad\mbox{thf}(\mbox{swap},\mbox{conjecture})$

\medskip\textbf{CAT015-4.p} Prove something exists

Can anything be proven to exist, directly from the axioms?
 Using all the kinds of resolution steps possible, no.




$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$x = y\mbox{ or }\mbox{there\_exists}(x)\mbox{ or }\mbox{there\_exists}(y)\qquad\mbox{cnf}(\mbox{equal\_things\_exist},\mbox{axiom})$

$\neg\,\mbox{there\_exists}(x)\qquad\mbox{cnf}(\mbox{prove\_something\_exists},\mbox{negated\_conjecture})$

\medskip\textbf{CAT002-4.p} X and Y monomorphisms, XY well-defined =$>$ XY monomorphism

If x and y are monomorphisms and xy is well-defined then
 xy is a monomorphism.




$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$( a\circ x = y\mbox{ and }a\circ z = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{cancellation\_for\_compose}_1,\mbox{hypothesis})$

$( b\circ x = y\mbox{ and }b\circ z = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{cancellation\_for\_compose}_2,\mbox{hypothesis})$

$\mbox{there\_exists}(h)\qquad\mbox{cnf}(\mbox{assume\_h\_exists},\mbox{hypothesis})$

$( a\circ b )\circ h = ( a\circ b )\circ g\qquad\mbox{cnf}(\mbox{ab\_h\_equals\_ab\_g},\mbox{hypothesis})$

$g\ne h\qquad\mbox{cnf}(\mbox{prove\_g\_equals\_h},\mbox{negated\_conjecture})$

\medskip\textbf{CAT003-1.p} XY epimorphism =$>$ X epimorphism

If xy is an epimorphism, then x is an epimorphism.




$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$a\cdot b{=}c\qquad\mbox{cnf}(\mbox{ab\_equals\_c},\mbox{hypothesis})$

$( x\cdot c{=}w\mbox{ and }y\cdot c{=}w ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{cancellation\_for\_product},\mbox{hypothesis})$

$h\cdot a{=}d\qquad\mbox{cnf}(\mbox{ha\_equals\_d},\mbox{hypothesis})$

$g\cdot a{=}d\qquad\mbox{cnf}(\mbox{ga\_equals\_d},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT011-2.p} domain(domain(x)) = domain(x)






$\mbox{include}(\mbox{'Axioms/CAT002-0.ax'})$

$1_{\text{dom}(1_{\text{dom}(a)})}\ne 1_{\text{dom}(a)}\qquad\mbox{cnf}(\mbox{prove\_domain\_is\_idempotent},\mbox{negated\_conjecture})$

\medskip\textbf{CAT020-3.p} Category theory axioms






$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

\medskip\textbf{CAT006-4.p} Codomain is the unique left identity

codomain(x) is the unique identity j such that jx is defined.




$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(d\circ a)\qquad\mbox{cnf}(\mbox{da\_exists},\mbox{hypothesis})$

$\mbox{there\_exists}(x\circ d) \ \Rightarrow \ x\circ d = x\qquad\mbox{cnf}(\mbox{xd\_equals\_x},\mbox{hypothesis})$

$\mbox{there\_exists}(d\circ x) \ \Rightarrow \ d\circ x = x\qquad\mbox{cnf}(\mbox{dx\_equals\_x},\mbox{hypothesis})$

$1_{\text{cod}(a)}\ne d\qquad\mbox{cnf}(\mbox{prove\_codomain\_of\_a\_is\_d},\mbox{negated\_conjecture})$

\medskip\textbf{CAT012-3.p} codomain(domain(x)) = domain(x)






$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(1_{\text{dom}(a)})\qquad\mbox{cnf}(\mbox{assume\_domain\_exists},\mbox{hypothesis})$

$1_{\text{cod}(1_{\text{dom}(a)})}\ne 1_{\text{dom}(a)}\qquad\mbox{cnf}(\mbox{prove\_codomain\_of\_domain\_is\_domain},\mbox{negated\_conjecture})$

\medskip\textbf{CAT003-3.p} XY epimorphism =$>$ X epimorphism

If xy is an epimorphism, then x is an epimorphism.




$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$( x\circ ( a\circ b ) = y\mbox{ and }z\circ ( a\circ b ) = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{epimorphism},\mbox{hypothesis})$

$\mbox{there\_exists}(h)\qquad\mbox{cnf}(\mbox{assume\_h\_exists},\mbox{hypothesis})$

$h\circ a = g\circ a\qquad\mbox{cnf}(\mbox{ha\_equals\_ga},\mbox{hypothesis})$

$g\ne h\qquad\mbox{cnf}(\mbox{prove\_g\_equals\_h},\mbox{negated\_conjecture})$

\medskip\textbf{CAT004-3.p} X and Y epimorphisms, XY well-defined =$>$ XY epimorphism

If x and y are epimorphisms and xy is well-defined, then
 xy is an epimorphism.




$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$( x\circ a = y\mbox{ and }z\circ a = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{cancellation\_for\_product}_1,\mbox{hypothesis})$

$( x\circ b = y\mbox{ and }z\circ b = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{cancellation\_for\_product}_2,\mbox{hypothesis})$

$\mbox{there\_exists}(h)\qquad\mbox{cnf}(\mbox{assume\_h\_exists},\mbox{hypothesis})$

$h\circ ( a\circ b ) = g\circ ( a\circ b )\qquad\mbox{cnf}(\mbox{h\_ab\_equals\_g\_ab},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT001-4.p} XY monomorphism =$>$ Y monomorphism

If xy is a monomorphism, then y is a monomorphism.




$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$( ( a\circ b )\circ x = y\mbox{ and }( a\circ b )\circ z = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{monomorphism},\mbox{hypothesis})$

$\mbox{there\_exists}(b\circ h)\qquad\mbox{cnf}(\mbox{assume\_bh\_exists},\mbox{hypothesis})$

$b\circ h = b\circ g\qquad\mbox{cnf}(\mbox{bh\_equals\_bg},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT001-3.p} XY monomorphism =$>$ Y monomorphism

If xy is a monomorphism, then y is a monomorphism.




$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$( ( a\circ b )\circ x = y\mbox{ and }( a\circ b )\circ z = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{monomorphism},\mbox{hypothesis})$

$\mbox{there\_exists}(b\circ h)\qquad\mbox{cnf}(\mbox{assume\_bh\_exists},\mbox{hypothesis})$

$b\circ h = b\circ g\qquad\mbox{cnf}(\mbox{bh\_equals\_bg},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT001-2.p} XY monomorphism =$>$ Y monomorphism

If xy is a monomorphism, then y is a monomorphism.




$\mbox{include}(\mbox{'Axioms/CAT002-0.ax'})$

$( 1_{\text{cod}(x)} = 1_{\text{dom}(a\circ b)}\mbox{ and }x\circ ( a\circ b ) = y\mbox{ and }1_{\text{cod}(z)} = 1_{\text{dom}(a\circ b)}\mbox{ and }z\circ ( a\circ b ) = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(c_1,\mbox{hypothesis})$

$1_{\text{cod}(a)} = 1_{\text{dom}(b)}\qquad\mbox{cnf}(\mbox{codomain\_of\_a\_equals\_domain\_of\_b},\mbox{hypothesis})$

$1_{\text{cod}(a)} = 1_{\text{dom}(h)}\qquad\mbox{cnf}(\mbox{codomain\_of\_a\_equals\_domain\_of\_h},\mbox{hypothesis})$

$1_{\text{cod}(a)} = 1_{\text{dom}(g)}\qquad\mbox{cnf}(\mbox{codomain\_of\_a\_equals\_domain\_of\_g},\mbox{hypothesis})$

$a\circ h = a\circ g\qquad\mbox{cnf}(\mbox{ah\_equals\_ag},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT018-1.p} If xy and yz exist, then so does x(yz)






$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$\mbox{defined}(a,b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$\mbox{defined}(b,c)\qquad\mbox{cnf}(\mbox{assume\_bc\_exists},\mbox{hypothesis})$

$\neg\,\mbox{defined}(a,b\circ c)\qquad\mbox{cnf}(\mbox{prove\_a\_bc\_exists},\mbox{negated\_conjecture})$

\medskip\textbf{CAT017-3.p} If x exists, then codomain(x) exists






$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(a)\qquad\mbox{cnf}(\mbox{assume\_a\_exists},\mbox{hypothesis})$

$\neg\,\mbox{there\_exists}(1_{\text{cod}(a)})\qquad\mbox{cnf}(\mbox{prove\_codomain\_of\_a\_exists},\mbox{negated\_conjecture})$

\medskip\textbf{CAT014-1.p} codomain(codomain(x)) = codomain(x)






$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$1_{\text{cod}(1_{\text{cod}(a)})}\ne 1_{\text{cod}(a)}\qquad\mbox{cnf}(\mbox{prove\_codomain\_is\_idempotent},\mbox{negated\_conjecture})$

\medskip\textbf{CAT019-2.p} Axiom of Indiscernibles

[all z (x=z $<$$\to$ y=z)] $\to$ x=y.




$\mbox{include}(\mbox{'Axioms/CAT002-0.ax'})$

$c_2 = z \ \Rightarrow \ c_1 = z\qquad\mbox{cnf}(\mbox{equality\_to\_c1\_and\_c2}_1,\mbox{hypothesis})$

$c_1 = z \ \Rightarrow \ c_2 = z\qquad\mbox{cnf}(\mbox{equality\_to\_c1\_and\_c2}_2,\mbox{hypothesis})$

$c_2\ne c_1\qquad\mbox{cnf}(\mbox{prove\_c1\_equals\_c}_2,\mbox{negated\_conjecture})$

\medskip\textbf{CAT003-2.p} XY epimorphism =$>$ X epimorphism

If xy is an epimorphism, then x is an epimorphism.




$\mbox{include}(\mbox{'Axioms/CAT002-0.ax'})$

$( 1_{\text{cod}(a\circ b)} = 1_{\text{dom}(x)}\mbox{ and }( a\circ b )\circ x = y\mbox{ and }1_{\text{cod}(a\circ b)} = 1_{\text{dom}(z)}\mbox{ and }( a\circ b )\circ z = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{endomorphism},\mbox{hypothesis})$

$1_{\text{cod}(a)} = 1_{\text{dom}(b)}\qquad\mbox{cnf}(\mbox{codomain\_of\_a\_equals\_domain\_of\_b},\mbox{hypothesis})$

$1_{\text{cod}(b)} = 1_{\text{dom}(h)}\qquad\mbox{cnf}(\mbox{codomain\_of\_b\_equals\_domain\_of\_h},\mbox{hypothesis})$

$1_{\text{cod}(b)} = 1_{\text{dom}(g)}\qquad\mbox{cnf}(\mbox{codomain\_of\_b\_equals\_domain\_of\_g},\mbox{hypothesis})$

$b\circ h = b\circ g\qquad\mbox{cnf}(\mbox{bh\_equals\_bg},\mbox{hypothesis})$

$g\ne h\qquad\mbox{cnf}(\mbox{prove\_g\_equals\_h},\mbox{negated\_conjecture})$

\medskip\textbf{CAT009-3.p} If xy is defined, then domain(xy) = domain(y)






$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{ab\_exists},\mbox{hypothesis})$

$1_{\text{dom}(a\circ b)}\ne 1_{\text{dom}(b)}\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_ab\_equals\_domain\_of\_b},\mbox{negated\_conjecture})$

\medskip\textbf{CAT004-4.p} X and Y epimorphisms, XY well-defined =$>$ XY epimorphism

If x and y are epimorphisms and xy is well-defined, then
 xy is an epimorphism.




$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$( x\circ a = y\mbox{ and }z\circ a = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{cancellation\_for\_product}_1,\mbox{hypothesis})$

$( x\circ b = y\mbox{ and }z\circ b = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{cancellation\_for\_product}_2,\mbox{hypothesis})$

$\mbox{there\_exists}(h)\qquad\mbox{cnf}(\mbox{assume\_h\_exists},\mbox{hypothesis})$

$h\circ ( a\circ b ) = g\circ ( a\circ b )\qquad\mbox{cnf}(\mbox{h\_ab\_equals\_g\_ab},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT010-4.p} If xy is defined, then codomain(xy) = codomain(x)






$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{ab\_exists},\mbox{hypothesis})$

$1_{\text{cod}(a\circ b)}\ne 1_{\text{cod}(a)}\qquad\mbox{cnf}(\mbox{prove\_codomain\_of\_ab\_equals\_codomain\_of\_a},\mbox{negated\_conjecture})$

\medskip\textbf{CAT020-1.p} Category theory axioms






$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

\medskip\textbf{CAT014-2.p} codomain(codomain(x)) = codomain(x)






$\mbox{include}(\mbox{'Axioms/CAT002-0.ax'})$

$1_{\text{cod}(1_{\text{cod}(a)})}\ne 1_{\text{cod}(a)}\qquad\mbox{cnf}(\mbox{prove\_codomain\_is\_idempotent},\mbox{negated\_conjecture})$

\medskip\textbf{CAT020-2.p} Category theory (equality) axioms






$\mbox{include}(\mbox{'Axioms/CAT002-0.ax'})$

\medskip\textbf{CAT001-1.p} XY monomorphism =$>$ Y monomorphism

If xy is a monomorphism, then y is a monomorphism.




$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$a\cdot b{=}c\qquad\mbox{cnf}(\mbox{ab\_equals\_c},\mbox{hypothesis})$

$( c\cdot x_1{=}x_2\mbox{ and }c\cdot x_3{=}x_2 ) \ \Rightarrow \ x_1 = x_3\qquad\mbox{cnf}(\mbox{cancellation\_for\_product},\mbox{hypothesis})$

$b\cdot h{=}d\qquad\mbox{cnf}(\mbox{bh\_equals\_d},\mbox{hypothesis})$

$b\cdot g{=}d\qquad\mbox{cnf}(\mbox{bg\_equals\_d},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT005-1.p} Domain is the unique right identity

domain(x) is the unique identity i such that xi is defined.




$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$\mbox{defined}(a,d)\qquad\mbox{cnf}(\mbox{ad\_defined},\mbox{hypothesis})$

$\mbox{identity\_map}(d)\qquad\mbox{cnf}(\mbox{d\_is\_identity\_map},\mbox{hypothesis})$

$1_{\text{dom}(a)}\ne d\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_a\_is\_d},\mbox{negated\_conjecture})$

\medskip\textbf{CAT007-3.p} If domain(x) = codomain(y) then xy is defined






$x{=}x\qquad\mbox{cnf}(\mbox{reflexivity},\mbox{axiom})$

$x{=}y \ \Rightarrow \ y{=}x\qquad\mbox{cnf}(\mbox{symmetry},\mbox{axiom})$

$( x{=}y\mbox{ and }y{=}z ) \ \Rightarrow \ x{=}z\qquad\mbox{cnf}(\mbox{transitivity},\mbox{axiom})$

$\mbox{there\_exists}(1_{\text{dom}(x)}) \ \Rightarrow \ \mbox{there\_exists}(x)\qquad\mbox{cnf}(\mbox{domain\_has\_elements},\mbox{axiom})$

$( \mbox{there\_exists}(1_{\text{dom}(x)})\mbox{ and }1_{\text{dom}(x)}{=}1_{\text{cod}(y)} ) \ \Rightarrow \ \mbox{there\_exists}(x\circ y)\qquad\mbox{cnf}(\mbox{domain\_codomain\_composition}_2,\mbox{axiom})$

$\mbox{there\_exists}(f_1(x,y))\mbox{ or }x{=}y\qquad\mbox{cnf}(\mbox{indiscernibles}_1,\mbox{axiom})$

$x{=}f_1(x,y)\mbox{ or }y{=}f_1(x,y)\mbox{ or }x{=}y\qquad\mbox{cnf}(\mbox{indiscernibles}_2,\mbox{axiom})$

$( x{=}f_1(x,y)\mbox{ and }y{=}f_1(x,y) ) \ \Rightarrow \ x{=}y\qquad\mbox{cnf}(\mbox{indiscernibles}_3,\mbox{axiom})$

$\mbox{there\_exists}(1_{\text{dom}(c_2)})\qquad\mbox{cnf}(\mbox{domain\_of\_c2\_exists},\mbox{hypothesis})$

$\mbox{there\_exists}(1_{\text{dom}(c_1)})\qquad\mbox{cnf}(\mbox{domain\_of\_c1\_exists},\mbox{hypothesis})$

$1_{\text{dom}(c_2)}{=}1_{\text{cod}(c_1)}\qquad\mbox{cnf}(\mbox{domain\_of\_c2\_equals\_codomain\_of\_c}_1,\mbox{hypothesis})$

$\neg\,\mbox{there\_exists}(c_2\circ c_1)\qquad\mbox{cnf}(\mbox{prove\_c1\_c2\_is\_defined},\mbox{negated\_conjecture})$

\medskip\textbf{CAT016-4.p} If x exists, then domain(x) exists






$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(a)\qquad\mbox{cnf}(\mbox{assume\_a\_exists},\mbox{hypothesis})$

$\neg\,\mbox{there\_exists}(1_{\text{dom}(a)})\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_a\_exists},\mbox{negated\_conjecture})$

\medskip\textbf{CAT013-3.p} domain(codomain(x)) = codomain(x)






$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(1_{\text{cod}(a)})\qquad\mbox{cnf}(\mbox{assume\_codomain\_exists},\mbox{hypothesis})$

$1_{\text{dom}(1_{\text{cod}(a)})}\ne 1_{\text{cod}(a)}\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_codomain\_is\_codomain},\mbox{negated\_conjecture})$

\medskip\textbf{CAT019-3.p} Axiom of Indiscernibles

[all z (x=z $<$$\to$ y=z)] $\to$ x=y.




$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$( \mbox{there\_exists}(z)\mbox{ and }a = z ) \ \Rightarrow \ b = z\qquad\mbox{cnf}(\mbox{equality\_of\_a\_and\_b}_1,\mbox{hypothesis})$

$( \mbox{there\_exists}(z)\mbox{ and }b = z ) \ \Rightarrow \ a = z\qquad\mbox{cnf}(\mbox{equality\_of\_a\_and\_b}_2,\mbox{hypothesis})$

$a\ne b\qquad\mbox{cnf}(\mbox{prove\_a\_equals\_b},\mbox{negated\_conjecture})$

\medskip\textbf{CAT008-1.p} If xy is defined then domain(x) = codomain(y)






$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$\mbox{defined}(a,b)\qquad\mbox{cnf}(\mbox{ab\_defined},\mbox{hypothesis})$

$1_{\text{dom}(a)}\ne 1_{\text{cod}(b)}\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_a\_equals\_codomain\_of\_b},\mbox{negated\_conjecture})$

\medskip\textbf{CAT017-4.p} If x exists, then codomain(x) exists






$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(a)\qquad\mbox{cnf}(\mbox{assume\_a\_exists},\mbox{hypothesis})$

$\neg\,\mbox{there\_exists}(1_{\text{cod}(a)})\qquad\mbox{cnf}(\mbox{prove\_codomain\_of\_a\_exists},\mbox{negated\_conjecture})$

\medskip\textbf{CAT011-3.p} domain(domain(x)) = domain(x)






$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(1_{\text{dom}(a)})\qquad\mbox{cnf}(\mbox{assume\_domain\_exists},\mbox{hypothesis})$

$1_{\text{dom}(1_{\text{dom}(a)})}\ne 1_{\text{dom}(a)}\qquad\mbox{cnf}(\mbox{prove\_domain\_is\_idempotent},\mbox{negated\_conjecture})$

\medskip\textbf{CAT004-2.p} X and Y epimorphisms, XY well-defined =$>$ XY epimorphism

If x and y are epimorphisms and xy is well-defined, then
 xy is an epimorphism.




$\mbox{include}(\mbox{'Axioms/CAT002-0.ax'})$

$( 1_{\text{cod}(a)} = 1_{\text{dom}(x)}\mbox{ and }a\circ x = y\mbox{ and }1_{\text{cod}(a)} = 1_{\text{dom}(z)}\mbox{ and }a\circ z = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{epimorphism}_1,\mbox{hypothesis})$

$( 1_{\text{cod}(b)} = 1_{\text{dom}(x)}\mbox{ and }b\circ x = y\mbox{ and }1_{\text{cod}(b)} = 1_{\text{dom}(z)}\mbox{ and }b\circ z = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{epimorphism}_2,\mbox{hypothesis})$

$1_{\text{cod}(a)} = 1_{\text{dom}(b)}\qquad\mbox{cnf}(\mbox{codomain\_of\_a\_equals\_domain\_of\_b},\mbox{hypothesis})$

$1_{\text{cod}(a\circ b)} = 1_{\text{dom}(h)}\qquad\mbox{cnf}(\mbox{codomain\_of\_ab\_equals\_domain\_of\_h},\mbox{hypothesis})$

$1_{\text{cod}(a\circ b)} = 1_{\text{dom}(g)}\qquad\mbox{cnf}(\mbox{codomain\_of\_ab\_equals\_domain\_of\_g},\mbox{hypothesis})$

$( a\circ b )\circ h = ( a\circ b )\circ g\qquad\mbox{cnf}(\mbox{ab\_h\_equals\_ab\_g},\mbox{hypothesis})$

$h\ne g\qquad\mbox{cnf}(\mbox{prove\_h\_equals\_g},\mbox{negated\_conjecture})$

\medskip\textbf{CAT019-4.p} Axiom of Indiscernibles

[all z (x=z $<$$\to$ y=z)] $\to$ x=y.




$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$( \mbox{there\_exists}(z)\mbox{ and }a = z ) \ \Rightarrow \ b = z\qquad\mbox{cnf}(\mbox{equality\_of\_a\_and\_b}_1,\mbox{hypothesis})$

$( \mbox{there\_exists}(z)\mbox{ and }b = z ) \ \Rightarrow \ a = z\qquad\mbox{cnf}(\mbox{equality\_of\_a\_and\_b}_2,\mbox{hypothesis})$

$a\ne b\qquad\mbox{cnf}(\mbox{prove\_a\_equals\_b},\mbox{negated\_conjecture})$

\medskip\textbf{CAT011-4.p} domain(domain(x)) = domain(x)






$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(1_{\text{dom}(a)})\qquad\mbox{cnf}(\mbox{assume\_domain\_exists},\mbox{hypothesis})$

$1_{\text{dom}(1_{\text{dom}(a)})}\ne 1_{\text{dom}(a)}\qquad\mbox{cnf}(\mbox{prove\_domain\_is\_idempotent},\mbox{negated\_conjecture})$

\medskip\textbf{CAT002-3.p} X and Y monomorphisms, XY well-defined =$>$ XY monomorphism

If x and y are monomorphisms and xy is well-defined then
 xy is a monomorphism.




$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{assume\_ab\_exists},\mbox{hypothesis})$

$( a\circ x = y\mbox{ and }a\circ z = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{cancellation\_for\_compose}_1,\mbox{hypothesis})$

$( b\circ x = y\mbox{ and }b\circ z = y ) \ \Rightarrow \ x = z\qquad\mbox{cnf}(\mbox{cancellation\_for\_compose}_2,\mbox{hypothesis})$

$\mbox{there\_exists}(h)\qquad\mbox{cnf}(\mbox{assume\_h\_exists},\mbox{hypothesis})$

$( a\circ b )\circ h = ( a\circ b )\circ g\qquad\mbox{cnf}(\mbox{ab\_h\_equals\_ab\_g},\mbox{hypothesis})$

$g\ne h\qquad\mbox{cnf}(\mbox{prove\_g\_equals\_h},\mbox{negated\_conjecture})$

\medskip\textbf{CAT009-4.p} If xy is defined, then domain(xy) = domain(y)






$\mbox{include}(\mbox{'Axioms/CAT004-0.ax'})$

$\mbox{there\_exists}(a\circ b)\qquad\mbox{cnf}(\mbox{ab\_exists},\mbox{hypothesis})$

$1_{\text{dom}(a\circ b)}\ne 1_{\text{dom}(b)}\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_ab\_equals\_domain\_of\_b},\mbox{negated\_conjecture})$

\medskip\textbf{CAT006-3.p} Codomain is the unique left identity

codomain(x) is the unique identity j such that jx is defined.




$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(d\circ a)\qquad\mbox{cnf}(\mbox{da\_exists},\mbox{hypothesis})$

$\mbox{there\_exists}(x\circ d) \ \Rightarrow \ x\circ d = x\qquad\mbox{cnf}(\mbox{xd\_equals\_x},\mbox{hypothesis})$

$\mbox{there\_exists}(d\circ x) \ \Rightarrow \ d\circ x = x\qquad\mbox{cnf}(\mbox{dx\_equals\_x},\mbox{hypothesis})$

$1_{\text{cod}(a)}\ne d\qquad\mbox{cnf}(\mbox{prove\_codomain\_of\_a\_is\_d},\mbox{negated\_conjecture})$

\medskip\textbf{CAT016-3.p} If x exists, then domain(x) exists






$\mbox{include}(\mbox{'Axioms/CAT003-0.ax'})$

$\mbox{there\_exists}(a)\qquad\mbox{cnf}(\mbox{assume\_a\_exists},\mbox{hypothesis})$

$\neg\,\mbox{there\_exists}(1_{\text{dom}(a)})\qquad\mbox{cnf}(\mbox{prove\_domain\_of\_a\_exists},\mbox{negated\_conjecture})$

\medskip\textbf{CAT012-1.p} codomain(domain(x)) = domain(x)






$\mbox{include}(\mbox{'Axioms/CAT001-0.ax'})$

$1_{\text{cod}(1_{\text{dom}(a)})}\ne 1_{\text{dom}(a)}\qquad\mbox{cnf}(\mbox{prove\_codomain\_of\_domain\_is\_domain},\mbox{negated\_conjecture})$

\medskip
\end{document}