diff --git a/prototyping/.gitignore b/prototyping/.gitignore
index cca4f464..9dde90a5 100644
--- a/prototyping/.gitignore
+++ b/prototyping/.gitignore
@@ -3,4 +3,7 @@
 Main
 MAlonzo
 PrettyPrinter
+Interpreter
+!Tests/Interpreter
+!Tests/PrettyPrinter
 .ghc.*
diff --git a/prototyping/Properties/Product.agda b/prototyping/Properties/Product.agda
new file mode 100644
index 00000000..2118d577
--- /dev/null
+++ b/prototyping/Properties/Product.agda
@@ -0,0 +1,12 @@
+module Properties.Product where
+
+record Σ {A : Set} (B : A → Set) : Set where
+
+  constructor _,_
+  field fst : A
+  field snd : B fst
+
+open Σ public
+
+_×_ : Set → Set → Set
+A × B = Σ (λ (a : A) → B)