Initial commit

1 files changed, 17 insertions, 0 deletions

diff --git a/megalodon/scraps.tex b/megalodon/scraps.tex
new file mode 100644
index 0000000..f79a630
--- /dev/null
+++ b/megalodon/scraps.tex
@@ -0,0 +1,17 @@
+\begin{axiom}\label{trivial}
+    For all $x$ we have $x = x$.
+\end{axiom}
+
+% Axiom EmptyAx : ~exists x:set, x :e Empty.
+\begin{axiom}\label{empty_axiom}
+    There exists no set $x$ such that $x\in\emptyset$.
+\end{axiom}
+
+% UnionEq : forall X x, x :e Union X <-> exists Y, x :e Y /\ Y :e X.
+\begin{axiom}\label{union_eq}
+    For all $x, X$ we have $x\in\unions{X}$ iff there exists $Y$ such that $x\in Y\in X$.
+\end{axiom}
+
+\begin{theorem}\label{eq_refl}
+    For all $x$ we have $x=x$.
+\end{theorem}