From ba5368c4ae229ea0e67c20f0207bbf6d28c5cb77 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 19 May 2017 14:44:39 -0400
Subject: [PATCH] feat(hott): various small changes

---
 hott/algebra/group_power.hlean | 55 ++++++++++++++++++++++++++++++----
 hott/init/equiv.hlean          |  6 ++++
 hott/types/fiber.hlean         |  4 +--
 hott/types/int/hott.hlean      |  2 +-
 4 files changed, 59 insertions(+), 8 deletions(-)

diff --git a/hott/algebra/group_power.hlean b/hott/algebra/group_power.hlean
index e83375608..fe652e030 100644
--- a/hott/algebra/group_power.hlean
+++ b/hott/algebra/group_power.hlean
@@ -11,10 +11,11 @@ a^n is used for the first, but users can locally redefine it to gpow when needed
 
 Note: power adopts the convention that 0^0=1.
 -/
-import types.nat.basic types.int.basic
+import types.nat.basic types.int.basic .homomorphism .group_theory
 open algebra
 
-variables {A : Type}
+namespace algebra
+variables {A B : Type}
 
 structure has_pow_nat [class] (A : Type) :=
 (pow_nat : A → nat → A)
@@ -118,6 +119,10 @@ theorem pow_inv_comm (a : A) : Πm n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m
 | (succ m) (succ n) := by rewrite [pow_succ' at {1}, pow_succ at {1}, pow_succ', pow_succ,
                             *mul.assoc, inv_mul_cancel_left, mul_inv_cancel_left, pow_inv_comm]
 
+lemma respect_pow [group B] (f : A → B) [is_mul_hom f] (a : A) : Πn, f (a ^ n) = (f a) ^ n
+| 0        := respect_one f
+| (succ n) := by rewrite [pow_succ, respect_mul, respect_pow]
+
 end nat
 
 open int
@@ -184,6 +189,10 @@ theorem gpow_mul (a : A) : Π n m, gpow a (n * m) = gpow (gpow a n) m
 | -[1+m]     (of_nat n) := by rewrite [↑gpow at {2,3}, inv_pow, -pow_mul, -gpow_eq_pow, -gpow_neg]
 | -[1+m]     -[1+n]     := by rewrite [↑gpow at {2,3}, inv_pow, inv_inv, -pow_mul]
 
+lemma respect_gpow [group B] (f : A → B) [is_mul_hom f] (a : A) : Πn, f (gpow a n) = gpow (f a) n
+| (of_nat n) := !respect_pow
+| -[1+n]     := by rewrite [↑gpow, respect_inv, respect_pow]
+
 end group
 
 section comm_monoid
@@ -228,6 +237,15 @@ theorem pow_two_add (n : ℕ) : (2:A)^n + 2^n = 2^(succ n) :=
 
 end ordered_ring
 
+section bundled
+open group
+lemma to_respect_pow {A B : Group} (f : A →g B) (a : A) (n : ℕ) : f (a ^ n) = (f a) ^ n :=
+respect_pow f a n
+
+lemma to_respect_gpow {A B : Group} (f : A →g B) (a : A) (n : ℤ) : f (gpow a n) = gpow (f a) n :=
+respect_gpow f a n
+end bundled
+
 /- additive monoid -/
 
 section add_monoid
@@ -238,7 +256,7 @@ open nat
 
 definition nmul : ℕ → A → A := λ n a, a^n
 
-infix [priority algebra.prio] `⬝` := nmul
+local infix [priority algebra.prio] `⬝` := nmul
 
 theorem zero_nmul (a : A) : (0:ℕ) ⬝ a = 0 := pow_zero a
 theorem succ_nmul (n : ℕ) (a : A) : nmul (succ n) a = a + (nmul n a) := pow_succ a n
@@ -251,12 +269,17 @@ theorem one_nmul (a : A) : 1 ⬝ a = a := pow_one a
 
 theorem add_nmul (m n : ℕ) (a : A) : (m + n) ⬝ a = (m ⬝ a) + (n ⬝ a) := pow_add a m n
 
-theorem mul_nmul (m n : ℕ) (a : A) : (m * n) ⬝ a = m ⬝ (n ⬝ a) := eq.subst (mul.comm n m) (pow_mul a n m)
+theorem mul_nmul (m n : ℕ) (a : A) : (m * n) ⬝ a = m ⬝ (n ⬝ a) :=
+eq.subst (mul.comm n m) (pow_mul a n m)
 
 theorem nmul_comm (m n : ℕ) (a : A) : (m ⬝ a) + (n ⬝ a) = (n ⬝ a) + (m ⬝ a) := pow_comm a m n
 
 end add_monoid
 
+namespace ops
+infix [priority algebra.prio] `⬝` := nmul
+end ops
+open algebra.ops
 /- additive commutative monoid -/
 
 section add_comm_monoid
@@ -280,7 +303,12 @@ theorem nmul_neg (n : ℕ) (a : A) : n ⬝ (-a) = -(n ⬝ a) := inv_pow a n
 
 theorem sub_nmul {m n : ℕ} (a : A) (H : m ≥ n) : (m - n) ⬝ a = (m ⬝ a) + -(n ⬝ a) := pow_sub a H
 
-theorem nmul_neg_comm (m n : ℕ) (a : A) : (m ⬝ (-a)) + (n ⬝ a) = (n ⬝ a) + (m ⬝ (-a)) := pow_inv_comm a m n
+theorem nmul_neg_comm (m n : ℕ) (a : A) : (m ⬝ (-a)) + (n ⬝ a) = (n ⬝ a) + (m ⬝ (-a)) :=
+pow_inv_comm a m n
+
+lemma respect_nmul [add_group B] (f : A → B) [H : is_add_hom f] (n : ℕ) (a : A) :
+  f (nmul n a) = nmul n (f a) :=
+to_respect_pow (group.homomorphism.mk f H) a n
 
 end nat
 
@@ -309,4 +337,21 @@ by rewrite [mul.comm]; apply gpow_mul
 lemma one_imul (a : A) : imul 1 a = a :=
 gpow_one a
 
+lemma respect_imul [add_group B] (f : A → B) [H : is_add_hom f] (n : ℤ) (a : A) :
+  f (imul n a) = imul n (f a) :=
+to_respect_gpow (group.homomorphism.mk f H) a n
+
 end add_ab_group
+
+section bundled
+open group
+
+lemma to_respect_nmul {A B : AddGroup} (f : A →g B) (n : ℕ) (a : A) : f (nmul n a) = nmul n (f a) :=
+to_respect_pow f a n
+
+lemma to_respect_imul {A B : AddGroup} (f : A →g B) (n : ℤ) (a : A) : f (imul n a) = imul n (f a) :=
+to_respect_gpow f a n
+
+end bundled
+
+end algebra
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 5f3dca246..601561b59 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -370,6 +370,12 @@ namespace equiv
   definition eq_of_fn_eq_fn_inv [unfold 3] (f : A ≃ B) {x y : B} (q : f⁻¹ x = f⁻¹ y) : x = y :=
   (right_inv f x)⁻¹ ⬝ ap f q ⬝ right_inv f y
 
+  definition ap_eq_of_fn_eq_fn (f : A ≃ B) {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q :=
+  ap_eq_of_fn_eq_fn' f q
+
+  definition eq_of_fn_eq_fn_ap (f : A ≃ B) {x y : A} (q : x = y) : eq_of_fn_eq_fn' f (ap f q) = q :=
+  eq_of_fn_eq_fn'_ap f q
+
   --we need this theorem for the funext_of_ua proof
   theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ :=
   eq.rec_on p idp
diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index e369549e4..37f89ecba 100644
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@@ -23,8 +23,8 @@ namespace fiber
   fapply equiv.MK,
     {intro x, exact ⟨point x, point_eq x⟩},
     {intro x, exact (fiber.mk x.1 x.2)},
-    {intro x, exact abstract begin cases x, apply idp end end},
-    {intro x, exact abstract begin cases x, apply idp end end},
+    {intro x, cases x, apply idp },
+    {intro x, cases x, apply idp },
   end
 
   definition fiber_eq_equiv [constructor] (x y : fiber f b)
diff --git a/hott/types/int/hott.hlean b/hott/types/int/hott.hlean
index 90d4f691f..9e9df1c02 100644
--- a/hott/types/int/hott.hlean
+++ b/hott/types/int/hott.hlean
@@ -38,7 +38,7 @@ namespace int
   adjointify neg neg (λx, !neg_neg) (λa, !neg_neg)
   definition equiv_neg [constructor] : ℤ ≃ ℤ := equiv.mk neg _
 
-  definition iterate {A : Type} (f : A ≃ A) (a : ℤ) : A ≃ A :=
+  definition iiterate {A : Type} (f : A ≃ A) (a : ℤ) : A ≃ A :=
   rec_nat_on a erfl
                (λb g, f ⬝e g)
                (λb g, g ⬝e f⁻¹ᵉ)