From 7e52c49dce75c77de9d809459257d437be432722 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 31 Aug 2015 12:23:34 -0400 Subject: [PATCH] feat(hott): many changes is the HoTT library Prove that 'is_left_adjoint F' is a mere proposition, although this proof is commented out because it takes ~10 seconds --- hott/algebra/category/adjoint.hlean | 176 ++++++++++++------ .../category/constructions/functor.hlean | 86 ++++++++- .../category/constructions/opposite.hlean | 4 +- hott/algebra/category/functor.hlean | 18 +- hott/algebra/category/iso.hlean | 10 +- hott/algebra/category/nat_trans.hlean | 75 ++++++-- hott/book.md | 4 +- hott/cubical/square.hlean | 93 ++++++++- hott/cubical/squareover.hlean | 18 +- hott/function.hlean | 33 ++++ hott/init/equiv.hlean | 85 +++++++-- hott/init/logic.hlean | 2 +- hott/init/path.hlean | 5 +- hott/init/pathover.hlean | 26 ++- hott/init/trunc.hlean | 10 + hott/types/arrow.hlean | 3 + hott/types/equiv.hlean | 19 +- hott/types/nat/basic.hlean | 10 +- hott/types/pi.hlean | 19 +- hott/types/sum.hlean | 65 ++++++- hott/types/trunc.hlean | 8 - src/emacs/lean-syntax.el | 2 +- 22 files changed, 618 insertions(+), 153 deletions(-) diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean index 0862139b65..c421237636 100644 --- a/hott/algebra/category/adjoint.hlean +++ b/hott/algebra/category/adjoint.hlean @@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ -import algebra.category.constructions .constructions function arity +import algebra.category.constructions function arity -open category functor nat_trans eq is_trunc iso equiv prod trunc function +open category functor nat_trans eq is_trunc iso equiv prod trunc function pi is_equiv namespace category - variables {C D : Precategory} {F : C ⇒ D} + variables {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C} -- do we want to have a structure "is_adjoint" and define -- structure is_left_adjoint (F : C ⇒ D) := @@ -18,8 +18,8 @@ namespace category structure is_left_adjoint [class] (F : C ⇒ D) := (G : D ⇒ C) - (η : functor.id ⟹ G ∘f F) - (ε : F ∘f G ⟹ functor.id) + (η : 1 ⟹ G ∘f F) + (ε : F ∘f G ⟹ 1) (H : Π(c : C), (ε (F c)) ∘ (F (η c)) = ID (F c)) (K : Π(d : D), (G (ε d)) ∘ (η (G d)) = ID (G d)) @@ -39,31 +39,23 @@ namespace category (is_iso_unit : is_iso η) (is_iso_counit : is_iso ε) + abbreviation inverse := @is_equivalence.G + postfix `⁻¹` := inverse + --a second notation for the inverse, which is not overloaded + postfix [parsing-only] `⁻¹F`:std.prec.max_plus := inverse + structure equivalence (C D : Precategory) := (to_functor : C ⇒ D) (struct : is_equivalence to_functor) --TODO: review and change - --TODO: make some or all of these structures? - definition faithful (F : C ⇒ D) := - Π⦃c c' : C⦄ (f f' : c ⟶ c'), F f = F f' → f = f' - - definition full (F : C ⇒ D) := Π⦃c c' : C⦄ (g : F c ⟶ F c'), ∃(f : c ⟶ c'), F f = g - - definition fully_faithful [reducible] (F : C ⇒ D) := - Π⦃c c' : C⦄, is_equiv (@(to_fun_hom F) c c') - - definition split_essentially_surjective (F : C ⇒ D) := - Π⦃d : D⦄, Σ(c : C), F c ≅ d - - definition essentially_surjective (F : C ⇒ D) := - Π⦃d : D⦄, ∃(c : C), F c ≅ d - - definition is_weak_equivalence (F : C ⇒ D) := - fully_faithful F × essentially_surjective F - - definition is_isomorphism (F : C ⇒ D) := - fully_faithful F × is_equiv (to_fun_ob F) + definition faithful [class] (F : C ⇒ D) := Π⦃c c' : C⦄ ⦃f f' : c ⟶ c'⦄, F f = F f' → f = f' + definition full [class] (F : C ⇒ D) := Π⦃c c' : C⦄, is_surjective (@(to_fun_hom F) c c') + definition fully_faithful [class] (F : C ⇒ D) := Π(c c' : C), is_equiv (@(to_fun_hom F) c c') + definition split_essentially_surjective [class] (F : C ⇒ D) := Π(d : D), Σ(c : C), F c ≅ d + definition essentially_surjective [class] (F : C ⇒ D) := Π(d : D), ∃(c : C), F c ≅ d + definition is_weak_equivalence [class] (F : C ⇒ D) := fully_faithful F × essentially_surjective F + definition is_isomorphism [class] (F : C ⇒ D) := fully_faithful F × is_equiv (to_fun_ob F) structure isomorphism (C D : Precategory) := (to_functor : C ⇒ D) @@ -73,43 +65,115 @@ namespace category infix `⋍`:25 := equivalence -- \backsimeq or \equiv infix `≌`:25 := isomorphism -- \backcong or \iso -/- - definition is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D) - : is_hprop (is_left_adjoint F) := - begin - apply is_hprop.mk, - intro G G', cases G with G η ε H K, cases G' with G' η' ε' H' K', - fapply (apd011111 is_left_adjoint.mk), - { fapply functor_eq, - { intro d, apply eq_of_iso, fapply iso.MK, - { exact (G' (ε d) ∘ η' (G d))}, - { exact (G (ε' d) ∘ η (G' d))}, - { apply sorry /-rewrite [assoc, -{((G (ε' d)) ∘ (η (G' d))) ∘ (G' (ε d))}(assoc)],-/ --- apply concat, apply (ap (λc, c ∘ η' _)), rewrite -assoc, apply idp -}, --- rewrite [-nat_trans.assoc] apply sorry ----assoc (G (ε' d)) (η (G' d)) (G' (ε d)) - { apply sorry}}, - { apply sorry}, -}, - { apply sorry}, - { apply sorry}, - { apply is_hprop.elim}, - { apply is_hprop.elim}, + definition is_equiv_of_fully_faithful [instance] (F : C ⇒ D) [H : fully_faithful F] (c c' : C) + : is_equiv (@(to_fun_hom F) c c') := + !H + + definition is_iso_unit [instance] (F : C ⇒ D) (H : is_equivalence F) : is_iso (unit F) := + !is_equivalence.is_iso_unit + + definition is_iso_counit [instance] (F : C ⇒ D) (H : is_equivalence F) : is_iso (counit F) := + !is_equivalence.is_iso_counit + + -- theorem is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D) + -- : is_hprop (is_left_adjoint F) := + -- begin + -- apply is_hprop.mk, + -- intro G G', cases G with G η ε H K, cases G' with G' η' ε' H' K', + -- assert lem : Π(p : G = G'), p ▸ η = η' → p ▸ ε = ε' + -- → is_left_adjoint.mk G η ε H K = is_left_adjoint.mk G' η' ε' H' K', + -- { intros p q r, induction p, induction q, induction r, esimp, + -- apply apd011 (is_left_adjoint.mk G η ε) !is_hprop.elim !is_hprop.elim}, + -- fapply lem, + -- { fapply functor.eq_of_pointwise_iso, + -- { fapply change_natural_map, + -- { exact (G' ∘fn1 ε) ∘n !assoc_natural_rev ∘n (η' ∘1nf G)}, + -- { intro d, exact (G' (ε d) ∘ η' (G d))}, + -- { intro d, exact ap (λx, _ ∘ x) !id_left}}, + -- { intro d, fconstructor, + -- { exact (G (ε' d) ∘ η (G' d))}, + -- { krewrite [▸*,assoc,-assoc (G (ε' d))], + -- krewrite [nf_fn_eq_fn_nf_pt' G' ε η d], + -- krewrite [assoc,-assoc], + -- rewrite [↑functor.compose, -respect_comp G], + -- krewrite [nf_fn_eq_fn_nf_pt ε ε' d,nf_fn_eq_fn_nf_pt η' η (G d),▸*], + -- rewrite [respect_comp G], + -- krewrite [assoc,-assoc (G (ε d))], + -- rewrite [↑functor.compose, -respect_comp G], + -- krewrite [H' (G d)], + -- rewrite [respect_id,id_right], + -- apply K}, + -- { krewrite [▸*,assoc,-assoc (G' (ε d))], + -- krewrite [nf_fn_eq_fn_nf_pt' G ε' η' d], + -- krewrite [assoc,-assoc], + -- rewrite [↑functor.compose, -respect_comp G'], + -- krewrite [nf_fn_eq_fn_nf_pt ε' ε d,nf_fn_eq_fn_nf_pt η η' (G' d),▸*], + -- rewrite [respect_comp G'], + -- krewrite [assoc,-assoc (G' (ε' d))], + -- rewrite [↑functor.compose, -respect_comp G'], + -- krewrite [H (G' d)], + -- rewrite [respect_id,id_right], + -- apply K'}}}, + -- { clear lem, refine transport_hom_of_eq_right _ η ⬝ _, + -- krewrite hom_of_eq_compose_right, + -- rewrite functor.hom_of_eq_eq_of_pointwise_iso, + -- apply nat_trans_eq, intro c, esimp, + -- refine !assoc⁻¹ ⬝ ap (λx, _ ∘ x) (nf_fn_eq_fn_nf_pt η η' c) ⬝ !assoc ⬝ _, + -- rewrite [▸*,-respect_comp G',H c,respect_id G',id_left]}, + -- { clear lem, refine transport_hom_of_eq_left _ ε ⬝ _, + -- krewrite inv_of_eq_compose_left, + -- rewrite functor.inv_of_eq_eq_of_pointwise_iso, + -- apply nat_trans_eq, intro d, esimp, + -- rewrite [respect_comp,assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]}, + -- end + + section + variables (F G) + variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) + include η ε + --definition inverse_of_unit_counit + + definition is_equivalence.mk : is_equivalence F := + begin + exact sorry + end + end - definition is_equivalence.mk (F : C ⇒ D) (G : D ⇒ C) (η : G ∘f F ≅ functor.id) - (ε : F ∘f G ≅ functor.id) : is_equivalence F := - sorry - definition full_of_fully_faithful (H : fully_faithful F) : full F := - sorry -- λc c' g, exists.intro ((@(to_fun_hom F) c c')⁻¹ g) _ + λc c', is_surjective.mk (λg, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv)) definition faithful_of_fully_faithful (H : fully_faithful F) : faithful F := λc c' f f' p, is_injective_of_is_embedding p definition fully_faithful_of_full_of_faithful (H : faithful F) (K : full F) : fully_faithful F := - sorry + begin + intro c c', + apply is_equiv_of_is_surjective_of_is_embedding, + { apply is_embedding_of_is_injective, + intros f f' p, exact H p}, + { apply K} + end + + definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F] + : fully_faithful F := + begin + intro c c', + fapply adjointify, + { intro g, exact natural_map (@(iso.inverse (unit F)) !is_iso_unit) c' ∘ F⁻¹ g ∘ unit F c}, + { intro g, rewrite [+respect_comp], exact sorry}, + { exact sorry}, + end + + definition split_essentially_surjective_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F] + : split_essentially_surjective F := + begin + intro d, fconstructor, + { exact F⁻¹ d}, + { exact componentwise_iso (@(iso.mk (counit F)) !is_iso_counit) d} + end + +/- definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) := sorry @@ -132,12 +196,12 @@ namespace category sorry definition is_isomorphism_equiv1 (F : C ⇒ D) : is_equivalence F - ≃ Σ(G : D ⇒ C) (η : functor.id = G ∘f F) (ε : F ∘f G = functor.id), + ≃ Σ(G : D ⇒ C) (η : 1 = G ∘f F) (ε : F ∘f G = 1), sorry ▸ ap (λ(H : C ⇒ C), F ∘f H) η = ap (λ(H : D ⇒ D), H ∘f F) ε⁻¹ := sorry definition is_isomorphism_equiv2 (F : C ⇒ D) : is_equivalence F - ≃ ∃(G : D ⇒ C), functor.id = G ∘f F × F ∘f G = functor.id := + ≃ ∃(G : D ⇒ C), 1 = G ∘f F × F ∘f G = 1 := sorry definition is_equivalence_of_isomorphism (H : is_isomorphism F) : is_equivalence F := diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 510d9cbd65..c6dea29313 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -31,7 +31,7 @@ namespace category variables {C D : Precategory} {F G : C ⇒ D} (η : F ⟹ G) [iso : Π(a : C), is_iso (η a)] include iso - definition nat_trans_inverse : G ⟹ F := + definition nat_trans_inverse [constructor] : G ⟹ F := nat_trans.mk (λc, (η c)⁻¹) (λc d f, @@ -58,16 +58,20 @@ namespace category apply is_hset.elim end - definition is_iso_nat_trans : is_iso η := + definition is_iso_nat_trans [constructor] [instance] : is_iso η := is_iso.mk (nat_trans_left_inverse η) (nat_trans_right_inverse η) + variable (iso) + definition functor_iso [constructor] : F ≅ G := + @(iso.mk η) !is_iso_nat_trans + end section /- and conversely, if a natural transformation is an iso, it is componentwise an iso -/ - variables {C D : Precategory} {F G : D ^c C} (η : hom F G) [isoη : is_iso η] (c : C) + variables {A B C D : Precategory} {F G : D ^c C} (η : hom F G) [isoη : is_iso η] (c : C) include isoη - definition componentwise_is_iso : is_iso (η c) := + definition componentwise_is_iso [instance] : is_iso (η c) := @is_iso.mk _ _ _ _ _ (natural_map η⁻¹ c) (ap010 natural_map ( left_inverse η) c) (ap010 natural_map (right_inverse η) c) @@ -107,6 +111,61 @@ namespace category : natural_map (inv_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c)⁻¹ := eq.rec_on p idp + definition hom_of_eq_compose_right {H : C ^c B} (p : F = G) + : hom_of_eq (ap (λx, x ∘f H) p) = hom_of_eq p ∘nf H := + eq.rec_on p idp + + definition inv_of_eq_compose_right {H : C ^c B} (p : F = G) + : inv_of_eq (ap (λx, x ∘f H) p) = inv_of_eq p ∘nf H := + eq.rec_on p idp + + definition hom_of_eq_compose_left {H : B ^c D} (p : F = G) + : hom_of_eq (ap (λx, H ∘f x) p) = H ∘fn hom_of_eq p := + by induction p; exact !fn_id⁻¹ + + definition inv_of_eq_compose_left {H : B ^c D} (p : F = G) + : inv_of_eq (ap (λx, H ∘f x) p) = H ∘fn inv_of_eq p := + by induction p; exact !fn_id⁻¹ + + definition assoc_natural [constructor] (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) + : H ∘f (G ∘f F) ⟹ (H ∘f G) ∘f F := + change_natural_map (hom_of_eq !functor.assoc) + (λa, id) + (λa, !natural_map_hom_of_eq ⬝ ap hom_of_eq !ap010_assoc) + + definition assoc_natural_rev [constructor] (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) + : (H ∘f G) ∘f F ⟹ H ∘f (G ∘f F) := + change_natural_map (inv_of_eq !functor.assoc) + (λa, id) + (λa, !natural_map_inv_of_eq ⬝ ap (λx, hom_of_eq x⁻¹) !ap010_assoc) + + definition id_left_natural [constructor] (F : C ⇒ D) : functor.id ∘f F ⟹ F := + change_natural_map + (hom_of_eq !functor.id_left) + (λc, id) + (λc, by induction F; exact !natural_map_hom_of_eq ⬝ ap hom_of_eq !ap010_functor_mk_eq_constant) + + + definition id_left_natural_rev [constructor] (F : C ⇒ D) : F ⟹ functor.id ∘f F := + change_natural_map + (inv_of_eq !functor.id_left) + (λc, id) + (λc, by induction F; exact !natural_map_inv_of_eq ⬝ + ap (λx, hom_of_eq x⁻¹) !ap010_functor_mk_eq_constant) + + definition id_right_natural [constructor] (F : C ⇒ D) : F ∘f functor.id ⟹ F := + change_natural_map + (hom_of_eq !functor.id_right) + (λc, id) + (λc, by induction F; exact !natural_map_hom_of_eq ⬝ ap hom_of_eq !ap010_functor_mk_eq_constant) + + definition id_right_natural_rev [constructor] (F : C ⇒ D) : F ⟹ F ∘f functor.id := + change_natural_map + (inv_of_eq !functor.id_right) + (λc, id) + (λc, by induction F; exact !natural_map_inv_of_eq ⬝ + ap (λx, hom_of_eq x⁻¹) !ap010_functor_mk_eq_constant) + end namespace functor @@ -171,5 +230,24 @@ namespace category infixr `^c2`:35 := Category_functor end ops + namespace functor + variables {C : Precategory} {D : Category} {F G : D ^c C} + + definition eq_of_pointwise_iso (η : F ⟹ G) (iso : Π(a : C), is_iso (η a)) : F = G := + eq_of_iso (functor_iso η iso) + + definition iso_of_eq_eq_of_pointwise_iso (η : F ⟹ G) (iso : Π(c : C), is_iso (η c)) + : iso_of_eq (eq_of_pointwise_iso η iso) = functor_iso η iso := + !iso_of_eq_eq_of_iso + + definition hom_of_eq_eq_of_pointwise_iso (η : F ⟹ G) (iso : Π(c : C), is_iso (η c)) + : hom_of_eq (eq_of_pointwise_iso η iso) = η := + !hom_of_eq_eq_of_iso + + definition inv_of_eq_eq_of_pointwise_iso (η : F ⟹ G) (iso : Π(c : C), is_iso (η c)) + : inv_of_eq (eq_of_pointwise_iso η iso) = nat_trans_inverse η := + !inv_of_eq_eq_of_iso + + end functor end category diff --git a/hott/algebra/category/constructions/opposite.hlean b/hott/algebra/category/constructions/opposite.hlean index 93a0f47f1e..a83fbb3ac9 100644 --- a/hott/algebra/category/constructions/opposite.hlean +++ b/hott/algebra/category/constructions/opposite.hlean @@ -38,7 +38,7 @@ namespace category definition opposite_opposite : Opposite (Opposite C) = C := (ap (Precategory.mk C) (opposite_opposite' C)) ⬝ !Precategory.eta - postfix `ᵒᵖ`:(max+1) := Opposite + postfix `ᵒᵖ`:(max+2) := Opposite definition opposite_functor [reducible] {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ := begin @@ -47,6 +47,6 @@ namespace category intros, apply (@respect_comp C D) end - infixr `ᵒᵖᶠ`:(max+1) := opposite_functor + infixr `ᵒᵖᶠ`:(max+2) := opposite_functor end category diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean index d1c40587da..2d2e8bd9cd 100644 --- a/hott/algebra/category/functor.hlean +++ b/hott/algebra/category/functor.hlean @@ -26,7 +26,8 @@ namespace functor -- The following lemmas will later be used to prove that the type of -- precategories forms a precategory itself - protected definition compose [reducible] (G : functor D E) (F : functor C D) : functor C E := + protected definition compose [reducible] [constructor] (G : functor D E) (F : functor C D) + : functor C E := functor.mk (λ x, G (F x)) (λ a b f, G (F f)) @@ -39,10 +40,11 @@ namespace functor infixr `∘f`:60 := functor.compose - protected definition id [reducible] {C : Precategory} : functor C C := + protected definition id [reducible] [constructor] {C : Precategory} : functor C C := mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp) - protected definition ID [reducible] (C : Precategory) : functor C C := @functor.id C + protected definition ID [reducible] [constructor] (C : Precategory) : functor C C := @functor.id C + notation 1 := functor.id definition functor_mk_eq' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)} {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) @@ -53,7 +55,7 @@ namespace functor definition functor_eq' {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ = to_fun_ob F₂), (transport (λx, Πa b f, hom (x a) (x b)) p (to_fun_hom F₁) = to_fun_hom F₂) → F₁ = F₂ := - functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_mk_eq')) + by induction F₁; induction F₂; apply functor_mk_eq' definition functor_mk_eq {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)} {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ ~ F₂) @@ -68,7 +70,7 @@ namespace functor definition functor_eq {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ~ to_fun_ob F₂), (Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) → F₁ = F₂ := - functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_mk_eq)) + by induction F₁; induction F₂; apply functor_mk_eq definition functor_mk_eq_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)} {H₂ : Π(a b : C), hom a b → hom (F a) (F b)} (id₁ id₂ comp₁ comp₂) @@ -108,13 +110,13 @@ namespace functor H ∘f (G ∘f F) = (H ∘f G) ∘f F := !functor_mk_eq_constant (λa b f, idp) - protected definition id_left (F : C ⇒ D) : functor.id ∘f F = F := + protected definition id_left (F : C ⇒ D) : 1 ∘f F = F := functor.rec_on F (λF1 F2 F3 F4, !functor_mk_eq_constant (λa b f, idp)) - protected definition id_right (F : C ⇒ D) : F ∘f functor.id = F := + protected definition id_right (F : C ⇒ D) : F ∘f 1 = F := functor.rec_on F (λF1 F2 F3 F4, !functor_mk_eq_constant (λa b f, idp)) - protected definition comp_id_eq_id_comp (F : C ⇒ D) : F ∘f functor.id = functor.id ∘f F := + protected definition comp_id_eq_id_comp (F : C ⇒ D) : F ∘f 1 = 1 ∘f F := !functor.id_right ⬝ !functor.id_left⁻¹ -- "functor C D" is equivalent to a certain sigma type diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index 4536f24c46..88a24654db 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -206,7 +206,15 @@ namespace iso variables {X : Type} {x y : X} {F G : X → ob} definition transport_hom_of_eq (p : F = G) (f : hom (F x) (F y)) : p ▸ f = hom_of_eq (apd10 p y) ∘ f ∘ inv_of_eq (apd10 p x) := - eq.rec_on p !id_leftright⁻¹ + by induction p; exact !id_leftright⁻¹ + + definition transport_hom_of_eq_right (p : x = y) (f : hom c (F x)) + : p ▸ f = hom_of_eq (ap F p) ∘ f := + by induction p; exact !id_left⁻¹ + + definition transport_hom_of_eq_left (p : x = y) (f : hom (F x) c) + : p ▸ f = f ∘ inv_of_eq (ap F p) := + by induction p; exact !id_right⁻¹ definition transport_hom (p : F ~ G) (f : hom (F x) (F y)) : eq_of_homotopy p ▸ f = hom_of_eq (p y) ∘ f ∘ inv_of_eq (p x) := diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean index 794d8341d4..8a3a8d0b12 100644 --- a/hott/algebra/category/nat_trans.hlean +++ b/hott/algebra/category/nat_trans.hlean @@ -13,11 +13,11 @@ structure nat_trans {C D : Precategory} (F G : C ⇒ D) := namespace nat_trans infixl `⟹`:25 := nat_trans -- \==> - variables {B C D E : Precategory} {F G H I : C ⇒ D} {F' G' : D ⇒ E} + variables {B C D E : Precategory} {F G H I : C ⇒ D} {F' G' : D ⇒ E} {F'' G'' : E ⇒ B} {J : C ⇒ C} attribute natural_map [coercion] - protected definition compose [reducible] (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := + protected definition compose [constructor] (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := nat_trans.mk (λ a, η a ∘ θ a) (λ a b f, @@ -31,12 +31,14 @@ namespace nat_trans infixr `∘n`:60 := nat_trans.compose - protected definition id [reducible] {C D : Precategory} {F : functor C D} : nat_trans F F := + protected definition id [reducible] {F : C ⇒ D} : nat_trans F F := mk (λa, id) (λa b f, !id_right ⬝ !id_left⁻¹) - protected definition ID [reducible] {C D : Precategory} (F : functor C D) : nat_trans F F := + protected definition ID [reducible] (F : C ⇒ D) : nat_trans F F := (@nat_trans.id C D F) + notation 1 := nat_trans.id + definition nat_trans_mk_eq {η₁ η₂ : Π (a : C), hom (F a) (G a)} (nat₁ : Π (a b : C) (f : hom a b), G f ∘ η₁ a = η₁ b ∘ F f) (nat₂ : Π (a b : C) (f : hom a b), G f ∘ η₂ a = η₂ b ∘ F f) @@ -45,16 +47,16 @@ namespace nat_trans apd011 nat_trans.mk (eq_of_homotopy p) !is_hprop.elim definition nat_trans_eq {η₁ η₂ : F ⟹ G} : natural_map η₁ ~ natural_map η₂ → η₁ = η₂ := - nat_trans.rec_on η₁ (λf₁ nat₁, nat_trans.rec_on η₂ (λf₂ nat₂ p, !nat_trans_mk_eq p)) + by induction η₁; induction η₂; apply nat_trans_mk_eq protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) : η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ := nat_trans_eq (λa, !assoc) - protected definition id_left (η : F ⟹ G) : nat_trans.id ∘n η = η := + protected definition id_left (η : F ⟹ G) : 1 ∘n η = η := nat_trans_eq (λa, !id_left) - protected definition id_right (η : F ⟹ G) : η ∘n nat_trans.id = η := + protected definition id_right (η : F ⟹ G) : η ∘n 1 = η := nat_trans_eq (λa, !id_right) protected definition sigma_char (F G : C ⇒ D) : @@ -78,12 +80,18 @@ namespace nat_trans definition is_hset_nat_trans [instance] : is_hset (F ⟹ G) := by apply is_trunc_is_equiv_closed; apply (equiv.to_is_equiv !nat_trans.sigma_char) - definition nat_trans_functor_compose [reducible] (η : G ⟹ H) (F : E ⇒ C) : G ∘f F ⟹ H ∘f F := + definition change_natural_map [constructor] (η : F ⟹ G) (f : Π (a : C), F a ⟶ G a) + (p : Πa, η a = f a) : F ⟹ G := + nat_trans.mk f (λa b g, p a ▸ p b ▸ naturality η g) + + definition nat_trans_functor_compose [constructor] (η : G ⟹ H) (F : E ⇒ C) + : G ∘f F ⟹ H ∘f F := nat_trans.mk (λ a, η (F a)) (λ a b f, naturality η (F f)) - definition functor_nat_trans_compose [reducible] (F : D ⇒ E) (η : G ⟹ H) : F ∘f G ⟹ F ∘f H := + definition functor_nat_trans_compose [constructor] (F : D ⇒ E) (η : G ⟹ H) + : F ∘f G ⟹ F ∘f H := nat_trans.mk (λ a, F (η a)) (λ a b f, calc @@ -91,13 +99,53 @@ namespace nat_trans ... = F (η b ∘ G f) : by rewrite (naturality η f) ... = F (η b) ∘ F (G f) : by rewrite respect_comp) + definition nat_trans_id_functor_compose [constructor] (η : J ⟹ 1) (F : E ⇒ C) + : J ∘f F ⟹ F := + nat_trans.mk + (λ a, η (F a)) + (λ a b f, naturality η (F f)) + + definition id_nat_trans_functor_compose [constructor] (η : 1 ⟹ J) (F : E ⇒ C) + : F ⟹ J ∘f F := + nat_trans.mk + (λ a, η (F a)) + (λ a b f, naturality η (F f)) + + definition functor_nat_trans_id_compose [constructor] (F : C ⇒ D) (η : J ⟹ 1) + : F ∘f J ⟹ F := + nat_trans.mk + (λ a, F (η a)) + (λ a b f, calc + F f ∘ F (η a) = F (f ∘ η a) : by rewrite respect_comp + ... = F (η b ∘ J f) : by rewrite (naturality η f) + ... = F (η b) ∘ F (J f) : by rewrite respect_comp) + + definition functor_id_nat_trans_compose [constructor] (F : C ⇒ D) (η : 1 ⟹ J) + : F ⟹ F ∘f J := + nat_trans.mk + (λ a, F (η a)) + (λ a b f, calc + F (J f) ∘ F (η a) = F (J f ∘ η a) : by rewrite respect_comp + ... = F (η b ∘ f) : by rewrite (naturality η f) + ... = F (η b) ∘ F f : by rewrite respect_comp) + infixr `∘nf`:62 := nat_trans_functor_compose infixr `∘fn`:62 := functor_nat_trans_compose + infixr `∘n1f`:62 := nat_trans_id_functor_compose + infixr `∘1nf`:62 := id_nat_trans_functor_compose + infixr `∘f1n`:62 := functor_id_nat_trans_compose + infixr `∘fn1`:62 := functor_nat_trans_id_compose definition nf_fn_eq_fn_nf_pt (η : F ⟹ G) (θ : F' ⟹ G') (c : C) : (θ (G c)) ∘ (F' (η c)) = (G' (η c)) ∘ (θ (F c)) := (naturality θ (η c))⁻¹ + variable (F') + definition nf_fn_eq_fn_nf_pt' (η : F ⟹ G) (θ : F'' ⟹ G'') (c : C) + : (θ (F' (G c))) ∘ (F'' (F' (η c))) = (G'' (F' (η c))) ∘ (θ (F' (F c))) := + (naturality θ (F' (η c)))⁻¹ + variable {F'} + definition nf_fn_eq_fn_nf (η : F ⟹ G) (θ : F' ⟹ G') : (θ ∘nf G) ∘n (F' ∘fn η) = (G' ∘fn η) ∘n (θ ∘nf F) := nat_trans_eq (λ c, nf_fn_eq_fn_nf_pt η θ c) @@ -110,19 +158,20 @@ namespace nat_trans : (η ∘n θ) ∘nf F' = (η ∘nf F') ∘n (θ ∘nf F') := nat_trans_eq (λc, idp) - definition fn_id (F' : D ⇒ E) : F' ∘fn nat_trans.ID F = nat_trans.id := + definition fn_id (F' : D ⇒ E) : F' ∘fn nat_trans.ID F = 1 := nat_trans_eq (λc, by apply respect_id) - definition id_nf (F' : B ⇒ C) : nat_trans.ID F ∘nf F' = nat_trans.id := + definition id_nf (F' : B ⇒ C) : nat_trans.ID F ∘nf F' = 1 := nat_trans_eq (λc, idp) - definition id_fn (η : G ⟹ H) (c : C) : (functor.id ∘fn η) c = η c := + definition id_fn (η : G ⟹ H) (c : C) : (1 ∘fn η) c = η c := idp - definition nf_id (η : G ⟹ H) (c : C) : (η ∘nf functor.id) c = η c := + definition nf_id (η : G ⟹ H) (c : C) : (η ∘nf 1) c = η c := idp definition nat_trans_of_eq [reducible] (p : F = G) : F ⟹ G := nat_trans.mk (λc, hom_of_eq (ap010 to_fun_ob p c)) (λa b f, eq.rec_on p (!id_right ⬝ !id_left⁻¹)) + end nat_trans diff --git a/hott/book.md b/hott/book.md index 0d5133928c..295cd6947a 100644 --- a/hott/book.md +++ b/hott/book.md @@ -23,7 +23,7 @@ The rows indicate the chapters, the columns the sections. | Ch 6 | . | + | + | + | + | ½ | ½ | ¼ | ¼ | ¼ | ¾ | - | . | | | | Ch 7 | + | + | + | - | - | - | - | | | | | | | | | | Ch 8 | ¾ | - | - | - | - | - | - | - | - | - | | | | | | -| Ch 9 | ¾ | + | ¼ | ¼ | ½ | ½ | - | - | - | | | | | | | +| Ch 9 | ¾ | + | + | ¼ | ½ | ½ | - | - | - | | | | | | | | Ch 10 | - | - | - | - | - | | | | | | | | | | | | Ch 11 | - | - | - | - | - | - | | | | | | | | | | @@ -155,7 +155,7 @@ Every file is in the folder [algebra.category](algebra/category/category.md) - 9.1 (Categories and precategories): [precategory](algebra/category/precategory.hlean), [iso](algebra/category/iso.hlean), [category](algebra/category/category.hlean), [groupoid](algebra/category/groupoid.hlean) (mostly) - 9.2 (Functors and transformations): [functor](algebra/category/functor.hlean), [nat_trans](algebra/category/nat_trans.hlean), [constructions.functor](algebra/category/constructions/functor.hlean) -- 9.3 (Adjunctions): [adjoint](algebra/category/adjoint.hlean) (only definition) +- 9.3 (Adjunctions): [adjoint](algebra/category/adjoint.hlean) - 9.4 (Equivalences): [adjoint](algebra/category/adjoint.hlean) (only definitions) - 9.5 (The Yoneda lemma): [constructions.opposite](algebra/category/constructions/opposite.hlean), [constructions.product](algebra/category/constructions/product.hlean), [yoneda](algebra/category/yoneda.hlean) (up to definition of Yoneda embedding) - 9.6 (Strict categories): [strict](algebra/category/strict.hlean) (only definition) diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index f1ecce4dee..0b4d24e11c 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -101,14 +101,103 @@ namespace eq square (p a) (p a') (ap f q) (ap g q) := eq.rec_on q vrfl + /- canceling, whiskering and moving thinks along the sides of the square -/ definition whisker_tl (p : a = a₀₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square (p ⬝ p₁₀) p₁₂ (p ⬝ p₀₁) p₂₁ := - by induction s₁₁;induction p;exact ids + by induction s₁₁;induction p;constructor definition whisker_br (p : a₂₂ = a) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀ (p₁₂ ⬝ p) p₀₁ (p₂₁ ⬝ p) := by induction p;exact s₁₁ + definition whisker_rt (p : a = a₂₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + : square (p₁₀ ⬝ p⁻¹) p₁₂ p₀₁ (p ⬝ p₂₁) := + by induction s₁₁;induction p;constructor + + definition whisker_tr (p : a₂₀ = a) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + : square (p₁₀ ⬝ p) p₁₂ p₀₁ (p⁻¹ ⬝ p₂₁) := + by induction s₁₁;induction p;constructor + + definition whisker_bl (p : a = a₀₂) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + : square p₁₀ (p ⬝ p₁₂) (p₀₁ ⬝ p⁻¹) p₂₁ := + by induction s₁₁;induction p;constructor + + definition whisker_lb (p : a₀₂ = a) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + : square p₁₀ (p⁻¹ ⬝ p₁₂) (p₀₁ ⬝ p) p₂₁ := + by induction s₁₁;induction p;constructor + + definition cancel_tl (p : a = a₀₀) (s₁₁ : square (p ⬝ p₁₀) p₁₂ (p ⬝ p₀₁) p₂₁) + : square p₁₀ p₁₂ p₀₁ p₂₁ := + by induction p; rewrite +idp_con at s₁₁; exact s₁₁ + + definition cancel_br (p : a₂₂ = a) (s₁₁ : square p₁₀ (p₁₂ ⬝ p) p₀₁ (p₂₁ ⬝ p)) + : square p₁₀ p₁₂ p₀₁ p₂₁ := + by induction p;exact s₁₁ + + definition cancel_rt (p : a = a₂₀) (s₁₁ : square (p₁₀ ⬝ p⁻¹) p₁₂ p₀₁ (p ⬝ p₂₁)) + : square p₁₀ p₁₂ p₀₁ p₂₁ := + by induction p; rewrite idp_con at s₁₁; exact s₁₁ + + definition cancel_tr (p : a₂₀ = a) (s₁₁ : square (p₁₀ ⬝ p) p₁₂ p₀₁ (p⁻¹ ⬝ p₂₁)) + : square p₁₀ p₁₂ p₀₁ p₂₁ := + by induction p; rewrite [▸* at s₁₁,idp_con at s₁₁]; exact s₁₁ + + definition cancel_bl (p : a = a₀₂) (s₁₁ : square p₁₀ (p ⬝ p₁₂) (p₀₁ ⬝ p⁻¹) p₂₁) + : square p₁₀ p₁₂ p₀₁ p₂₁ := + by induction p; rewrite idp_con at s₁₁; exact s₁₁ + + definition cancel_lb (p : a₀₂ = a) (s₁₁ : square p₁₀ (p⁻¹ ⬝ p₁₂) (p₀₁ ⬝ p) p₂₁) + : square p₁₀ p₁₂ p₀₁ p₂₁ := + by induction p; rewrite [▸* at s₁₁,idp_con at s₁₁]; exact s₁₁ + + definition move_top_of_left {p : a₀₀ = a} {q : a = a₀₂} (s : square p₁₀ p₁₂ (p ⬝ q) p₂₁) + : square (p⁻¹ ⬝ p₁₀) p₁₂ q p₂₁ := + by apply cancel_tl p; rewrite con_inv_cancel_left; exact s + + definition move_top_of_left' {p : a = a₀₀} {q : a = a₀₂} (s : square p₁₀ p₁₂ (p⁻¹ ⬝ q) p₂₁) + : square (p ⬝ p₁₀) p₁₂ q p₂₁ := + by apply cancel_tl p⁻¹; rewrite inv_con_cancel_left; exact s + + definition move_left_of_top {p : a₀₀ = a} {q : a = a₂₀} (s : square (p ⬝ q) p₁₂ p₀₁ p₂₁) + : square q p₁₂ (p⁻¹ ⬝ p₀₁) p₂₁ := + by apply cancel_tl p; rewrite con_inv_cancel_left; exact s + + definition move_left_of_top' {p : a = a₀₀} {q : a = a₂₀} (s : square (p⁻¹ ⬝ q) p₁₂ p₀₁ p₂₁) + : square q p₁₂ (p ⬝ p₀₁) p₂₁ := + by apply cancel_tl p⁻¹; rewrite inv_con_cancel_left; exact s + + definition move_bot_of_right {p : a₂₀ = a} {q : a = a₂₂} (s : square p₁₀ p₁₂ p₀₁ (p ⬝ q)) + : square p₁₀ (p₁₂ ⬝ q⁻¹) p₀₁ p := + by apply cancel_br q; rewrite inv_con_cancel_right; exact s + + definition move_bot_of_right' {p : a₂₀ = a} {q : a₂₂ = a} (s : square p₁₀ p₁₂ p₀₁ (p ⬝ q⁻¹)) + : square p₁₀ (p₁₂ ⬝ q) p₀₁ p := + by apply cancel_br q⁻¹; rewrite con_inv_cancel_right; exact s + + definition move_right_of_bot {p : a₀₂ = a} {q : a = a₂₂} (s : square p₁₀ (p ⬝ q) p₀₁ p₂₁) + : square p₁₀ p p₀₁ (p₂₁ ⬝ q⁻¹) := + by apply cancel_br q; rewrite inv_con_cancel_right; exact s + + definition move_right_of_bot' {p : a₀₂ = a} {q : a₂₂ = a} (s : square p₁₀ (p ⬝ q⁻¹) p₀₁ p₂₁) + : square p₁₀ p p₀₁ (p₂₁ ⬝ q) := + by apply cancel_br q⁻¹; rewrite con_inv_cancel_right; exact s + + definition move_top_of_right {p : a₂₀ = a} {q : a = a₂₂} (s : square p₁₀ p₁₂ p₀₁ (p ⬝ q)) + : square (p₁₀ ⬝ p) p₁₂ p₀₁ q := + by apply cancel_rt p; rewrite con_inv_cancel_right; exact s + + definition move_right_of_top {p : a₀₀ = a} {q : a = a₂₀} (s : square (p ⬝ q) p₁₂ p₀₁ p₂₁) + : square p p₁₂ p₀₁ (q ⬝ p₂₁) := + by apply cancel_tr q; rewrite inv_con_cancel_left; exact s + + definition move_bot_of_left {p : a₀₀ = a} {q : a = a₀₂} (s : square p₁₀ p₁₂ (p ⬝ q) p₂₁) + : square p₁₀ (q ⬝ p₁₂) p p₂₁ := + by apply cancel_lb q; rewrite inv_con_cancel_left; exact s + + definition move_left_of_bot {p : a₀₂ = a} {q : a = a₂₂} (s : square p₁₀ (p ⬝ q) p₀₁ p₂₁) + : square p₁₀ q (p₀₁ ⬝ p) p₂₁ := + by apply cancel_bl p; rewrite con_inv_cancel_right; exact s + /- some higher ∞-groupoid operations -/ definition vconcat_vrfl (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) @@ -125,7 +214,7 @@ namespace eq by induction s₁₁; apply idp definition square_of_eq (r : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : square p₁₀ p₁₂ p₀₁ p₂₁ := - by induction p₁₂; esimp [concat] at r; induction r; induction p₂₁; induction p₁₀; exact ids + by induction p₁₂; esimp at r; induction r; induction p₂₁; induction p₁₀; exact ids definition eq_top_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹ := diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean index 6b5652abd6..21cefa2122 100644 --- a/hott/cubical/squareover.hlean +++ b/hott/cubical/squareover.hlean @@ -103,10 +103,18 @@ namespace eq square.rec_on q idso -- relating pathovers to squareovers - definition pathover_of_squareover (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) + definition pathover_of_squareover' (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) : q₁₀ ⬝o q₂₁ =[eq_of_square s₁₁] q₀₁ ⬝o q₁₂ := by induction t₁₁; constructor + definition pathover_of_squareover {s : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂} + (t₁₁ : squareover B (square_of_eq s) q₁₀ q₁₂ q₀₁ q₂₁) + : q₁₀ ⬝o q₂₁ =[s] q₀₁ ⬝o q₁₂ := + begin + revert s t₁₁, refine equiv_rect' !square_equiv_eq⁻¹ᵉ (λa b, squareover B b _ _ _ _ → _) _, + intro s, exact pathover_of_squareover' + end + definition squareover_of_pathover {s : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂} (r : q₁₀ ⬝o q₂₁ =[s] q₀₁ ⬝o q₁₂) : squareover B (square_of_eq s) q₁₀ q₁₂ q₀₁ q₂₁ := by induction q₁₂; esimp [concato] at r;induction r;induction q₂₁;induction q₁₀;constructor @@ -120,6 +128,14 @@ namespace eq : squareover B (square_of_eq_top s) q₁₀ q₁₂ q₀₁ q₂₁ := by induction q₂₁; induction q₁₂; esimp at r;induction r;induction q₁₀;constructor + definition pathover_of_hdeg_squareover {p₀₁' : a₀₀ = a₀₂} {r : p₀₁ = p₀₁'} {q₀₁' : b₀₀ =[p₀₁'] b₀₂} + (t : squareover B (hdeg_square r) idpo idpo q₀₁ q₀₁') : q₀₁ =[r] q₀₁' := + by induction r; induction q₀₁'; exact (pathover_of_squareover' t)⁻¹ᵒ + + definition pathover_of_vdeg_squareover {p₁₀' : a₀₀ = a₂₀} {r : p₁₀ = p₁₀'} {q₁₀' : b₀₀ =[p₁₀'] b₂₀} + (t : squareover B (vdeg_square r) q₁₀ q₁₀' idpo idpo) : q₁₀ =[r] q₁₀' := + by induction r; induction q₁₀'; exact pathover_of_squareover' t + definition squareover_of_eq_top (r : change_path (eq_top_of_square s₁₁) q₁₀ = q₀₁ ⬝o q₁₂ ⬝o q₂₁⁻¹ᵒ) : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁ := begin diff --git a/hott/function.hlean b/hott/function.hlean index 84429c6473..318f54eece 100644 --- a/hott/function.hlean +++ b/hott/function.hlean @@ -91,6 +91,39 @@ namespace function exact H, end + -- definition is_hprop_is_split_surjective [instance] (f : A → B) : is_hprop (is_split_surjective f) := + -- begin + -- have H : (Π(b : B), fiber f b) ≃ is_split_surjective f, + -- begin + -- fapply equiv.MK, + -- {exact is_split_surjective.mk}, + -- {intro h, cases h, exact elim}, + -- {intro h, cases h, apply idp}, + -- {intro p, apply idp}, + -- end, + -- apply is_trunc_equiv_closed, + -- exact H, + -- apply is_trunc_pi, intro b, + -- apply is_trunc_equiv_closed_rev, + -- apply fiber.sigma_char, + -- end + + -- definition is_hprop_is_retraction [instance] (f : A → B) : is_hprop (is_retraction f) := + -- begin + -- have H : (Σ(g : B → A), Πb, f (g b) = b) ≃ is_retraction f, + -- begin + -- fapply equiv.MK, + -- {intro x, induction x with g p, constructor, exact p}, + -- {intro h, induction h, apply sigma.mk, assumption}, + -- {intro h, induction h, reflexivity}, + -- {intro x, induction x, reflexivity}, + -- end, + -- apply is_trunc_equiv_closed, + -- exact H, + -- apply is_trunc_of_imp_is_trunc, intro x, induction x with g p, + -- apply is_contr_right_inverse + -- end + definition is_embedding_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_embedding f := is_embedding.mk _ diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index b7d493f57e..693252b41e 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -69,7 +69,7 @@ namespace is_equiv parameters {A B : Type} (f : A → B) (g : B → A) (ret : Πb, f (g b) = b) (sec : Πa, g (f a) = a) - private definition adjointify_left_inv' (a : A) : g (f a) = a := + private abbreviation adjointify_left_inv' (a : A) : g (f a) = a := ap g (ap f (inverse (sec a))) ⬝ ap g (ret (f a)) ⬝ sec a private definition adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) := @@ -93,7 +93,7 @@ namespace is_equiv ... = (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite ap_inv ... = ((ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con.assoc' ... = ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f (sec a)⁻¹)) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con_ap_eq_con - ... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite ap_compose + ... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite ap_compose ... = (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : by rewrite con.assoc' ... = retrfa⁻¹ ⬝ ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : by rewrite ap_con ... = retrfa⁻¹ ⬝ (ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : by rewrite con.assoc' @@ -121,7 +121,8 @@ namespace is_equiv (λ b, ap f !Hty⁻¹ ⬝ right_inv f b) (λ a, !Hty⁻¹ ⬝ left_inv f a) - definition is_equiv_up [instance] [constructor] (A : Type) : is_equiv (up : A → lift A) := + definition is_equiv_up [instance] [constructor] (A : Type) + : is_equiv (up : A → lift A) := adjointify up down (λa, by induction a;reflexivity) (λa, idp) section @@ -143,6 +144,12 @@ namespace is_equiv definition eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : x = y := (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y + theorem ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q := + begin + rewrite [↑eq_of_fn_eq_fn',+ap_con,ap_inv,-+adj,-ap_compose,con.assoc, + ap_con_eq_con_ap (right_inv f) q,inv_con_cancel_left,ap_id], + end + definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f : x = y → f x = f y) := adjointify (ap f) @@ -168,9 +175,11 @@ namespace is_equiv -- once pulled back along an equivalence f : A → B, then it has a section -- over all of B. - definition is_equiv_rect (P : B → Type) : - (Πx, P (f x)) → (Πy, P y) := - (λg y, eq.transport _ (right_inv f y) (g (f⁻¹ y))) + definition is_equiv_rect (P : B → Type) (g : Πa, P (f a)) (b : B) : P b := + right_inv f b ▸ g (f⁻¹ b) + + definition is_equiv_rect' (P : A → B → Type) (g : Πb, P (f⁻¹ b) b) (a : A) : P a (f a) := + left_inv f a ▸ g (f a) definition is_equiv_rect_comp (P : B → Type) (df : Π (x : A), P (f x)) (x : A) : is_equiv_rect f P df (f x) = df x := @@ -181,6 +190,13 @@ namespace is_equiv ... = left_inv f x ▸ df (f⁻¹ (f x)) : by rewrite -tr_compose ... = df x : by rewrite (apd df (left_inv f x)) + theorem adj_inv (b : B) : left_inv f (f⁻¹ b) = ap f⁻¹ (right_inv f b) := + is_equiv_rect f _ + (λa, + eq.cancel_right (whisker_left _ !ap_id⁻¹ ⬝ (ap_con_eq_con_ap (left_inv f) (left_inv f a))⁻¹) ⬝ + !ap_compose ⬝ ap02 f⁻¹ (adj f a)⁻¹) + b + end section @@ -202,10 +218,29 @@ namespace is_equiv end --Transporting is an equivalence - definition is_equiv_tr [instance] [constructor] {A : Type} (P : A → Type) {x y : A} (p : x = y) - : (is_equiv (transport P p)) := + definition is_equiv_tr [instance] [constructor] {A : Type} (P : A → Type) {x y : A} + (p : x = y) : (is_equiv (transport P p)) := is_equiv.mk _ (transport P p⁻¹) (tr_inv_tr p) (inv_tr_tr p) (tr_inv_tr_lemma p) + section + variables {A : Type} {B C : A → Type} (f : Π{a}, B a → C a) [H : Πa, is_equiv (@f a)] + {g : A → A} (h : Π{a}, B a → B (g a)) (h' : Π{a}, C a → C (g a)) + include H + definition inv_commute' (p : Π⦃a : A⦄ (b : B a), f (h b) = h' (f b)) {a : A} (c : C a) : + 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))⁻¹) + + definition fun_commute_of_inv_commute' (p : Π⦃a : A⦄ (c : C a), f⁻¹ (h' c) = h (f⁻¹ c)) + {a : A} (b : B a) : f (h b) = h' (f b) := + eq_of_fn_eq_fn' f⁻¹ (left_inv f (h b) ⬝ ap h (left_inv f b)⁻¹ ⬝ (p (f b))⁻¹) + + definition ap_inv_commute' (p : Π⦃a : A⦄ (b : B a), f (h b) = h' (f b)) {a : A} (c : C a) : + ap f (inv_commute' @f @h @h' p c) + = right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹ := + !ap_eq_of_fn_eq_fn' + + end + end is_equiv open is_equiv @@ -216,7 +251,7 @@ namespace eq p⁻¹ ▸ b = (transport B p)⁻¹ b := idp definition cast_inv_fn {A B : Type} (p : A = B) : cast p⁻¹ = (cast p)⁻¹ := idp - definition cast_inv {A B : Type} (p : A = B) (b : B) : cast p⁻¹ b = (cast p)⁻¹ b := idp + definition cast_inv {A B : Type} (p : A = B) (b : B) : cast p⁻¹ b = (cast p)⁻¹ b := idp end eq namespace equiv @@ -228,6 +263,7 @@ namespace equiv infix `≃`:25 := equiv + section variables {A B C : Type} protected definition MK [reducible] [constructor] (f : A → B) (g : B → A) @@ -291,9 +327,11 @@ namespace equiv definition equiv_lift (A : Type) : A ≃ lift A := equiv.mk up _ - definition equiv_rect (f : A ≃ B) (P : B → Type) : - (Πx, P (f x)) → (Πy, P y) := - (λg y, eq.transport _ (right_inv f y) (g (f⁻¹ y))) + definition equiv_rect (f : A ≃ B) (P : B → Type) (g : Πa, P (f a)) (b : B) : P b := + right_inv f b ▸ g (f⁻¹ b) + + definition equiv_rect' (f : A ≃ B) (P : A → B → Type) (g : Πb, P (f⁻¹ b) b) (a : A) : P a (f a) := + left_inv f a ▸ g (f a) definition equiv_rect_comp (f : A ≃ B) (P : B → Type) (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x := @@ -303,6 +341,20 @@ namespace equiv ... = ap f (left_inv f x) ▸ df (f⁻¹ (f x)) : by rewrite -adj ... = left_inv f x ▸ df (f⁻¹ (f x)) : by rewrite -tr_compose ... = df x : by rewrite (apd df (left_inv f x)) + end + + section + variables {A : Type} {B C : A → Type} (f : Π{a}, B a ≃ C a) + {g : A → A} (h : Π{a}, B a → B (g a)) (h' : Π{a}, C a → C (g a)) + + definition inv_commute (p : Π⦃a : A⦄ (b : B a), f (h b) = h' (f b)) {a : A} (c : C a) : + f⁻¹ (h' c) = h (f⁻¹ c) := + inv_commute' @f @h @h' p c + + definition fun_commute_of_inv_commute (p : Π⦃a : A⦄ (c : C a), f⁻¹ (h' c) = h (f⁻¹ c)) + {a : A} (b : B a) : f (h b) = h' (f b) := + fun_commute_of_inv_commute' @f @h @h' p b + end namespace ops @@ -310,4 +362,13 @@ namespace equiv end ops end equiv +open equiv equiv.ops +namespace is_equiv + + definition is_equiv_of_equiv_of_homotopy [constructor] {A B : Type} (f : A ≃ B) + {f' : A → B} (Hty : f ~ f') : is_equiv f' := + homotopy_closed f Hty + +end is_equiv + export [unfold-hints] equiv [unfold-hints] is_equiv diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 8016656817..ef7b48ca3f 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -9,7 +9,7 @@ import init.reserved_notation /- not -/ -definition not (a : Type) := a → empty +definition not [reducible] (a : Type) := a → empty prefix `¬` := not definition absurd {a b : Type} (H₁ : a) (H₂ : ¬a) : b := diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 385f376823..fda7b380ac 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -218,6 +218,9 @@ namespace eq (H1 : f ~ g) (H2 : g ~ h) : f ~ h := λ x, H1 x ⬝ H2 x + definition homotopy_of_eq {f g : Πx, P x} (H1 : f = g) : f ~ g := + H1 ▸ homotopy.refl f + definition apd10 [unfold 5] {f g : Πx, P x} (H : f = g) : f ~ g := λx, eq.rec_on H idp @@ -298,6 +301,7 @@ namespace eq eq.rec_on p idp -- Naturality of [ap]. + -- see also natural_square in cubical.square definition ap_con_eq_con_ap {f g : A → B} (p : f ~ g) {x y : A} (q : x = y) : ap f q ⬝ p y = p x ⬝ ap g q := eq.rec_on q !idp_con @@ -484,7 +488,6 @@ namespace eq ap (transport P p) s ⬝ transport2 P r w = transport2 P r z ⬝ ap (transport P q) s := eq.rec_on r !idp_con⁻¹ - definition fn_tr_eq_tr_fn {P Q : A → Type} {x y : A} (p : x = y) (f : Πx, P x → Q x) (z : P x) : f y (p ▸ z) = (p ▸ (f x z)) := eq.rec_on p idp diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index 1743cf3009..a4bdf59706 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -11,10 +11,10 @@ import .path .equiv open equiv is_equiv equiv.ops -variables {A A' : Type} {B B' : A → Type} {C : Πa, B a → Type} +variables {A A' : Type} {B B' : A → Type} {C : Π⦃a⦄, B a → Type} {a a₂ a₃ a₄ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄} {b b' : B a} {b₂ b₂' : B a₂} {b₃ : B a₃} {b₄ : B a₄} - {c : C a b} {c₂ : C a₂ b₂} + {c : C b} {c₂ : C b₂} namespace eq inductive pathover.{l} (B : A → Type.{l}) (b : B a) : Π{a₂ : A}, a = a₂ → B a₂ → Type.{l} := @@ -26,10 +26,10 @@ namespace eq pathover.idpatho b /- equivalences with equality using transport -/ - definition pathover_of_tr_eq (r : p ▸ b = b₂) : b =[p] b₂ := + definition pathover_of_tr_eq [unfold 5 8] (r : p ▸ b = b₂) : b =[p] b₂ := by cases p; cases r; exact idpo - definition pathover_of_eq_tr (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ := + definition pathover_of_eq_tr [unfold 5 8] (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ := by cases p; cases r; exact idpo definition tr_eq_of_pathover [unfold 8] (r : b =[p] b₂) : p ▸ b = b₂ := @@ -205,7 +205,17 @@ namespace eq definition tr_pathover_of_eq (q : b₂ = b₂') : p⁻¹ ▸ b₂ =[p] b₂' := by cases q;apply tr_pathover - definition apo (f : Πa, B a → B' a) (Ha : a = a₂) (Hb : b =[Ha] b₂) + variable (C) + definition transporto (r : b =[p] b₂) (c : C b) : C b₂ := + by induction r;exact c + infix `▸o`:75 := transporto _ + + definition fn_tro_eq_tro_fn (C' : Π ⦃a : A⦄, B a → Type) (q : b =[p] b₂) + (f : Π(b : B a), C b → C' b) (c : C b) : f b (q ▸o c) = (q ▸o (f b c)) := + by induction q;reflexivity + variable {C} + + definition apo (f : Πa, B a → B' a) {Ha : a = a₂} (Hb : b =[Ha] b₂) : f a b =[Ha] f a₂ b₂ := by induction Hb; exact idpo @@ -213,15 +223,15 @@ namespace eq : f a b = f a₂ b₂ := by cases Hb; exact idp - definition apo0111 (f : Πa b, C a b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂) + definition apo0111 (f : Πa b, C b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂) (Hc : c =[apo011 C Ha Hb] c₂) : f a b c = f a₂ b₂ c₂ := by cases Hb; apply (idp_rec_on Hc); apply idp - definition apo11 {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g) + definition apo11 {f : Πb, C b} {g : Πb₂, C b₂} (r : f =[p] g) {b : B a} {b₂ : B a₂} (q : b =[p] b₂) : f b =[apo011 C p q] g b₂ := by cases r; apply (idp_rec_on q); exact idpo - definition apdo10 {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g) + definition apdo10 {f : Πb, C b} {g : Πb₂, C b₂} (r : f =[p] g) (b : B a) : f b =[apo011 C p !pathover_tr] g (p ▸ b) := by cases r; exact idpo diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 1e234eb315..0662499c14 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -143,6 +143,16 @@ namespace is_trunc @is_trunc_succ_intro A m (λx y, IHm n (x = y) (trunc_index.le_of_succ_le_succ Hnm) _)), trunc_index.rec_on m base step n A Hnm Hn + definition is_trunc_of_imp_is_trunc {n : trunc_index} (H : A → is_trunc (n.+1) A) + : is_trunc (n.+1) A := + @is_trunc_succ_intro _ _ (λx y, @is_trunc_eq _ _ (H x) x y) + + definition is_trunc_of_imp_is_trunc_of_leq {n : trunc_index} (Hn : -1 ≤ n) (H : A → is_trunc n A) + : is_trunc n A := + trunc_index.rec_on n (λHn H, empty.rec _ Hn) + (λn IH Hn, is_trunc_of_imp_is_trunc) + Hn H + -- the following cannot be instances in their current form, because they are looping theorem is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A := trunc_index.rec_on n H _ diff --git a/hott/types/arrow.hlean b/hott/types/arrow.hlean index 576e7d4b3a..0f1743e149 100644 --- a/hott/types/arrow.hlean +++ b/hott/types/arrow.hlean @@ -44,6 +44,9 @@ namespace pi definition arrow_equiv_arrow_left (f0 : A ≃ A') : (A → B) ≃ (A' → B) := arrow_equiv_arrow f0 equiv.refl + definition arrow_equiv_arrow_right' (f1 : A → (B ≃ B')) : (A → B) ≃ (A → B') := + pi_equiv_pi_id f1 + /- Transport -/ definition arrow_transport {B C : A → Type} (p : a = a') (f : B a → C a) diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 06514f0e2a..bf06b063bd 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -20,14 +20,14 @@ namespace is_equiv (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 - ... = (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))) + 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 + ... = (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 @@ -76,7 +76,8 @@ namespace is_equiv local attribute is_contr_right_coherence [instance] [priority 1600] theorem is_hprop_is_equiv [instance] : is_hprop (is_equiv f) := - is_hprop_of_imp_is_contr (λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !is_equiv.sigma_char')) + is_hprop_of_imp_is_contr + (λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !is_equiv.sigma_char')) definition inv_eq_inv {A B : Type} {f f' : A → B} {Hf : is_equiv f} {Hf' : is_equiv f'} (p : f = f') : f⁻¹ = f'⁻¹ := diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean index df664b300c..a745067e16 100644 --- a/hott/types/nat/basic.hlean +++ b/hott/types/nat/basic.hlean @@ -59,8 +59,7 @@ rfl definition eq_zero_or_eq_succ_pred (n : ℕ) : n = 0 ⊎ n = succ (pred n) := nat.rec_on n (sum.inl rfl) - (take m IH, sum.inr - (show succ m = succ (pred (succ m)), from ap succ !pred_succ⁻¹)) + (take m IH, sum.inr rfl) definition exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : Σk : ℕ, n = succ k := sigma.mk _ (sum_resolve_right !eq_zero_or_eq_succ_pred H) @@ -118,11 +117,8 @@ nat.rec_on n definition succ_add (n m : ℕ) : (succ n) + m = succ (n + m) := nat.rec_on m - (!add_zero ▸ !add_zero) - (take k IH, calc - succ n + succ k = succ (succ n + k) : add_succ - ... = succ (succ (n + k)) : IH - ... = succ (n + succ k) : add_succ) + (rfl) + (take k IH, eq.ap succ IH) definition add.comm (n m : ℕ) : n + m = m + n := nat.rec_on m diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index eb7eb1fa41..2d08232e0d 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -47,7 +47,8 @@ namespace pi definition pi_eq_equiv (f g : Πx, B x) : (f = g) ≃ (f ~ g) := !eq_equiv_homotopy - definition is_equiv_eq_of_homotopy (f g : Πx, B x) : is_equiv (@eq_of_homotopy _ _ f g) := + definition is_equiv_eq_of_homotopy (f g : Πx, B x) + : is_equiv (eq_of_homotopy : f ~ g → f = g) := _ definition homotopy_equiv_eq (f g : Πx, B x) : (f ~ g) ≃ (f = g) := @@ -57,15 +58,14 @@ namespace pi /- Transport -/ definition pi_transport (p : a = a') (f : Π(b : B a), C a b) - : (transport (λa, Π(b : B a), C a b) p f) - ~ (λb, transport (C a') !tr_inv_tr (transportD _ p _ (f (p⁻¹ ▸ b)))) := - eq.rec_on p (λx, idp) + : (transport (λa, Π(b : B a), C a b) p f) ~ (λb, !tr_inv_tr ▸ (p ▸D (f (p⁻¹ ▸ b)))) := + by induction p; reflexivity /- A special case of [transport_pi] where the type [B] does not depend on [A], and so it is just a fixed type [B]. -/ definition pi_transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b) (b : A') : (transport _ p f) b = p ▸ (f b) := - eq.rec_on p idp + by induction p; reflexivity /- Pathovers -/ @@ -171,7 +171,7 @@ namespace pi /- Equivalences -/ definition is_equiv_pi_functor [instance] [H0 : is_equiv f0] - [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] : is_equiv (pi_functor f0 f1) := + [H1 : Πa', is_equiv (f1 a')] : is_equiv (pi_functor f0 f1) := begin apply (adjointify (pi_functor f0 f1) (pi_functor f0⁻¹ (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (right_inv f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))), @@ -188,7 +188,7 @@ namespace pi end definition pi_equiv_pi_of_is_equiv [H : is_equiv f0] - [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] : (Πa, B a) ≃ (Πa', B' a') := + [H1 : Πa', is_equiv (f1 a')] : (Πa, B a) ≃ (Πa', B' a') := equiv.mk (pi_functor f0 f1) _ definition pi_equiv_pi (f0 : A' ≃ A) (f1 : Πa', (B (to_fun f0 a') ≃ B' a')) @@ -237,8 +237,11 @@ namespace pi assert H : is_contr A, from is_contr.mk a f, _) + definition is_hprop_neg (A : Type) : is_hprop (¬A) := _ + /- Symmetry of Π -/ - definition is_equiv_flip [instance] {P : A → A' → Type} : is_equiv (@function.flip A A' P) := + definition is_equiv_flip [instance] {P : A → A' → Type} + : is_equiv (@function.flip A A' P) := begin fapply is_equiv.mk, exact (@function.flip _ _ (function.flip P)), diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean index eab5f15e22..1d08ea8f2a 100644 --- a/hott/types/sum.hlean +++ b/hott/types/sum.hlean @@ -6,6 +6,8 @@ Author: Floris van Doorn Theorems about sums/coproducts/disjoint unions -/ +import .pi + open lift eq is_equiv equiv equiv.ops prod prod.ops is_trunc sigma bool namespace sum @@ -16,8 +18,8 @@ namespace sum by induction z; all_goals reflexivity protected definition code [unfold 3 4] : A + B → A + B → Type.{max u v} - | code (inl a) (inl a') := lift.{u v} (a = a') - | code (inr b) (inr b') := lift.{v u} (b = b') + | code (inl a) (inl a') := lift (a = a') + | code (inr b) (inr b') := lift (b = b') | code _ _ := lift empty protected definition decode [unfold 3 4] : Π(z z' : A + B), sum.code z z' → z = z' @@ -72,10 +74,10 @@ namespace sum protected definition decodeo (p : a = a') : Π(z : P a + Q a) (z' : P a' + Q a'), sum.codeo p z z' → z =[p] z' - | decodeo (inl x) (inl x') := λc, apo (λa, inl) p (down c) + | decodeo (inl x) (inl x') := λc, apo (λa, inl) (down c) | decodeo (inl x) (inr y') := λc, empty.elim (down c) _ | decodeo (inr y) (inl x') := λc, empty.elim (down c) _ - | decodeo (inr y) (inr y') := λc, apo (λa, inr) p (down c) + | decodeo (inr y) (inr y') := λc, apo (λa, inr) (down c) variables {z z'} protected definition encodeo {p : a = a'} {z : P a + Q a} {z' : P a' + Q a'} (q : z =[p] z') @@ -157,12 +159,17 @@ namespace sum definition sum_empty_equiv [constructor] (A : Type) : A + empty ≃ A := begin fapply equiv.MK, - intro z, induction z, assumption, contradiction, - exact inl, - intro a, reflexivity, - intro z, induction z, reflexivity, contradiction + { intro z, induction z, assumption, contradiction}, + { exact inl}, + { intro a, reflexivity}, + { intro z, induction z, reflexivity, contradiction} end + definition empty_sum_equiv (A : Type) : empty + A ≃ A := + !sum_comm_equiv ⬝e !sum_empty_equiv + + /- universal property -/ + definition sum_rec_unc {P : A + B → Type} (fg : (Πa, P (inl a)) × (Πb, P (inr b))) : Πz, P z := sum.rec fg.1 fg.2 @@ -182,6 +189,9 @@ namespace sum : (A → C) × (B → C) ≃ (A + B → C) := !equiv_sum_rec + /- truncatedness -/ + + variables (A B) definition is_trunc_sum (n : trunc_index) [HA : is_trunc (n.+2) A] [HB : is_trunc (n.+2) B] : is_trunc (n.+2) (A + B) := begin @@ -191,6 +201,23 @@ namespace sum all_goals exact _, end + definition is_trunc_sum_excluded (n : trunc_index) [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, + { exfalso, exact H !center !center}, + { clear IH, induction n with n IH, + { apply is_hprop.mk, intros x y, + induction x, all_goals induction y, all_goals esimp, + all_goals try (exfalso;apply H;assumption;assumption), all_goals apply ap _ !is_hprop.elim}, + { apply is_trunc_sum}} + end + + variable {B} + definition is_contr_sum_left [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))) + /- Sums are equivalent to dependent sigmas where the first component is a bool. @@ -198,7 +225,6 @@ namespace sum If we need it for A and B in different universes, we need to insert some lifts. -/ - definition sum_of_sigma_bool {A B : Type.{u}} (v : Σ(b : bool), bool.rec A B b) : A + B := by induction v with b x; induction b; exact inl x; exact inr x @@ -213,3 +239,24 @@ namespace sum begin intro z, induction z with a b, all_goals reflexivity end end sum + +namespace decidable + open sum pi + + definition decidable_equiv (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 (A : Type) (n : trunc_index) [H : is_trunc n A] : + is_trunc n (decidable A) := + begin + apply is_trunc_equiv_closed_rev, + apply decidable_equiv, + induction n with n IH, + { apply is_contr_sum_left, exact λna, na !center}, + { apply is_trunc_sum_excluded, exact λa na, na a} + end + +end decidable diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 0f4e38141a..f35de985d9 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -16,14 +16,6 @@ open eq sigma sigma.ops pi function equiv is_trunc.trunctype namespace is_trunc variables {A B : Type} {n : trunc_index} - definition is_trunc_succ_of_imp_is_trunc_succ (H : A → is_trunc (n.+1) A) : is_trunc (n.+1) A := - @is_trunc_succ_intro _ _ (λx y, @is_trunc_eq _ _ (H x) x y) - - definition is_trunc_of_imp_is_trunc_of_leq (Hn : -1 ≤ n) (H : A → is_trunc n A) : is_trunc n A := - trunc_index.rec_on n (λHn H, empty.rec _ Hn) - (λn IH Hn, is_trunc_succ_of_imp_is_trunc_succ) - Hn H - /- theorems about trunctype -/ protected definition trunctype.sigma_char.{l} (n : trunc_index) : (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) := diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index ef5ebe1d6b..05d64c8516 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -20,7 +20,7 @@ "using" "namespace" "section" "fields" "find_decl" "attribute" "local" "set_option" "extends" "include" "omit" "classes" "instances" "coercions" "metaclasses" "raw" "migrate" "replacing" - "calc" "have" "show" "suffices" "by" "in" "at" "let" "forall" "fun" + "calc" "have" "show" "suffices" "by" "in" "at" "let" "forall" "Pi" "fun" "exists" "if" "dif" "then" "else" "assume" "assert" "take" "obtain" "from") "lean keywords ending with 'word' (not symbol)")