diff --git a/hott/algebra/category/constructions/comma.hlean b/hott/algebra/category/constructions/comma.hlean index e2473c61d..29342b46d 100644 --- a/hott/algebra/category/constructions/comma.hlean +++ b/hott/algebra/category/constructions/comma.hlean @@ -1,7 +1,6 @@ /- 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 Comma category diff --git a/hott/algebra/category/constructions/constructions.md b/hott/algebra/category/constructions/constructions.md index fa853b93c..c1f2cd11a 100644 --- a/hott/algebra/category/constructions/constructions.md +++ b/hott/algebra/category/constructions/constructions.md @@ -14,6 +14,7 @@ Common categories and constructions on categories. The following files are in th Pushout of categories, pushout of groupoids. * [fundamental_groupoid](fundamental_groupoid.hlean) : The fundamental groupoid of a type * [rezk](rezk.hlean) : Rezk completion +* [pullback](pullback.hlean) : Pulling back the structure of a precategory along a map between types. This is not about pullbacks in a 1-category. Discrete, indiscrete or finite categories: diff --git a/hott/algebra/category/constructions/default.hlean b/hott/algebra/category/constructions/default.hlean index 2d73adaa5..d517ab117 100644 --- a/hott/algebra/category/constructions/default.hlean +++ b/hott/algebra/category/constructions/default.hlean @@ -5,4 +5,4 @@ Authors: Floris van Doorn -/ import .functor .set .opposite .product .comma .sum .discrete .indiscrete .terminal .initial .order - .pushout .fundamental_groupoid + .pushout .fundamental_groupoid .pullback diff --git a/hott/algebra/category/constructions/pullback.hlean b/hott/algebra/category/constructions/pullback.hlean new file mode 100644 index 000000000..c1029d142 --- /dev/null +++ b/hott/algebra/category/constructions/pullback.hlean @@ -0,0 +1,62 @@ +/- +Copyright (c) 2018 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn + +We pull back the structure of a category B along a map between the types A and (ob B). +We shorten the word "pullback" to "pb" to keep names relatively short. +-/ + + +import ..functor.equivalence + +open category eq is_trunc is_equiv sigma function equiv prod + +namespace category + open functor + + definition pb_precategory [constructor] {A B : Type} (f : A → B) (C : precategory B) : + precategory A := + precategory.mk (λa a', hom (f a) (f a')) (λa a' a'' h g, h ∘ g) (λa, ID (f a)) + (λa a' a'' a''' k h g, assoc k h g) (λa a' g, id_left g) (λa a' g, id_right g) + + definition pb_Precategory [constructor] {A : Type} (C : Precategory) (f : A → C) : + Precategory := + Precategory.mk A (pb_precategory f C) + + definition pb_Precategory_functor [constructor] {A : Type} (C : Precategory) (f : A → C) : + pb_Precategory C f ⇒ C := + functor.mk f (λa a' g, g) proof (λa, idp) qed proof (λa a' a'' h g, idp) qed + + definition fully_faithful_pb_Precategory_functor {A : Type} (C : Precategory) + (f : A → C) : fully_faithful (pb_Precategory_functor C f) := + begin intro a a', apply is_equiv_id end + + definition split_essentially_surjective_pb_Precategory_functor {A : Type} (C : Precategory) + (f : A → C) (H : is_split_surjective f) : + split_essentially_surjective (pb_Precategory_functor C f) := + begin intro c, cases H c with a p, exact ⟨a, iso.iso_of_eq p⟩ end + + definition is_equivalence_pb_Precategory_functor {A : Type} (C : Precategory) + (f : A → C) (H : is_split_surjective f) : is_equivalence (pb_Precategory_functor C f) := + @(is_equivalence_of_fully_faithful_of_split_essentially_surjective _) + (fully_faithful_pb_Precategory_functor C f) + (split_essentially_surjective_pb_Precategory_functor C f H) + + definition pb_Precategory_equivalence [constructor] {A : Type} (C : Precategory) (f : A → C) + (H : is_split_surjective f) : pb_Precategory C f ≃c C := + equivalence.mk _ (is_equivalence_pb_Precategory_functor C f H) + + definition pb_Precategory_equivalence_of_equiv [constructor] {A : Type} (C : Precategory) + (f : A ≃ C) : pb_Precategory C f ≃c C := + pb_Precategory_equivalence C f (is_split_surjective_of_is_retraction f) + + definition is_isomorphism_pb_Precategory_functor [constructor] {A : Type} (C : Precategory) + (f : A ≃ C) : is_isomorphism (pb_Precategory_functor C f) := + (fully_faithful_pb_Precategory_functor C f, to_is_equiv f) + + definition pb_Precategory_isomorphism [constructor] {A : Type} (C : Precategory) (f : A ≃ C) : + pb_Precategory C f ≅c C := + isomorphism.mk _ (is_isomorphism_pb_Precategory_functor C f) + +end category diff --git a/hott/algebra/graph.hlean b/hott/algebra/graph.hlean index a86b7aeb8..7817aa8da 100644 --- a/hott/algebra/graph.hlean +++ b/hott/algebra/graph.hlean @@ -326,5 +326,23 @@ namespace paths { exact v_0 ⬝ v_1} end + inductive all (T : Π⦃a₁ a₂ : A⦄, R a₁ a₂ → Type) : Π⦃a₁ a₂ : A⦄, paths R a₁ a₂ → Type := + | nil {} : Π{a : A}, all T (@nil A R a) + | cons : Π{a₁ a₂ a₃ : A} {r : R a₂ a₃} {p : paths R a₁ a₂}, T r → all T p → all T (cons r p) + + inductive Exists (T : Π⦃a₁ a₂ : A⦄, R a₁ a₂ → Type) : Π⦃a₁ a₂ : A⦄, paths R a₁ a₂ → Type := + | base : Π{a₁ a₂ a₃ : A} {r : R a₂ a₃} (p : paths R a₁ a₂), T r → Exists T (cons r p) + | cons : Π{a₁ a₂ a₃ : A} (r : R a₂ a₃) {p : paths R a₁ a₂}, Exists T p → Exists T (cons r p) + + inductive mem (l : R a₃ a₄) : Π⦃a₁ a₂ : A⦄, paths R a₁ a₂ → Type := + | base : Π{a₂ : A} (p : paths R a₂ a₃), mem l (cons l p) + | cons : Π{a₁ a₂ a₃ : A} (r : R a₂ a₃) {p : paths R a₁ a₂}, mem l p → mem l (cons r p) + + definition len (p : paths R a₁ a₂) : ℕ := + begin + induction p with a a₁ a₂ a₃ r p IH, + { exact 0 }, + { exact nat.succ IH } + end end paths diff --git a/hott/function.hlean b/hott/function.hlean index 6f2cf3a46..d10c8f333 100644 --- a/hott/function.hlean +++ b/hott/function.hlean @@ -42,6 +42,9 @@ structure is_constant [class] (f : A → B) := (pt : B) (eq : Π(a : A), f a = pt) +definition merely_constant {A B : Type} (f : A → B) : Type := +Σb, Πa, merely (f a = b) + structure is_conditionally_constant [class] (f : A → B) := (g : ∥A∥ → B) (eq : Π(a : A), f a = g (tr a)) @@ -171,6 +174,14 @@ namespace function exact tr (fiber.mk (f a) p) end + definition is_contr_of_is_surjective (f : A → B) (H : is_surjective f) (HA : is_contr A) + (HB : is_set B) : is_contr B := + is_contr.mk (f !center) begin intro b, induction H b, exact ap f !is_prop.elim ⬝ p end + + definition is_surjective_of_is_contr [constructor] (f : A → B) (a : A) (H : is_contr B) : + is_surjective f := + λb, image.mk a !eq_of_is_contr + definition is_weakly_constant_ap [instance] [H : is_weakly_constant f] (a a' : A) : is_weakly_constant (ap f : a = a' → f a = f a') := take p q : a = a', @@ -359,6 +370,20 @@ namespace function is_surjective f' := is_surjective_homotopy_closed p⁻¹ʰᵗʸ H + definition is_surjective_factor {g : B → C} (f : A → B) (h : A → C) (H : g ∘ f ~ h) : + is_surjective h → is_surjective g := + begin + induction H using homotopy.rec_on_idp, + intro S, + intro c, + note p := S c, + induction p, + apply tr, + fapply fiber.mk, + exact f a, + exact p + end + definition is_equiv_ap1_gen_of_is_embedding {A B : Type} (f : A → B) [is_embedding f] {a a' : A} {b b' : B} (q : f a = b) (q' : f a' = b') : is_equiv (ap1_gen f q q') := begin @@ -383,6 +408,32 @@ namespace function !loopn_succ_in⁻¹ᵉ* end + definition is_contr_of_is_embedding (f : A → B) (H : is_embedding f) (HB : is_prop B) + (a₀ : A) : is_contr A := + is_contr.mk a₀ (λa, is_injective_of_is_embedding (is_prop.elim (f a₀) (f a))) + + definition is_embedding_of_square {A B C D : Type} {f : A → B} {g : C → D} (h : A ≃ C) + (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (Hf : is_embedding f) : is_embedding g := + begin + apply is_embedding_homotopy_closed, exact inv_homotopy_of_homotopy_pre _ _ _ s, + apply is_embedding_compose, apply is_embedding_compose, + apply is_embedding_of_is_equiv, exact Hf, apply is_embedding_of_is_equiv + end + + definition is_embedding_of_square_rev {A B C D : Type} {f : A → B} {g : C → D} (h : A ≃ C) + (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (Hg : is_embedding g) : is_embedding f := + is_embedding_of_square h⁻¹ᵉ k⁻¹ᵉ s⁻¹ʰᵗʸᵛ Hg + + definition is_embedding_factor [is_set A] [is_set B] (g : B → C) (h : A → C) (H : g ∘ f ~ h) : + is_embedding h → is_embedding f := + begin + induction H using homotopy.rec_on_idp, + intro E, + fapply is_embedding_of_is_injective, + intro x y p, + fapply @is_injective_of_is_embedding _ _ _ E _ _ (ap g p) + end + /- The definitions is_surjective_of_is_equiv diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index 132d87b1e..4bd1cb63e 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -724,6 +724,24 @@ namespace chain_complex apply LES_is_equiv_of_trivial, apply HX1, apply HX2 end + definition LES_is_contr_of_is_embedding_of_is_surjective (n : ℕ) + (H : is_embedding (π→[n] f)) (H2 : is_surjective (π→[n+1] f)) : is_contr (π[n] (pfiber f)) := + begin + rexact @is_contr_of_is_embedding_of_is_surjective +3ℕ LES_of_homotopy_groups (n, 0) + (is_exact_LES_of_homotopy_groups _) proof H qed proof H2 qed + end + + definition is_contr_homotopy_group_fiber {n : ℕ} + (H1 : is_embedding (π→[n] f)) (H2 : is_surjective (π→g[n+1] f)) : is_contr (π[n] (pfiber f)) := + begin + apply @is_contr_of_is_embedding_of_is_surjective +3ℕ LES_of_homotopy_groups (n, 0), + exact is_exact_LES_of_homotopy_groups (n, 1), exact H1, exact H2 + end + + definition is_contr_homotopy_group_fiber_of_is_equiv {n : ℕ} + (H1 : is_equiv (π→[n] f)) (H2 : is_equiv (π→g[n+1] f)) : is_contr (π[n] (pfiber f)) := + is_contr_homotopy_group_fiber (is_embedding_of_is_equiv _) (is_surjective_of_is_equiv _) + end /- diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index aecccb4d7..e375511a8 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -27,6 +27,13 @@ namespace is_conn exact is_contr_equiv_closed (trunc_equiv_trunc n H) C, end + definition is_conn_equiv_closed_rev (n : ℕ₋₂) {A B : Type} (f : A ≃ B) (H : is_conn n B) : + is_conn n A := + is_conn_equiv_closed n f⁻¹ᵉ _ + + definition is_conn_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_conn n A) : is_conn m A := + transport (λk, is_conn k A) p H + theorem is_conn_of_le (A : Type) {n k : ℕ₋₂} (H : n ≤ k) [is_conn k A] : is_conn n A := is_contr_equiv_closed (trunc_trunc_equiv_left _ H) _ @@ -256,6 +263,7 @@ namespace is_conn @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H + /- introduction rules for connectedness -/ -- all types are -2-connected definition is_conn_minus_two (A : Type) : is_conn -2 A := _ @@ -267,6 +275,26 @@ namespace is_conn definition is_conn_minus_one_pointed [instance] (A : Type*) : is_conn -1 A := is_conn_minus_one A (tr pt) + definition is_conn_succ_intro {n : ℕ₋₂} {A : Type} (a : trunc (n.+1) A) + (H2 : Π(a a' : A), is_conn n (a = a')) : is_conn (n.+1) A := + begin + refine is_contr_of_inhabited_prop _ _, + { exact a }, + { apply is_trunc_succ_intro, + refine trunc.rec _, intro a, refine trunc.rec _, intro a', + exact is_contr_equiv_closed !tr_eq_tr_equiv⁻¹ᵉ _ } + end + + definition is_conn_zero {A : Type} (a₀ : trunc 0 A) (p : Πa a' : A, ∥ a = a' ∥) : is_conn 0 A := + is_conn_succ_intro a₀ (λa a', is_conn_minus_one _ (p a a')) + + definition is_conn_zero_pointed {A : Type*} (p : Πa a' : A, ∥ a = a' ∥) : is_conn 0 A := + is_conn_zero (tr pt) p + + definition is_conn_zero_pointed' {A : Type*} (p : Πa : A, ∥ a = pt ∥) : is_conn 0 A := + is_conn_zero_pointed (λa a', tconcat (p a) (tinverse (p a'))) + + /- connectedness of certain types -/ definition is_conn_trunc [instance] (A : Type) (n k : ℕ₋₂) [H : is_conn n A] : is_conn n (trunc k A) := is_contr_equiv_closed !trunc_trunc_equiv_trunc_trunc _ @@ -283,8 +311,60 @@ namespace is_conn : is_conn n (ptrunc k A) := is_conn_trunc A n k - -- the following trivial cases are solved by type class inference + definition is_conn_pathover (n : ℕ₋₂) {A : Type} {B : A → Type} {a a' : A} (p : a = a') (b : B a) + (b' : B a') [is_conn (n.+1) (B a')] : is_conn n (b =[p] b') := + is_conn_equiv_closed_rev n !pathover_equiv_tr_eq _ + + open sigma + lemma is_conn_sigma [instance] {A : Type} (B : A → Type) (n : ℕ₋₂) + [HA : is_conn n A] [HB : Πa, is_conn n (B a)] : is_conn n (Σa, B a) := + begin + revert A B HA HB, induction n with n IH: intro A B HA HB, + { apply is_conn_minus_two }, + apply is_conn_succ_intro, + { induction center (trunc (n.+1) A) with a, induction center (trunc (n.+1) (B a)) with b, + exact tr ⟨a, b⟩ }, + intro a a', refine is_conn_equiv_closed_rev n !sigma_eq_equiv _, + apply IH, apply is_conn_eq, intro p, apply is_conn_pathover + /- an alternative proof of the successor case -/ + -- induction center (trunc (n.+1) A) with a₀, + -- induction center (trunc (n.+1) (B a₀)) with b₀, + -- apply is_contr.mk (tr ⟨a₀, b₀⟩), + -- intro ab, induction ab with ab, induction ab with a b, + -- induction tr_eq_tr_equiv n a₀ a !is_prop.elim with p, induction p, + -- induction tr_eq_tr_equiv n b₀ b !is_prop.elim with q, induction q, + -- reflexivity + end + + lemma is_conn_prod [instance] (A B : Type) (n : ℕ₋₂) [is_conn n A] [is_conn n B] : + is_conn n (A × B) := + is_conn_equiv_closed n !sigma.equiv_prod _ + + lemma is_conn_fun_of_is_conn {A B : Type} (n : ℕ₋₂) (f : A → B) + [HA : is_conn n A] [HB : is_conn (n.+1) B] : is_conn_fun n f := + λb, is_conn_equiv_closed_rev n !fiber.sigma_char _ + + definition is_conn_fiber_of_is_conn (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B) [is_conn n A] + [is_conn (n.+1) B] : is_conn n (fiber f b) := + is_conn_fun_of_is_conn n f b + + lemma is_conn_pfiber_of_is_conn {A B : Type*} (n : ℕ₋₂) (f : A →* B) + [HA : is_conn n A] [HB : is_conn (n.+1) B] : is_conn n (pfiber f) := + is_conn_fun_of_is_conn n f pt + definition is_conn_of_is_contr (k : ℕ₋₂) (A : Type) [is_contr A] : is_conn k A := _ + + definition is_conn_succ_of_is_conn_loop {n : ℕ₋₂} {A : Type*} + (H : is_conn 0 A) (H2 : is_conn n (Ω A)) : is_conn (n.+1) A := + begin + apply is_conn_succ_intro, exact tr pt, + intros a a', + induction merely_of_minus_one_conn (is_conn_eq -1 a a') with p, induction p, + induction merely_of_minus_one_conn (is_conn_eq -1 pt a) with p, induction p, + exact H2 + end + + /- connected functions -/ definition is_conn_fun_of_is_equiv (k : ℕ₋₂) {A B : Type} (f : A → B) [is_equiv f] : is_conn_fun k f := _ @@ -292,6 +372,10 @@ namespace is_conn definition is_conn_fun_id (k : ℕ₋₂) (A : Type) : is_conn_fun k (@id A) := λa, _ + definition is_conn_fun_compose (k : ℕ₋₂) {A B C : Type} {g : B → C} {f : A → B} + (Hg : is_conn_fun k g) (Hf : is_conn_fun k f) : is_conn_fun k (g ∘ f) := + λc, is_conn_equiv_closed_rev k (fiber_compose_equiv g f c) _ + -- Lemma 7.5.14 theorem is_equiv_trunc_functor_of_is_conn_fun [instance] {A B : Type} (n : ℕ₋₂) (f : A → B) [H : is_conn_fun n f] : is_equiv (trunc_functor n f) := @@ -303,10 +387,14 @@ namespace is_conn { intro a, induction a with a, esimp, rewrite [center_eq (tr (fiber.mk a idp))]} end - theorem trunc_equiv_trunc_of_is_conn_fun {A B : Type} (n : ℕ₋₂) (f : A → B) + definition trunc_equiv_trunc_of_is_conn_fun {A B : Type} (n : ℕ₋₂) (f : A → B) [H : is_conn_fun n f] : trunc n A ≃ trunc n B := equiv.mk (trunc_functor n f) (is_equiv_trunc_functor_of_is_conn_fun n f) + definition ptrunc_pequiv_ptrunc_of_is_conn_fun {A B : Type*} (n : ℕ₋₂) (f : A →* B) + [H : is_conn_fun n f] : ptrunc n A ≃* ptrunc n B := + pequiv_of_pmap (ptrunc_functor n f) (is_equiv_trunc_functor_of_is_conn_fun n f) + definition is_conn_fun_trunc_functor_of_le {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : k ≤ n) [H2 : is_conn_fun k f] : is_conn_fun k (trunc_functor n f) := begin @@ -362,57 +450,6 @@ namespace is_conn rewrite -of_nat_add_two, exact _ end - definition is_conn_equiv_closed_rev (n : ℕ₋₂) {A B : Type} (f : A ≃ B) (H : is_conn n B) : - is_conn n A := - is_conn_equiv_closed n f⁻¹ᵉ _ - - definition is_conn_succ_intro {n : ℕ₋₂} {A : Type} (a : trunc (n.+1) A) - (H2 : Π(a a' : A), is_conn n (a = a')) : is_conn (n.+1) A := - begin - refine is_contr_of_inhabited_prop _ _, - { exact a }, - { apply is_trunc_succ_intro, - refine trunc.rec _, intro a, refine trunc.rec _, intro a', - exact is_contr_equiv_closed !tr_eq_tr_equiv⁻¹ᵉ _ } - end - - definition is_conn_pathover (n : ℕ₋₂) {A : Type} {B : A → Type} {a a' : A} (p : a = a') (b : B a) - (b' : B a') [is_conn (n.+1) (B a')] : is_conn n (b =[p] b') := - is_conn_equiv_closed_rev n !pathover_equiv_tr_eq _ - - open sigma - lemma is_conn_sigma [instance] {A : Type} (B : A → Type) (n : ℕ₋₂) - [HA : is_conn n A] [HB : Πa, is_conn n (B a)] : is_conn n (Σa, B a) := - begin - revert A B HA HB, induction n with n IH: intro A B HA HB, - { apply is_conn_minus_two }, - apply is_conn_succ_intro, - { induction center (trunc (n.+1) A) with a, induction center (trunc (n.+1) (B a)) with b, - exact tr ⟨a, b⟩ }, - intro a a', refine is_conn_equiv_closed_rev n !sigma_eq_equiv _, - apply IH, apply is_conn_eq, intro p, apply is_conn_pathover - /- an alternative proof of the successor case -/ - -- induction center (trunc (n.+1) A) with a₀, - -- induction center (trunc (n.+1) (B a₀)) with b₀, - -- apply is_contr.mk (tr ⟨a₀, b₀⟩), - -- intro ab, induction ab with ab, induction ab with a b, - -- induction tr_eq_tr_equiv n a₀ a !is_prop.elim with p, induction p, - -- induction tr_eq_tr_equiv n b₀ b !is_prop.elim with q, induction q, - -- reflexivity - end - - lemma is_conn_prod [instance] (A B : Type) (n : ℕ₋₂) [is_conn n A] [is_conn n B] : - is_conn n (A × B) := - is_conn_equiv_closed n !sigma.equiv_prod _ - - lemma is_conn_fun_of_is_conn {A B : Type} (n : ℕ₋₂) (f : A → B) - [HA : is_conn n A] [HB : is_conn (n.+1) B] : is_conn_fun n f := - λb, is_conn_equiv_closed_rev n !fiber.sigma_char _ - - lemma is_conn_pfiber {A B : Type*} (n : ℕ₋₂) (f : A →* B) - [HA : is_conn n A] [HB : is_conn (n.+1) B] : is_conn n (pfiber f) := - is_conn_fun_of_is_conn n f pt - definition is_conn_fun_trunc_elim_of_le {n k : ℕ₋₂} {A B : Type} [is_trunc n B] (f : A → B) (H : k ≤ n) [H2 : is_conn_fun k f] : is_conn_fun k (trunc.elim f : trunc n A → B) := begin @@ -545,12 +582,173 @@ section definition is_trunc_ptruncconntype [instance] {n k : ℕ₋₂} (X : n-Type*[k]) : is_trunc n (ptruncconntype._trans_of_to_pconntype X) := trunctype.struct X - - definition ptruncconntype_eq {n k : ℕ₋₂} {X Y : n-Type*[k]} (p : X ≃* Y) : X = Y := - begin - induction X with X Xt Xp Xc, induction Y with Y Yt Yp Yc, - note q := pType_eq_elim (eq_of_pequiv p), - cases q with r s, esimp at *, induction r, - exact ap0111 (ptruncconntype.mk X) !is_prop.elim (eq_of_pathover_idp s) !is_prop.elim - end end + +namespace is_conn + +open sigma sigma.ops prod prod.ops + +definition pconntype.sigma_char [constructor] (k : ℕ₋₂) : + Type*[k] ≃ Σ(X : Type*), is_conn k X := +equiv.MK (λX, ⟨pconntype.to_pType X, _⟩) + (λX, pconntype.mk (carrier X.1) X.2 pt) + begin intro X, induction X with X HX, induction X, reflexivity end + begin intro X, induction X, reflexivity end + +definition is_embedding_pconntype_to_pType (k : ℕ₋₂) : is_embedding (@pconntype.to_pType k) := +begin + intro X Y, fapply is_equiv_of_equiv_of_homotopy, + { exact eq_equiv_fn_eq (pconntype.sigma_char k) _ _ ⬝e subtype_eq_equiv _ _ }, + intro p, induction p, reflexivity +end + +definition pconntype_eq_equiv {k : ℕ₋₂} (X Y : Type*[k]) : (X = Y) ≃ (X ≃* Y) := +equiv.mk _ (is_embedding_pconntype_to_pType k X Y) ⬝e pType_eq_equiv X Y + +definition pconntype_eq {k : ℕ₋₂} {X Y : Type*[k]} (e : X ≃* Y) : X = Y := +(pconntype_eq_equiv X Y)⁻¹ᵉ e + +definition ptruncconntype.sigma_char [constructor] (n k : ℕ₋₂) : + n-Type*[k] ≃ Σ(X : Type*), is_trunc n X × is_conn k X := +equiv.MK (λX, ⟨ptruncconntype._trans_of_to_pconntype_1 X, (_, _)⟩) + (λX, ptruncconntype.mk (carrier X.1) X.2.1 pt X.2.2) + begin intro X, induction X with X HX, induction HX, induction X, reflexivity end + begin intro X, induction X, reflexivity end + +definition ptruncconntype.sigma_char_pconntype [constructor] (n k : ℕ₋₂) : + n-Type*[k] ≃ Σ(X : Type*[k]), is_trunc n X := +equiv.MK (λX, ⟨ptruncconntype.to_pconntype X, _⟩) + (λX, ptruncconntype.mk (pconntype._trans_of_to_pType X.1) X.2 pt _) + begin intro X, induction X with X HX, induction HX, induction X, reflexivity end + begin intro X, induction X, reflexivity end + +definition is_embedding_ptruncconntype_to_pconntype (n k : ℕ₋₂) : + is_embedding (@ptruncconntype.to_pconntype n k) := +begin + intro X Y, fapply is_equiv_of_equiv_of_homotopy, + { exact eq_equiv_fn_eq (ptruncconntype.sigma_char_pconntype n k) _ _ ⬝e subtype_eq_equiv _ _ }, + intro p, induction p, reflexivity +end + +definition ptruncconntype_eq_equiv {n k : ℕ₋₂} (X Y : n-Type*[k]) : (X = Y) ≃ (X ≃* Y) := +equiv.mk _ (is_embedding_ptruncconntype_to_pconntype n k X Y) ⬝e pconntype_eq_equiv X Y + +definition ptruncconntype_eq {n k : ℕ₋₂} {X Y : n-Type*[k]} (e : X ≃* Y) : X = Y := +(ptruncconntype_eq_equiv X Y)⁻¹ᵉ e + +definition ptruncconntype_functor [constructor] {n n' k k' : ℕ₋₂} (p : n = n') (q : k = k') + (X : n-Type*[k]) : n'-Type*[k'] := +ptruncconntype.mk X (is_trunc_of_eq p _) pt (is_conn_of_eq q _) + +definition ptruncconntype_equiv [constructor] {n n' k k' : ℕ₋₂} (p : n = n') (q : k = k') : + n-Type*[k] ≃ n'-Type*[k'] := +equiv.MK (ptruncconntype_functor p q) (ptruncconntype_functor p⁻¹ q⁻¹) + (λX, ptruncconntype_eq pequiv.rfl) (λX, ptruncconntype_eq pequiv.rfl) + + +/- the k-connected cover of X, the fiber of the map X → ∥X∥ₖ. -/ +open trunc_index + +definition connect (k : ℕ) (X : Type*) : Type* := +pfiber (ptr k X) + +definition is_conn_connect (k : ℕ) (X : Type*) : is_conn k (connect k X) := +is_conn_fun_tr k X (tr pt) + +definition connconnect [constructor] (k : ℕ) (X : Type*) : Type*[k] := +pconntype.mk (connect k X) (is_conn_connect k X) pt + +definition connect_intro [constructor] {k : ℕ} {X : Type*} {Y : Type*} (H : is_conn k X) + (f : X →* Y) : X →* connect k Y := +pmap.mk (λx, fiber.mk (f x) (is_conn.elim (k.-1) _ (ap tr (respect_pt f)) x)) + begin + fapply fiber_eq, exact respect_pt f, apply is_conn.elim_β + end + +definition ppoint_connect_intro [constructor] {k : ℕ} {X : Type*} {Y : Type*} (H : is_conn k X) + (f : X →* Y) : ppoint (ptr k Y) ∘* connect_intro H f ~* f := +begin + induction f with f f₀, induction Y with Y y₀, esimp at (f,f₀), induction f₀, + fapply phomotopy.mk, + { intro x, reflexivity }, + { symmetry, esimp, apply point_fiber_eq } +end + +definition connect_intro_ppoint [constructor] {k : ℕ} {X : Type*} {Y : Type*} (H : is_conn k X) + (f : X →* connect k Y) : connect_intro H (ppoint (ptr k Y) ∘* f) ~* f := +begin + cases f with f f₀, + fapply phomotopy.mk, + { intro x, fapply fiber_eq, reflexivity, + refine @is_conn.elim (k.-1) _ _ _ (λx', !is_trunc_eq) _ x, + refine !is_conn.elim_β ⬝ _, + refine _ ⬝ !idp_con⁻¹, + symmetry, refine _ ⬝ !con_idp, exact fiber_eq_pr2 f₀ }, + { esimp, refine whisker_left _ !fiber_eq_eta ⬝ !fiber_eq_con ⬝ apd011 fiber_eq !idp_con _, esimp, + apply eq_pathover_constant_left, + refine whisker_right _ (whisker_right _ (whisker_right _ !is_conn.elim_β)) ⬝pv _, + esimp [connect], refine _ ⬝vp !con_idp, + apply move_bot_of_left, refine !idp_con ⬝ !con_idp⁻¹ ⬝ph _, + refine !con.assoc ⬝ !con.assoc ⬝pv _, apply whisker_tl, + note r := eq_bot_of_square (transpose (whisker_left_idp_square (fiber_eq_pr2 f₀))⁻¹ᵛ), + refine !con.assoc⁻¹ ⬝ whisker_right _ r⁻¹ ⬝pv _, clear r, + apply move_top_of_left, + refine whisker_right_idp (ap_con tr idp (ap point f₀))⁻¹ᵖ ⬝pv _, + exact (ap_con_idp_left tr (ap point f₀))⁻¹ʰ } +end + +definition connect_intro_equiv [constructor] {k : ℕ} {X : Type*} (Y : Type*) (H : is_conn k X) : + (X →* connect k Y) ≃ (X →* Y) := +begin + fapply equiv.MK, + { intro f, exact ppoint (ptr k Y) ∘* f }, + { intro g, exact connect_intro H g }, + { intro g, apply eq_of_phomotopy, exact ppoint_connect_intro H g }, + { intro f, apply eq_of_phomotopy, exact connect_intro_ppoint H f } +end + +definition connect_intro_pequiv [constructor] {k : ℕ} {X : Type*} (Y : Type*) (H : is_conn k X) : + ppmap X (connect k Y) ≃* ppmap X Y := +pequiv_of_equiv (connect_intro_equiv Y H) (eq_of_phomotopy !pcompose_pconst) + +definition connect_pequiv {k : ℕ} {X : Type*} (H : is_conn k X) : connect k X ≃* X := +@pfiber_pequiv_of_is_contr _ _ (ptr k X) H + +definition loop_connect (k : ℕ) (X : Type*) : Ω (connect (k+1) X) ≃* connect k (Ω X) := +loop_pfiber (ptr (k+1) X) ⬝e* +pfiber_pequiv_of_square pequiv.rfl (loop_ptrunc_pequiv k X) + (phomotopy_of_phomotopy_pinv_left (ap1_ptr k X)) + +definition loopn_connect (k : ℕ) (X : Type*) : Ω[k+1] (connect k X) ≃* Ω[k+1] X := +loopn_pfiber (k+1) (ptr k X) ⬝e* +@pfiber_pequiv_of_is_contr _ _ _ (@is_contr_loop_of_is_trunc (k+1) _ !is_trunc_trunc) + +definition is_conn_of_is_conn_succ_nat (n : ℕ) (A : Type) [is_conn (n+1) A] : is_conn n A := +is_conn_of_is_conn_succ n A + +definition connect_functor (k : ℕ) {X Y : Type*} (f : X →* Y) : connect k X →* connect k Y := +pfiber_functor f (ptrunc_functor k f) (ptr_natural k f)⁻¹* + +definition connect_intro_pequiv_natural {k : ℕ} {X X' : Type*} {Y Y' : Type*} (f : X' →* X) + (g : Y →* Y') (H : is_conn k X) (H' : is_conn k X') : + psquare (connect_intro_pequiv Y H) (connect_intro_pequiv Y' H') + (ppcompose_left (connect_functor k g) ∘* ppcompose_right f) + (ppcompose_left g ∘* ppcompose_right f) := +begin + refine _ ⬝v* _, exact connect_intro_pequiv Y H', + { fapply phomotopy.mk, + { intro h, apply eq_of_phomotopy, apply passoc }, + { xrewrite [▸*, pcompose_right_eq_of_phomotopy, pcompose_left_eq_of_phomotopy, + -+eq_of_phomotopy_trans], + apply ap eq_of_phomotopy, apply passoc_pconst_middle }}, + { fapply phomotopy.mk, + { intro h, apply eq_of_phomotopy, + refine !passoc⁻¹* ⬝* pwhisker_right h (ppoint_natural _ _ _) ⬝* !passoc }, + { xrewrite [▸*, +pcompose_left_eq_of_phomotopy, -+eq_of_phomotopy_trans], + apply ap eq_of_phomotopy, + refine !trans_assoc ⬝ idp ◾** !passoc_pconst_right ⬝ _, + refine !trans_assoc ⬝ idp ◾** !pcompose_pconst_phomotopy ⬝ _, + apply symm_trans_eq_of_eq_trans, symmetry, apply passoc_pconst_right }} +end + +end is_conn diff --git a/hott/homotopy/freudenthal.hlean b/hott/homotopy/freudenthal.hlean index c634ea7ca..a7806ea8b 100644 --- a/hott/homotopy/freudenthal.hlean +++ b/hott/homotopy/freudenthal.hlean @@ -198,78 +198,90 @@ begin apply homotopy_group_succ_in_con} end - definition to_pmap_freudenthal_pequiv (n k : ℕ) (H : k ≤ 2 * n) (A : Type*) [is_conn n A] - : freudenthal_pequiv H A ~* ptrunc_functor k (loop_susp_unit A) := - begin - fapply phomotopy.mk, - { intro x, induction x with a, reflexivity }, - { refine !idp_con ⬝ _, refine _ ⬝ ap02 _ !idp_con⁻¹, refine _ ⬝ !ap_compose, apply ap_compose } - end +definition to_pmap_freudenthal_pequiv (n k : ℕ) (H : k ≤ 2 * n) (A : Type*) [is_conn n A] + : freudenthal_pequiv H A ~* ptrunc_functor k (loop_susp_unit A) := +begin + fapply phomotopy.mk, + { intro x, induction x with a, reflexivity }, + { refine !idp_con ⬝ _, refine _ ⬝ ap02 _ !idp_con⁻¹, refine _ ⬝ !ap_compose, apply ap_compose } +end - definition ptrunc_elim_freudenthal_pequiv (n k : ℕ) (H : k ≤ 2 * n) {A B : Type*} [is_conn n A] - (f : A →* Ω B) [is_trunc (k.+1) (B)] : - ptrunc.elim k (Ω→ (susp_elim f)) ∘* freudenthal_pequiv H A ~* ptrunc.elim k f := - begin - refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _, - refine !ptrunc_elim_ptrunc_functor ⬝* _, - exact ptrunc_elim_phomotopy k !ap1_susp_elim, - end +definition ptrunc_elim_freudenthal_pequiv (n k : ℕ) (H : k ≤ 2 * n) {A B : Type*} [is_conn n A] + (f : A →* Ω B) [is_trunc (k.+1) (B)] : + ptrunc.elim k (Ω→ (susp_elim f)) ∘* freudenthal_pequiv H A ~* ptrunc.elim k f := +begin + refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _, + refine !ptrunc_elim_ptrunc_functor ⬝* _, + exact ptrunc_elim_phomotopy k !ap1_susp_elim, +end + +definition freudenthal_pequiv_trunc_index' (A : Type*) (n : ℕ) (k : ℕ₋₂) [HA : is_conn n A] + (H : k ≤ of_nat (2 * n)) : ptrunc k A ≃* ptrunc k (Ω (susp A)) := +begin + assert lem : Π(l : ℕ₋₂), l ≤ 0 → ptrunc l A ≃* ptrunc l (Ω (susp A)), + { intro l H', exact ptrunc_pequiv_ptrunc_of_le H' (freudenthal_pequiv (zero_le (2 * n)) A) }, + cases k with k, { exact lem -2 (minus_two_le 0) }, + cases k with k, { exact lem -1 (succ_le_succ (minus_two_le -1)) }, + rewrite [-of_nat_add_two at *, add_two_sub_two at HA], + exact freudenthal_pequiv (le_of_of_nat_le_of_nat H) A +end namespace susp - definition iterate_susp_stability_pequiv_of_is_conn_0 (A : Type*) {k n : ℕ} [is_conn 0 A] - (H : k ≤ 2 * n) : π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) := - have is_conn n (iterate_susp n A), by rewrite [-zero_add n]; exact _, - freudenthal_homotopy_group_pequiv H (iterate_susp n A) +definition iterate_susp_stability_pequiv_of_is_conn_0 (A : Type*) {k n : ℕ} [is_conn 0 A] + (H : k ≤ 2 * n) : π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) := +have is_conn n (iterate_susp n A), by rewrite [-zero_add n]; exact _, +freudenthal_homotopy_group_pequiv H (iterate_susp n A) - definition iterate_susp_stability_isomorphism_of_is_conn_0 {k n : ℕ} (H : k + 1 ≤ 2 * n) - (A : Type*) [is_conn 0 A] : πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) := - have is_conn n (iterate_susp n A), by rewrite [-zero_add n]; exact _, - freudenthal_homotopy_group_isomorphism H (iterate_susp n A) +definition iterate_susp_stability_isomorphism_of_is_conn_0 {k n : ℕ} (H : k + 1 ≤ 2 * n) + (A : Type*) [is_conn 0 A] : πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) := +have is_conn n (iterate_susp n A), by rewrite [-zero_add n]; exact _, +freudenthal_homotopy_group_isomorphism H (iterate_susp n A) - definition stability_helper1 {k n : ℕ} (H : k + 2 ≤ 2 * n) : k ≤ 2 * pred n := - begin - rewrite [mul_pred_right], change pred (pred (k + 2)) ≤ pred (pred (2 * n)), - apply pred_le_pred, apply pred_le_pred, exact H - end +definition stability_helper1 {k n : ℕ} (H : k + 2 ≤ 2 * n) : k ≤ 2 * pred n := +begin + rewrite [mul_pred_right], change pred (pred (k + 2)) ≤ pred (pred (2 * n)), + apply pred_le_pred, apply pred_le_pred, exact H +end - definition stability_helper2 {k n : ℕ} (H : k + 2 ≤ 2 * n) (A : Type*) : - is_conn (pred n) (iterate_susp n A) := - have Π(n : ℕ), n = -1 + (n + 1), - begin intro n, induction n with n IH, reflexivity, exact ap succ IH end, - begin - cases n with n, - { exfalso, exact not_succ_le_zero _ H }, - { esimp, rewrite [this n], exact is_conn_iterate_susp -1 _ A } - end +definition stability_helper2 {k n : ℕ} (H : k + 2 ≤ 2 * n) (A : Type*) : + is_conn (pred n) (iterate_susp n A) := +have Π(n : ℕ), n = -1 + (n + 1), +begin intro n, induction n with n IH, reflexivity, exact ap succ IH end, +begin + cases n with n, + { exfalso, exact not_succ_le_zero _ H }, + { esimp, rewrite [this n], exact is_conn_iterate_susp -1 _ A } +end - definition iterate_susp_stability_pequiv {k n : ℕ} (H : k + 2 ≤ 2 * n) (A : Type*) : - π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) := - have is_conn (pred n) (iterate_susp n A), from stability_helper2 H A, - freudenthal_homotopy_group_pequiv (stability_helper1 H) (iterate_susp n A) +definition iterate_susp_stability_pequiv {k n : ℕ} (H : k + 2 ≤ 2 * n) (A : Type*) : + π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) := +have is_conn (pred n) (iterate_susp n A), from stability_helper2 H A, +freudenthal_homotopy_group_pequiv (stability_helper1 H) (iterate_susp n A) - definition iterate_susp_stability_isomorphism {k n : ℕ} (H : k + 3 ≤ 2 * n) (A : Type*) : - πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) := - have is_conn (pred n) (iterate_susp n A), from @stability_helper2 (k+1) n H A, - freudenthal_homotopy_group_isomorphism (stability_helper1 H) (iterate_susp n A) +definition iterate_susp_stability_isomorphism {k n : ℕ} (H : k + 3 ≤ 2 * n) (A : Type*) : + πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) := +have is_conn (pred n) (iterate_susp n A), from @stability_helper2 (k+1) n H A, +freudenthal_homotopy_group_isomorphism (stability_helper1 H) (iterate_susp n A) + +definition iterated_freudenthal_pequiv {n k m : ℕ} (H : k ≤ 2 * n) (A : Type*) [HA : is_conn n A] + : ptrunc k A ≃* ptrunc k (Ω[m] (iterate_susp m A)) := +begin + revert A n k HA H, induction m with m IH: intro A n k HA H, + { reflexivity }, + { have H2 : succ k ≤ 2 * succ n, + from calc + succ k ≤ succ (2 * n) : succ_le_succ H + ... ≤ 2 * succ n : self_le_succ, + exact calc + ptrunc k A ≃* ptrunc k (Ω (susp A)) : freudenthal_pequiv H A + ... ≃* Ω (ptrunc (succ k) (susp A)) : loop_ptrunc_pequiv + ... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_susp m (susp A)))) : + loop_pequiv_loop (IH (susp A) (succ n) (succ k) _ H2) + ... ≃* ptrunc k (Ω[succ m] (iterate_susp m (susp A))) : loop_ptrunc_pequiv + ... ≃* ptrunc k (Ω[succ m] (iterate_susp (succ m) A)) : + ptrunc_pequiv_ptrunc _ (loopn_pequiv_loopn _ !iterate_susp_succ_in)} +end - definition iterated_freudenthal_pequiv {n k m : ℕ} (H : k ≤ 2 * n) (A : Type*) [HA : is_conn n A] - : ptrunc k A ≃* ptrunc k (Ω[m] (iterate_susp m A)) := - begin - revert A n k HA H, induction m with m IH: intro A n k HA H, - { reflexivity }, - { have H2 : succ k ≤ 2 * succ n, - from calc - succ k ≤ succ (2 * n) : succ_le_succ H - ... ≤ 2 * succ n : self_le_succ, - exact calc - ptrunc k A ≃* ptrunc k (Ω (susp A)) : freudenthal_pequiv H A - ... ≃* Ω (ptrunc (succ k) (susp A)) : loop_ptrunc_pequiv - ... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_susp m (susp A)))) : - loop_pequiv_loop (IH (susp A) (succ n) (succ k) _ H2) - ... ≃* ptrunc k (Ω[succ m] (iterate_susp m (susp A))) : loop_ptrunc_pequiv - ... ≃* ptrunc k (Ω[succ m] (iterate_susp (succ m) A)) : - ptrunc_pequiv_ptrunc _ (loopn_pequiv_loopn _ !iterate_susp_succ_in)} - end end susp diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 4a6b2b330..2471f5121 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -407,6 +407,23 @@ namespace equiv ... = df x : by rewrite (apdt df (left_inv f x)) end + definition rec_eq_of_equiv {A : Type} {P : A → A → Type} (e : Πa a', a = a' ≃ P a a') + {a a' : A} (Q : P a a' → Type) (H : Π(q : a = a'), Q (e a a' q)) : + Π(p : P a a'), Q p := + equiv_rect (e a a') Q H + + definition rec_idp_of_equiv {A : Type} {P : A → A → Type} (e : Πa a', a = a' ≃ P a a') {a : A} + (r : P a a) (s : e a a idp = r) (Q : Πa', P a a' → Type) (H : Q a r) ⦃a' : A⦄ (p : P a a') : + Q a' p := + rec_eq_of_equiv e _ begin intro q, induction q, induction s, exact H end p + + definition rec_idp_of_equiv_idp {A : Type} {P : A → A → Type} (e : Πa a', a = a' ≃ P a a') {a : A} + (r : P a a) (s : e a a idp = r) (Q : Πa', P a a' → Type) (H : Q a r) : + rec_idp_of_equiv e r s Q H r = H := + begin + induction s, refine !is_equiv_rect_comp ⬝ _, reflexivity + end + section variables {A B : Type} (f : A ≃ B) {a : A} {b : B} diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 556bcee22..c320de092 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -314,7 +314,7 @@ namespace is_trunc (HA : is_prop A) (HB : is_prop B) : A ≃ B := equiv.mk f (is_equiv_of_is_prop f g _ _) - definition equiv_of_iff_of_is_prop [unfold 5] (HA : is_prop A) (HB : is_prop B) (H : A ↔ B) : + definition equiv_of_iff_of_is_prop [unfold 5] (H : A ↔ B) (HA : is_prop A) (HB : is_prop B) : A ≃ B := equiv_of_is_prop (iff.elim_left H) (iff.elim_right H) _ _ diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 4b622df0b..bf04ad552 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -15,19 +15,6 @@ namespace is_equiv variables {A B : Type} (f : A → B) [H : is_equiv f] include H /- is_equiv f is a mere proposition -/ - definition is_contr_fiber_of_is_equiv [instance] (b : B) : is_contr (fiber f b) := - is_contr.mk - (fiber.mk (f⁻¹ b) (right_inv f b)) - (λz, fiber.rec_on z (λa p, - fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc - right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) - : by rewrite inv_con_cancel_left - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p) : by rewrite ap_con_eq_con - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite [adj f] - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite con.assoc - ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_compose - ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_inv - ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p : by rewrite ap_con))) definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ~ id) := begin diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index fd35c7939..9b96c658b 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -138,7 +138,8 @@ namespace fiber begin intro x, induction x with a p, esimp at p, cases p, reflexivity end /- the general functoriality between fibers -/ - -- todo: show that this is an equivalence if g and h are, and use that for the special cases below + -- todo: transpose the hsquare in fiber_functor? + -- todo: show that the underlying map of fiber_equiv_of_square is fiber_functor definition fiber_functor [constructor] {A A' B B' : Type} {f : A → B} {f' : A' → B'} {b : B} {b' : B'} (g : A → A') (h : B → B') (H : hsquare g h f f') (p : h b = b') (x : fiber f b) : fiber f' b' := @@ -175,6 +176,17 @@ namespace fiber ... ≃ Σa b, f a = b : sigma_comm_equiv ... ≃ A : sigma_equiv_of_is_contr_right + definition fiber_compose_equiv {A B C : Type} (g : B → C) (f : A → B) (c : C) : + fiber (g ∘ f) c ≃ Σ(x : fiber g c), fiber f (point x) := + begin + fapply equiv.MK, + { intro x, exact ⟨fiber.mk (f (point x)) (point_eq x), fiber.mk (point x) idp⟩ }, + { intro x, exact fiber.mk (point x.2) (ap g (point_eq x.2) ⬝ point_eq x.1) }, + { intro x, induction x with x₁ x₂, induction x₁ with b p, induction x₂ with a q, + induction p, esimp at q, induction q, reflexivity }, + { intro x, induction x with a p, induction p, reflexivity } + end + -- pre and post composition with equivalences variable (f) protected definition equiv_postcompose [constructor] {B' : Type} (g : B ≃ B') --[H : is_equiv g] @@ -198,7 +210,7 @@ namespace fiber ... ≃ fiber f b : fiber.sigma_char definition fiber_equiv_of_square {A B C D : Type} {b : B} {d : D} {f : A → B} {g : C → D} - (h : A ≃ C) (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (p : k b = d) : fiber f b ≃ fiber g d := + (h : A ≃ C) (k : B ≃ D) (s : hsquare f g h k) (p : k b = d) : fiber f b ≃ fiber g d := calc fiber f b ≃ fiber (k ∘ f) (k b) : fiber.equiv_postcompose ... ≃ fiber (k ∘ f) d : fiber_equiv_basepoint (k ∘ f) p ... ≃ fiber (g ∘ h) d : fiber_equiv_of_homotopy s d @@ -208,6 +220,14 @@ namespace fiber (s : f ~ g ∘ h) : fiber f b ≃ fiber g b := fiber_equiv_of_square h erfl s idp + definition is_contr_fiber_equiv [instance] (f : A ≃ B) (b : B) : is_contr (fiber f b) := + is_contr_equiv_closed + (fiber_equiv_of_homotopy (to_left_inv f)⁻¹ʰᵗʸ _ ⬝e fiber.equiv_postcompose f f⁻¹ᵉ b) + !is_contr_fiber_id + + definition is_contr_fiber_of_is_equiv [instance] [is_equiv f] (b : B) : is_contr (fiber f b) := + is_contr_fiber_equiv (equiv.mk f _) b + definition fiber_star_equiv [constructor] (A : Type) : fiber (λx : A, star) star ≃ A := begin fapply equiv.MK, @@ -435,7 +455,7 @@ namespace fiber end definition is_contr_pfiber_pid (A : Type*) : is_contr (pfiber (pid A)) := - is_contr_fiber_id A pt + by exact is_contr_fiber_id A pt definition pfiber_functor [constructor] {A A' B B' : Type*} {f : A →* B} {f' : A' →* B'} (g : A →* A') (h : B →* B') (H : psquare g h f f') : pfiber f →* pfiber f' := @@ -470,3 +490,7 @@ definition is_contr_fun [reducible] (f : A → B) := is_trunc_fun -2 f definition is_trunc_fun_id (k : ℕ₋₂) (A : Type) : is_trunc_fun k (@id A) := λa, is_trunc_of_is_contr _ _ !is_contr_fiber_id + +definition is_trunc_fun_compose (k : ℕ₋₂) {A B C : Type} {g : B → C} {f : A → B} + (Hg : is_trunc_fun k g) (Hf : is_trunc_fun k f) : is_trunc_fun k (g ∘ f) := +λc, is_trunc_equiv_closed_rev k (fiber_compose_equiv g f c) _ diff --git a/hott/types/fin.hlean b/hott/types/fin.hlean index 94070f402..cfdf42f09 100644 --- a/hott/types/fin.hlean +++ b/hott/types/fin.hlean @@ -135,12 +135,11 @@ theorem val_lt : Π i : fin n, val i < n lemma max_lt (i j : fin n) : max i j < n := max_lt (is_lt i) (is_lt j) -definition lift [constructor] : fin n → Π m : nat, fin (n + m) -| (mk v h) m := mk v (lt_add_of_lt_right h m) +definition lift [constructor] (x : fin n) (m : ℕ) : fin (n + m) := +fin.mk x (lt_add_of_lt_right (is_lt x) m) -definition lift_succ [constructor] (i : fin n) : fin (nat.succ n) := -have r : fin (n+1), from lift i 1, -r +definition lift_succ [constructor] ⦃n : ℕ⦄ (x : fin n) : fin (nat.succ n) := +fin.mk x (le.step (is_lt x)) definition maxi [reducible] : fin (succ n) := mk n !lt_succ_self @@ -219,7 +218,7 @@ lemma lift_fun_eq {f : fin n → fin n} {i : fin n} : lift_fun f (lift_succ i) = lift_succ (f i) := begin rewrite [lift_fun_of_ne_max lift_succ_ne_max], do 2 congruence, - apply eq_of_veq, esimp, rewrite -val_lift, + apply eq_of_veq, reflexivity end lemma lift_fun_of_inj {f : fin n → fin n} : is_embedding f → is_embedding (lift_fun f) := @@ -238,8 +237,8 @@ begin rewrite [lift_fun_of_ne_max Pinmax, lift_fun_of_ne_max Pjnmax], intro Peq, apply eq_of_veq, cases i with i ilt, cases j with j jlt, esimp at *, - fapply veq_of_eq, apply is_injective_of_is_embedding, - apply @is_injective_of_is_embedding _ _ lift_succ _ _ _ Peq, + fapply veq_of_eq, apply @is_injective_of_is_embedding _ _ f, + apply @is_injective_of_is_embedding _ _ (@lift_succ _) _ _ _ Peq, end lemma lift_fun_inj : is_embedding (@lift_fun n) := @@ -329,9 +328,9 @@ lemma val_succ : Π (i : fin n), val (succ i) = nat.succ (val i) lemma succ_max : fin.succ maxi = (@maxi (nat.succ n)) := rfl -lemma lift_succ.comm : lift_succ ∘ (@succ n) = succ ∘ lift_succ := +lemma lift_succ.comm : @lift_succ _ ∘ (@succ n) = succ ∘ @lift_succ _ := eq_of_homotopy take i, - eq_of_veq (begin rewrite [↑lift_succ, -val_lift, *val_succ, -val_lift] end) + eq_of_veq (begin rewrite [↑lift_succ, *val_succ] end) definition elim0 {C : fin 0 → Type} : Π i : fin 0, C i | (mk v h) := absurd h !not_lt_zero @@ -388,9 +387,7 @@ begin { intro ilt', esimp[val_inj], apply concat, apply ap (λ x, eq.rec_on x _), esimp[eq_of_veq, rfl], reflexivity, have H : ilt = ilt', by apply is_prop.elim, cases H, - have H' : is_prop.elim (lt_add_of_lt_right ilt 1) (lt_add_of_lt_right ilt 1) = idp, - by apply is_prop.elim, - krewrite H' }, + apply ap (λx, eq.rec_on x _), apply ap02, apply is_prop_elim_self }, { intro a, exact absurd ilt a }, end @@ -522,7 +519,7 @@ begin ... ≃ fin 0 : fin_zero_equiv_empty }, { have H : (a + 1) * m = a * m + m, by rewrite [nat.right_distrib, one_mul], calc fin (a + 1) × fin m - ≃ (fin a + unit) × fin m : prod.prod_equiv_prod_right !fin_succ_equiv + ≃ (fin a + unit) × fin m : prod_equiv_prod_left !fin_succ_equiv ... ≃ (fin a × fin m) + (unit × fin m) : sum_prod_right_distrib ... ≃ (fin a × fin m) + (fin m × unit) : prod_comm_equiv ... ≃ fin (a * m) + (fin m × unit) : v_0 diff --git a/hott/types/list.hlean b/hott/types/list.hlean index f5aee1015..41c24cb53 100644 --- a/hott/types/list.hlean +++ b/hott/types/list.hlean @@ -10,7 +10,7 @@ Some lemmas are commented out, their proofs need to be repaired when needed import .pointed .nat .pi -open eq lift nat is_trunc pi pointed sum function prod option sigma algebra +open eq lift nat is_trunc pi pointed sum function prod option sigma algebra prod.ops unit sigma.ops inductive list (T : Type) : Type := | nil {} : list T @@ -19,11 +19,12 @@ inductive list (T : Type) : Type := definition pointed_list [instance] (A : Type) : pointed (list A) := pointed.mk list.nil +universe variable u + namespace list notation h :: t := cons h t notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l -universe variable u variable {T : Type.{u}} lemma cons_ne_nil (a : T) (l : list T) : a::l ≠ [] := @@ -744,7 +745,7 @@ attribute list.has_decidable_eq [instance] namespace list -variables {A B C : Type} +variables {A B C X : Type} /- map -/ definition map (f : A → B) : list A → list B | [] := [] @@ -924,4 +925,94 @@ theorem foldr_append (f : A → B → B) : Π (b : B) (l₁ l₂ : list A), fold | b [] l₂ := rfl | b (a::l₁) l₂ := by rewrite [append_cons, *foldr_cons, foldr_append] +definition foldl_homotopy {f g : A → B → A} (h : f ~2 g) (a : A) : foldl f a ~ foldl g a := +begin + intro bs, revert a, induction bs with b bs p: intro a, reflexivity, esimp [foldl], + exact p (f a b) ⬝ ap010 (foldl g) (h a b) bs +end + +definition cons_eq_cons {x x' : X} {l l' : list X} (p : x::l = x'::l') : x = x' × l = l' := +begin + refine lift.down (list.no_confusion p _), intro q r, split, exact q, exact r +end + +definition concat_neq_nil (x : X) (l : list X) : concat x l ≠ nil := +begin + intro p, cases l: cases p, +end + +definition concat_eq_singleton {x x' : X} {l : list X} (p : concat x l = [x']) : + x = x' × l = [] := +begin + cases l with x₂ l, + { cases cons_eq_cons p with q r, subst q, split: reflexivity }, + { exfalso, esimp [concat] at p, apply concat_neq_nil x l, revert p, generalize (concat x l), + intro l' p, cases cons_eq_cons p with q r, exact r } +end + +definition foldr_concat (f : A → B → B) (b : B) (a : A) (l : list A) : + foldr f b (concat a l) = foldr f (f a b) l := +begin + induction l with a' l p, reflexivity, rewrite [concat_cons, foldr_cons, p] +end + +definition iterated_prod (X : Type.{u}) (n : ℕ) : Type.{u} := +iterate (prod X) n (lift unit) + +definition is_trunc_iterated_prod {k : ℕ₋₂} {X : Type} {n : ℕ} (H : is_trunc k X) : + is_trunc k (iterated_prod X n) := +begin + induction n with n IH, + { apply is_trunc_of_is_contr, apply is_trunc_lift }, + { exact @is_trunc_prod _ _ _ H IH } +end + +definition list_of_iterated_prod {n : ℕ} (x : iterated_prod X n) : list X := +begin + induction n with n IH, + { exact [] }, + { exact x.1::IH x.2 } +end + +definition list_of_iterated_prod_succ {n : ℕ} (x : X) (xs : iterated_prod X n) : + @list_of_iterated_prod X (succ n) (x, xs) = x::list_of_iterated_prod xs := +by reflexivity + +definition iterated_prod_of_list (l : list X) : Σn, iterated_prod X n := +begin + induction l with x l IH, + { exact ⟨0, up ⋆⟩ }, + { exact ⟨succ IH.1, (x, IH.2)⟩ } +end + +definition iterated_prod_of_list_cons (x : X) (l : list X) : + iterated_prod_of_list (x::l) = + ⟨succ (iterated_prod_of_list l).1, (x, (iterated_prod_of_list l).2)⟩ := +by reflexivity + +protected definition sigma_char [constructor] (X : Type) : list X ≃ Σ(n : ℕ), iterated_prod X n := +begin + apply equiv.MK iterated_prod_of_list (λv, list_of_iterated_prod v.2), + { intro x, induction x with n x, esimp, induction n with n IH, + { induction x with x, induction x, reflexivity }, + { revert x, change Π(x : X × iterated_prod X n), _, intro xs, cases xs with x xs, + rewrite [list_of_iterated_prod_succ, iterated_prod_of_list_cons], + apply sigma_eq (ap succ (IH xs)..1), + apply pathover_ap, refine prod_pathover _ _ _ _ (IH xs)..2, + apply pathover_of_eq, reflexivity }}, + { intro l, induction l with x l IH, + { reflexivity }, + { exact ap011 cons idp IH }} +end + +local attribute [instance] is_trunc_iterated_prod +definition is_trunc_list [instance] {n : ℕ₋₂} {X : Type} (H : is_trunc (n.+2) X) : + is_trunc (n.+2) (list X) := +begin + assert H : is_trunc (n.+2) (Σ(k : ℕ), iterated_prod X k), + { apply is_trunc_sigma, refine is_trunc_succ_succ_of_is_set _ _ _, + intro, exact is_trunc_iterated_prod H }, + apply is_trunc_equiv_closed_rev _ (list.sigma_char X) _, +end + end list diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 96692f1dd..2211711b5 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -263,6 +263,15 @@ namespace pi { intro f, apply eq_of_homotopy, intro b, induction b: reflexivity}, end + definition pi_bool_left_natural {A B : bool → Type} (g : Πx, A x → B x) : + hsquare (pi_bool_left A) (pi_bool_left B) (pi_functor_right g) (prod_functor (g ff) (g tt)) := + begin intro h, esimp end + + definition pi_bool_left_inv_natural {A B : bool → Type} (g : Πx, A x → B x) : + hsquare (pi_bool_left A)⁻¹ᵉ (pi_bool_left B)⁻¹ᵉ + (prod_functor (g ff) (g tt)) (pi_functor_right g) := + (pi_bool_left_natural g)⁻¹ʰᵗʸʰ + /- Truncatedness: any dependent product of n-types is an n-type -/ theorem is_trunc_pi (B : A → Type) (n : trunc_index) diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index fc3923448..0b73686d7 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -341,6 +341,10 @@ namespace pointed /- equalities and equivalences relating pointed homotopies -/ + definition to_homotopy_pt_mk {A B : Type*} {f g : A →* B} (h : f ~ g) + (p : h pt ⬝ respect_pt g = respect_pt f) : to_homotopy_pt (phomotopy.mk h p) = p := + to_right_inv !eq_con_inv_equiv_con_eq p + definition phomotopy.rec' [recursor] (B : k ~* l → Type) (H : Π(h : k ~ l) (p : h pt ⬝ respect_pt l = respect_pt k), B (phomotopy.mk h p)) (h : k ~* l) : B h := @@ -353,8 +357,8 @@ namespace pointed definition phomotopy.eta_expand [constructor] (p : k ~* l) : k ~* l := phomotopy.mk p (to_homotopy_pt p) - definition is_trunc_ppi [instance] (n : ℕ₋₂) {A : Type*} (B : A → Type) (b₀ : B pt) [Πa, is_trunc n (B a)] : - is_trunc n (ppi B b₀) := + definition is_trunc_ppi [instance] (n : ℕ₋₂) {A : Type*} (B : A → Type) (b₀ : B pt) + [Πa, is_trunc n (B a)] : is_trunc n (ppi B b₀) := is_trunc_equiv_closed_rev _ !ppi.sigma_char _ definition is_trunc_pmap [instance] (n : ℕ₋₂) (A B : Type*) [is_trunc n B] : @@ -1108,6 +1112,9 @@ namespace pointed definition pointed_eta_pequiv [constructor] (A : Type*) : A ≃* pointed.MK A pt := pequiv.mk id !is_equiv_id idp + definition pbool_pequiv_add_point_unit [constructor] : pbool ≃* unit₊ := + pequiv_of_equiv (bool_equiv_option_unit) idp + /- every pointed map is homotopic to one of the form `pmap_of_map _ _`, up to some pointed equivalences -/ definition phomotopy_pmap_of_map {A B : Type*} (f : A →* B) : diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean index d65f45caf..120bb878c 100644 --- a/hott/types/pointed2.hlean +++ b/hott/types/pointed2.hlean @@ -1,7 +1,7 @@ /- Copyright (c) 2017 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn +Authors: Floris van Doorn, Yuri Sulyma More results about pointed types. @@ -15,7 +15,7 @@ Contains import eq2 .unit -open pointed eq unit is_trunc trunc nat is_equiv equiv sigma function bool sigma.ops +open pointed eq unit is_trunc trunc nat is_equiv equiv sigma function bool sigma.ops fiber namespace pointed variables {A B C : Type*} {P : A → Type} {p₀ : P pt} {k k' l m n : ppi P p₀} @@ -758,6 +758,24 @@ namespace pointed ap1_gen_const (g b) p := begin induction p, reflexivity end + definition ap1_phomotopy_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : (Ω⇒ p)⁻¹* = Ω⇒ (p⁻¹*) := + begin + induction p using phomotopy_rec_idp, + rewrite ap1_phomotopy_refl, + xrewrite [+refl_symm], + rewrite ap1_phomotopy_refl + end + + definition ap1_phomotopy_trans {A B : Type*} {f g h : A →* B} (q : g ~* h) (p : f ~* g) : + Ω⇒ (p ⬝* q) = Ω⇒ p ⬝* Ω⇒ q := + begin + induction p using phomotopy_rec_idp, + induction q using phomotopy_rec_idp, + rewrite trans_refl, + rewrite [+ap1_phomotopy_refl], + rewrite trans_refl + end + definition ap1_pcompose_pconst_left {A B C : Type*} (f : A →* B) : phsquare (ap1_pcompose (pconst B C) f) (ap1_pconst A C) diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index f3c8217e5..2e46a14e1 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -173,6 +173,8 @@ namespace prod definition prod_functor [unfold 7] (u : A × B) : A' × B' := (f u.1, g u.2) + infix ` ×→ `:63 := prod_functor + definition ap_prod_functor (p : u.1 = v.1) (q : u.2 = v.2) : ap (prod_functor f g) (prod_eq p q) = prod_eq (ap f p) (ap g q) := by induction u; induction v; esimp at *; induction p; induction q; reflexivity @@ -213,12 +215,12 @@ namespace prod definition prod_equiv_prod [constructor] (f : A ≃ A') (g : B ≃ B') : A × B ≃ A' × B' := equiv.mk (prod_functor f g) _ - -- rename - definition prod_equiv_prod_left [constructor] (g : B ≃ B') : A × B ≃ A × B' := + infix ` ×≃ `:63 := prod_equiv_prod + + definition prod_equiv_prod_right [constructor] (g : B ≃ B') : A × B ≃ A × B' := prod_equiv_prod equiv.rfl g - -- rename - definition prod_equiv_prod_right [constructor] (f : A ≃ A') : A × B ≃ A' × B := + definition prod_equiv_prod_left [constructor] (f : A ≃ A') : A × B ≃ A' × B := prod_equiv_prod f equiv.rfl /- Symmetry -/ @@ -340,5 +342,7 @@ namespace prod definition pprod_functor [constructor] {A B C D : Type*} (f : A →* C) (g : B →* D) : A ×* B →* C ×* D := pmap.mk (prod_functor f g) (prod_eq (respect_pt f) (respect_pt g)) + definition pprod_incl1 [constructor] (X Y : Type*) : X →* X ×* Y := pmap.mk (λx, (x, pt)) idp + definition pprod_incl2 [constructor] (X Y : Type*) : Y →* X ×* Y := pmap.mk (λy, (pt, y)) idp end prod diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean index da49a0043..8ea07b411 100644 --- a/hott/types/sum.hlean +++ b/hott/types/sum.hlean @@ -114,6 +114,8 @@ namespace sum | sum_functor (inl a) := inl (f a) | sum_functor (inr b) := inr (g b) + infix ` +→ `:62 := sum_functor + /- Equivalences -/ definition is_equiv_sum_functor [constructor] [instance] [Hf : is_equiv f] [Hg : is_equiv g] @@ -136,6 +138,8 @@ namespace sum definition sum_equiv_sum [constructor] (f : A ≃ A') (g : B ≃ B') : A + B ≃ A' + B' := equiv.mk _ (is_equiv_sum_functor f g) + infix ` +≃ `:62 := sum_equiv_sum + definition sum_equiv_sum_left [constructor] (g : B ≃ B') : A + B ≃ A + B' := sum_equiv_sum equiv.rfl g @@ -146,13 +150,11 @@ namespace sum | flip (inl a) := inr a | flip (inr b) := inl b + definition flip_flip (x : A ⊎ B) : flip (flip x) = x := + begin induction x: reflexivity end + definition sum_comm_equiv [constructor] (A B : Type) : A + B ≃ B + A := - begin - fapply equiv.MK, - exact flip, - exact flip, - all_goals (intro z; induction z; all_goals reflexivity) - end + equiv.MK flip flip flip_flip flip_flip definition sum_assoc_equiv [constructor] (A B C : Type) : A + (B + C) ≃ (A + B) + C := begin @@ -211,7 +213,7 @@ namespace sum variables (H : unit + A ≃ unit + B) include H - open unit decidable sigma.ops + open unit sigma.ops definition unit_sum_equiv_cancel_map : A → B := begin @@ -306,8 +308,7 @@ namespace sum /- truncatedness -/ - variables (A B) - theorem is_trunc_sum (n : trunc_index) [HA : is_trunc (n.+2) A] [HB : is_trunc (n.+2) B] + theorem is_trunc_sum (n : ℕ₋₂) (A B : Type) [HA : is_trunc (n.+2) A] [HB : is_trunc (n.+2) B] : is_trunc (n.+2) (A + B) := begin apply is_trunc_succ_intro, intro z z', @@ -316,7 +317,7 @@ namespace sum all_goals exact _, end - theorem is_trunc_sum_excluded (n : trunc_index) [HA : is_trunc n A] [HB : is_trunc n B] + theorem is_trunc_sum_excluded (n : ℕ₋₂) (A B : Type) [HA : is_trunc n A] [HB : is_trunc n B] (H : A → B → empty) : is_trunc n (A + B) := begin induction n with n IH, @@ -328,8 +329,8 @@ namespace sum { apply is_trunc_sum}} end - variable {B} - definition is_contr_sum_left [HA : is_contr A] (H : ¬B) : is_contr (A + B) := + definition is_contr_sum_left (A : Type) {B : Type} [HA : is_contr A] (H : ¬B) : + is_contr (A + B) := is_contr.mk (inl !center) (λx, sum.rec_on x (λa, ap inl !center_eq) (λb, empty.elim (H b))) @@ -353,6 +354,35 @@ namespace sum begin intro v, induction v with b x, induction b, all_goals reflexivity end begin intro z, induction z with a b, all_goals reflexivity end + variables {A₀₀ A₂₀ A₀₂ A₂₂ B₀₀ B₂₀ B₀₂ B₂₂ C C' : Type} + {f₁₀ : A₀₀ → A₂₀} {f₁₂ : A₀₂ → A₂₂} {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} + {g₁₀ : B₀₀ → B₂₀} {g₁₂ : B₀₂ → B₂₂} {g₀₁ : B₀₀ → B₀₂} {g₂₁ : B₂₀ → B₂₂} + {h₀₁ : B₀₀ → A₀₂} {h₂₁ : B₂₀ → A₂₂} + open function + + definition sum_rec_hsquare [unfold 16] (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁) + (k : hsquare g₁₀ f₁₂ h₀₁ h₂₁) : hsquare (f₁₀ +→ g₁₀) f₁₂ (sum.rec f₀₁ h₀₁) (sum.rec f₂₁ h₂₁) := + begin intro x, induction x with a b, exact h a, exact k b end + + definition sum_functor_hsquare [unfold 19] (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁) + (k : hsquare g₁₀ g₁₂ g₀₁ g₂₁) : hsquare (f₁₀ +→ g₁₀) (f₁₂ +→ g₁₂) (f₀₁ +→ g₀₁) (f₂₁ +→ g₂₁) := + sum_rec_hsquare (λa, ap inl (h a)) (λb, ap inr (k b)) + + definition sum_functor_compose (g : B → C) (f : A → B) (g' : B' → C') (f' : A' → B') : + (g ∘ f) +→ (g' ∘ f') ~ g +→ g' ∘ f +→ f' := + begin intro x, induction x with a a': reflexivity end + + definition sum_rec_sum_functor (g : B → C) (g' : B' → C) (f : A → B) (f' : A' → B') : + sum.rec g g' ∘ sum_functor f f' ~ sum.rec (g ∘ f) (g' ∘ f') := + begin intro x, induction x with a a': reflexivity end + + definition sum_rec_same_compose (g : B → C) (f : A → B) : + sum.rec (g ∘ f) (g ∘ f) ~ g ∘ sum.rec f f := + begin intro x, induction x with a a': reflexivity end + + definition sum_rec_same (f : A → B) : sum.rec f f ~ f ∘ sum.rec id id := + by exact sum_rec_same_compose f id + /- pointed sums. We arbitrarily choose (inl pt) as basepoint for the sum -/ open pointed @@ -367,13 +397,15 @@ open sum pi namespace decidable + /- some properties about the inductive type `decidable` + decidable A is equivalent to A + ¬A -/ definition decidable_equiv [constructor] (A : Type) : decidable A ≃ A + ¬A := begin fapply equiv.MK:intro a;induction a:try (constructor;assumption;now), all_goals reflexivity end - definition is_trunc_decidable [constructor] (A : Type) (n : trunc_index) [H : is_trunc n A] : + definition is_trunc_decidable [constructor] (A : Type) (n : ℕ₋₂) [H : is_trunc n A] : is_trunc n (decidable A) := begin apply is_trunc_equiv_closed_rev, @@ -383,11 +415,60 @@ namespace decidable { apply is_trunc_sum_excluded, exact λa na, na a} end + definition double_neg_elim {A : Type} (H : decidable A) (p : ¬ ¬ A) : A := + begin induction H, assumption, contradiction end + + definition dite_true {C : Type} [H : decidable C] {A : Type} + {t : C → A} {e : ¬ C → A} (c : C) (H' : is_prop C) : dite C t e = t c := + begin + induction H with H H, + exact ap t !is_prop.elim, + contradiction + end + + definition dite_false {C : Type} [H : decidable C] {A : Type} + {t : C → A} {e : ¬ C → A} (c : ¬ C) : dite C t e = e c := + begin + induction H with H H, + contradiction, + exact ap e !is_prop.elim, + end + + definition decidable_eq_of_is_prop (A : Type) [is_prop A] : decidable_eq A := + λa a', decidable.inl !is_prop.elim + + definition decidable_eq_sigma [instance] {A : Type} (B : A → Type) [HA : decidable_eq A] + [HB : Πa, decidable_eq (B a)] : decidable_eq (Σa, B a) := + begin + intro v v', induction v with a b, induction v' with a' b', + cases HA a a' with p np, + { induction p, cases HB a b b' with q nq, + induction q, exact decidable.inl idp, + apply decidable.inr, intro p, apply nq, apply @eq_of_pathover_idp A B, + exact change_path !is_prop.elim p..2 }, + { apply decidable.inr, intro p, apply np, exact p..1 } + end + + open sum + definition decidable_eq_sum [instance] (A B : Type) [HA : decidable_eq A] [HB : decidable_eq B] : + decidable_eq (A ⊎ B) := + begin + intro v v', induction v with a b: induction v' with a' b', + { cases HA a a' with p np, + { exact decidable.inl (ap sum.inl p) }, + { apply decidable.inr, intro p, apply np, exact down (sum.encode p) }}, + { apply decidable.inr, intro p, cases p }, + { apply decidable.inr, intro p, cases p }, + { cases HB b b' with p np, + { exact decidable.inl (ap sum.inr p) }, + { apply decidable.inr, intro p, apply np, exact down (sum.encode p) }}, + end + end decidable attribute sum.is_trunc_sum [instance] [priority 1480] -definition tsum [constructor] {n : trunc_index} (A B : (n.+2)-Type) : (n.+2)-Type := +definition tsum [constructor] {n : ℕ₋₂} (A B : (n.+2)-Type) : (n.+2)-Type := trunctype.mk (A + B) _ infixr `+t`:25 := tsum diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 9f1745219..906b5493e 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -1087,6 +1087,7 @@ end eq /- some consequences for properties about functions (surjectivity etc.) -/ namespace function + open fiber variables {A B : Type} definition is_surjective_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_surjective f := λb, begin esimp, apply center, apply is_trunc_trunc_of_is_trunc end