From 98fb55e428ca804c146eee25e91a277be5369b40 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 20 Sep 2018 01:48:55 +0200 Subject: [PATCH] fix two errors in the hott library --- hott/algebra/group_power.hlean | 4 ++-- hott/homotopy/freudenthal.hlean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/hott/algebra/group_power.hlean b/hott/algebra/group_power.hlean index fe652e030..f1b5a3c7a 100644 --- a/hott/algebra/group_power.hlean +++ b/hott/algebra/group_power.hlean @@ -12,7 +12,7 @@ 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 .homomorphism .group_theory -open algebra +open algebra eq namespace algebra variables {A B : Type} @@ -172,7 +172,7 @@ theorem gpow_comm (a : A) (i j : ℤ) : gpow a i * gpow a j = gpow a j * gpow a by rewrite [-*gpow_add, add.comm] lemma gpow_neg (a : A) : Π(n : ℤ), gpow a (-n) = (gpow a n)⁻¹ -| (of_nat n) := by cases n with n; rewrite [gpow_zero,one_inv]; reflexivity +| (of_nat n) := begin cases n with n, exact !one_inv⁻¹, reflexivity end | -[1+n] := by rewrite [↑gpow at {2}, inv_inv] lemma inv_gpow (a : A) : Π(n : ℤ), gpow a⁻¹ n = (gpow a n)⁻¹ diff --git a/hott/homotopy/freudenthal.hlean b/hott/homotopy/freudenthal.hlean index a7806ea8b..65507312a 100644 --- a/hott/homotopy/freudenthal.hlean +++ b/hott/homotopy/freudenthal.hlean @@ -192,7 +192,7 @@ begin { exact equiv_of_pequiv (freudenthal_homotopy_group_pequiv H A)}, { intro g h, refine _ ⬝ !homotopy_group_pequiv_loop_ptrunc_inv_con, - apply ap !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, + refine ap !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ* _, refine ap (loopn_pequiv_loopn _ _) _ ⬝ !loopn_pequiv_loopn_con, refine ap !homotopy_group_pequiv_loop_ptrunc _ ⬝ !homotopy_group_pequiv_loop_ptrunc_con, apply homotopy_group_succ_in_con}