diff --git a/Katydid.lean b/Katydid.lean
index 9b0931a..c844900 100644
--- a/Katydid.lean
+++ b/Katydid.lean
@@ -1,6 +1,5 @@
 import Katydid.Std.Ordering
 import Katydid.Std.OrderingThunk
-import Katydid.Std.Tipe
 import Katydid.Std.Lists
 import Katydid.Std.Ltac
 import Katydid.Std.Balistic
@@ -10,6 +9,7 @@ import Katydid.Example.SimpLibrary
 import Katydid.Expr.Desc
 import Katydid.Expr.Regex
 
+import Katydid.Conal.Tipe
 import Katydid.Conal.Decidability
 import Katydid.Conal.Function
 import Katydid.Conal.Language
diff --git a/Katydid/Conal/Calculus.lean b/Katydid/Conal/Calculus.lean
index cca0056..7c31f9d 100644
--- a/Katydid/Conal/Calculus.lean
+++ b/Katydid/Conal/Calculus.lean
@@ -1,7 +1,7 @@
 -- A translation to Lean from Agda
 -- https://github.com/conal/paper-2021-language-derivatives/blob/main/Calculus.lagda
 
-import Katydid.Std.Tipe
+import Katydid.Conal.Tipe
 import Katydid.Conal.Function
 import Katydid.Conal.Language
 
diff --git a/Katydid/Conal/Function.lean b/Katydid/Conal/Function.lean
index 4aedf73..e87b433 100644
--- a/Katydid/Conal/Function.lean
+++ b/Katydid/Conal/Function.lean
@@ -1,6 +1,6 @@
 -- An approximation of the Function module in the Agda standard library.
 
-import Katydid.Std.Tipe
+import Katydid.Conal.Tipe
 import Mathlib.Logic.Equiv.Defs
 
 -- A ↔ B = Inverse A B
diff --git a/Katydid/Conal/Language.lean b/Katydid/Conal/Language.lean
index e233af8..f5f58ed 100644
--- a/Katydid/Conal/Language.lean
+++ b/Katydid/Conal/Language.lean
@@ -1,7 +1,7 @@
 -- A translation to Lean from Agda
 -- https://github.com/conal/paper-2021-language-derivatives/blob/main/Language.lagda
 
-import Katydid.Std.Tipe
+import Katydid.Conal.Tipe
 
 namespace Language
 
diff --git a/Katydid/Std/Tipe.lean b/Katydid/Conal/Tipe.lean
similarity index 100%
rename from Katydid/Std/Tipe.lean
rename to Katydid/Conal/Tipe.lean