From 4ba4929cd7c3188371e4633bb4fcd3e1ecfdd49e Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 30 Jun 2017 15:29:52 +0100 Subject: [PATCH] simplify definition of loop_ptrunc_maxm2_pequiv --- homotopy/strunc.hlean | 4 ++-- pointed.hlean | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean index 3be732f..4de0e9d 100644 --- a/homotopy/strunc.hlean +++ b/homotopy/strunc.hlean @@ -42,8 +42,8 @@ definition loop_ptrunc_maxm2_pequiv (k : ℤ) (X : Type*) : begin induction k with k k, { exact loop_ptrunc_pequiv k X }, - { refine _ ⬝e* (pequiv_punit_of_is_contr _ !is_trunc_trunc)⁻¹ᵉ*, - apply @loop_pequiv_punit_of_is_set, + { refine pequiv_of_is_contr _ _ _ !is_trunc_trunc, + apply is_contr_loop, cases k with k, { change is_set (trunc 0 X), apply _ }, { change is_set (trunc -2 X), apply _ }} diff --git a/pointed.hlean b/pointed.hlean index 4214dc7..f1e1e85 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -195,6 +195,9 @@ namespace pointed definition is_contr_loop (A : Type*) [is_set A] : is_contr (Ω A) := is_contr.mk idp (λa, !is_prop.elim) + definition pequiv_of_is_contr (A B : Type*) (HA : is_contr A) (HB : is_contr B) : A ≃* B := + pequiv_punit_of_is_contr A _ ⬝e* (pequiv_punit_of_is_contr B _)⁻¹ᵉ* + definition loop_pequiv_punit_of_is_set (X : Type*) [is_set X] : Ω X ≃* punit := pequiv_punit_of_is_contr _ (is_contr_loop X)