diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..173cd64
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+*.agdai
+.#*
+.pijul
diff --git a/Everything/Safe.agda b/Everything/Safe.agda
new file mode 100644
index 0000000..37dce6b
--- /dev/null
+++ b/Everything/Safe.agda
@@ -0,0 +1,37 @@
+{-# OPTIONS --warning=error --safe --without-K #-}
+
+-- This file contains everything that can be compiled in --safe mode.
+
+open import Numbers.Naturals
+open import Numbers.BinaryNaturals.Definition
+
+open import Lists.Lists
+
+open import Groups.Groups
+open import Groups.FinitePermutations
+open import Groups.GroupsLemmas
+
+open import Fields.Fields
+open import Fields.FieldOfFractions
+open import Fields.FieldOfFractionsOrder
+
+open import Rings.Definition
+open import Rings.Lemmas
+open import Rings.IntegralDomains
+
+open import Setoids.Setoids
+open import Setoids.Lists
+open import Setoids.Orders
+
+open import Sets.Cardinality
+open import Sets.FinSet
+
+open import DecidableSet
+
+open import Maybe
+open import Orders
+open import WellFoundedInduction
+
+open import ClassicalLogic.ClassicalFive
+
+module Everything.Safe where
diff --git a/Everything/WithK.agda b/Everything/WithK.agda
new file mode 100644
index 0000000..b084cc2
--- /dev/null
+++ b/Everything/WithK.agda
@@ -0,0 +1,31 @@
+{-# OPTIONS --warning=error --safe #-}
+
+-- This file contains everything that is --safe, but uses K.
+
+open import PrimeNumbers
+open import Numbers.Integers
+open import Numbers.Rationals
+open import Numbers.RationalsLemmas
+open import Numbers.BinaryNaturals.Multiplication -- TODO there's no reason for this to need K
+open import Numbers.BinaryNaturals.Order -- TODO likewise this
+
+open import Logic.PropositionalLogic
+open import Logic.PropositionalLogicExamples
+open import Logic.PropositionalAxiomsTautology
+
+open import IntegersModN
+
+open import Sets.FinSetWithK
+
+open import Vectors
+
+open import KeyValue
+open import KeyValueWithDomain
+
+open import Rings.Examples.Examples
+open import Rings.Examples.Proofs
+
+open import Groups.FreeGroups
+open import Groups.Groups2
+
+module Everything.WithK where