From 8db4676c465d9c938e71d84992635dbfa6dd8981 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 11 Apr 2016 13:11:59 -0400 Subject: [PATCH] feat(hott): various changes and additions in the HoTT library Add more theorems about mapping cylinders, fibers, truncated 2-quotient, truncated univalence, pre/postcomposition with an iso in a precategory. renamings: equiv.refl -> equiv.rfl and equiv_eq <-> equiv_eq' --- hott/algebra/category/constructions/set.hlean | 4 +- hott/algebra/category/groupoid.hlean | 22 +++-- hott/algebra/category/iso.hlean | 32 +++++++ hott/algebra/e_closure.hlean | 93 +++++++++++++------ hott/algebra/homotopy_group.hlean | 55 +++++++++-- hott/algebra/ring.hlean | 7 ++ hott/eq2.hlean | 8 ++ hott/hit/pushout.hlean | 7 +- hott/hit/quotient.hlean | 5 + hott/hit/two_quotient.hlean | 7 +- hott/homotopy/cylinder.hlean | 54 ++++++++++- hott/homotopy/hopf.hlean | 10 +- hott/homotopy/sphere.hlean | 4 +- hott/homotopy/susp.hlean | 18 ++-- hott/init/equiv.hlean | 17 +++- hott/init/path.hlean | 13 ++- hott/init/pointed.hlean | 5 + hott/init/ua.hlean | 6 +- hott/types/arrow.hlean | 6 +- hott/types/eq.hlean | 6 +- hott/types/equiv.hlean | 27 ++++-- hott/types/fiber.hlean | 16 +++- hott/types/int/hott.hlean | 2 +- hott/types/lift.hlean | 8 +- hott/types/pi.hlean | 4 +- hott/types/pointed.hlean | 30 ++++-- hott/types/prod.hlean | 4 +- hott/types/sigma.hlean | 19 ++-- hott/types/sum.hlean | 4 +- hott/types/trunc.hlean | 42 +++++++++ hott/types/univ.hlean | 2 +- library/theories/move.lean | 11 ++- 32 files changed, 435 insertions(+), 113 deletions(-) diff --git a/hott/algebra/category/constructions/set.hlean b/hott/algebra/category/constructions/set.hlean index 826bee75f..fc51ac1bc 100644 --- a/hott/algebra/category/constructions/set.hlean +++ b/hott/algebra/category/constructions/set.hlean @@ -44,7 +44,7 @@ namespace category : is_equiv (@iso_of_equiv A B) := adjointify _ (λf, equiv_of_iso f) (λf, proof iso_eq idp qed) - (λf, equiv_eq idp) + (λf, equiv_eq' idp) local attribute is_equiv_iso_of_equiv [instance] @@ -60,7 +60,7 @@ namespace category (ap10 (to_right_inverse f)) (ap10 (to_left_inverse f)) qed) (λf, proof iso_eq idp qed) - (λf, proof equiv_eq idp qed) + (λf, proof equiv_eq' idp qed) definition equiv_eq_iso (A B : set) : (A ≃ B) = (A ≅ B) := ua !equiv_equiv_iso diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean index 4642a7d9a..03294e446 100644 --- a/hott/algebra/category/groupoid.hlean +++ b/hott/algebra/category/groupoid.hlean @@ -23,12 +23,13 @@ namespace category precategory.rec_on C groupoid.mk' H -- We can turn each group into a groupoid on the unit type - definition groupoid_of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{0 l} unit := + definition groupoid_of_group.{l} [constructor] (A : Type.{l}) [G : group A] : + groupoid.{0 l} unit := begin fapply groupoid.mk, fapply precategory.mk, intros, exact A, intros, apply (@group.is_set_carrier A G), - intros [a, b, c, g, h], exact (@group.mul A G g h), + intros a b c g h, exact (@group.mul A G g h), intro a, exact (@group.one A G), intros, exact (@group.mul_assoc A G h g f)⁻¹, intros, exact (@group.one_mul A G f), @@ -38,8 +39,7 @@ namespace category apply mul.right_inv, end - definition hom_group {A : Type} [G : groupoid A] (a : A) : - group (hom a a) := + definition hom_group [constructor] {A : Type} [G : groupoid A] (a : A) : group (hom a a) := begin fapply group.mk, intro f g, apply (comp f g), @@ -64,15 +64,19 @@ namespace category attribute Groupoid.struct [instance] [coercion] - definition Groupoid.to_Precategory [coercion] [reducible] (C : Groupoid) : Precategory := + definition Groupoid.to_Precategory [coercion] [reducible] [unfold 1] (C : Groupoid) + : Precategory := Precategory.mk (Groupoid.carrier C) _ - definition groupoid.Mk [reducible] := Groupoid.mk - definition groupoid.MK [reducible] (C : Precategory) (H : Π (a b : C) (f : a ⟶ b), is_iso f) - : Groupoid := + attribute Groupoid._trans_of_to_Precategory_1 [unfold 1] + + definition groupoid.Mk [reducible] [constructor] := Groupoid.mk + definition groupoid.MK [reducible] [constructor] (C : Precategory) + (H : Π (a b : C) (f : a ⟶ b), is_iso f) : Groupoid := Groupoid.mk C (groupoid.mk C H) - definition Groupoid.eta (C : Groupoid) : Groupoid.mk C C = C := + definition Groupoid.eta [unfold 1] (C : Groupoid) : Groupoid.mk C C = C := Groupoid.rec (λob c, idp) C + end category diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index 962291e23..cec39ec31 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -383,3 +383,35 @@ namespace iso by rewrite [-comp_inverse_cancel_right r q, H, comp_inverse_cancel_right _ q] end end iso + +namespace iso + + /- precomposition and postcomposition by an iso is an equivalence -/ + + definition is_equiv_postcompose [constructor] {ob : Type} [precategory ob] {a b c : ob} + (g : b ⟶ c) [is_iso g] : is_equiv (λ(f : a ⟶ b), g ∘ f) := + begin + fapply adjointify, + { exact λf', g⁻¹ ∘ f'}, + { intro f', apply comp_inverse_cancel_left}, + { intro f, apply inverse_comp_cancel_left} + end + + definition equiv_postcompose [constructor] {ob : Type} [precategory ob] {a b c : ob} + (g : b ⟶ c) [is_iso g] : (a ⟶ b) ≃ (a ⟶ c) := + equiv.mk (λ(f : a ⟶ b), g ∘ f) (is_equiv_postcompose g) + + definition is_equiv_precompose [constructor] {ob : Type} [precategory ob] {a b c : ob} + (f : a ⟶ b) [is_iso f] : is_equiv (λ(g : b ⟶ c), g ∘ f) := + begin + fapply adjointify, + { exact λg', g' ∘ f⁻¹}, + { intro g', apply comp_inverse_cancel_right}, + { intro g, apply inverse_comp_cancel_right} + end + + definition equiv_precompose [constructor] {ob : Type} [precategory ob] {a b c : ob} + (f : a ⟶ b) [is_iso f] : (b ⟶ c) ≃ (a ⟶ c) := + equiv.mk (λ(g : b ⟶ c), g ∘ f) (is_equiv_precompose f) + +end iso diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean index 3048e6938..2aa3cc3d4 100644 --- a/hott/algebra/e_closure.hlean +++ b/hott/algebra/e_closure.hlean @@ -10,7 +10,7 @@ A more appropriate intuition is the type of words formed from the relation, import algebra.relation eq2 arity cubical.pathover2 -open eq equiv +open eq equiv function inductive e_closure {A : Type} (R : A → A → Type) : A → A → Type := | of_rel : Π{a a'} (r : R a a'), e_closure R a a' @@ -58,22 +58,51 @@ section exact ap_con g (e_closure.elim e r) (e_closure.elim e r') ⬝ (IH₁ ◾ IH₂) end + definition ap_e_closure_elim_h_symm [unfold_full] {B C : Type} {f : A → B} {g : B → C} + {e : Π⦃a a' : A⦄, R a a' → f a = f a'} + {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')} + (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a') : + ap_e_closure_elim_h e p t⁻¹ʳ = ap_inv g (e_closure.elim e t) ⬝ (ap_e_closure_elim_h e p t)⁻² := + by reflexivity + + definition ap_e_closure_elim_h_trans [unfold_full] {B C : Type} {f : A → B} {g : B → C} + {e : Π⦃a a' : A⦄, R a a' → f a = f a'} + {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')} + (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a') (t' : T a' a'') + : ap_e_closure_elim_h e p (t ⬝r t') = ap_con g (e_closure.elim e t) (e_closure.elim e t') ⬝ + (ap_e_closure_elim_h e p t ◾ ap_e_closure_elim_h e p t') := + by reflexivity + definition ap_e_closure_elim [unfold 10] {B C : Type} {f : A → B} (g : B → C) (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : ap g (e_closure.elim e t) = e_closure.elim (λa a' r, ap g (e r)) t := ap_e_closure_elim_h e (λa a' s, idp) t - definition ap_e_closure_elim_inv [unfold_full] {B C : Type} {f : A → B} (g : B → C) + definition ap_e_closure_elim_symm [unfold_full] {B C : Type} {f : A → B} (g : B → C) (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : ap_e_closure_elim g e t⁻¹ʳ = ap_inv g (e_closure.elim e t) ⬝ (ap_e_closure_elim g e t)⁻² := by reflexivity - definition ap_e_closure_elim_con [unfold_full] {B C : Type} {f : A → B} (g : B → C) + definition ap_e_closure_elim_trans [unfold_full] {B C : Type} {f : A → B} (g : B → C) (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') (t' : T a' a'') : ap_e_closure_elim g e (t ⬝r t') = ap_con g (e_closure.elim e t) (e_closure.elim e t') ⬝ (ap_e_closure_elim g e t ◾ ap_e_closure_elim g e t') := by reflexivity + definition e_closure_elim_eq [unfold 8] {f : A → B} + {e e' : Π⦃a a' : A⦄, R a a' → f a = f a'} (p : e ~3 e') (t : T a a') + : e_closure.elim e t = e_closure.elim e' t := + begin + induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂, + apply p, + reflexivity, + exact IH⁻², + exact IH₁ ◾ IH₂ + end + + -- TODO: formulate and prove this without using function extensionality, + -- and modify the proofs using this to also not use function extensionality + -- strategy: use `e_closure_elim_eq` instead of `ap ... (eq_of_homotopy3 p)` definition ap_e_closure_elim_h_eq {B C : Type} {f : A → B} {g : B → C} (e : Π⦃a a' : A⦄, R a a' → f a = f a') {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')} @@ -116,9 +145,38 @@ section : square (ap (ap h) (ap_e_closure_elim g e t)) (ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) t) (ap_compose h g (e_closure.elim e t))⁻¹ - (ap_e_closure_elim h (λa a' r, ap g (e r)) t) := + (ap_e_closure_elim h (λa a' r, ap g (e r)) t) := !ap_ap_e_closure_elim_h + definition ap_e_closure_elim_h_zigzag {B C D : Type} {f : A → B} + {g : B → C} (h : C → D) + (e : Π⦃a a' : A⦄, R a a' → f a = f a') + {e' : Π⦃a a' : A⦄, R a a' → h (g (f a)) = h (g (f a'))} + (p : Π⦃a a' : A⦄ (s : R a a'), ap (h ∘ g) (e s) = e' s) (t : T a a') + : ap_e_closure_elim h (λa a' s, ap g (e s)) t ⬝ + (ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) t)⁻¹ ⬝ + ap_e_closure_elim_h e p t = + ap_e_closure_elim_h (λa a' s, ap g (e s)) (λa a' s, (ap_compose h g (e s))⁻¹ ⬝ p s) t := + begin + refine whisker_right (eq_of_square (ap_ap_e_closure_elim g h e t)⁻¹ʰ)⁻¹ _ ⬝ _, + refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con, apply eq_of_square, + apply transpose, + -- the rest of the proof is almost the same as the proof of ap_ap_e_closure_elim[_h]. + -- Is there a connection between these theorems? + induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂, + { esimp, apply square_of_eq, apply idp_con}, + { induction pp, apply ids}, + { rewrite [▸*,ap_con (ap h)], + refine (transpose !ap_compose_inv)⁻¹ᵛ ⬝h _, + rewrite [con_inv,inv_inv,-inv2_inv], + exact !ap_inv2 ⬝v square_inv2 IH}, + { rewrite [▸*,ap_con (ap h)], + refine (transpose !ap_compose_con)⁻¹ᵛ ⬝h _, + rewrite [con_inv,inv_inv,con2_inv], + refine !ap_con2 ⬝v square_con2 IH₁ IH₂}, + + end + definition is_equivalence_e_closure : is_equivalence T := begin constructor, @@ -127,23 +185,6 @@ section intro a a' a'' t t', exact t ⬝r t', end -/- - definition e_closure.transport_left {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a') - (t : e_closure R a a') (p : a = a'') - : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t := - by induction p; exact !idp_con⁻¹ - - definition e_closure.transport_right {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a') - (t : e_closure R a a') (p : a' = a'') - : e_closure.elim e (p ▸ t) = e_closure.elim e t ⬝ (ap f p) := - by induction p; reflexivity - - definition e_closure.transport_lr {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a') - (t : e_closure R a a) (p : a = a') - : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t ⬝ (ap f p) := - by induction p; esimp; exact !idp_con⁻¹ --/ - /- dependent elimination -/ variables {P : B → Type} {Q : C → Type} {f : A → B} {g : B → C} {f' : Π(a : A), P (f a)} @@ -158,12 +199,12 @@ section exact IH₁ ⬝o IH₂ end - definition elimo_inv [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a') + definition elimo_symm [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a') (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') (t : T a a') : e_closure.elimo p po t⁻¹ʳ = (e_closure.elimo p po t)⁻¹ᵒ := by reflexivity - definition elimo_con [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a') + definition elimo_trans [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a') (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') (t : T a a') (t' : T a' a'') : e_closure.elimo p po (t ⬝r t') = e_closure.elimo p po t ⬝o e_closure.elimo p po t' := by reflexivity @@ -192,10 +233,10 @@ section induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂, { reflexivity}, { induction pp; reflexivity}, - { rewrite [+elimo_inv, ap_e_closure_elim_inv, IH, con_inv, change_path_con, ▸*, -inv2_inv, + { rewrite [+elimo_symm, ap_e_closure_elim_symm, IH, con_inv, change_path_con, ▸*, -inv2_inv, change_path_invo, pathover_of_pathover_ap_invo]}, - { rewrite [+elimo_con, ap_e_closure_elim_con, IH₁, IH₂, con_inv, change_path_con, ▸*, con2_inv, - change_path_cono, pathover_of_pathover_ap_cono]}, + { rewrite [+elimo_trans, ap_e_closure_elim_trans, IH₁, IH₂, con_inv, change_path_con, ▸*, + con2_inv, change_path_cono, pathover_of_pathover_ap_cono]}, end end diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 04b24bc04..36f050eec 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -6,26 +6,26 @@ Authors: Floris van Doorn homotopy groups of a pointed space -/ -import .trunc_group .hott types.trunc +import .trunc_group types.trunc .group_theory open nat eq pointed trunc is_trunc algebra namespace eq - definition phomotopy_group [constructor] (n : ℕ) (A : Type*) : Set* := + definition phomotopy_group [reducible] [constructor] (n : ℕ) (A : Type*) : Set* := ptrunc 0 (Ω[n] A) definition homotopy_group [reducible] (n : ℕ) (A : Type*) : Type := phomotopy_group n A - notation `π*[`:95 n:0 `] `:0 A:95 := phomotopy_group n A - notation `π[`:95 n:0 `] `:0 A:95 := homotopy_group n A + notation `π*[`:95 n:0 `] `:0 := phomotopy_group n + notation `π[`:95 n:0 `] `:0 := homotopy_group n - definition group_homotopy_group [instance] [constructor] (n : ℕ) (A : Type*) + definition group_homotopy_group [instance] [constructor] [reducible] (n : ℕ) (A : Type*) : group (π[succ n] A) := trunc_group concat inverse idp con.assoc idp_con con_idp con.left_inv - definition comm_group_homotopy_group [constructor] (n : ℕ) (A : Type*) + definition comm_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*) : comm_group (π[succ (succ n)] A) := trunc_comm_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton @@ -43,7 +43,15 @@ namespace eq notation `πg[`:95 n:0 ` +1] `:0 A:95 := ghomotopy_group n A notation `πag[`:95 n:0 ` +2] `:0 A:95 := cghomotopy_group n A - prefix `π₁`:95 := fundamental_group + notation `π₁` := fundamental_group + + definition tr_mul_tr {n : ℕ} {A : Type*} (p q : Ω[n + 1] A) : + tr p *[πg[n+1] A] tr q = tr (p ⬝ q) := + by reflexivity + + definition tr_mul_tr' {n : ℕ} {A : Type*} (p q : Ω[succ n] A) + : tr p *[π[succ n] A] tr q = tr (p ⬝ q) := + idp definition phomotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B) : π*[n] A ≃* π*[n] B := @@ -105,8 +113,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 f:95 := phomotopy_group_functor n f - notation `π→[`:95 n:0 `] `:0 f:95 := homotopy_group_functor n f + notation `π→*[`:95 n:0 `] `:0 := phomotopy_group_functor n + notation `π→[`:95 n:0 `] `:0 := homotopy_group_functor n definition tinverse [constructor] {X : Type*} : π*[1] X →* π*[1] X := ptrunc_functor 0 pinverse @@ -132,7 +140,36 @@ namespace eq apply ap tr, apply apn_con end + open group function + /- some homomorphisms -/ + definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) : + is_homomorphism + (cast (ap (trunc 0 ∘ pointed.carrier) (loop_space_succ_eq_in A (succ n))) + : πg[n+1+1] A → πg[n+1] Ω A) := + begin + intro g h, induction g with g, induction h with h, + xrewrite [tr_mul_tr, - + fn_cast_eq_cast_fn _ (λn, tr), tr_mul_tr, ↑cast, -tr_compose, + loop_space_succ_eq_in_concat, - + tr_compose], + end + + definition is_homomorphism_inverse (A : Type*) (n : ℕ) + : is_homomorphism (λp, p⁻¹ : πag[n+2] A → πag[n+2] A) := + begin + intro g h, rewrite mul.comm, + induction g with g, induction h with h, + exact ap tr !con_inv + end + + definition homotopy_group_homomorphism [constructor] (n : ℕ) {A B : Type*} (f : A →* B) + : πg[n+1] A →g πg[n+1] B := + begin + fconstructor, + { exact phomotopy_group_functor (n+1) f}, + { apply phomotopy_group_functor_mul} + end + + notation `π→g[`:95 n:0 ` +1] `:0 f:95 := homotopy_group_homomorphism n f end eq diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean index ce8105ceb..a356a7066 100644 --- a/hott/algebra/ring.hlean +++ b/hott/algebra/ring.hlean @@ -61,6 +61,13 @@ section semiring theorem distrib_three_right (a b c d : A) : (a + b + c) * d = a * d + b * d + c * d := by rewrite *right_distrib + + theorem mul_two : a * 2 = a + a := + by rewrite [-one_add_one_eq_two, left_distrib, +mul_one] + + theorem two_mul : 2 * a = a + a := + by rewrite [-one_add_one_eq_two, right_distrib, +one_mul] + end semiring /- comm semiring -/ diff --git a/hott/eq2.hlean b/hott/eq2.hlean index 556398361..ee86f6ec7 100644 --- a/hott/eq2.hlean +++ b/hott/eq2.hlean @@ -118,5 +118,13 @@ namespace eq con_tr idp q u = ap (λp, p ▸ u) (idp_con q) := by induction q;reflexivity + definition transport_eq_Fl_idp_left {A B : Type} {a : A} {b : B} (f : A → B) (q : f a = b) + : transport_eq_Fl idp q = !idp_con⁻¹ := + by induction q; reflexivity + + definition whisker_left_idp_con_eq_assoc + {A : Type} {a₁ a₂ a₃ : A} (p : a₁ = a₂) (q : a₂ = a₃) + : whisker_left p (idp_con q)⁻¹ = con.assoc p idp q := + by induction q; reflexivity end eq diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index 482e8b2b5..1d29b0f1e 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -3,7 +3,7 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -Declaration of the pushout +Declaration and properties of the pushout -/ import .quotient types.sigma types.arrow_2 @@ -84,6 +84,11 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) : transport (elim_type Pinl Pinr Pglue) (glue x) = Pglue x := !elim_type_eq_of_rel_fn + theorem elim_type_glue_inv (Pinl : BL → Type) (Pinr : TR → Type) + (Pglue : Π(x : TL), Pinl (f x) ≃ Pinr (g x)) (x : TL) + : transport (elim_type Pinl Pinr Pglue) (glue x)⁻¹ = to_inv (Pglue x) := + !elim_type_eq_of_rel_inv + protected definition rec_prop {P : pushout → Type} [H : Πx, is_prop (P x)] (Pinl : Π(x : BL), P (inl x)) (Pinr : Π(x : TR), P (inr x)) (y : pushout) := rec Pinl Pinr (λx, !is_prop.elimo) y diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index 94968740c..1ba872cd7 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -58,6 +58,11 @@ namespace quotient : transport (quotient.elim_type Pc Pp) (eq_of_rel R H) = to_fun (Pp H) := by rewrite [tr_eq_cast_ap_fn, ↑quotient.elim_type, elim_eq_of_rel];apply cast_ua_fn + theorem elim_type_eq_of_rel_inv (Pc : A → Type) + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a') + : transport (quotient.elim_type Pc Pp) (eq_of_rel R H)⁻¹ = to_inv (Pp H) := + by rewrite [tr_eq_cast_ap_fn, ↑quotient.elim_type, ap_inv, elim_eq_of_rel];apply cast_ua_inv_fn + theorem elim_type_eq_of_rel.{u} (Pc : A → Type.{u}) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a') (p : Pc a) : transport (quotient.elim_type Pc Pp) (eq_of_rel R H) p = to_fun (Pp H) p := diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index baafed5b9..f7da0347f 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -332,6 +332,7 @@ namespace simple_two_quotient end end simple_two_quotient +export [unfold] simple_two_quotient attribute simple_two_quotient.j simple_two_quotient.incl0 [constructor] attribute simple_two_quotient.rec simple_two_quotient.elim [unfold 8] [recursor 8] --attribute simple_two_quotient.elim_type [unfold 9] -- TODO @@ -370,8 +371,8 @@ namespace two_quotient { exact P0 a}, { exact P1 s}, { exact abstract [irreducible] begin induction q with a a' t t' q, - rewrite [elimo_con (simple_two_quotient.incl1 R Q2) P1, - elimo_inv (simple_two_quotient.incl1 R Q2) P1, + rewrite [elimo_trans (simple_two_quotient.incl1 R Q2) P1, + elimo_symm (simple_two_quotient.incl1 R Q2) P1, -whisker_right_eq_of_con_inv_eq_idp (simple_two_quotient.incl2 R Q2 (Qmk R q)), change_path_con], xrewrite [change_path_cono], @@ -430,7 +431,7 @@ namespace two_quotient {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'} (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t := - !elim_inclt + ap_e_closure_elim_h incl1 (elim_incl1 P2) t theorem elim_incl2 {P : Type} (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') diff --git a/hott/homotopy/cylinder.hlean b/hott/homotopy/cylinder.hlean index 410da225f..e53d551bf 100644 --- a/hott/homotopy/cylinder.hlean +++ b/hott/homotopy/cylinder.hlean @@ -8,13 +8,12 @@ Declaration of mapping cylinders import hit.quotient -open quotient eq sum equiv +open quotient eq sum equiv fiber namespace cylinder section -universe u -parameters {A B : Type.{u}} (f : A → B) + parameters {A B : Type} (f : A → B) local abbreviation C := B + A inductive cylinder_rel : C → C → Type := @@ -24,6 +23,7 @@ parameters {A B : Type.{u}} (f : A → B) definition cylinder := quotient cylinder_rel -- TODO: define this in root namespace + parameter {f} definition base (b : B) : cylinder := class_of R (inl b) @@ -93,3 +93,51 @@ attribute cylinder.rec cylinder.elim [unfold 8] [recursor 8] attribute cylinder.elim_type [unfold 7] attribute cylinder.rec_on cylinder.elim_on [unfold 5] attribute cylinder.elim_type_on [unfold 4] + +namespace cylinder + open sigma sigma.ops + variables {A B : Type} (f : A → B) + + /- cylinder as a dependent family -/ + definition pr1 [unfold 4] : cylinder f → B := + cylinder.elim id f (λa, idp) + + definition fcylinder : B → Type := fiber (pr1 f) + + definition cylinder_equiv_sigma_fcylinder [constructor] : cylinder f ≃ Σb, fcylinder f b := + !sigma_fiber_equiv⁻¹ᵉ + + variable {f} + definition fbase (b : B) : fcylinder f b := + fiber.mk (base b) idp + + definition ftop (a : A) : fcylinder f (f a) := + fiber.mk (top a) idp + + definition fseg (a : A) : fbase (f a) = ftop a := + fiber_eq (seg a) !elim_seg⁻¹ + +-- set_option pp.notation false +-- -- The induction principle for the dependent mapping cylinder (TODO) +-- protected definition frec {P : Π(b), fcylinder f b → Type} +-- (Pbase : Π(b : B), P _ (fbase b)) (Ptop : Π(a : A), P _ (ftop a)) +-- (Pseg : Π(a : A), Pbase (f a) =[fseg a] Ptop a) {b : B} (x : fcylinder f b) : P _ x := +-- begin +-- cases x with x p, induction p, +-- induction x: esimp, +-- { apply Pbase}, +-- { apply Ptop}, +-- { esimp, --fapply fiber_pathover, +-- --refine pathover_of_pathover_ap P (λx, fiber.mk x idp), + +-- exact sorry} +-- end + +-- theorem frec_fseg {P : Π(b), fcylinder f b → Type} +-- (Pbase : Π(b : B), P _ (fbase b)) (Ptop : Π(a : A), P _ (ftop a)) +-- (Pseg : Π(a : A), Pbase (f a) =[fseg a] Ptop a) (a : A) +-- : apd (cylinder.frec Pbase Ptop Pseg) (fseg a) = Pseg a := +-- sorry + + +end cylinder diff --git a/hott/homotopy/hopf.hlean b/hott/homotopy/hopf.hlean index d199ace9d..017ae94b3 100644 --- a/hott/homotopy/hopf.hlean +++ b/hott/homotopy/hopf.hlean @@ -69,14 +69,14 @@ section { fapply equiv.MK (λz : A × A, (z.1 * z.2, z.2)) (λz : A × A, ((λx, x * z.2)⁻¹ z.1, z.2)), - { intro z, induction z with u v, esimp, + { intro z, induction z with u v, esimp, exact prod_eq (right_inv (λx, x * v) u) idp }, { intro z, induction z with a b, esimp, exact prod_eq (left_inv (λx, x * b) a) idp } }, - { exact erfl }, - { exact erfl }, - { intro z, reflexivity }, - { intro z, reflexivity } + { reflexivity }, + { reflexivity }, + { reflexivity }, + { reflexivity } end end diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index cfa080707..573b8d08b 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -67,7 +67,7 @@ namespace sphere_index | sp_refl : le a a | step : Π {b}, le a b → le a (b.+1) - infix `+1+`:65 := sphere_index.add_plus_one + infix ` +1+ `:65 := sphere_index.add_plus_one definition has_add_sphere_index [instance] [priority 2000] [reducible] : has_add ℕ₋₁ := has_add.mk sphere_index.add @@ -75,7 +75,7 @@ namespace sphere_index definition has_le_sphere_index [instance] : has_le ℕ₋₁ := has_le.mk sphere_index.le - definition of_nat [coercion] [reducible] (n : nat) : ℕ₋₁ := + definition of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₁ := (nat.rec_on n -1 (λ n k, k.+1)).+1 definition sub_one [reducible] (n : ℕ) : ℕ₋₁ := diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index f2b491c76..228d705a6 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -69,6 +69,10 @@ namespace susp (a : A) : transport (susp.elim_type PN PS Pm) (merid a) = Pm a := !elim_type_glue + theorem elim_type_merid_inv {A : Type} (PN : Type) (PS : Type) (Pm : A → PN ≃ PS) + (a : A) : transport (susp.elim_type PN PS Pm) (merid a)⁻¹ = to_inv (Pm a) := + !elim_type_glue_inv + protected definition merid_square {a a' : A} (p : a = a') : square (merid a) (merid a') idp idp := by cases p; apply vrefl @@ -198,12 +202,12 @@ namespace susp end susp open susp -definition psusp [constructor] (X : Type) : pType := +definition psusp [constructor] (X : Type) : Type* := pointed.mk' (susp X) namespace susp open pointed - variables {X Y Z : pType} + variables {X Y Z : Type*} definition psusp_functor (f : X →* Y) : psusp X →* psusp Y := begin @@ -234,7 +238,7 @@ namespace susp -- adjunction from Coq-HoTT - definition loop_susp_unit [constructor] (X : pType) : X →* Ω(psusp X) := + definition loop_susp_unit [constructor] (X : Type*) : X →* Ω(psusp X) := begin fconstructor, { intro x, exact merid x ⬝ (merid pt)⁻¹}, @@ -263,7 +267,7 @@ namespace susp xrewrite [idp_con_idp, -ap_compose (concat idp)]}, end - definition loop_susp_counit [constructor] (X : pType) : psusp (Ω X) →* X := + definition loop_susp_counit [constructor] (X : Type*) : psusp (Ω X) →* X := begin fconstructor, { intro x, induction x, exact pt, exact pt, exact a}, @@ -284,7 +288,7 @@ namespace susp { reflexivity} end - definition loop_susp_counit_unit (X : pType) + definition loop_susp_counit_unit (X : Type*) : ap1 (loop_susp_counit X) ∘* loop_susp_unit (Ω X) ~* pid (Ω X) := begin induction X with X x, fconstructor, @@ -298,7 +302,7 @@ namespace susp xrewrite [ap_con_right_inv (susp.elim x x (λa, a)) (merid idp),idp_con_idp,-ap_compose]} end - definition loop_susp_unit_counit (X : pType) + definition loop_susp_unit_counit (X : Type*) : loop_susp_counit (psusp X) ∘* psusp_functor (loop_susp_unit X) ~* pid (psusp X) := begin induction X with X x, fconstructor, @@ -311,7 +315,7 @@ namespace susp { reflexivity} end - definition susp_adjoint_loop (X Y : pType) : map₊ (pointed.mk' (susp X)) Y ≃ map₊ X (Ω Y) := + definition susp_adjoint_loop (X Y : Type*) : pointed.mk' (susp X) →* Y ≃ X →* Ω Y := begin fapply equiv.MK, { intro f, exact ap1 f ∘* loop_susp_unit X}, diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 18fba5ff1..7f283a1f1 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -276,6 +276,12 @@ namespace is_equiv !ap_eq_of_fn_eq_fn' end + + -- This is inv_commute' for A ≡ unit + definition inv_commute1' {B C : Type} (f : B → C) [is_equiv f] (h : B → B) (h' : C → C) + (p : Π(b : B), f (h b) = h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) := + eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹) + end is_equiv open is_equiv @@ -310,9 +316,12 @@ namespace equiv definition to_left_inv [reducible] [unfold 3] (f : A ≃ B) (a : A) : f⁻¹ (f a) = a := left_inv f a - protected definition refl [refl] [constructor] : A ≃ A := + protected definition rfl [refl] [constructor] : A ≃ A := equiv.mk id !is_equiv_id + protected definition refl [constructor] [reducible] (A : Type) : A ≃ A := + @equiv.rfl A + protected definition symm [symm] [constructor] (f : A ≃ B) : B ≃ A := equiv.mk f⁻¹ !is_equiv_inv @@ -322,7 +331,7 @@ namespace equiv infixl ` ⬝e `:75 := equiv.trans postfix `⁻¹ᵉ`:(max + 1) := equiv.symm -- notation for inverse which is not overloaded - abbreviation erfl [constructor] := @equiv.refl + abbreviation erfl [constructor] := @equiv.rfl definition to_inv_trans [reducible] [unfold_full] (f : A ≃ B) (g : B ≃ C) : to_inv (f ⬝e g) = to_fun (g⁻¹ᵉ ⬝e f⁻¹ᵉ) := @@ -395,6 +404,10 @@ namespace equiv {a : A} (b : B (g' a)) : f (h b) = h' (f b) := fun_commute_of_inv_commute' @f @h @h' p b + definition inv_commute1 {B C : Type} (f : B ≃ C) (h : B → B) (h' : C → C) + (p : Π(b : B), f (h b) = h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) := + inv_commute1' (to_fun f) h h' p c + end infixl ` ⬝pe `:75 := equiv_of_equiv_of_eq diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 6406a00b1..f47bec2f2 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -92,7 +92,6 @@ namespace eq definition inv_con_inv_left (p : y = x) (q : y = z) : (p⁻¹ ⬝ q)⁻¹ = q⁻¹ ⬝ p := by induction q; induction p; reflexivity - -- universe metavariables definition inv_con_inv_right (p : x = y) (q : z = y) : (p ⬝ q⁻¹)⁻¹ = q ⬝ p⁻¹ := by induction q; induction p; reflexivity @@ -444,6 +443,14 @@ namespace eq p⁻¹ ▸ p ▸ z = z := (con_tr p p⁻¹ z)⁻¹ ⬝ ap (λr, transport P r z) (con.right_inv p) + definition cast_cast_inv {A : Type} {P : A → Type} {x y : A} (p : x = y) (z : P y) : + cast (ap P p) (cast (ap P p⁻¹) z) = z := + by induction p; reflexivity + + definition cast_inv_cast {A : Type} {P : A → Type} {x y : A} (p : x = y) (z : P x) : + cast (ap P p⁻¹) (cast (ap P p) z) = z := + by induction p; reflexivity + definition con_con_tr {P : A → Type} {x y z w : A} (p : x = y) (q : y = z) (r : z = w) (u : P x) : ap (λe, e ▸ u) (con.assoc' p q r) ⬝ (con_tr (p ⬝ q) r u) ⬝ @@ -515,6 +522,10 @@ namespace eq f y (p ▸ z) = p ▸ f x z := by induction p; reflexivity + definition fn_cast_eq_cast_fn {A : Type} {P Q : A → Type} {x y : A} (p : x = y) + (f : Πx, P x → Q x) (z : P x) : f y (cast (ap P p) z) = cast (ap Q p) (f x z) := + by induction p; reflexivity + /- Transporting in particular fibrations -/ /- diff --git a/hott/init/pointed.hlean b/hott/init/pointed.hlean index dce7158f6..f7c7ea810 100644 --- a/hott/init/pointed.hlean +++ b/hott/init/pointed.hlean @@ -40,6 +40,11 @@ open pointed section universe variable u structure ptrunctype (n : trunc_index) extends trunctype.{u} n, pType.{u} + + definition is_trunc_ptrunctype [instance] {n : ℕ₋₂} (X : ptrunctype n) + : is_trunc n (ptrunctype.to_pType X) := + trunctype.struct X + end notation n `-Type*` := ptrunctype n diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean index 22aa941da..6ba8c5756 100644 --- a/hott/init/ua.hlean +++ b/hott/init/ua.hlean @@ -22,7 +22,7 @@ section equiv.mk _ (is_equiv_cast_of_eq H) definition equiv_of_eq_refl [reducible] [unfold_full] (A : Type) - : equiv_of_eq (refl A) = equiv.refl := + : equiv_of_eq (refl A) = equiv.refl A := idp @@ -75,7 +75,7 @@ namespace equiv -- a variant where we immediately recurse on the equality in the new goal definition rec_on_ua_idp [recursor] {A : Type} {P : Π{B}, A ≃ B → Type} {B : Type} - (f : A ≃ B) (H : P equiv.refl) : P f := + (f : A ≃ B) (H : P equiv.rfl) : P f := rec_on_ua f (λq, eq.rec_on q H) -- a variant where (equiv_of_eq (ua f)) will be replaced by f in the new goal @@ -85,7 +85,7 @@ namespace equiv -- a variant where we do both definition rec_on_ua_idp' {A : Type} {P : Π{B}, A ≃ B → A = B → Type} {B : Type} - (f : A ≃ B) (H : P equiv.refl idp) : P f (ua f) := + (f : A ≃ B) (H : P equiv.rfl idp) : P f (ua f) := rec_on_ua' f (λq, eq.rec_on q H) definition ua_refl (A : Type) : ua erfl = idpath A := diff --git a/hott/types/arrow.hlean b/hott/types/arrow.hlean index 91a892eb1..a496dba53 100644 --- a/hott/types/arrow.hlean +++ b/hott/types/arrow.hlean @@ -38,14 +38,14 @@ namespace pi variable (A) definition arrow_equiv_arrow_right [constructor] (f1 : B ≃ B') : (A → B) ≃ (A → B') := - arrow_equiv_arrow_rev equiv.refl f1 + arrow_equiv_arrow_rev equiv.rfl f1 variables {A} (B) definition arrow_equiv_arrow_left_rev [constructor] (f0 : A' ≃ A) : (A → B) ≃ (A' → B) := - arrow_equiv_arrow_rev f0 equiv.refl + arrow_equiv_arrow_rev f0 equiv.rfl definition arrow_equiv_arrow_left [constructor] (f0 : A ≃ A') : (A → B) ≃ (A' → B) := - arrow_equiv_arrow f0 equiv.refl + arrow_equiv_arrow f0 equiv.rfl variables {B} definition arrow_equiv_arrow_right' [constructor] (f1 : A → (B ≃ B')) : (A → B) ≃ (A → B') := diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index ec8c91372..af916be3b 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -456,13 +456,13 @@ namespace eq parameters {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a)) (p : (center (Σa, code a)).1 = a₀) include p - definition encode {a : A} (q : a₀ = a) : code a := + protected definition encode {a : A} (q : a₀ = a) : code a := (p ⬝ q) ▸ (center (Σa, code a)).2 - definition decode' {a : A} (c : code a) : a₀ = a := + protected definition decode' {a : A} (c : code a) : a₀ = a := (is_prop.elim ⟨a₀, encode idp⟩ ⟨a, c⟩)..1 - definition decode {a : A} (c : code a) : a₀ = a := + protected definition decode {a : A} (c : code a) : a₀ = a := (decode' (encode idp))⁻¹ ⬝ decode' c definition total_space_method (a : A) : (a₀ = a) ≃ code a := diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 149cfe4f5..725e2cfbe 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -208,17 +208,17 @@ namespace equiv : equiv.mk f H = equiv.mk f' H' := apd011 equiv.mk p !is_prop.elim - definition equiv_eq {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' := + definition equiv_eq' {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' := by (cases f; cases f'; apply (equiv_mk_eq p)) - definition equiv_eq' {f f' : A ≃ B} (p : to_fun f ~ to_fun f') : f = f' := - by apply equiv_eq;apply eq_of_homotopy p + definition equiv_eq {f f' : A ≃ B} (p : to_fun f ~ to_fun f') : f = f' := + by apply equiv_eq'; apply eq_of_homotopy p definition trans_symm (f : A ≃ B) (g : B ≃ C) : (f ⬝e g)⁻¹ᵉ = g⁻¹ᵉ ⬝e f⁻¹ᵉ :> (C ≃ A) := - equiv_eq idp + equiv_eq' idp definition symm_symm (f : A ≃ B) : f⁻¹ᵉ⁻¹ᵉ = f :> (A ≃ B) := - equiv_eq idp + equiv_eq' idp protected definition equiv.sigma_char [constructor] (A B : Type) : (A ≃ B) ≃ Σ(f : A → B), is_equiv f := @@ -235,7 +235,7 @@ namespace equiv (f = f') ≃ (to_fun !equiv.sigma_char f = to_fun !equiv.sigma_char f') : eq_equiv_fn_eq (to_fun !equiv.sigma_char) ... ≃ ((to_fun !equiv.sigma_char f).1 = (to_fun !equiv.sigma_char f').1 ) : equiv_subtype - ... ≃ (to_fun f = to_fun f') : equiv.refl + ... ≃ (to_fun f = to_fun f') : equiv.rfl definition is_equiv_ap_to_fun (f f' : A ≃ B) : is_equiv (ap to_fun : f = f' → to_fun f = to_fun f') := @@ -276,4 +276,19 @@ namespace equiv [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A ≃ B) := by cases n; apply !is_contr_equiv; apply !is_trunc_succ_equiv + definition eq_of_fn_eq_fn'_idp {A B : Type} (f : A → B) [is_equiv f] (x : A) + : eq_of_fn_eq_fn' f (idpath (f x)) = idpath x := + !con.left_inv + + definition eq_of_fn_eq_fn'_con {A B : Type} (f : A → B) [is_equiv f] {x y z : A} + (p : f x = f y) (q : f y = f z) + : eq_of_fn_eq_fn' f (p ⬝ q) = eq_of_fn_eq_fn' f p ⬝ eq_of_fn_eq_fn' f q := + begin + unfold eq_of_fn_eq_fn', + refine _ ⬝ !con.assoc, apply whisker_right, + refine _ ⬝ !con.assoc⁻¹ ⬝ !con.assoc⁻¹, apply whisker_left, + refine !ap_con ⬝ _, apply whisker_left, + refine !con_inv_cancel_left⁻¹ + end + end equiv diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 700602e7b..e595d7b5e 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -7,7 +7,7 @@ Ported from Coq HoTT Theorems about fibers -/ -import .sigma .eq .pi +import .sigma .eq .pi cubical.squareover open equiv sigma sigma.ops eq pi structure fiber {A B : Type} (f : A → B) (b : B) := @@ -43,6 +43,20 @@ namespace fiber (q : point_eq x = ap f p ⬝ point_eq y) : x = y := to_inv !fiber_eq_equiv ⟨p, q⟩ + definition fiber_pathover {X : Type} {A B : X → Type} {x₁ x₂ : X} {p : x₁ = x₂} + {f : Πx, A x → B x} {b : Πx, B x} {v₁ : fiber (f x₁) (b x₁)} {v₂ : fiber (f x₂) (b x₂)} + (q : point v₁ =[p] point v₂) + (r : squareover B hrfl (pathover_idp_of_eq (point_eq v₁)) (pathover_idp_of_eq (point_eq v₂)) + (apo f q) (apd b p)) + : v₁ =[p] v₂ := + begin + apply pathover_of_fn_pathover_fn (λa, !fiber.sigma_char), esimp, + fapply sigma_pathover: esimp, + { exact q}, + { induction v₁ with a₁ p₁, induction v₂ with a₂ p₂, esimp at *, induction q, esimp at *, + apply pathover_idp_of_eq, apply eq_of_vdeg_square, apply square_of_squareover_ids r} + end + open is_trunc definition fiber_pr1 (B : A → Type) (a : A) : fiber (pr1 : (Σa, B a) → A) a ≃ B a := calc diff --git a/hott/types/int/hott.hlean b/hott/types/int/hott.hlean index c2a7cb8c4..36ff46209 100644 --- a/hott/types/int/hott.hlean +++ b/hott/types/int/hott.hlean @@ -14,7 +14,7 @@ namespace int section open algebra - definition group_integers : Group := + definition group_integers [constructor] : Group := Group.mk ℤ (group_of_add_group _) notation `gℤ` := group_integers diff --git a/hott/types/lift.hlean b/hott/types/lift.hlean index 86f90da02..fc16a6a29 100644 --- a/hott/types/lift.hlean +++ b/hott/types/lift.hlean @@ -73,7 +73,7 @@ namespace lift equiv.mk _ (is_equiv_lift_functor f) definition lift_equiv_lift_refl (A : Type) : lift_equiv_lift (erfl : A ≃ A) = erfl := - by apply equiv_eq'; intro z; induction z with a; reflexivity + by apply equiv_eq; intro z; induction z with a; reflexivity definition lift_inv_functor [unfold_full] (a : A) : A' := down (g (up a)) @@ -119,7 +119,7 @@ namespace lift intro f, apply equiv_eq, reflexivity end end abstract begin - intro g, apply equiv_eq, esimp, apply eq_of_homotopy, intro z, + intro g, apply equiv_eq', esimp, apply eq_of_homotopy, intro z, induction z with a, esimp, apply lift.eta end end @@ -134,12 +134,12 @@ namespace lift exact _, { intro p, induction p, esimp [lift_eq_lift_equiv,equiv.trans,equiv.symm,eq_equiv_equiv], - rewrite [equiv_of_eq_refl,lift_equiv_lift_refl], + rewrite [equiv_of_eq_refl, lift_equiv_lift_refl], apply ua_refl} end definition plift [constructor] (A : pType.{u}) : pType.{max u v} := - pType.mk (lift A) (up pt) + pointed.MK (lift A) (up pt) definition plift_functor [constructor] {A B : Type*} (f : A →* B) : plift A →* plift B := pmap.mk (lift_functor f) (ap up (respect_pt f)) diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 19dd30710..1e35829c9 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -176,7 +176,7 @@ namespace pi (f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) : (Π(b : B a), (sigma_eq p !pathover_tr) ▸ (f b) = g (p ▸ b)) ≃ (Π(b : B a), p ▸D (f b) = g (p ▸ b)) := - eq.rec_on p (λg, !equiv.refl) g + eq.rec_on p (λg, !equiv.rfl) g end /- Functorial action -/ @@ -234,7 +234,7 @@ namespace pi definition pi_equiv_pi_right [constructor] {P Q : A → Type} (g : Πa, P a ≃ Q a) : (Πa, P a) ≃ (Πa, Q a) := - pi_equiv_pi equiv.refl g + pi_equiv_pi equiv.rfl g /- Equivalence if one of the types is contractible -/ diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index ccb68c5da..f2c218b0d 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -318,7 +318,7 @@ namespace pointed definition apn_succ [unfold_full] (n : ℕ) (f : map₊ A B) : Ω→[n + 1] f = ap1 (Ω→[n] f) := idp definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B := - proof pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity) qed + pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity) definition pinverse [constructor] {X : Type*} : Ω X →* Ω X := pmap.mk eq.inverse idp @@ -439,6 +439,9 @@ namespace pointed : f ~* h := phomotopy_of_eq p ⬝* q + infix ` ⬝*p `:75 := pconcat_eq + infix ` ⬝p* `:75 := eq_pconcat + definition pwhisker_left [constructor] (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g := phomotopy.mk (λa, ap h (p a)) abstract begin @@ -508,8 +511,12 @@ namespace pointed theorem apn_inv (n : ℕ) (f : A →* B) (p : Ω[n+1] A) : apn (n+1) f p⁻¹ = (apn (n+1) f p)⁻¹ := by rewrite [+apn_succ, ap1_inv] - infix ` ⬝*p `:75 := pconcat_eq - infix ` ⬝p* `:75 := eq_pconcat + definition pinverse_pinverse (A : Type*) : pinverse ∘* pinverse ~* pid (Ω A) := + begin + fapply phomotopy.mk, + { apply inv_inv}, + { reflexivity} + end /- pointed equivalences -/ @@ -529,6 +536,10 @@ namespace pointed definition to_pinv [constructor] (f : A ≃* B) : B →* A := pmap.mk f⁻¹ ((ap f⁻¹ (respect_pt f))⁻¹ ⬝ left_inv f pt) + definition to_pmap_pequiv_of_pmap {A B : Type*} (f : A →* B) (H : is_equiv f) + : pequiv.to_pmap (pequiv_of_pmap f H) = f := + by cases f; reflexivity + /- A version of pequiv.MK with stronger conditions. The advantage of defining a pointed equivalence with this definition is that there is a @@ -570,11 +581,15 @@ namespace pointed pequiv_of_pmap (to_pinv f) !is_equiv_inv protected definition pequiv.trans [trans] (f : A ≃* B) (g : B ≃* C) : A ≃* C := - pequiv_of_pmap (pcompose g f) !is_equiv_compose + pequiv_of_pmap (g ∘* f) !is_equiv_compose postfix `⁻¹ᵉ*`:(max + 1) := pequiv.symm infix ` ⬝e* `:75 := pequiv.trans + definition to_pmap_pequiv_trans {A B C : Type*} (f : A ≃* B) (g : B ≃* C) + : pequiv.to_pmap (f ⬝e* g) = g ∘* f := + !to_pmap_pequiv_of_pmap + definition pequiv_change_fun [constructor] (f : A ≃* B) (f' : A →* B) (Heq : f ~ f') : A ≃* B := pequiv_of_pmap f' (is_equiv.homotopy_closed f Heq) @@ -736,14 +751,14 @@ namespace pointed ap1_con (loopn_pequiv_loopn n f) p q definition loopn_pequiv_loopn_rfl (n : ℕ) (A : Type*) : - loopn_pequiv_loopn n (@pequiv.refl A) = @pequiv.refl (Ω[n] A) := + loopn_pequiv_loopn n (pequiv.refl A) = pequiv.refl (Ω[n] A) := begin apply pequiv_eq, apply eq_of_phomotopy, exact !to_pmap_loopn_pequiv_loopn ⬝* apn_pid n, end definition loop_pequiv_loop_rfl (A : Type*) : - loop_pequiv_loop (@pequiv.refl A) = @pequiv.refl (Ω A) := + loop_pequiv_loop (pequiv.refl A) = pequiv.refl (Ω A) := loopn_pequiv_loopn_rfl 1 A definition pmap_functor [constructor] {A A' B B' : Type*} (f : A' →* A) (g : B →* B') : @@ -755,6 +770,9 @@ namespace pointed { rewrite [▸*, ap_constant], apply idp_con} end end + definition pequiv_pinverse (A : Type*) : Ω A ≃* Ω A := + pequiv_of_pmap pinverse !is_equiv_eq_inverse + /- -- TODO definition pmap_pequiv_pmap {A A' B B' : Type*} (f : A ≃* A') (g : B ≃* B') : ppmap A B ≃* ppmap A' B' := diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index 81b88c520..8f3288a5e 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -155,10 +155,10 @@ namespace prod equiv.mk (prod_functor f g) _ definition prod_equiv_prod_left [constructor] (g : B ≃ B') : A × B ≃ A × B' := - prod_equiv_prod equiv.refl g + prod_equiv_prod equiv.rfl g definition prod_equiv_prod_right [constructor] (f : A ≃ A') : A × B ≃ A' × B := - prod_equiv_prod f equiv.refl + prod_equiv_prod f equiv.rfl /- Symmetry -/ diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index b13912ad5..8b449d179 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -73,7 +73,7 @@ namespace sigma /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/ - definition sigma_eq_unc : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2), u = v + definition sigma_eq_unc [unfold 5] : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2), u = v | sigma_eq_unc ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂ definition dpair_sigma_eq_unc : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2), @@ -96,14 +96,15 @@ namespace sigma : transport (λx, B' x.1) (@sigma_eq_unc A B u v pq) = transport B' pq.1 := destruct pq tr_pr1_sigma_eq - definition is_equiv_sigma_eq [instance] (u v : Σa, B a) + definition is_equiv_sigma_eq [instance] [constructor] (u v : Σa, B a) : is_equiv (@sigma_eq_unc A B u v) := adjointify sigma_eq_unc (λp, ⟨p..1, p..2⟩) sigma_eq_eta_unc dpair_sigma_eq_unc - definition sigma_eq_equiv (u v : Σa, B a) : (u = v) ≃ (Σ(p : u.1 = v.1), u.2 =[p] v.2) := + definition sigma_eq_equiv [constructor] (u v : Σa, B a) + : (u = v) ≃ (Σ(p : u.1 = v.1), u.2 =[p] v.2) := (equiv.mk sigma_eq_unc _)⁻¹ᵉ definition dpair_eq_dpair_con (p1 : a = a' ) (q1 : b =[p1] b' ) @@ -243,7 +244,7 @@ namespace sigma definition sigma_equiv_sigma_right [constructor] {B' : A → Type} (Hg : Π a, B a ≃ B' a) : (Σa, B a) ≃ Σa, B' a := - sigma_equiv_sigma equiv.refl Hg + sigma_equiv_sigma equiv.rfl Hg definition sigma_equiv_sigma_left [constructor] (Hf : A ≃ A') : (Σa, B a) ≃ (Σa', B (to_inv Hf a')) := @@ -307,7 +308,7 @@ namespace sigma calc (Σa a', C (a, a')) ≃ Σu, C u : assoc_equiv_prod ... ≃ Σv, C (flip v) : sigma_equiv_sigma !prod_comm_equiv - (λu, prod.destruct u (λa a', equiv.refl)) + (λu, prod.destruct u (λa a', equiv.rfl)) ... ≃ Σa' a, C (a, a') : assoc_equiv_prod definition sigma_comm_equiv [constructor] (C : A → A' → Type) @@ -447,15 +448,17 @@ namespace sigma notation [parsing_only] `{` binder `|` r:(scoped:1 P, subtype P) `}` := r /- To prove equality in a subtype, we only need equality of the first component. -/ - definition subtype_eq [H : Πa, is_prop (B a)] {u v : {a | B a}} : u.1 = v.1 → u = v := + definition subtype_eq [unfold_full] [H : Πa, is_prop (B a)] {u v : {a | B a}} : + u.1 = v.1 → u = v := sigma_eq_unc ∘ inv pr1 - definition is_equiv_subtype_eq [H : Πa, is_prop (B a)] (u v : {a | B a}) + definition is_equiv_subtype_eq [constructor] [H : Πa, is_prop (B a)] (u v : {a | B a}) : is_equiv (subtype_eq : u.1 = v.1 → u = v) := !is_equiv_compose local attribute is_equiv_subtype_eq [instance] - definition equiv_subtype [H : Πa, is_prop (B a)] (u v : {a | B a}) : (u.1 = v.1) ≃ (u = v) := + definition equiv_subtype [constructor] [H : Πa, is_prop (B a)] (u v : {a | B a}) : + (u.1 = v.1) ≃ (u = v) := equiv.mk !subtype_eq _ definition subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_prop (B a)] (u v : Σa, B a) diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean index 652f5a290..91365b1f5 100644 --- a/hott/types/sum.hlean +++ b/hott/types/sum.hlean @@ -137,10 +137,10 @@ namespace sum equiv.mk _ (is_equiv_sum_functor f g) definition sum_equiv_sum_left [constructor] (g : B ≃ B') : A + B ≃ A + B' := - sum_equiv_sum equiv.refl g + sum_equiv_sum equiv.rfl g definition sum_equiv_sum_right [constructor] (f : A ≃ A') : A + B ≃ A' + B := - sum_equiv_sum f equiv.refl + sum_equiv_sum f equiv.rfl definition flip [unfold 3] : A + B → B + A | flip (inl a) := inr a diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 048defcca..0ebf33c30 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -298,6 +298,48 @@ namespace is_trunc { apply minus_one_le_succ}} end + /- univalence for truncated types -/ + definition teq_equiv_equiv {n : ℕ₋₂} {A B : n-Type} : (A = B) ≃ (A ≃ B) := + trunctype_eq_equiv n A B ⬝e eq_equiv_equiv A B + + definition tua {n : ℕ₋₂} {A B : n-Type} (f : A ≃ B) : A = B := + (trunctype_eq_equiv n A B)⁻¹ᶠ (ua f) + + definition tua_refl {n : ℕ₋₂} (A : n-Type) : tua (@erfl A) = idp := + begin + refine ap (trunctype_eq_equiv n A A)⁻¹ᶠ (ua_refl A) ⬝ _, + esimp, refine ap (eq_of_fn_eq_fn _) _ ⬝ !eq_of_fn_eq_fn'_idp , + esimp, apply ap (dpair_eq_dpair idp), apply is_prop.elim + end + + definition tua_trans {n : ℕ₋₂} {A B C : n-Type} (f : A ≃ B) (g : B ≃ C) + : tua (f ⬝e g) = tua f ⬝ tua g := + begin + refine ap (trunctype_eq_equiv n A C)⁻¹ᶠ (ua_trans f g) ⬝ _, + esimp, refine ap (eq_of_fn_eq_fn _) _ ⬝ !eq_of_fn_eq_fn'_con, + refine _ ⬝ !dpair_eq_dpair_con, + apply ap (dpair_eq_dpair _), apply is_prop.elim + end + + definition tua_symm {n : ℕ₋₂} {A B : n-Type} (f : A ≃ B) : tua f⁻¹ᵉ = (tua f)⁻¹ := + begin + apply eq_inv_of_con_eq_idp', + refine !tua_trans⁻¹ ⬝ _, + refine ap tua _ ⬝ !tua_refl, + apply equiv_eq, exact to_right_inv f + end + + definition tcast [unfold 4] {n : ℕ₋₂} {A B : n-Type} (p : A = B) (a : A) : B := + cast (ap trunctype.carrier p) a + + theorem tcast_tua_fn {n : ℕ₋₂} {A B : n-Type} (f : A ≃ B) : tcast (tua f) = to_fun f := + begin + cases A with A HA, cases B with B HB, esimp at *, + induction f using rec_on_ua_idp, esimp, + have HA = HB, from !is_prop.elim, cases this, + exact ap tcast !tua_refl + end + /- theorems about decidable equality and axiom K -/ theorem is_set_of_axiom_K {A : Type} (K : Π{a : A} (p : a = a), p = idp) : is_set A := is_set.mk _ (λa b p q, eq.rec K q p) diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean index f60e2fdc0..4734bfcf6 100644 --- a/hott/types/univ.hlean +++ b/hott/types/univ.hlean @@ -120,7 +120,7 @@ namespace univ (λb, !sigma_assoc_equiv⁻¹ᵉ) ... ≃ Σb (Y : Type*), Y = fiber f b : sigma_equiv_sigma_right (λb, sigma_equiv_sigma (pType.sigma_char)⁻¹ᵉ - (λv, sigma.rec_on v (λx y, equiv.refl))) + (λv, sigma.rec_on v (λx y, equiv.rfl))) ... ≃ Σ(Y : Type*) b, Y = fiber f b : sigma_comm_equiv ... ≃ pullback pType.carrier (fiber f) : !pullback.sigma_char⁻¹ᵉ ) diff --git a/library/theories/move.lean b/library/theories/move.lean index b2d468368..eafd096cc 100644 --- a/library/theories/move.lean +++ b/library/theories/move.lean @@ -42,9 +42,18 @@ quot.exact (by rewrite quot.mk_repr_eq) end quot - -- move to data.set.basic +-- move to algebra.ring + +theorem mul_two {A : Type} [semiring A] (a : A) : a * 2 = a + a := +by rewrite [-one_add_one_eq_two, left_distrib, +mul_one] + +theorem two_mul {A : Type} [semiring A] (a : A) : 2 * a = a + a := +by rewrite [-one_add_one_eq_two, right_distrib, +one_mul] + +-- move to data.set + namespace set open function