From 5cacebcf86fa8ae0754bbf9f379ec05e2f0521ba Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 3 Mar 2016 10:48:27 -0500 Subject: [PATCH] feat(hott): replace assert by have and merge namespace equiv.ops into equiv MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The coercion A ≃ B -> (A -> B) is now in namespace equiv. The notation ⁻¹ for symmetry of equivalences is not supported anymore. Use ⁻¹ᵉ --- hott/algebra/binary.hlean | 2 +- hott/algebra/category/category.hlean | 2 +- hott/algebra/category/functor/yoneda.hlean | 53 +++++++++++++------ .../category/limits/functor_preserve.hlean | 8 +-- hott/algebra/category/precategory.hlean | 2 +- hott/algebra/hott.hlean | 2 +- hott/cubical/cube.hlean | 12 ++--- hott/cubical/squareover.hlean | 2 +- hott/hit/coeq.hlean | 2 +- hott/hit/colimit.hlean | 2 +- hott/hit/pushout.hlean | 2 +- hott/hit/quotient.hlean | 2 +- hott/hit/quotient_functor.hlean | 1 - hott/hit/trunc.hlean | 1 - hott/homotopy/circle.hlean | 4 +- hott/homotopy/connectedness.hlean | 3 +- hott/homotopy/cylinder.hlean | 2 +- hott/homotopy/interval.hlean | 2 +- hott/homotopy/susp.hlean | 4 +- hott/init/equiv.hlean | 18 ++----- hott/init/pathover.hlean | 2 +- hott/init/trunc.hlean | 11 ++-- hott/init/ua.hlean | 2 +- hott/types/arrow.hlean | 2 +- hott/types/eq.hlean | 2 +- hott/types/equiv.hlean | 2 +- hott/types/int/hott.hlean | 2 +- hott/types/lift.hlean | 2 +- hott/types/nat/div.hlean | 46 ++++++++-------- hott/types/pointed.hlean | 3 +- hott/types/pointed2.hlean | 2 +- hott/types/prod.hlean | 2 +- hott/types/pullback.hlean | 2 +- hott/types/sum.hlean | 39 +++++++------- hott/types/trunc.hlean | 1 - hott/types/univ.hlean | 6 +-- tests/lean/extra/597a.hlean | 1 - tests/lean/extra/597b.hlean | 3 +- 38 files changed, 131 insertions(+), 125 deletions(-) diff --git a/hott/algebra/binary.hlean b/hott/algebra/binary.hlean index 423023deb..18a5525cd 100644 --- a/hott/algebra/binary.hlean +++ b/hott/algebra/binary.hlean @@ -104,7 +104,7 @@ namespace is_equiv end end is_equiv namespace equiv - open is_equiv equiv.ops + open is_equiv definition inv_preserve_binary {A B : Type} (f : A ≃ B) (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), mB (f a) (f a') = f (mA a a')) (b b' : B) : f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b') := diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean index c40dfb4da..8200b84e1 100644 --- a/hott/algebra/category/category.hlean +++ b/hott/algebra/category/category.hlean @@ -6,7 +6,7 @@ Author: Jakob von Raumer import .iso -open iso is_equiv equiv eq is_trunc sigma equiv.ops +open iso is_equiv equiv eq is_trunc sigma /- A category is a precategory extended by a witness diff --git a/hott/algebra/category/functor/yoneda.hlean b/hott/algebra/category/functor/yoneda.hlean index dda9e0a56..3a5c79bbc 100644 --- a/hott/algebra/category/functor/yoneda.hlean +++ b/hott/algebra/category/functor/yoneda.hlean @@ -8,10 +8,12 @@ Yoneda embedding and Yoneda lemma import .examples .attributes -open category eq functor prod.ops is_trunc iso is_equiv equiv category.set nat_trans lift +open category eq functor prod.ops is_trunc iso is_equiv category.set nat_trans lift namespace yoneda + universe variables u v + variable {C : Precategory.{u v}} /- These attributes make sure that the fields of the category "set" reduce to the right things However, we don't want to have them globally, because that will unfold the composition g ∘ f @@ -28,7 +30,7 @@ namespace yoneda we use (change_fun) to make sure that (to_fun_ob (yoneda_embedding C) c) will reduce to (hom_functor_left c) instead of (functor_curry_rev_ob (hom_functor C) c) -/ - definition yoneda_embedding [constructor] (C : Precategory) : C ⇒ cset ^c Cᵒᵖ := + definition yoneda_embedding [constructor] (C : Precategory.{u v}) : C ⇒ cset ^c Cᵒᵖ := --(functor_curry_rev !hom_functor) change_fun (functor_curry_rev !hom_functor) @@ -39,17 +41,30 @@ namespace yoneda notation `ɏ` := yoneda_embedding _ - definition yoneda_lemma_hom [constructor] {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ cset) + definition yoneda_lemma_hom_fun [unfold_full] (c : C) (F : Cᵒᵖ ⇒ cset) + (x : trunctype.carrier (F c)) (c' : Cᵒᵖ) : to_fun_ob (ɏ c) c' ⟶ F c' := + begin + esimp [yoneda_embedding], intro f, exact F f x + end + + definition yoneda_lemma_hom_nat (c : C) (F : Cᵒᵖ ⇒ cset) + (x : trunctype.carrier (F c)) {c₁ c₂ : Cᵒᵖ} (f : c₁ ⟶ c₂) + : F f ∘ yoneda_lemma_hom_fun c F x c₁ = yoneda_lemma_hom_fun c F x c₂ ∘ to_fun_hom (ɏ c) f := + begin + esimp [yoneda_embedding], apply eq_of_homotopy, intro f', + refine _ ⬝ ap (λy, to_fun_hom F y x) !(@id_left _ C)⁻¹, + exact ap10 !(@respect_comp Cᵒᵖ cset)⁻¹ x + end + + definition yoneda_lemma_hom [constructor] (c : C) (F : Cᵒᵖ ⇒ cset) (x : trunctype.carrier (F c)) : ɏ c ⟹ F := begin fapply nat_trans.mk, - { intro c', esimp [yoneda_embedding], intro f, exact F f x}, - { intro c' c'' f, esimp [yoneda_embedding], apply eq_of_homotopy, intro f', - refine _ ⬝ ap (λy, to_fun_hom F y x) !(@id_left _ C)⁻¹, - exact ap10 !(@respect_comp Cᵒᵖ cset)⁻¹ x} + { exact yoneda_lemma_hom_fun c F x}, + { intro c₁ c₂ f, exact yoneda_lemma_hom_nat c F x f} end - definition yoneda_lemma_equiv [constructor] {C : Precategory} (c : C) + definition yoneda_lemma_equiv [constructor] (c : C) (F : Cᵒᵖ ⇒ cset) : hom (ɏ c) F ≃ lift (trunctype.carrier (to_fun_ob F c)) := begin fapply equiv.MK, @@ -64,13 +79,13 @@ namespace yoneda rewrite naturality, esimp [yoneda_embedding], rewrite [id_left], apply ap _ !id_left end end}, end - definition yoneda_lemma {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ cset) : + definition yoneda_lemma (c : C) (F : Cᵒᵖ ⇒ cset) : homset (ɏ c) F ≅ functor_lift (F c) := begin apply iso_of_equiv, esimp, apply yoneda_lemma_equiv, end - theorem yoneda_lemma_natural_ob {C : Precategory} (F : Cᵒᵖ ⇒ cset) {c c' : C} (f : c' ⟶ c) + theorem yoneda_lemma_natural_ob (F : Cᵒᵖ ⇒ cset) {c c' : C} (f : c' ⟶ c) (η : ɏ c ⟹ F) : to_fun_hom (functor_lift ∘f F) f (to_hom (yoneda_lemma c F) η) = to_hom (yoneda_lemma c' F) (η ∘n to_fun_hom ɏ f) := @@ -89,7 +104,7 @@ namespace yoneda -- attribute yoneda_lemma functor_lift Precategory_Set precategory_Set homset -- yoneda_embedding nat_trans.compose functor_nat_trans_compose [reducible] -- attribute tlift functor.compose [reducible] - theorem yoneda_lemma_natural_functor.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ cset) + theorem yoneda_lemma_natural_functor (c : C) (F F' : Cᵒᵖ ⇒ cset) (θ : F ⟹ F') (η : to_fun_ob ɏ c ⟹ F) : (functor_lift.{v u} ∘fn θ) c (to_hom (yoneda_lemma c F) η) = proof to_hom (yoneda_lemma c F') (θ ∘n η) qed := @@ -107,20 +122,21 @@ namespace yoneda -- proof _ qed := -- by reflexivity - definition fully_faithful_yoneda_embedding [instance] (C : Precategory) : + open equiv + definition fully_faithful_yoneda_embedding [instance] (C : Precategory.{u v}) : fully_faithful (ɏ : C ⇒ cset ^c Cᵒᵖ) := begin intro c c', fapply is_equiv_of_equiv_of_homotopy, { symmetry, transitivity _, apply @equiv_of_iso (homset _ _), - rexact yoneda_lemma c (ɏ c'), esimp [yoneda_embedding], exact !equiv_lift⁻¹ᵉ}, + exact @yoneda_lemma C c (ɏ c'), esimp [yoneda_embedding], exact !equiv_lift⁻¹ᵉ}, { intro f, apply nat_trans_eq, intro c, apply eq_of_homotopy, intro f', esimp [equiv.symm,equiv.trans], esimp [yoneda_lemma,yoneda_embedding,Opposite], rewrite [id_left,id_right]} end - definition is_embedding_yoneda_embedding (C : Category) : + definition is_embedding_yoneda_embedding (C : Category.{u v}) : is_embedding (ɏ : C → Cᵒᵖ ⇒ cset) := begin intro c c', fapply is_equiv_of_equiv_of_homotopy, @@ -134,15 +150,18 @@ namespace yoneda rewrite [▸*, category.category.id_left], apply id_right} end - definition is_representable {C : Precategory} (F : Cᵒᵖ ⇒ cset) := Σ(c : C), ɏ c ≅ F + definition is_representable (F : Cᵒᵖ ⇒ cset) := Σ(c : C), ɏ c ≅ F section set_option apply.class_instance false - definition is_prop_representable {C : Category} (F : Cᵒᵖ ⇒ cset) + open functor.ops + definition is_prop_representable {C : Category.{u v}} (F : Cᵒᵖ ⇒ cset) : is_prop (is_representable F) := begin fapply is_trunc_equiv_closed, - { exact proof fiber.sigma_char ɏ F qed ⬝e sigma.sigma_equiv_sigma_right (λc, !eq_equiv_iso)}, + { unfold [is_representable], + rexact fiber.sigma_char ɏ F ⬝e sigma.sigma_equiv_sigma_right + (λc, @eq_equiv_iso (cset ^c2 Cᵒᵖ) _ (hom_functor_left c) F)}, { apply function.is_prop_fiber_of_is_embedding, apply is_embedding_yoneda_embedding} end end diff --git a/hott/algebra/category/limits/functor_preserve.hlean b/hott/algebra/category/limits/functor_preserve.hlean index edca7849e..7d84db9d8 100644 --- a/hott/algebra/category/limits/functor_preserve.hlean +++ b/hott/algebra/category/limits/functor_preserve.hlean @@ -52,7 +52,8 @@ namespace category local attribute category.to_precategory [constructor] - definition preserves_existing_limits_yoneda_embedding_lemma [constructor] (y : cone_obj F) + definition preserves_existing_limits_yoneda_embedding_lemma [constructor] + (y : cone_obj F) [H : is_terminal y] {G : Cᵒᵖ ⇒ cset} (η : constant_functor I G ⟹ ɏ ∘f F) : G ⟹ hom_functor_left (cone_to_obj y) := begin @@ -70,15 +71,14 @@ namespace category refine _ ⬝ ap10 (naturality (η i) f) x, rewrite [▸*, id_left]} -- abstracting here fails end --- print preserves_existing_limits_yoneda_embedding_lemma_11 theorem preserves_existing_limits_yoneda_embedding (C : Precategory) : preserves_existing_limits (yoneda_embedding C) := begin intro I F H Gη, induction H with y H, induction Gη with G η, esimp at *, - have lem : Π (i : carrier I), + have lem : Π(i : carrier I), nat_trans_hom_functor_left (natural_map (cone_to_nat y) i) - ∘n preserves_existing_limits_yoneda_embedding_lemma y η = natural_map η i, + ∘n @preserves_existing_limits_yoneda_embedding_lemma I C F y H G η = natural_map η i, begin intro i, apply nat_trans_eq, intro c, apply eq_of_homotopy, intro x, esimp, refine !assoc ⬝ !id_right ⬝ !to_hom_limit_commute diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean index 007375a08..b3a88b12c 100644 --- a/hott/algebra/category/precategory.hlean +++ b/hott/algebra/category/precategory.hlean @@ -5,7 +5,7 @@ Authors: Floris van Doorn -/ import types.trunc types.pi arity -open eq is_trunc pi equiv equiv.ops +open eq is_trunc pi equiv namespace category diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean index 1eab2f961..a4b81d20e 100644 --- a/hott/algebra/hott.hlean +++ b/hott/algebra/hott.hlean @@ -8,7 +8,7 @@ Theorems about algebra specific to HoTT import .group arity types.pi prop_trunc types.unit .bundled -open equiv eq equiv.ops is_trunc unit +open equiv eq is_trunc unit namespace algebra diff --git a/hott/cubical/cube.hlean b/hott/cubical/cube.hlean index 2e0a806bc..51af5b37c 100644 --- a/hott/cubical/cube.hlean +++ b/hott/cubical/cube.hlean @@ -8,7 +8,7 @@ Cubes import .square -open equiv equiv.ops is_equiv sigma sigma.ops +open equiv is_equiv sigma sigma.ops namespace eq @@ -48,7 +48,7 @@ namespace eq definition refl2 : cube hrfl hrfl s₁₀₁ s₁₀₁ hrfl hrfl := by induction s₁₀₁; exact idc - + definition refl3 : cube vrfl vrfl vrfl vrfl s₁₁₀ s₁₁₀ := by induction s₁₁₀; exact idc @@ -169,9 +169,9 @@ namespace eq variables {a₀ a₁ : A} {p₀₀ p₀₂ p₂₀ p₂₂ : a₀ = a₁} {s₁₀ : p₀₀ = p₂₀} {s₁₂ : p₀₂ = p₂₂} {s₀₁ : p₀₀ = p₀₂} {s₂₁ : p₂₀ = p₂₂} (sq : square s₁₀ s₁₂ s₀₁ s₂₁) - + include sq - + definition ids3_cube_of_square : cube (hdeg_square s₀₁) (hdeg_square s₂₁) (hdeg_square s₁₀) (hdeg_square s₁₂) ids ids := by induction p₀₀; induction sq; apply idc @@ -194,7 +194,7 @@ namespace eq definition cube_fill110 : Σ lid, cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ lid s₁₁₂ := begin induction s₀₁₁, induction s₂₁₁, - let fillsq := square_fill_l (eq_of_vdeg_square s₁₀₁) + let fillsq := square_fill_l (eq_of_vdeg_square s₁₀₁) (eq_of_hdeg_square s₁₁₂) (eq_of_vdeg_square s₁₂₁), apply sigma.mk, apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁), @@ -206,7 +206,7 @@ namespace eq definition cube_fill112 : Σ lid, cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ lid := begin induction s₀₁₁, induction s₂₁₁, - let fillsq := square_fill_r (eq_of_vdeg_square s₁₀₁) + let fillsq := square_fill_r (eq_of_vdeg_square s₁₀₁) (eq_of_hdeg_square s₁₁₀) (eq_of_vdeg_square s₁₂₁), apply sigma.mk, apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁), diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean index f9f76513b..e3d048487 100644 --- a/hott/cubical/squareover.hlean +++ b/hott/cubical/squareover.hlean @@ -8,7 +8,7 @@ Squareovers import .square -open eq equiv is_equiv equiv.ops +open eq equiv is_equiv namespace eq diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index eeac11354..d10da154c 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -8,7 +8,7 @@ Declaration of the coequalizer import .quotient_functor types.equiv -open quotient eq equiv equiv.ops is_trunc sigma sigma.ops +open quotient eq equiv is_trunc sigma sigma.ops namespace coeq section diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index 9ab899dd6..f877f4a96 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -7,7 +7,7 @@ Definition of general colimits and sequential colimits. -/ /- definition of a general colimit -/ -open eq nat quotient sigma equiv equiv.ops is_trunc +open eq nat quotient sigma equiv is_trunc namespace colimit section diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index e30863fa0..9eef15b8b 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -8,7 +8,7 @@ Declaration of the pushout import .quotient cubical.square types.sigma -open quotient eq sum equiv equiv.ops is_trunc +open quotient eq sum equiv is_trunc namespace pushout section diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index c91f6fba2..88f320cd5 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -16,7 +16,7 @@ See also .set_quotient import arity cubical.squareover types.arrow cubical.pathover2 types.pointed -open eq equiv sigma sigma.ops equiv.ops pi is_trunc pointed +open eq equiv sigma sigma.ops pi is_trunc pointed namespace quotient diff --git a/hott/hit/quotient_functor.hlean b/hott/hit/quotient_functor.hlean index b5704e9e9..36d09b0ae 100644 --- a/hott/hit/quotient_functor.hlean +++ b/hott/hit/quotient_functor.hlean @@ -104,7 +104,6 @@ section end section - open equiv.ops variables {A : Type} (R : A → A → Type) {B : Type} (Q : B → B → Type) (f : A ≃ B) (k : Πa a' : A, R a a' ≃ Q (f a) (f a')) diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean index 0a123d4b9..1501b2e2a 100644 --- a/hott/hit/trunc.hlean +++ b/hott/hit/trunc.hlean @@ -82,7 +82,6 @@ namespace trunc λxx, trunc.rec_on xx (λx, ap tr (p x)) section - open equiv.ops definition trunc_equiv_trunc [constructor] (f : X ≃ Y) : trunc n X ≃ trunc n Y := equiv.mk _ (is_equiv_trunc_functor n f) end diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index 249d90b5f..ff32cc781 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -10,7 +10,7 @@ import .sphere import types.bool types.int.hott types.equiv import algebra.homotopy_group algebra.hott .connectedness -open eq susp bool sphere_index is_equiv equiv equiv.ops is_trunc pi algebra homotopy +open eq susp bool sphere_index is_equiv equiv is_trunc pi algebra homotopy definition circle : Type₀ := sphere 1 @@ -235,7 +235,7 @@ namespace circle preserve_binary_of_inv_preserve base_eq_base_equiv concat (@add ℤ _) decode_add p q --the carrier of π₁(S¹) is the set-truncation of base = base. - open algebra trunc equiv.ops + open algebra trunc definition fg_carrier_equiv_int : π[1](S¹.) ≃ ℤ := trunc_equiv_trunc 0 base_eq_base_equiv ⬝e @(trunc_equiv ℤ _) proof _ qed diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index 9ed5e68dd..f30d809b8 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -275,10 +275,11 @@ namespace homotopy end open trunc_index + -- Corollary 8.2.2 theorem is_conn_sphere [instance] (n : ℕ₋₁) : is_conn (n..-1) (sphere n) := begin induction n with n IH, - { apply is_trunc_trunc}, + { apply minus_two_conn}, { rewrite [succ_sub_one, sphere.sphere_succ], apply is_conn_susp} end diff --git a/hott/homotopy/cylinder.hlean b/hott/homotopy/cylinder.hlean index 33df53e9a..62f661c67 100644 --- a/hott/homotopy/cylinder.hlean +++ b/hott/homotopy/cylinder.hlean @@ -8,7 +8,7 @@ Declaration of mapping cylinders import hit.quotient -open quotient eq sum equiv equiv.ops +open quotient eq sum equiv namespace cylinder section diff --git a/hott/homotopy/interval.hlean b/hott/homotopy/interval.hlean index 05bb96132..154511c4e 100644 --- a/hott/homotopy/interval.hlean +++ b/hott/homotopy/interval.hlean @@ -7,7 +7,7 @@ Declaration of the interval -/ import .susp types.eq types.prod cubical.square -open eq susp unit equiv equiv.ops is_trunc nat prod +open eq susp unit equiv is_trunc nat prod definition interval : Type₀ := susp unit diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index d40c877c9..3d6cadefe 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -8,7 +8,7 @@ Declaration of suspension import hit.pushout types.pointed cubical.square -open pushout unit eq equiv equiv.ops +open pushout unit eq equiv definition susp (A : Type) : Type := pushout (λ(a : A), star) (λ(a : A), star) @@ -220,7 +220,7 @@ namespace susp end definition susp_adjoint_loop_nat_left (f : Y →* Ω Z) (g : X →* Y) - : (susp_adjoint_loop X Z)⁻¹ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ f ∘* psusp_functor g := + : (susp_adjoint_loop X Z)⁻¹ᵉ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ᵉ f ∘* psusp_functor g := begin esimp [susp_adjoint_loop], refine _ ⬝* !passoc⁻¹*, diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index fe5198169..0c9158419 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -269,14 +269,11 @@ namespace eq definition cast_inv {A B : Type} (p : A = B) (b : B) : cast p⁻¹ b = (cast p)⁻¹ b := idp end eq -namespace equiv - namespace ops - attribute to_fun [coercion] - end ops - open equiv.ops - attribute to_is_equiv [instance] +infix ` ≃ `:25 := equiv +attribute equiv.to_is_equiv [instance] - infix ` ≃ `:25 := equiv +namespace equiv + attribute to_fun [coercion] section variables {A B C : Type} @@ -395,17 +392,12 @@ namespace equiv end - - namespace ops - postfix ⁻¹ := equiv.symm -- overloaded notation for inverse - end ops - infixl ` ⬝pe `:75 := equiv_of_equiv_of_eq infixl ` ⬝ep `:75 := equiv_of_eq_of_equiv end equiv -open equiv equiv.ops +open equiv namespace is_equiv definition is_equiv_of_equiv_of_homotopy [constructor] {A B : Type} (f : A ≃ B) diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index fc24d191b..3eeb04432 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -9,7 +9,7 @@ Basic theorems about pathovers prelude import .path .equiv -open equiv is_equiv equiv.ops function +open equiv is_equiv function variables {A A' : Type} {B B' : A → Type} {B'' : A' → Type} {C : Π⦃a⦄, B a → Type} {a a₂ a₃ a₄ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄} {p₁₃ : a = a₃} diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 196697050..e1e01f139 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -278,11 +278,12 @@ namespace is_trunc theorem is_trunc_is_equiv_closed (n : ℕ₋₂) (f : A → B) [H : is_equiv f] [HA : is_trunc n A] : is_trunc n B := - trunc_index.rec_on n - (λA (HA : is_contr A) B f (H : is_equiv f), is_contr_is_equiv_closed f) - (λn IH A (HA : is_trunc n.+1 A) B f (H : is_equiv f), @is_trunc_succ_intro _ _ (λ x y : B, - IH (f⁻¹ x = f⁻¹ y) _ (x = y) (ap f⁻¹)⁻¹ !is_equiv_inv)) - A HA B f H + begin + revert A HA B f H, induction n with n IH: intros, + { exact is_contr_is_equiv_closed f}, + { apply is_trunc_succ_intro, intro x y, + exact IH (f⁻¹ x = f⁻¹ y) _ (x = y) (ap f⁻¹)⁻¹ !is_equiv_inv} + end definition is_trunc_is_equiv_closed_rev (n : ℕ₋₂) (f : A → B) [H : is_equiv f] [HA : is_trunc n B] : is_trunc n A := diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean index fba2c1dd5..5ece71c4c 100644 --- a/hott/init/ua.hlean +++ b/hott/init/ua.hlean @@ -8,7 +8,7 @@ Ported from Coq HoTT prelude import .equiv -open eq equiv is_equiv equiv.ops +open eq equiv is_equiv --Ensure that the types compared are in the same universe section diff --git a/hott/types/arrow.hlean b/hott/types/arrow.hlean index 34fcc74bd..91a892eb1 100644 --- a/hott/types/arrow.hlean +++ b/hott/types/arrow.hlean @@ -9,7 +9,7 @@ Theorems about arrow types (function spaces) import types.pi -open eq equiv is_equiv funext pi equiv.ops is_trunc unit +open eq equiv is_equiv funext pi is_trunc unit namespace pi diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index b2c0c688a..bb6f04be5 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -8,7 +8,7 @@ Theorems about path types (identity types) -/ import types.sigma -open eq sigma sigma.ops equiv is_equiv equiv.ops is_trunc +open eq sigma sigma.ops equiv is_equiv is_trunc -- TODO: Rename transport_eq_... and pathover_eq_... to eq_transport_... and eq_pathover_... diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 2fce2cfa2..a7f122714 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -9,7 +9,7 @@ Theorems about the types equiv and is_equiv import .fiber .arrow arity ..prop_trunc -open eq is_trunc sigma sigma.ops pi fiber function equiv equiv.ops +open eq is_trunc sigma sigma.ops pi fiber function equiv namespace is_equiv variables {A B : Type} (f : A → B) [H : is_equiv f] diff --git a/hott/types/int/hott.hlean b/hott/types/int/hott.hlean index 073439408..7507c5604 100644 --- a/hott/types/int/hott.hlean +++ b/hott/types/int/hott.hlean @@ -7,7 +7,7 @@ Theorems about the integers specific to HoTT -/ import .basic types.eq arity algebra.bundled -open core eq is_equiv equiv equiv.ops algebra is_trunc +open core eq is_equiv equiv algebra is_trunc open nat (hiding pred) namespace int diff --git a/hott/types/lift.hlean b/hott/types/lift.hlean index 26236eeee..86f90da02 100644 --- a/hott/types/lift.hlean +++ b/hott/types/lift.hlean @@ -7,7 +7,7 @@ Theorems about lift -/ import ..function -open eq equiv equiv.ops is_equiv is_trunc pointed +open eq equiv is_equiv is_trunc pointed namespace lift diff --git a/hott/types/nat/div.hlean b/hott/types/nat/div.hlean index 3884181ec..8bd1fc4e3 100644 --- a/hott/types/nat/div.hlean +++ b/hott/types/nat/div.hlean @@ -168,15 +168,15 @@ begin intro x IH, show succ x = succ x / y * y + succ x % y, from if H1 : succ x < y then - assert H2 : succ x / y = 0, from div_eq_zero_of_lt H1, - assert H3 : succ x % y = succ x, from mod_eq_of_lt H1, + have H2 : succ x / y = 0, from div_eq_zero_of_lt H1, + have H3 : succ x % y = succ x, from mod_eq_of_lt H1, begin rewrite [H2, H3, zero_mul, zero_add] end else have H2 : y ≤ succ x, from le_of_not_gt H1, - assert H3 : succ x / y = succ ((succ x - y) / y), from div_eq_succ_sub_div H H2, - assert H4 : succ x % y = (succ x - y) % y, from mod_eq_sub_mod H H2, + have H3 : succ x / y = succ ((succ x - y) / y), from div_eq_succ_sub_div H H2, + have H4 : succ x % y = (succ x - y) % y, from mod_eq_sub_mod H H2, have H5 : succ x - y < succ x, from sub_lt !succ_pos H, - assert H6 : succ x - y ≤ x, from le_of_lt_succ H5, + have H6 : succ x - y ≤ x, from le_of_lt_succ H5, (calc succ x / y * y + succ x % y = succ ((succ x - y) / y) * y + succ x % y : by rewrite H3 @@ -213,7 +213,7 @@ by_cases_zero_pos n assume npos : n > 0, assume H1 : (m + i) % n = (k + i) % n, have H2 : (m + i % n) % n = (k + i % n) % n, by rewrite [*add_mod_mod, H1], - assert H3 : (m + i % n + (n - i % n)) % n = (k + i % n + (n - i % n)) % n, + have H3 : (m + i % n + (n - i % n)) % n = (k + i % n + (n - i % n)) % n, from add_mod_eq_add_mod_right _ H2, begin revert H3, @@ -301,11 +301,11 @@ theorem mul_mod_eq_mul_mod_mod (m n k : nat) : (m * n) % k = (m * (n % k)) % k : !mul.comm ▸ !mul.comm ▸ !mul_mod_eq_mod_mul_mod protected theorem div_one (n : ℕ) : n / 1 = n := -assert n / 1 * 1 + n % 1 = n, from !eq_div_mul_add_mod⁻¹, +have n / 1 * 1 + n % 1 = n, from !eq_div_mul_add_mod⁻¹, begin rewrite [-this at {2}, mul_one, mod_one] end protected theorem div_self {n : ℕ} (H : n > 0) : n / n = 1 := -assert (n * 1) / (n * 1) = 1 / 1, from !nat.mul_div_mul_left H, +have (n * 1) / (n * 1) = 1 / 1, from !nat.mul_div_mul_left H, by rewrite [nat.div_one at this, -this, *mul_one] theorem div_mul_cancel_of_mod_eq_zero {m n : ℕ} (H : m % n = 0) : m / n * n = m := @@ -451,11 +451,11 @@ end lemma le_of_dvd {m n : nat} : n > 0 → m ∣ n → m ≤ n := assume (h₁ : n > 0) (h₂ : m ∣ n), -assert h₃ : n % m = 0, from mod_eq_zero_of_dvd h₂, +have h₃ : n % m = 0, from mod_eq_zero_of_dvd h₂, by_contradiction (λ nle : ¬ m ≤ n, have h₄ : m > n, from lt_of_not_ge nle, - assert h₅ : n % m = n, from mod_eq_of_lt h₄, + have h₅ : n % m = n, from mod_eq_of_lt h₄, begin rewrite h₃ at h₅, subst n, exact absurd h₁ (lt.irrefl 0) @@ -516,7 +516,7 @@ lt_of_mul_lt_mul_right (calc ... < n * k : H) protected theorem lt_mul_of_div_lt {m n k : ℕ} (H1 : k > 0) (H2 : m / k < n) : m < n * k := -assert H3 : succ (m / k) * k ≤ n * k, from !mul_le_mul_right (succ_le_of_lt H2), +have H3 : succ (m / k) * k ≤ n * k, from !mul_le_mul_right (succ_le_of_lt H2), have H4 : m / k * k + k ≤ n * k, by rewrite [succ_mul at H3]; apply H3, calc m = m / k * k + m % k : eq_div_mul_add_mod @@ -567,28 +567,28 @@ nat.strong_rec_on a (λ a ih, let k₁ := a / (b*c) in let k₂ := a %(b*c) in - assert bc_pos : b*c > 0, from mul_pos `b > 0` `c > 0`, - assert k₂ < b * c, from mod_lt _ bc_pos, - assert k₂ ≤ a, from !mod_le, + have bc_pos : b*c > 0, from mul_pos `b > 0` `c > 0`, + have k₂ < b * c, from mod_lt _ bc_pos, + have k₂ ≤ a, from !mod_le, sum.elim (eq_sum_lt_of_le this) (suppose k₂ = a, - assert i₁ : a < b * c, by rewrite -this; assumption, - assert k₁ = 0, from div_eq_zero_of_lt i₁, - assert a / b < c, by rewrite [mul.comm at i₁]; exact nat.div_lt_of_lt_mul i₁, + have i₁ : a < b * c, by rewrite -this; assumption, + have k₁ = 0, from div_eq_zero_of_lt i₁, + have a / b < c, by rewrite [mul.comm at i₁]; exact nat.div_lt_of_lt_mul i₁, begin rewrite [`k₁ = 0`], show (a / b) / c = 0, from div_eq_zero_of_lt `a / b < c` end) (suppose k₂ < a, - assert a = k₁*(b*c) + k₂, from eq_div_mul_add_mod a (b*c), - assert a / b = k₁*c + k₂ / b, by + have a = k₁*(b*c) + k₂, from eq_div_mul_add_mod a (b*c), + have a / b = k₁*c + k₂ / b, by rewrite [this at {1}, mul.comm b c at {2}, -mul.assoc, add.comm, add_mul_div_self `b > 0`, add.comm], - assert e₁ : (a / b) / c = k₁ + (k₂ / b) / c, by + have e₁ : (a / b) / c = k₁ + (k₂ / b) / c, by rewrite [this, add.comm, add_mul_div_self `c > 0`, add.comm], - assert e₂ : (k₂ / b) / c = k₂ / (b * c), from ih k₂ `k₂ < a`, - assert e₃ : k₂ / (b * c) = 0, from div_eq_zero_of_lt `k₂ < b * c`, - assert (k₂ / b) / c = 0, by rewrite [e₂, e₃], + have e₂ : (k₂ / b) / c = k₂ / (b * c), from ih k₂ `k₂ < a`, + have e₃ : k₂ / (b * c) = 0, from div_eq_zero_of_lt `k₂ < b * c`, + have (k₂ / b) / c = 0, by rewrite [e₂, e₃], show (a / b) / c = k₁, by rewrite [e₁, this])) protected lemma div_div_eq_div_mul (a b c : nat) : (a / b) / c = a / (b * c) := diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 5b2538ae8..178fd7dd4 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -7,7 +7,7 @@ Ported from Coq HoTT -/ import arity .eq .bool .unit .sigma .nat.basic prop_trunc -open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra equiv.ops sigma.ops +open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra sigma.ops structure pointed [class] (A : Type) := (point : A) @@ -97,7 +97,6 @@ namespace pointed definition iterated_loop_space [unfold 3] (A : Type) [H : pointed A] (n : ℕ) : Type := Ω[n] (pointed.mk' A) - open equiv.ops definition pType_eq {A B : Type*} (f : A ≃ B) (p : f pt = pt) : A = B := begin cases A with A a, cases B with B b, esimp at *, diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean index fabe73695..aee4af759 100644 --- a/hott/types/pointed2.hlean +++ b/hott/types/pointed2.hlean @@ -9,7 +9,7 @@ Ported from Coq HoTT import .equiv cubical.square -open eq is_equiv equiv equiv.ops pointed is_trunc +open eq is_equiv equiv pointed is_trunc -- structure pequiv (A B : Type*) := -- (to_pmap : A →* B) diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index 8e5375340..c2db35d3e 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -7,7 +7,7 @@ Ported from Coq HoTT Theorems about products -/ -open eq equiv is_equiv is_trunc prod prod.ops unit equiv.ops +open eq equiv is_equiv is_trunc prod prod.ops unit variables {A A' B B' C D : Type} {P Q : A → Type} {a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B} diff --git a/hott/types/pullback.hlean b/hott/types/pullback.hlean index bbf0c86ed..f2ae1ca65 100644 --- a/hott/types/pullback.hlean +++ b/hott/types/pullback.hlean @@ -7,7 +7,7 @@ Theorems about pullbacks -/ import cubical.square -open eq equiv is_equiv function equiv.ops prod unit is_trunc sigma +open eq equiv is_equiv function prod unit is_trunc sigma variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ : Type} (f₁₀ : A₀₀ → A₂₀) (f₃₀ : A₂₀ → A₄₀) diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean index 02fa076ae..270062c4d 100644 --- a/hott/types/sum.hlean +++ b/hott/types/sum.hlean @@ -8,7 +8,7 @@ Theorems about sums/coproducts/disjoint unions import .pi .equiv logic -open lift eq is_equiv equiv equiv.ops prod prod.ops is_trunc sigma bool +open lift eq is_equiv equiv prod prod.ops is_trunc sigma bool namespace sum universe variables u v u' v' @@ -226,9 +226,8 @@ namespace sum end definition unit_sum_equiv_cancel_inv (b : B) : - unit_sum_equiv_cancel_map H (unit_sum_equiv_cancel_map H⁻¹ b) = b := + unit_sum_equiv_cancel_map H (unit_sum_equiv_cancel_map H⁻¹ᵉ b) = b := begin - have HH : to_fun H⁻¹ = (to_fun H)⁻¹, begin cases H, reflexivity end, esimp[unit_sum_equiv_cancel_map], apply sum.rec, { intro x, cases x with u Hu, esimp, apply sum.rec, { intro x, exfalso, cases x with u' Hu', apply empty_of_inl_eq_inr, @@ -238,28 +237,28 @@ namespace sum ... = H⁻¹ (H (inr _)) : {Hu⁻¹} ... = inr _ : to_left_inv H }, { intro x, cases x with b' Hb', esimp, cases sum.mem_cases (H⁻¹ (inr b)) with x x, - { cases x with u' Hu', cases u', apply eq_of_inr_eq_inr, rewrite -HH at Hu', - calc inr b' = H (inl ⋆) : Hb'⁻¹ - ... = H (H⁻¹ (inr b)) : {(ap (to_fun H) Hu')⁻¹} - ... = inr b : to_right_inv H (inr b) }, - { exfalso, cases x with a Ha, rewrite -HH at Ha, apply empty_of_inl_eq_inr, + { cases x with u' Hu', cases u', apply eq_of_inr_eq_inr, + calc inr b' = H (inl ⋆) : Hb'⁻¹ + ... = H (H⁻¹ (inr b)) : (ap (to_fun H) Hu')⁻¹ + ... = inr b : to_right_inv H (inr b)}, + { exfalso, cases x with a Ha, apply empty_of_inl_eq_inr, cases u, apply concat, apply Hu⁻¹, apply concat, rotate 1, apply !(to_right_inv H), - apply ap (to_fun H), krewrite -HH, + apply ap (to_fun H), apply concat, rotate 1, apply Ha⁻¹, apply ap inr, esimp, apply sum.rec, intro x, exfalso, apply empty_of_inl_eq_inr, apply concat, exact x.2⁻¹, apply Ha, intro x, cases x with a' Ha', esimp, apply eq_of_inr_eq_inr, apply Ha'⁻¹ ⬝ Ha } } }, { intro x, cases x with b' Hb', esimp, apply eq_of_inr_eq_inr, refine Hb'⁻¹ ⬝ _, - cases sum.mem_cases (to_fun H⁻¹ (inr b)) with x x, - { cases x with u Hu, esimp, cases sum.mem_cases (to_fun H⁻¹ (inl ⋆)) with x x, + cases sum.mem_cases (to_fun H⁻¹ᵉ (inr b)) with x x, + { cases x with u Hu, esimp, cases sum.mem_cases (to_fun H⁻¹ᵉ (inl ⋆)) with x x, { cases x with u' Hu', exfalso, apply empty_of_inl_eq_inr, - calc inl ⋆ = H (H⁻¹ (inl ⋆)) : (to_right_inv H (inl ⋆))⁻¹ - ... = H (inl u') : {ap H Hu'} - ... = H (inl u) : {!is_prop.elim} - ... = H (H⁻¹ (inr b)) : {ap H Hu⁻¹} - ... = inr b : to_right_inv H (inr b) }, + calc inl ⋆ = H (H⁻¹ (inl ⋆)) : (to_right_inv H (inl ⋆))⁻¹ + ... = H (inl u') : ap H Hu' + ... = H (inl u) : by rewrite [is_prop.elim u' u] + ... = H (H⁻¹ᵉ (inr b)) : ap H Hu⁻¹ + ... = inr b : to_right_inv H (inr b) }, { cases x with a Ha, exfalso, apply empty_of_inl_eq_inr, - apply concat, rotate 1, exact Hb', krewrite HH at Ha, + apply concat, rotate 1, exact Hb', have Ha' : inl ⋆ = H (inr a), by apply !(to_right_inv H)⁻¹ ⬝ ap H Ha, apply concat Ha', apply ap H, apply ap inr, apply sum.rec, intro x, cases x with u' Hu', esimp, apply sum.rec, @@ -269,15 +268,15 @@ namespace sum intro x, exfalso, cases x with a'' Ha'', apply empty_of_inl_eq_inr, apply Hu⁻¹ ⬝ Ha'', } }, { cases x with a' Ha', esimp, refine _ ⬝ !(to_right_inv H), apply ap H, - rewrite -HH, apply Ha'⁻¹ } } + apply Ha'⁻¹ } } end definition unit_sum_equiv_cancel : A ≃ B := begin fapply equiv.MK, apply unit_sum_equiv_cancel_map H, - apply unit_sum_equiv_cancel_map H⁻¹, + apply unit_sum_equiv_cancel_map H⁻¹ᵉ, intro b, apply unit_sum_equiv_cancel_inv, - { intro a, have H = (H⁻¹)⁻¹, from !equiv.symm_symm⁻¹, rewrite this at {2}, + { intro a, have H = (H⁻¹ᵉ)⁻¹ᵉ, from !equiv.symm_symm⁻¹, rewrite this at {2}, apply unit_sum_equiv_cancel_inv } end diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 619087808..25d62e781 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -428,7 +428,6 @@ namespace trunc { exact (IH _ _ _)}}} end - open equiv.ops definition unique_choice {P : A → Type} [H : Πa, is_prop (P a)] (f : Πa, ∥ P a ∥) (a : A) : P a := !trunc_equiv (f a) diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean index 0f3129cd1..bf396ba67 100644 --- a/hott/types/univ.hlean +++ b/hott/types/univ.hlean @@ -10,7 +10,7 @@ Theorems about the universe import .bool .trunc .lift .pullback -open is_trunc bool lift unit eq pi equiv equiv.ops sum sigma fiber prod pullback is_equiv sigma.ops +open is_trunc bool lift unit eq pi equiv sum sigma fiber prod pullback is_equiv sigma.ops pointed namespace univ @@ -117,9 +117,9 @@ namespace univ (λb, sigma_equiv_sigma_right (λX, !comm_equiv_nondep)) ... ≃ Σb (v : ΣX, X), v.1 = fiber f b : sigma_equiv_sigma_right - (λb, !sigma_assoc_equiv⁻¹) + (λb, !sigma_assoc_equiv⁻¹ᵉ) ... ≃ Σb (Y : Type*), Y = fiber f b : sigma_equiv_sigma_right - (λb, sigma_equiv_sigma (pType.sigma_char)⁻¹ + (λb, sigma_equiv_sigma (pType.sigma_char)⁻¹ᵉ (λv, sigma.rec_on v (λx y, equiv.refl))) ... ≃ Σ(Y : Type*) b, Y = fiber f b : sigma_comm_equiv ... ≃ pullback pType.carrier (fiber f) : !pullback.sigma_char⁻¹ᵉ diff --git a/tests/lean/extra/597a.hlean b/tests/lean/extra/597a.hlean index 4bed44674..66769a3b6 100644 --- a/tests/lean/extra/597a.hlean +++ b/tests/lean/extra/597a.hlean @@ -1,4 +1,3 @@ open equiv -open equiv.ops constants (A B : Type₀) (f : A ≃ B) definition foo : A → B := f diff --git a/tests/lean/extra/597b.hlean b/tests/lean/extra/597b.hlean index c7bdb2583..41c23257c 100644 --- a/tests/lean/extra/597b.hlean +++ b/tests/lean/extra/597b.hlean @@ -1,4 +1,3 @@ -open equiv --- open equiv.ops +-- open equiv constants (A B : Type₀) (f : A ≃ B) definition foo : A → B := f -- should fail