diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean index ddfd8ba66..3a31aa775 100644 --- a/hott/algebra/category/adjoint.hlean +++ b/hott/algebra/category/adjoint.hlean @@ -27,9 +27,11 @@ namespace category (H : Π(c : C), ε (F c) ∘ F (η c) = ID (F c)) (K : Π(d : D), G (ε d) ∘ η (G d) = ID (G d)) - abbreviation right_adjoint := @is_left_adjoint.G - abbreviation unit := @is_left_adjoint.η - abbreviation counit := @is_left_adjoint.ε + abbreviation right_adjoint [unfold 4] := @is_left_adjoint.G + abbreviation unit [unfold 4] := @is_left_adjoint.η + abbreviation counit [unfold 4] := @is_left_adjoint.ε + abbreviation counit_unit_eq [unfold 4] := @is_left_adjoint.H + abbreviation unit_counit_eq [unfold 4] := @is_left_adjoint.K structure is_equivalence [class] (F : C ⇒ D) extends is_left_adjoint F := mk' :: @@ -38,7 +40,7 @@ namespace category abbreviation inverse := @is_equivalence.G postfix ⁻¹ := inverse - --a second notation for the inverse, which is not overloaded + --a second notation for the inverse, which is not overloaded (there is no unicode superscript F) postfix [parsing_only] `⁻¹F`:std.prec.max_plus := inverse --TODO: review and change @@ -59,8 +61,8 @@ namespace category (struct : is_isomorphism to_functor) -- infix `⊣`:55 := adjoint - infix ` ⋍ `:25 := equivalence -- \backsimeq or \equiv - infix ` ≌ `:25 := isomorphism -- \backcong or \iso + infix ` ≃c `:25 := equivalence + infix ` ≅c `:25 := isomorphism definition is_equiv_of_fully_faithful [instance] [reducible] (F : C ⇒ D) [H : fully_faithful F] (c c' : C) : is_equiv (@(to_fun_hom F) c c') := @@ -235,128 +237,85 @@ namespace category section parameters {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C} (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) - -- variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d) - -- (pη : Π(c c' : C) (f : hom c c'), f ∘ to_hom (η c) = to_hom (η c') ∘ G (F f)) - -- (pε : Π⦃d d' : D⦄ (f : hom d d'), f ∘ to_hom (ε d) = to_hom (ε d') ∘ F (G f)) + -- variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d) + -- (pη : Π(c c' : C) (f : hom c c'), f ∘ to_hom (η c) = to_hom (η c') ∘ G (F f)) + -- (pε : Π⦃d d' : D⦄ (f : hom d d'), f ∘ to_hom (ε d) = to_hom (ε d') ∘ F (G f)) - private definition ηn : 1 ⟹ G ∘f F := to_inv η - private definition εn : F ∘f G ⟹ 1 := to_hom ε + private definition ηn : 1 ⟹ G ∘f F := to_inv η + private definition εn : F ∘f G ⟹ 1 := to_hom ε - private definition ηi (c : C) : G (F c) ≅ c := componentwise_iso η c - private definition εi (d : D) : F (G d) ≅ d := componentwise_iso ε d + private definition ηi (c : C) : G (F c) ≅ c := componentwise_iso η c + private definition εi (d : D) : F (G d) ≅ d := componentwise_iso ε d - private definition ηi' (c : C) : G (F c) ≅ c := - to_fun_iso G (to_fun_iso F (ηi c)⁻¹ⁱ) ⬝i to_fun_iso G (εi (F c)) ⬝i ηi c -exit - set_option pp.implicit true - private theorem adj_η_natural {c c' : C} (f : hom c c') - : G (F f) ∘ to_inv (ηi' c) = to_inv (ηi c') ∘ f := - let ηi'_nat : G ∘f F ⟹ 1 := - /- 1 ⇐ G ∘f F :-/ to_hom η - ∘n /- ... ⇐ (G ∘f 1) ∘f F :-/ hom_of_eq !functor.id_right ∘nf F - ∘n /- ... ⇐ (G ∘f (F ∘f G)) ∘f F :-/ (G ∘fn εn) ∘nf F - ∘n /- ... ⇐ ((G ∘f F) ∘f G) ∘f F :-/ hom_of_eq !functor.assoc⁻¹ ∘nf F - ∘n /- ... ⇐ (G ∘f F) ∘f (G ∘f F) :-/ hom_of_eq !functor.assoc - ∘n /- ... ⇐ (G ∘f F) ∘f 1 :-/ (G ∘f F) ∘fn ηn - ∘n /- ... ⇐ G ∘f F :-/ hom_of_eq !functor.id_right⁻¹ - in - have ηi'_nat ~ ηi', begin intro c, fold [precategory_functor C C] - /-rewrite [+natural_map_hom_of_eq],-/ end, - _ + private definition ηi' (c : C) : G (F c) ≅ c := + to_fun_iso G (to_fun_iso F (ηi c)⁻¹ⁱ) ⬝i to_fun_iso G (εi (F c)) ⬝i ηi c - private theorem adjointify_adjH (c : C) : - to_hom (ε (F c)) ∘ F (to_hom (adj_η η ε c)⁻¹ⁱ) = id := - begin - exact sorry - end + local attribute ηn εn ηi εi ηi' [reducible] - private theorem adjointify_adjK (d : D) : - G (to_hom (ε d)) ∘ to_hom (adj_η η ε (G d))⁻¹ⁱ = id := - begin - exact sorry - end - - attribute functor.id [reducible] - variables (F G) - definition is_equivalence.mk : is_equivalence F := + private theorem adj_η_natural {c c' : C} (f : hom c c') + : G (F f) ∘ to_inv (ηi' c) = to_inv (ηi' c') ∘ f := + let ηi'_nat : G ∘f F ⟹ 1 := + calc + G ∘f F ⟹ (G ∘f F) ∘f 1 : id_right_natural_rev (G ∘f F) + ... ⟹ (G ∘f F) ∘f (G ∘f F) : (G ∘f F) ∘fn ηn + ... ⟹ ((G ∘f F) ∘f G) ∘f F : assoc_natural (G ∘f F) G F + ... ⟹ (G ∘f (F ∘f G)) ∘f F : assoc_natural_rev G F G ∘nf F + ... ⟹ (G ∘f 1) ∘f F : (G ∘fn εn) ∘nf F + ... ⟹ G ∘f F : id_right_natural G ∘nf F + ... ⟹ 1 : to_hom η + in begin - fapply is_equivalence.mk', - { exact G}, - { fapply nat_trans.mk, - { intro c, exact to_inv (adj_η η ε c)}, - { intro c c' f, exact adj_η_natural η ε pη pε f}}, - { fapply nat_trans.mk, - { exact λd, to_hom (ε d)}, - { exact pε}}, - { exact adjointify_adjH η ε pη pε}, - { exact adjointify_adjK η ε pη pε}, - { exact @(is_iso_nat_trans _) (λc, !is_iso_inverse)}, - { apply is_iso_nat_trans}, + refine is_natural_inverse' (G ∘f F) functor.id ηi' ηi'_nat _ f, + intro c, esimp, rewrite [+id_left,id_right] end - end + private theorem adjointify_adjH (c : C) : + to_hom (εi (F c)) ∘ F (to_hom (ηi' c))⁻¹ = id := + begin + rewrite [respect_inv], apply comp_inverse_eq_of_eq_comp, + rewrite [id_left,↑ηi',+respect_comp,+respect_inv',assoc], apply eq_comp_inverse_of_comp_eq, + rewrite [↑εi,-naturality_iso_id ε (F c)], + symmetry, exact naturality εn (F (to_hom (ηi c))) + end - definition is_equivalence.mk2 (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) : is_equivalence F := - is_equivalence.mk F G - (componentwise_iso η) (componentwise_iso ε) - begin intro c c' f, esimp, apply naturality (to_hom η) f end - begin intro c c' f, esimp, apply naturality (to_hom ε) f end + private theorem adjointify_adjK (d : D) : + G (to_hom (εi d)) ∘ to_hom (ηi' (G d))⁻¹ⁱ = id := + begin + apply comp_inverse_eq_of_eq_comp, + rewrite [id_left,↑ηi',+respect_inv',assoc], apply eq_comp_inverse_of_comp_eq, + rewrite [↑ηi,-naturality_iso_id η (G d),↑εi,naturality_iso_id ε d], + exact naturality (to_hom η) (G (to_hom (εi d))), + end -exit - - section - variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) -- we need some kind of naturality + parameters (F G) include η ε - - -- private definition adj_η : G ∘f F ≅ functor.id := - -- change_inv - -- ( calc - -- G ∘f F ≅ (G ∘f F) ∘f 1 : iso_of_eq !functor.id_right - -- ... ≅ (G ∘f F) ∘f (G ∘f F) : _ - -- ... ≅ G ∘f (F ∘f (G ∘f F)) : _ - -- ... ≅ G ∘f ((F ∘f G) ∘f F) : _ - -- ... ≅ G ∘f (1 ∘f F) : _ - -- ... ≅ G ∘f F : _ - -- ... ≅ 1 : η) - -- _ - -- _ --change_natural_map _ _ - --sorry --to_fun_iso G (to_fun_iso F (η c)⁻¹ⁱ) ⬝i to_fun_iso G (ε (F c)) ⬝i η c - open iso - - -- definition nat_map_of_iso [reducible] {C D : Precategory} {F G : C ⇒ D} (η : F ≅ G) (c : C) - -- : F c ⟶ G c := - -- natural_map (to_hom η) c - - private theorem adjointify_adjH (c : C) : - natural_map (to_hom ε) (F c) ∘ F (natural_map (to_inv (adj_η η ε)) c) = id := - begin - exact sorry - end - - -- (H : Π(c : C), ε (F c) ∘ F (η c) = ID (F c)) - -- (K : Π(d : D), G (ε d) ∘ η (G d) = ID (G d)) - - private theorem adjointify_adjK (d : D) : - G (natural_map (to_hom ε) d) ∘ natural_map (to_inv (adj_η η ε)) (G d) = id := - begin - exact sorry - end - - variables (F G) definition is_equivalence.mk : is_equivalence F := begin fapply is_equivalence.mk', { exact G}, - { exact to_inv (adj_η η ε)}, - { exact to_hom ε}, - { exact adjointify_adjH η ε}, - { exact adjointify_adjK η ε}, - { unfold to_inv, apply is_iso_inverse}, - { apply iso.struct}, + { fapply nat_trans.mk, + { intro c, exact to_inv (ηi' c)}, + { intro c c' f, exact adj_η_natural f}}, + { exact εn}, + { exact adjointify_adjH}, + { exact adjointify_adjK}, + { exact @(is_iso_nat_trans _) (λc, !is_iso_inverse)}, + { unfold εn, apply iso.struct, }, end + definition equivalence.MK : C ≃c D := + equivalence.mk F is_equivalence.mk + end + + variables {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C} + + --TODO: add variants + definition unit_eq_counit_inv (F : C ⇒ D) [H : is_equivalence F] (c : C) : + to_fun_hom F (natural_map (unit F) c) = + @(is_iso.inverse (counit F (F c))) (@(componentwise_is_iso (counit F)) !is_iso_counit (F c)) := + begin + apply eq_inverse_of_comp_eq_id, apply counit_unit_eq end -/- definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F] : fully_faithful F := @@ -367,10 +326,77 @@ exit { intro g, rewrite [+respect_comp,▸*], krewrite [natural_map_inverse], xrewrite [respect_inv'], apply inverse_comp_eq_of_eq_comp, - exact sorry /-this is basically the naturality of the counit-/ }, + let H := @(naturality (F ∘fn (unit F))), + rewrite [+unit_eq_counit_inv], exact sorry}, + /-this is basically the naturality of the counit-/ { exact sorry}, end + definition is_isomorphism.mk {F : C ⇒ D} (G : D ⇒ C) (p : G ∘f F = 1) (q : F ∘f G = 1) + : is_isomorphism F := + begin + constructor, + { apply fully_faithful_of_is_equivalence, fapply is_equivalence.mk, + { exact G}, + { apply iso_of_eq p}, + { apply iso_of_eq q}}, + { fapply adjointify, + { exact G}, + { exact ap010 to_fun_ob q}, + { exact ap010 to_fun_ob p}} + end + + definition is_equiv_of_is_isomorphism (F : C ⇒ D) [H : is_isomorphism F] + : is_equiv (to_fun_ob F) := + pr2 H + + definition is_fully_faithful_of_is_isomorphism (F : C ⇒ D) [H : is_isomorphism F] + : fully_faithful F := + pr1 H + + local attribute is_fully_faithful_of_is_isomorphism is_equiv_of_is_isomorphism [instance] + + definition strict_inverse [constructor] (F : C ⇒ D) [H : is_isomorphism F] : D ⇒ C := + begin + fapply functor.mk, + { intro d, exact (to_fun_ob F)⁻¹ᶠ d}, + { intro d d' g, exact (to_fun_hom F)⁻¹ᶠ (inv_of_eq !right_inv ∘ g ∘ hom_of_eq !right_inv)}, + { intro d, apply inv_eq_of_eq, rewrite [respect_id,id_left], apply left_inverse}, + { intro d₁ d₂ d₃ g₂ g₁, apply inv_eq_of_eq, rewrite [respect_comp F,+right_inv (to_fun_hom F)], + rewrite [+assoc], esimp, /-apply ap (λx, _ ∘ x), FAILS-/ refine ap (λx, (x ∘ _) ∘ _) _, + refine !id_right⁻¹ ⬝ _, rewrite [▸*,-+assoc], refine ap (λx, _ ∘ _ ∘ x) _, + exact !right_inverse⁻¹}, + end + + definition strict_right_inverse (F : C ⇒ D) [H : is_isomorphism F] : F ∘f strict_inverse F = 1 := + begin + fapply functor_eq, + { intro d, esimp, apply right_inv}, + { intro d d' g, + rewrite [▸*, right_inv (to_fun_hom F), +assoc], + rewrite [↑[hom_of_eq,inv_of_eq,iso.to_inv], right_inverse], + rewrite [id_left], apply comp_inverse_cancel_right}, + end + + definition strict_left_inverse (F : C ⇒ D) [H : is_isomorphism F] : strict_inverse F ∘f F = 1 := + begin + fapply functor_eq, + { intro d, esimp, apply left_inv}, + { intro d d' g, esimp, apply comp_eq_of_eq_inverse_comp, apply comp_inverse_eq_of_eq_comp, + apply inv_eq_of_eq, rewrite [+respect_comp,-assoc], apply ap011 (λx y, x ∘ F g ∘ y), + { rewrite [adj], rewrite [▸*,respect_inv_of_eq F]}, + { rewrite [adj,▸*,respect_hom_of_eq F]}}, + end + + definition is_equivalence_of_is_isomorphism [instance] (F : C ⇒ D) [H : is_isomorphism F] + : is_equivalence F := + begin + fapply is_equivalence.mk, + { apply strict_inverse F}, + { apply iso_of_eq !strict_left_inverse}, + { apply iso_of_eq !strict_right_inverse}, + end + definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) := sorry @@ -400,23 +426,20 @@ exit ≃ ∃(G : D ⇒ C), 1 = G ∘f F × F ∘f G = 1 := sorry - definition is_equivalence_of_isomorphism (H : is_isomorphism F) : is_equivalence F := - sorry - definition is_isomorphism_of_is_equivalence {C D : Category} {F : C ⇒ D} (H : is_equivalence F) : is_isomorphism F := sorry - definition isomorphism_of_eq {C D : Precategory} (p : C = D) : C ≌ D := + definition isomorphism_of_eq {C D : Precategory} (p : C = D) : C ≅c D := sorry definition is_equiv_isomorphism_of_eq (C D : Precategory) : is_equiv (@isomorphism_of_eq C D) := sorry - definition equivalence_of_eq {C D : Precategory} (p : C = D) : C ⋍ D := + definition equivalence_of_eq {C D : Precategory} (p : C = D) : C ≃c D := sorry definition is_equiv_equivalence_of_eq (C D : Category) : is_equiv (@equivalence_of_eq C D) := sorry --/ + end category diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean index 56fc4840e..59b961b46 100644 --- a/hott/algebra/category/category.hlean +++ b/hott/algebra/category/category.hlean @@ -14,8 +14,9 @@ open iso is_equiv equiv eq is_trunc -/ namespace category /- - TODO: restructure this. is_univalent should probably be a class with as argument - (C : Precategory) + TODO: restructure this. Should is_univalent be a class with as argument + (C : Precategory). Or is that problematic if we want to apply this to cases where e.g. + a b are functors, and we need to synthesize ? : precategory (functor C D). -/ definition is_univalent [class] {ob : Type} (C : precategory ob) := Π(a b : ob), is_equiv (iso_of_eq : a = b → a ≅ b) diff --git a/hott/algebra/category/colimits.hlean b/hott/algebra/category/colimits.hlean index f7ef6d23e..8a96b3ab2 100644 --- a/hott/algebra/category/colimits.hlean +++ b/hott/algebra/category/colimits.hlean @@ -168,7 +168,8 @@ namespace category definition coproduct_object : D := colimit_object (c2_functor D d d') - infixr + := coproduct_object + infixr `+l`:27 := coproduct_object + local infixr + := coproduct_object definition inl : d ⟶ d + d' := colimit_morphism (c2_functor D d d') ff @@ -317,4 +318,8 @@ namespace category : has_limits_of_shape D I := by induction I with I Is; induction Is; exact H + namespace ops + infixr + := coproduct_object + end ops + end category diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index c27bc4af4..c3910c0fb 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -65,13 +65,27 @@ namespace functor definition functor_iso [constructor] : F ≅ G := @(iso.mk η) !is_iso_nat_trans + omit iso + variables (F G) + + definition is_natural_inverse (η : Πc, F c ≅ G c) + (nat : Π⦃a b : C⦄ (f : hom a b), G f ∘ to_hom (η a) = to_hom (η b) ∘ F f) + {a b : C} (f : hom a b) : F f ∘ to_inv (η a) = to_inv (η b) ∘ G f := + let η' : F ⟹ G := nat_trans.mk (λc, to_hom (η c)) @nat in + naturality (nat_trans_inverse η') f + + definition is_natural_inverse' (η₁ : Πc, F c ≅ G c) (η₂ : F ⟹ G) (p : η₁ ~ η₂) + {a b : C} (f : hom a b) : F f ∘ to_inv (η₁ a) = to_inv (η₁ b) ∘ G f := + is_natural_inverse F G η₁ abstract λa b g, (p a)⁻¹ ▸ (p b)⁻¹ ▸ naturality η₂ g end f + end + section /- and conversely, if a natural transformation is an iso, it is componentwise an iso -/ variables {A B C D : Precategory} {F G : C ⇒ D} (η : hom F G) [isoη : is_iso η] (c : C) include isoη - definition componentwise_is_iso [instance] [constructor] : is_iso (η c) := + definition componentwise_is_iso [constructor] : is_iso (η c) := @is_iso.mk _ _ _ _ _ (natural_map η⁻¹ c) (ap010 natural_map ( left_inverse η) c) (ap010 natural_map (right_inverse η) c) @@ -105,6 +119,11 @@ namespace functor : componentwise_iso (iso_of_eq p) c = iso_of_eq (ap010 to_fun_ob p c) := eq.rec_on p !componentwise_iso_id + theorem naturality_iso_id {F : C ⇒ C} (η : F ≅ 1) (c : C) + : componentwise_iso η (F c) = F (componentwise_iso η c) := + comp.cancel_left (to_hom (componentwise_iso η c)) + ((naturality (to_hom η)) (to_hom (componentwise_iso η c))) + definition natural_map_hom_of_eq (p : F = G) (c : C) : natural_map (hom_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c) := eq.rec_on p idp diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean index 8dc3d7282..093f85e58 100644 --- a/hott/algebra/category/functor.hlean +++ b/hott/algebra/category/functor.hlean @@ -124,6 +124,18 @@ namespace functor : to_fun_iso F (f ⬝i g) = to_fun_iso F f ⬝i to_fun_iso F g := iso_eq !respect_comp + definition respect_iso_of_eq (F : C ⇒ D) {a b : C} (p : a = b) : + to_fun_iso F (iso_of_eq p) = iso_of_eq (ap F p) := + by induction p; apply respect_refl + + theorem respect_hom_of_eq (F : C ⇒ D) {a b : C} (p : a = b) : + F (hom_of_eq p) = hom_of_eq (ap F p) := + by induction p; apply respect_id + + definition respect_inv_of_eq (F : C ⇒ D) {a b : C} (p : a = b) : + F (inv_of_eq p) = inv_of_eq (ap F p) := + by induction p; apply respect_id + protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) : H ∘f (G ∘f F) = (H ∘f G) ∘f F := !functor_mk_eq_constant (λa b f, idp) diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean index 18153d38a..7e5fcc47c 100644 --- a/hott/algebra/category/groupoid.hlean +++ b/hott/algebra/category/groupoid.hlean @@ -16,7 +16,7 @@ namespace category mk' :: (all_iso : Π ⦃a b : ob⦄ (f : hom a b), @is_iso ob parent a b f) abbreviation all_iso := @groupoid.all_iso - attribute groupoid.all_iso [instance] [priority 100000] + attribute groupoid.all_iso [instance] [priority 3000] definition groupoid.mk [reducible] {ob : Type} (C : precategory ob) (H : Π (a b : ob) (f : a ⟶ b), is_iso f) : groupoid ob := diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index 6af7abccd..914f862e5 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -132,7 +132,7 @@ structure iso {ob : Type} [C : precategory ob] (a b : ob) := [struct : is_iso to_hom] infix ` ≅ `:50 := iso - attribute iso.struct [instance] [priority 4000] + attribute iso.struct [instance] [priority 2000] namespace iso variables {ob : Type} [C : precategory ob] @@ -146,7 +146,7 @@ namespace iso @(mk f) (is_iso.mk H1 H2) variable {C} - definition to_inv [unfold 5] (f : a ≅ b) : b ⟶ a := (to_hom f)⁻¹ + definition to_inv [reducible] [unfold 5] (f : a ≅ b) : b ⟶ a := (to_hom f)⁻¹ definition to_left_inverse [unfold 5] (f : a ≅ b) : (to_hom f)⁻¹ ∘ (to_hom f) = id := left_inverse (to_hom f) definition to_right_inverse [unfold 5] (f : a ≅ b) : (to_hom f) ∘ (to_hom f)⁻¹ = id := @@ -300,72 +300,79 @@ namespace iso (r : c ⟶ d) (q : b ⟶ c) (p : a ⟶ b) (g : d ⟶ c) variable [Hq : is_iso q] include Hq - definition comp.right_inverse : q ∘ q⁻¹ = id := !right_inverse - definition comp.left_inverse : q⁻¹ ∘ q = id := !left_inverse - definition inverse_comp_cancel_left : q⁻¹ ∘ (q ∘ p) = p := + theorem comp.right_inverse : q ∘ q⁻¹ = id := !right_inverse + theorem comp.left_inverse : q⁻¹ ∘ q = id := !left_inverse + + theorem inverse_comp_cancel_left : q⁻¹ ∘ (q ∘ p) = p := by rewrite [assoc, left_inverse, id_left] - definition comp_inverse_cancel_left : q ∘ (q⁻¹ ∘ g) = g := + theorem comp_inverse_cancel_left : q ∘ (q⁻¹ ∘ g) = g := by rewrite [assoc, right_inverse, id_left] - definition comp_inverse_cancel_right : (r ∘ q) ∘ q⁻¹ = r := + theorem comp_inverse_cancel_right : (r ∘ q) ∘ q⁻¹ = r := by rewrite [-assoc, right_inverse, id_right] - definition inverse_comp_cancel_right : (f ∘ q⁻¹) ∘ q = f := + theorem inverse_comp_cancel_right : (f ∘ q⁻¹) ∘ q = f := by rewrite [-assoc, left_inverse, id_right] - definition comp_inverse [Hp : is_iso p] [Hpq : is_iso (q ∘ p)] : (q ∘ p)⁻¹ʰ = p⁻¹ʰ ∘ q⁻¹ʰ := + theorem comp_inverse [Hp : is_iso p] [Hpq : is_iso (q ∘ p)] : (q ∘ p)⁻¹ʰ = p⁻¹ʰ ∘ q⁻¹ʰ := inverse_eq_left (show (p⁻¹ʰ ∘ q⁻¹ʰ) ∘ q ∘ p = id, from by rewrite [-assoc, inverse_comp_cancel_left, left_inverse]) - definition inverse_comp_inverse_left [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q := + theorem inverse_comp_inverse_left [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q := inverse_involutive q ▸ comp_inverse q⁻¹ g - definition inverse_comp_inverse_right [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ := + theorem inverse_comp_inverse_right [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ := inverse_involutive f ▸ comp_inverse q f⁻¹ - definition inverse_comp_inverse_inverse [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q := + theorem inverse_comp_inverse_inverse [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q := inverse_involutive r ▸ inverse_comp_inverse_left q r⁻¹ end section variables {ob : Type} {C : precategory ob} include C variables {d c b a : ob} - {i : b ⟶ c} {f : b ⟶ a} + {r' : c ⟶ d} {i : b ⟶ c} {f : b ⟶ a} {r : c ⟶ d} {q : b ⟶ c} {p : a ⟶ b} - {g : d ⟶ c} {h : c ⟶ b} + {g : d ⟶ c} {h : c ⟶ b} {p' : a ⟶ b} {x : b ⟶ d} {z : a ⟶ c} {y : d ⟶ b} {w : c ⟶ a} variable [Hq : is_iso q] include Hq - definition comp_eq_of_eq_inverse_comp (H : y = q⁻¹ ∘ g) : q ∘ y = g := + theorem comp_eq_of_eq_inverse_comp (H : y = q⁻¹ ∘ g) : q ∘ y = g := H⁻¹ ▸ comp_inverse_cancel_left q g - definition comp_eq_of_eq_comp_inverse (H : w = f ∘ q⁻¹) : w ∘ q = f := + theorem comp_eq_of_eq_comp_inverse (H : w = f ∘ q⁻¹) : w ∘ q = f := H⁻¹ ▸ inverse_comp_cancel_right f q - definition eq_comp_of_inverse_comp_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y := + theorem eq_comp_of_inverse_comp_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y := (comp_eq_of_eq_inverse_comp H⁻¹)⁻¹ - definition eq_comp_of_comp_inverse_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q := + theorem eq_comp_of_comp_inverse_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q := (comp_eq_of_eq_comp_inverse H⁻¹)⁻¹ variable {Hq} - definition inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p := + theorem inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p := H⁻¹ ▸ inverse_comp_cancel_left q p - definition comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r := + theorem comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r := H⁻¹ ▸ comp_inverse_cancel_right r q - definition eq_inverse_comp_of_comp_eq (H : q ∘ p = z) : p = q⁻¹ ∘ z := + theorem eq_inverse_comp_of_comp_eq (H : q ∘ p = z) : p = q⁻¹ ∘ z := (inverse_comp_eq_of_eq_comp H⁻¹)⁻¹ - definition eq_comp_inverse_of_comp_eq (H : r ∘ q = x) : r = x ∘ q⁻¹ := + theorem eq_comp_inverse_of_comp_eq (H : r ∘ q = x) : r = x ∘ q⁻¹ := (comp_inverse_eq_of_eq_comp H⁻¹)⁻¹ - definition eq_inverse_of_comp_eq_id' (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_left H)⁻¹ - definition eq_inverse_of_comp_eq_id (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_right H)⁻¹ - definition inverse_eq_of_id_eq_comp (H : id = h ∘ q) : q⁻¹ = h := + theorem eq_inverse_of_comp_eq_id' (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_left H)⁻¹ + theorem eq_inverse_of_comp_eq_id (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_right H)⁻¹ + theorem inverse_eq_of_id_eq_comp (H : id = h ∘ q) : q⁻¹ = h := (eq_inverse_of_comp_eq_id' H⁻¹)⁻¹ - definition inverse_eq_of_id_eq_comp' (H : id = q ∘ h) : q⁻¹ = h := + theorem inverse_eq_of_id_eq_comp' (H : id = q ∘ h) : q⁻¹ = h := (eq_inverse_of_comp_eq_id H⁻¹)⁻¹ variable [Hq] - definition eq_of_comp_inverse_eq_id (H : i ∘ q⁻¹ = id) : i = q := + theorem eq_of_comp_inverse_eq_id (H : i ∘ q⁻¹ = id) : i = q := eq_inverse_of_comp_eq_id' H ⬝ inverse_involutive q - definition eq_of_inverse_comp_eq_id (H : q⁻¹ ∘ i = id) : i = q := + theorem eq_of_inverse_comp_eq_id (H : q⁻¹ ∘ i = id) : i = q := eq_inverse_of_comp_eq_id H ⬝ inverse_involutive q - definition eq_of_id_eq_comp_inverse (H : id = i ∘ q⁻¹) : q = i := (eq_of_comp_inverse_eq_id H⁻¹)⁻¹ - definition eq_of_id_eq_inverse_comp (H : id = q⁻¹ ∘ i) : q = i := (eq_of_inverse_comp_eq_id H⁻¹)⁻¹ + theorem eq_of_id_eq_comp_inverse (H : id = i ∘ q⁻¹) : q = i := (eq_of_comp_inverse_eq_id H⁻¹)⁻¹ + theorem eq_of_id_eq_inverse_comp (H : id = q⁻¹ ∘ i) : q = i := (eq_of_inverse_comp_eq_id H⁻¹)⁻¹ + + variables (q) + theorem comp.cancel_left (H : q ∘ p = q ∘ p') : p = p' := + by rewrite [-inverse_comp_cancel_left q, H, inverse_comp_cancel_left q] + theorem comp.cancel_right (H : r ∘ q = r' ∘ q) : r = r' := + by rewrite [-comp_inverse_cancel_right _ q, H, comp_inverse_cancel_right _ q] end end iso diff --git a/hott/algebra/category/limits.hlean b/hott/algebra/category/limits.hlean index c17256a8b..61e6f2eca 100644 --- a/hott/algebra/category/limits.hlean +++ b/hott/algebra/category/limits.hlean @@ -180,7 +180,8 @@ namespace category definition product_object : D := limit_object (c2_functor D d d') - infixr × := product_object + infixr `×l`:30 := product_object + local infixr × := product_object definition pr1 : d × d' ⟶ d := limit_morphism (c2_functor D d d') ff @@ -340,4 +341,8 @@ namespace category end pullbacks + namespace ops + infixr × := product_object + end ops + end category diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean index 3130cb261..26358cf3d 100644 --- a/hott/algebra/category/nat_trans.hlean +++ b/hott/algebra/category/nat_trans.hlean @@ -177,7 +177,7 @@ namespace nat_trans nat_trans.mk (λc, hom_of_eq (ap010 to_fun_ob p c)) (λa b f, eq.rec_on p (!id_right ⬝ !id_left⁻¹)) - definition compose_rev (θ : F ⟹ G) (η : G ⟹ H) : F ⟹ H := η ∘n θ + definition compose_rev [unfold-full] (θ : F ⟹ G) (η : G ⟹ H) : F ⟹ H := η ∘n θ end nat_trans diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index bf2f6825d..743c2cd2b 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -167,7 +167,7 @@ namespace circle from λA a p, calc p = ap (circle.elim a p) loop : elim_loop ... = ap (circle.elim a p) (refl base) : by rewrite H, - absurd H2 eq_bnot_ne_idp + eq_bnot_ne_idp H2 definition nonidp (x : circle) : x = x := begin diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index d21d80781..7a017857d 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -40,6 +40,7 @@ namespace sphere_index postfix `.+2`:(max+1) := λ(n : sphere_index), (n .+1 .+1) notation `-1` := minus_one export [coercions] nat + notation `ℕ₋₁` := sphere_index definition add (n m : sphere_index) : sphere_index := sphere_index.rec_on m n (λ k l, l .+1) diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index ae23aa3ed..4baeb3a97 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -31,6 +31,7 @@ namespace is_trunc notation `-2` := trunc_index.minus_two notation `-1` := -2.+1 -- ISSUE: -1 gets printed as -2.+1 export [coercions] nat + notation `ℕ₋₂` := trunc_index namespace trunc_index definition add (n m : trunc_index) : trunc_index := diff --git a/hott/init/types.hlean b/hott/init/types.hlean index 7dd46caaf..33c520e51 100644 --- a/hott/init/types.hlean +++ b/hott/init/types.hlean @@ -51,6 +51,7 @@ end sigma namespace sum infixr ⊎ := sum infixr + := sum + infixr [parsing-only] `+t`:25 := sum -- notation which is never overloaded namespace low_precedence_plus reserve infixr ` + `:25 -- conflicts with notation for addition infixr ` + ` := sum @@ -83,6 +84,7 @@ namespace prod -- notation for n-ary tuples notation `(` h `, ` t:(foldl `,` (e r, prod.mk r e) h) `)` := t infixr × := prod + infixr [parsing-only] `×t`:30 := prod -- notation which is never overloaded namespace ops infixr [parsing_only] * := prod