diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..171a389
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+*.agdai
diff --git a/cubical-playground.agda-lib b/cubical-playground.agda-lib
new file mode 100644
index 0000000..672cf91
--- /dev/null
+++ b/cubical-playground.agda-lib
@@ -0,0 +1,2 @@
+include: src
+depend: standard-library
diff --git a/2022-10-03-notes.lagda.md b/src/2022-10-03-notes.lagda.md
similarity index 98%
rename from 2022-10-03-notes.lagda.md
rename to src/2022-10-03-notes.lagda.md
index 8e1dbe5..2f020df 100644
--- a/2022-10-03-notes.lagda.md
+++ b/src/2022-10-03-notes.lagda.md
@@ -1,5 +1,5 @@
 ```
-{#- OPTIONS --cubical -#}
+{-# OPTIONS --cubical #-}
 
 ----------
 
diff --git a/src/2022-10-10-notes.lagda.md b/src/2022-10-10-notes.lagda.md
new file mode 100644
index 0000000..188023f
--- /dev/null
+++ b/src/2022-10-10-notes.lagda.md
@@ -0,0 +1,8 @@
+2022 Oct 10
+===
+
+```agda
+{-# OPTIONS --cubical #-}
+
+-- Hello
+```
diff --git a/src/Dedekind/Bool.agda b/src/Dedekind/Bool.agda
new file mode 100644
index 0000000..eb288fb
--- /dev/null
+++ b/src/Dedekind/Bool.agda
@@ -0,0 +1,8 @@
+module Dedekind.Bool where
+
+-- Booleans
+data Bool : Set where
+  true : Bool
+  false : Bool
+
+
diff --git a/src/Dedekind/Integer.agda b/src/Dedekind/Integer.agda
new file mode 100644
index 0000000..4c9e181
--- /dev/null
+++ b/src/Dedekind/Integer.agda
@@ -0,0 +1,8 @@
+module Dedekind.Integer where
+
+open import Dedekind.Natural using (ℕ)
+
+-- Integers
+data ℤ : Set where
+  pos : ℕ → ℤ
+  negsuc : ℕ → ℤ
diff --git a/src/Dedekind/Natural.agda b/src/Dedekind/Natural.agda
new file mode 100644
index 0000000..2399d68
--- /dev/null
+++ b/src/Dedekind/Natural.agda
@@ -0,0 +1,15 @@
+module Dedekind.Natural where
+
+open import Dedekind.Set using (⊤; ⊥)
+
+-- Natural
+data ℕ : Set where
+  zero : ℕ
+  suc : ℕ → ℕ
+
+NonZero : ℕ → Set
+NonZero zero = ⊥
+NonZero (suc n) = ⊤
+
+gcd : (x y : ℕ) .{{ _ : NonZero x }} .{{ _ : NonZero y }} → ℕ
+gcd x y = ?
diff --git a/src/Dedekind/Rational.agda b/src/Dedekind/Rational.agda
new file mode 100644
index 0000000..2153f33
--- /dev/null
+++ b/src/Dedekind/Rational.agda
@@ -0,0 +1,12 @@
+module Dedekind.Rational where
+
+open import Dedekind.Bool using (Bool)
+open import Dedekind.Integer using (ℤ)
+open import Dedekind.Natural using (ℕ; NonZero)
+
+-- Rational
+data ℚ : Set where
+  rat : ℤ → (d : ℕ) .{{ _ : NonZero d }} → ℚ
+
+_<_ : ℚ → ℚ → Bool
+x < y = ?
diff --git a/src/Dedekind/Real.agda b/src/Dedekind/Real.agda
new file mode 100644
index 0000000..e442b56
--- /dev/null
+++ b/src/Dedekind/Real.agda
@@ -0,0 +1,20 @@
+-- Dedekind cuts using Cubical Agda
+{-# OPTIONS --cubical #-}
+
+module Dedekind.Real where
+
+open import Dedekind.Rational using (ℚ; _<_)
+
+-- Dedekind cuts
+record ℝ : Set where
+  constructor real
+  field
+    lower : (ℚ → Bool)
+    closed : ∀ (x y : ℚ) → x < y
+
+-- Operations on reals
+_+_ : ℝ → ℝ → ℝ
+a + b = real 
+  (λ q → ℝ.lower a q)
+
+-- Properties of reals
diff --git a/src/Dedekind/Set.agda b/src/Dedekind/Set.agda
new file mode 100644
index 0000000..45fa565
--- /dev/null
+++ b/src/Dedekind/Set.agda
@@ -0,0 +1,6 @@
+module Dedekind.Set where
+
+record ⊥ : Set where
+
+record ⊤ : Set where
+  instance constructor tt
diff --git a/src/main.agda b/src/main.agda
new file mode 100644
index 0000000..4fd8129
--- /dev/null
+++ b/src/main.agda
@@ -0,0 +1,14 @@
+{-# OPTIONS --guardedness #-}
+
+module main where
+
+open import Agda.Builtin.IO using (IO)
+open import Agda.Builtin.Unit using (⊤)
+open import Agda.Builtin.String using (String)
+
+postulate putStrLn : String → IO ⊤
+{-# FOREIGN GHC import qualified Data.Text as T #-}
+{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}
+
+main : IO ⊤
+main = putStrLn "Hello world!"