From a588c0f205513db6ccd44579d17037a080948b5d Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 10 Apr 2017 20:33:30 -0400
Subject: [PATCH] chore(algebra): clean up some imports

Also add some notation to lean-input.el
---
 hott/algebra/bundled.hlean       | 2 +-
 hott/algebra/field.hlean         | 2 +-
 hott/algebra/homomorphism.hlean  | 2 +-
 hott/algebra/order.hlean         | 2 +-
 hott/algebra/ordered_group.hlean | 2 +-
 hott/algebra/ring.hlean          | 2 +-
 hott/homotopy/EM.hlean           | 2 --
 src/emacs/lean-input.el          | 2 ++
 8 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/hott/algebra/bundled.hlean b/hott/algebra/bundled.hlean
index a3e5b8a9d..cb6942964 100644
--- a/hott/algebra/bundled.hlean
+++ b/hott/algebra/bundled.hlean
@@ -5,7 +5,7 @@ Authors: Jeremy Avigad
 
 Bundled structures
 -/
-import algebra.group homotopy.interval
+import algebra.group
 open algebra pointed is_trunc
 
 namespace algebra
diff --git a/hott/algebra/field.hlean b/hott/algebra/field.hlean
index 7e59b73c9..e4faf53bf 100644
--- a/hott/algebra/field.hlean
+++ b/hott/algebra/field.hlean
@@ -6,7 +6,7 @@ Authors: Robert Lewis
 Structures with multiplicative and additive components, including division rings and fields.
 The development is modeled after Isabelle's library.
 -/
-import algebra.binary algebra.group algebra.ring
+import algebra.ring
 open eq eq.ops algebra
 set_option class.force_new true
 
diff --git a/hott/algebra/homomorphism.hlean b/hott/algebra/homomorphism.hlean
index 3cfa8c31b..e65b7d2e1 100644
--- a/hott/algebra/homomorphism.hlean
+++ b/hott/algebra/homomorphism.hlean
@@ -5,7 +5,7 @@ Author: Jeremy Avigad
 
 Homomorphisms between structures.
 -/
-import algebra.ring algebra.category.category
+import algebra.ring function
 open eq function is_trunc
 
 namespace algebra
diff --git a/hott/algebra/order.hlean b/hott/algebra/order.hlean
index 71ce0a29d..c1f8516d4 100644
--- a/hott/algebra/order.hlean
+++ b/hott/algebra/order.hlean
@@ -5,7 +5,7 @@ Author: Jeremy Avigad
 
 Weak orders "≤", strict orders "<", and structures that include both.
 -/
-import algebra.binary algebra.priority
+import algebra.binary
 open eq eq.ops algebra
 -- set_option class.force_new true
 
diff --git a/hott/algebra/ordered_group.hlean b/hott/algebra/ordered_group.hlean
index 1feba7a98..93c2be157 100644
--- a/hott/algebra/ordered_group.hlean
+++ b/hott/algebra/ordered_group.hlean
@@ -6,7 +6,7 @@ Authors: Jeremy Avigad
 Partially ordered additive groups, modeled on Isabelle's library. These classes can be refined
 if necessary.
 -/
-import algebra.binary algebra.group algebra.order
+import algebra.group algebra.order
 open eq eq.ops algebra   -- note: ⁻¹ will be overloaded
 set_option class.force_new true
 
diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean
index a9242a5d6..af943af64 100644
--- a/hott/algebra/ring.hlean
+++ b/hott/algebra/ring.hlean
@@ -7,7 +7,7 @@ Structures with multiplicative and additive components, including semirings, rin
 The development is modeled after Isabelle's library.
 -/
 
-import algebra.binary algebra.group
+import algebra.group
 open eq eq.ops algebra
 set_option class.force_new true
 
diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean
index 3a1f78a85..6d44bdfc0 100644
--- a/hott/homotopy/EM.hlean
+++ b/hott/homotopy/EM.hlean
@@ -465,8 +465,6 @@ namespace EM
     { exact EMadd1_functor φ n }
   end
 
-  -- TODO: (K G n →* K H n) ≃ (G →g H)
-
   /- Equivalence of Groups and pointed connected 1-truncated types -/
 
   definition ptruncconntype10_pequiv (X Y : 1-Type*[0]) (e : π₁ X ≃g π₁ Y) : X ≃* Y :=
diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el
index 0f7bfc5aa..75c27937e 100644
--- a/src/emacs/lean-input.el
+++ b/src/emacs/lean-input.el
@@ -357,6 +357,8 @@ order for the change to take effect."
   ("-1v"       . ("⁻¹ᵛ"))
   ("-1E"       . ("⁻¹ᴱ"))
   ("-1hty"     . ("⁻¹ʰᵗʸ"))
+  ("-1lm"      . ("⁻¹ˡᵐ"))
+  ("-1gm"      . ("⁻¹ᵍᵐ"))
   ("-2"        . ("⁻²" "₋₂"))
   ("-2o"       . ("⁻²ᵒ"))
   ("-3"        . ("⁻³"))