From 467001c0a9a51e0d95ae0940cbaefdbc1e03b873 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 13 Jul 2016 09:39:16 +0100 Subject: [PATCH] feat(hott): minor changes --- hott/algebra/homotopy_group.hlean | 10 +++++----- hott/hit/two_quotient.hlean | 2 +- hott/homotopy/LES_of_homotopy_groups.hlean | 1 - hott/homotopy/homotopy_group.hlean | 9 +++++++++ hott/homotopy/wedge.hlean | 2 +- hott/init/path.hlean | 2 +- hott/types/fin.hlean | 2 ++ library/data/set/basic.lean | 2 +- 8 files changed, 20 insertions(+), 10 deletions(-) diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 0ce6b6a87..54ed467f6 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -19,8 +19,8 @@ namespace eq definition homotopy_group [reducible] (n : ℕ) (A : Type*) : Type := phomotopy_group n A - notation `π*[`:95 n:0 `] `:0 := phomotopy_group n - notation `π[`:95 n:0 `] `:0 := homotopy_group n + notation `π*[`:95 n:0 `]`:0 := phomotopy_group n + notation `π[`:95 n:0 `]`:0 := homotopy_group n definition group_homotopy_group [instance] [constructor] [reducible] (n : ℕ) (A : Type*) : group (π[succ n] A) := @@ -126,8 +126,8 @@ namespace eq definition homotopy_group_functor (n : ℕ) {A B : Type*} (f : A →* B) : π[n] A → π[n] B := phomotopy_group_functor n f - notation `π→*[`:95 n:0 `] `:0 := phomotopy_group_functor n - notation `π→[`:95 n:0 `] `:0 := homotopy_group_functor n + notation `π→*[`:95 n:0 `]`:0 := phomotopy_group_functor n + notation `π→[`:95 n:0 `]`:0 := homotopy_group_functor n definition phomotopy_group_functor_phomotopy [constructor] (n : ℕ) {A B : Type*} {f g : A →* B} (p : f ~* g) : π→*[n] f ~* π→*[n] g := @@ -267,6 +267,6 @@ namespace eq exact ap tr !con_inv end - notation `π→g[`:95 n:0 ` +1] `:0 f:95 := homotopy_group_homomorphism n f + notation `π→g[`:95 n:0 ` +1]`:0 := homotopy_group_homomorphism n end eq diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index 6b974c261..0919efe09 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -1,4 +1,4 @@ -/- + /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index 41844f951..19e7e6bfb 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -76,7 +76,6 @@ We get the long exact sequence of homotopy groups by taking the set-truncation o import .chain_complex algebra.homotopy_group eq2 open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function sum - /-------------- PART 1 --------------/ diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean index fcc6ae4c5..1331bc036 100644 --- a/hott/homotopy/homotopy_group.hlean +++ b/hott/homotopy/homotopy_group.hlean @@ -53,6 +53,15 @@ namespace is_trunc [H : is_conn_fun n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) := @(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt) + theorem homotopy_group_trunc_of_le (A : Type*) (n k : ℕ) (H : k ≤ n) + : π*[k] (ptrunc n A) ≃* π*[k] A := + begin + refine !phomotopy_group_pequiv_loop_ptrunc ⬝e* _, + refine loopn_pequiv_loopn _ (ptrunc_ptrunc_pequiv_left _ _) ⬝e* _, + exact of_nat_le_of_nat H, + exact !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, + end + /- Corollaries of the LES of homotopy groups -/ local attribute comm_group.to_group [coercion] local attribute is_equiv_tinverse [instance] diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean index a70f8799b..d159c9ccd 100644 --- a/hott/homotopy/wedge.hlean +++ b/hott/homotopy/wedge.hlean @@ -3,7 +3,7 @@ Copyright (c) 2016 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jakob von Raumer, Ulrik Buchholtz -The Wedge Sum of Two pType Types +The Wedge Sum of Two Pointed Types -/ import hit.pointed_pushout .connectedness types.unit diff --git a/hott/init/path.hlean b/hott/init/path.hlean index bc7cf478e..c7114d9b6 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -49,7 +49,7 @@ namespace eq definition con_idp [unfold_full] (p : x = y) : p ⬝ idp = p := idp - -- The identity path is a right unit. + -- The identity path is a left unit. definition idp_con [unfold 4] (p : x = y) : idp ⬝ p = p := by induction p; reflexivity diff --git a/hott/types/fin.hlean b/hott/types/fin.hlean index 67b8274cf..534e4d385 100644 --- a/hott/types/fin.hlean +++ b/hott/types/fin.hlean @@ -39,6 +39,8 @@ begin intro p, induction p, apply ap (mk i), apply !is_prop.elim end +definition fin_eq := @eq_of_veq + definition eq_of_veq_refl (i : fin n) : eq_of_veq (refl (val i)) = idp := !is_prop.elim diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index bcef05ade..44a6253cc 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -496,7 +496,7 @@ end /- set difference -/ definition diff (s t : set X) : set X := {x ∈ s | x ∉ t} -infix `\`:70 := diff +infix ` \ `:70 := diff theorem mem_diff {s t : set X} {x : X} (H1 : x ∈ s) (H2 : x ∉ t) : x ∈ s \ t := and.intro H1 H2