From ee4cba4e0bf07dc0ddcb851e95a1ee22a88fe344 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 13 Apr 2015 21:51:22 -0400
Subject: [PATCH] style(hott): a bit of cleanup

---
 hott/init/path.hlean    |  1 -
 hott/types/sigma.hlean  | 11 +++--------
 src/emacs/lean-input.el |  1 +
 3 files changed, 4 insertions(+), 9 deletions(-)

diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 6b1b0ecfb..5e4b18a2d 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -497,7 +497,6 @@ namespace eq
   eq.rec_on r (idp_con _)⁻¹
 
   -- Transporting in a pulled back fibration.
-  -- TODO: P can probably be implicit
   -- rename: tr_compose
   definition transport_compose (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) :
     transport (P ∘ f) p z  =  transport P (ap f p) z :=
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 0102ed4f5..09d49d47e 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -19,7 +19,6 @@ namespace sigma
             {D : Πa b, C a b → Type}
             {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
 
-  -- sigma.eta is already used for the eta rule for strict equality
   protected definition eta : Π (u : Σa, B a), ⟨u.1 , u.2⟩ = u
   | eta ⟨u₁, u₂⟩ := idp
 
@@ -32,7 +31,6 @@ namespace sigma
   definition dpair_eq_dpair (p : a = a') (q : p ▹ b = b') : ⟨a, b⟩ = ⟨a', b'⟩ :=
   by cases p; cases q; apply idp
 
-  /- In Coq they often have to give u and v explicitly -/
   definition sigma_eq (p : u.1 = v.1) (q : p ▹ u.2 = v.2) : u = v :=
   by cases u; cases v; apply (dpair_eq_dpair p q)
 
@@ -46,9 +44,6 @@ namespace sigma
   definition eq_pr2 (p : u = v) : p..1 ▹ u.2 = v.2 :=
   by cases p; apply idp
 
-  --Coq uses the following proof, which only computes if u,v are dpairs AND p is idp
-  --(transport_compose B dpr1 p u.2)⁻¹ ⬝ apD dpr2 p
-
   postfix `..2`:(max+1) := eq_pr2
 
   private definition dpair_sigma_eq (p : u.1 = v.1) (q : p ▹ u.2 = v.2)
@@ -71,11 +66,11 @@ namespace sigma
 
   /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/
 
-  definition sigma_eq_uncurried : Π (pq : Σ(p : pr1 u = pr1 v), p ▹ (pr2 u) = pr2 v), u = v
+  definition sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2), u = v
   | sigma_eq_uncurried ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂
 
   definition dpair_sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2),
-        sigma.mk (sigma_eq_uncurried pq)..1 (sigma_eq_uncurried pq)..2 = pq
+        ⟨(sigma_eq_uncurried pq)..1, (sigma_eq_uncurried pq)..2⟩ = pq
   | dpair_sigma_eq_uncurried ⟨pq₁, pq₂⟩ := dpair_sigma_eq pq₁ pq₂
 
   definition sigma_eq_pr1_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
@@ -86,7 +81,7 @@ namespace sigma
       : (sigma_eq_pr1_uncurried pq) ▹ (sigma_eq_uncurried pq)..2 = pq.2 :=
   (dpair_sigma_eq_uncurried pq)..2
 
-  definition sigma_eq_eta_uncurried (p : u = v) : sigma_eq_uncurried (sigma.mk p..1 p..2) = p :=
+  definition sigma_eq_eta_uncurried (p : u = v) : sigma_eq_uncurried ⟨p..1, p..2⟩ = p :=
   sigma_eq_eta p
 
   definition tr_sigma_eq_pr1_uncurried {B' : A → Type}
diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el
index 1e0843a34..686883cff 100644
--- a/src/emacs/lean-input.el
+++ b/src/emacs/lean-input.el
@@ -331,6 +331,7 @@ order for the change to take effect."
   ("-1e"       . ("⁻¹ᵉ"))
   ("-1h"       . ("⁻¹ʰ"))
   ("-1g"       . ("⁻¹ᵍ"))
+  ("-1o"       . ("⁻¹ᵒ"))
   ("qed"       . ("∎"))
   ("x"         . ("×"))
   ("o"         . ("∘"))