diff --git a/.gitignore b/.gitignore
index f105203..d53be04 100644
--- a/.gitignore
+++ b/.gitignore
@@ -306,3 +306,5 @@ TSWLatexianTemp*
 MAlonzo/**
 
 *.html
+agda/public
+agda/Everything.agda
diff --git a/agda/algebra.lagda.md b/agda/algebra.lagda.md
index 63afea7..7b75ae7 100644
--- a/agda/algebra.lagda.md
+++ b/agda/algebra.lagda.md
@@ -1,4 +1,5 @@
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import equality
 module algebra where
 ```