From 519dcee739fbca5a4ab77d66db7652097b4604cd Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 30 Jun 2017 16:21:23 +0100 Subject: [PATCH] fix(hott/algebra/homomorphism): fix typos --- hott/algebra/homomorphism.hlean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hott/algebra/homomorphism.hlean b/hott/algebra/homomorphism.hlean index 971e5efad..cf94ae103 100644 --- a/hott/algebra/homomorphism.hlean +++ b/hott/algebra/homomorphism.hlean @@ -103,7 +103,7 @@ section group_A_B have f (a⁻¹) * f a = 1, by rewrite [-respect_mul f, mul.left_inv, respect_one f], eq_inv_of_mul_eq_one this - definition is_embedding_of_is_mul_hom [group B] (f : A → B) [is_mul_hom f] + definition is_embedding_of_is_mul_hom (f : A → B) [is_mul_hom f] (H : ∀ x, f x = 1 → x = 1) : is_embedding f := is_embedding_of_is_injective @@ -113,7 +113,7 @@ section group_A_B have x₁ * x₂⁻¹ = 1, from H _ this, eq_of_mul_inv_eq_one this) - definition eq_one_of_is_mul_hom [add_group B] {f : A → B} [is_mul_hom f] + definition eq_one_of_is_mul_hom {f : A → B} [is_mul_hom f] [is_embedding f] {a : A} (fa1 : f a = 1) : a = 1 := have f a = f 1, by rewrite [fa1, respect_one f],