From f2d07ca23c00b8750d7930dac9555baa588128d9 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 23 Oct 2015 01:12:34 -0400 Subject: [PATCH] feat(category): various small changes in category theory --- hott/algebra/category/colimits.hlean | 51 ++++++---- .../category/constructions/comma.hlean | 16 ++-- .../algebra/category/constructions/cone.hlean | 4 - .../category/constructions/constructions.md | 2 +- .../category/constructions/discrete.hlean | 23 ++++- .../category/constructions/finite_cats.hlean | 2 +- .../category/constructions/functor.hlean | 38 +++++--- .../category/constructions/functor2.hlean | 19 ++-- .../algebra/category/constructions/hset.hlean | 27 +----- .../category/constructions/initial.hlean | 2 +- .../category/constructions/opposite.hlean | 72 +++++++++++--- .../category/constructions/product.hlean | 1 - .../category/constructions/terminal.hlean | 4 +- hott/algebra/category/functor/adjoint.hlean | 12 ++- hott/algebra/category/functor/adjoint2.hlean | 83 ++++++++++++++++ .../algebra/category/functor/attributes.hlean | 2 +- .../functor/{functor.hlean => basic.hlean} | 7 +- hott/algebra/category/functor/default.hlean | 2 +- .../category/functor/equivalence.hlean | 2 +- .../category/functor/exponential_laws.hlean | 94 +++++++++++++++++-- hott/algebra/category/functor/functor.md | 3 +- hott/algebra/category/iso.hlean | 10 +- hott/algebra/category/limits.hlean | 34 +++++-- hott/algebra/category/nat_trans.hlean | 6 +- hott/algebra/category/precategory.hlean | 6 ++ hott/algebra/category/strict.hlean | 2 +- hott/algebra/category/yoneda.hlean | 36 +++---- hott/book.md | 26 ++--- hott/cubical/square.hlean | 14 +-- hott/cubical/squareover.hlean | 18 ++-- hott/init/pathover.hlean | 6 +- hott/types/sigma.hlean | 8 +- src/emacs/lean-input.el | 1 + 33 files changed, 449 insertions(+), 184 deletions(-) create mode 100644 hott/algebra/category/functor/adjoint2.hlean rename hott/algebra/category/functor/{functor.hlean => basic.hlean} (99%) diff --git a/hott/algebra/category/colimits.hlean b/hott/algebra/category/colimits.hlean index 8a96b3ab2..9c78526c0 100644 --- a/hott/algebra/category/colimits.hlean +++ b/hott/algebra/category/colimits.hlean @@ -19,10 +19,12 @@ namespace category definition is_initial [reducible] (c : ob) := @is_terminal _ (opposite C) c - definition is_contr_of_is_initial [instance] (c d : ob) [H : is_initial d] + definition is_contr_of_is_initial (c d : ob) [H : is_initial d] : is_contr (d ⟶ c) := H c + local attribute is_contr_of_is_initial [instance] + definition initial_morphism (c c' : ob) [H : is_initial c'] : c' ⟶ c := !center @@ -85,67 +87,67 @@ namespace category variables {D I} (F : I ⇒ D) [H : has_colimits_of_shape D I] {i j : I} include H - abbreviation cocone := (cone Fᵒᵖ)ᵒᵖ + abbreviation cocone := (cone Fᵒᵖᶠ)ᵒᵖ definition has_initial_object_cocone [H : has_colimits_of_shape D I] (F : I ⇒ D) : has_initial_object (cocone F) := begin unfold [has_colimits_of_shape,has_limits_of_shape] at H, - exact H Fᵒᵖ + exact H Fᵒᵖᶠ end local attribute has_initial_object_cocone [instance] - definition colimit_cocone : cocone F := limit_cone Fᵒᵖ + definition colimit_cocone : cocone F := limit_cone Fᵒᵖᶠ definition is_initial_colimit_cocone [instance] : is_initial (colimit_cocone F) := - is_terminal_limit_cone Fᵒᵖ + is_terminal_limit_cone Fᵒᵖᶠ definition colimit_object : D := - limit_object Fᵒᵖ + limit_object Fᵒᵖᶠ - definition colimit_nat_trans : constant_functor Iᵒᵖ (colimit_object F) ⟹ Fᵒᵖ := - limit_nat_trans Fᵒᵖ + definition colimit_nat_trans : constant_functor Iᵒᵖ (colimit_object F) ⟹ Fᵒᵖᶠ := + limit_nat_trans Fᵒᵖᶠ definition colimit_morphism (i : I) : F i ⟶ colimit_object F := - limit_morphism Fᵒᵖ i + limit_morphism Fᵒᵖᶠ i variable {H} theorem colimit_commute {i j : I} (f : i ⟶ j) : colimit_morphism F j ∘ to_fun_hom F f = colimit_morphism F i := - by rexact limit_commute Fᵒᵖ f + by rexact limit_commute Fᵒᵖᶠ f variable [H] definition colimit_cone_obj [constructor] {d : D} {η : Πi, F i ⟶ d} - (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) : cone_obj Fᵒᵖ := - limit_cone_obj Fᵒᵖ proof p qed + (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) : cone_obj Fᵒᵖᶠ := + limit_cone_obj Fᵒᵖᶠ proof p qed variable {H} definition colimit_hom {d : D} (η : Πi, F i ⟶ d) (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) : colimit_object F ⟶ d := - hom_limit Fᵒᵖ η proof p qed + hom_limit Fᵒᵖᶠ η proof p qed theorem colimit_hom_commute {d : D} (η : Πi, F i ⟶ d) (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) (i : I) : colimit_hom F η p ∘ colimit_morphism F i = η i := - by rexact hom_limit_commute Fᵒᵖ η proof p qed i + by rexact hom_limit_commute Fᵒᵖᶠ η proof p qed i definition colimit_cone_hom [constructor] {d : D} {η : Πi, F i ⟶ d} (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) {h : colimit_object F ⟶ d} (q : Πi, h ∘ colimit_morphism F i = η i) : cone_hom (colimit_cone_obj F p) (colimit_cocone F) := - by rexact limit_cone_hom Fᵒᵖ proof p qed proof q qed + by rexact limit_cone_hom Fᵒᵖᶠ proof p qed proof q qed variable {F} theorem eq_colimit_hom {d : D} {η : Πi, F i ⟶ d} (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) {h : colimit_object F ⟶ d} (q : Πi, h ∘ colimit_morphism F i = η i) : h = colimit_hom F η p := - by rexact @eq_hom_limit _ _ Fᵒᵖ _ _ _ proof p qed _ proof q qed + by rexact @eq_hom_limit _ _ Fᵒᵖᶠ _ _ _ proof p qed _ proof q qed theorem colimit_cocone_unique {d : D} {η : Πi, F i ⟶ d} (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) {h₁ : colimit_object F ⟶ d} (q₁ : Πi, h₁ ∘ colimit_morphism F i = η i) {h₂ : colimit_object F ⟶ d} (q₂ : Πi, h₂ ∘ colimit_morphism F i = η i) : h₁ = h₂ := - @limit_cone_unique _ _ Fᵒᵖ _ _ _ proof p qed _ proof q₁ qed _ proof q₂ qed + @limit_cone_unique _ _ Fᵒᵖᶠ _ _ _ proof p qed _ proof q₁ qed _ proof q₂ qed definition colimit_hom_colimit [reducible] {F G : I ⇒ D} (η : F ⟹ G) : colimit_object F ⟶ colimit_object G := @@ -157,7 +159,19 @@ namespace category variable (F) definition colimit_object_iso_colimit_object [constructor] (H₁ H₂ : has_colimits_of_shape D I) : @(colimit_object F) H₁ ≅ @(colimit_object F) H₂ := - iso_of_opposite_iso (limit_object_iso_limit_object Fᵒᵖ H₁ H₂) + iso_of_opposite_iso (limit_object_iso_limit_object Fᵒᵖᶠ H₁ H₂) + + definition colimit_functor [constructor] (D I : Precategory) [H : has_colimits_of_shape D I] + : D ^c I ⇒ D := + begin + fapply functor.mk: esimp, + { intro F, exact colimit_object F}, + { apply @colimit_hom_colimit}, + { intro F, unfold colimit_hom_colimit, refine (eq_colimit_hom _ _)⁻¹, intro i, + apply id_comp_eq_comp_id}, + { intro F G H η θ, unfold colimit_hom_colimit, refine (eq_colimit_hom _ _)⁻¹, intro i, + rewrite [-assoc, colimit_hom_commute, assoc, colimit_hom_commute, -assoc]} + end section bin_coproducts open bool prod.ops @@ -198,6 +212,7 @@ namespace category eq_coproduct_hom p₁ q₁ ⬝ (eq_coproduct_hom p₂ q₂)⁻¹ variable (D) + -- TODO: define this in terms of colimit_functor and functor_two_left (in exponential_laws) definition coproduct_functor [constructor] : D ×c D ⇒ D := functor.mk (λx, coproduct_object x.1 x.2) diff --git a/hott/algebra/category/constructions/comma.hlean b/hott/algebra/category/constructions/comma.hlean index 94cd05090..f6477420a 100644 --- a/hott/algebra/category/constructions/comma.hlean +++ b/hott/algebra/category/constructions/comma.hlean @@ -7,7 +7,7 @@ Authors: Floris van Doorn Comma category -/ -import ..functor.functor ..strict ..category +import ..functor.basic ..strict ..category open eq functor equiv sigma sigma.ops is_trunc iso is_equiv @@ -46,21 +46,17 @@ namespace category end --TODO: remove. This is a different version where Hq is not in square brackets - axiom eq_comp_inverse_of_comp_eq' {ob : Type} {C : precategory ob} {d c b : ob} {r : hom c d} - {q : hom b c} {x : hom b d} {Hq : is_iso q} (p : r ∘ q = x) : r = x ∘ q⁻¹ʰ + -- definition eq_comp_inverse_of_comp_eq' {ob : Type} {C : precategory ob} {d c b : ob} {r : hom c d} + -- {q : hom b c} {x : hom b d} {Hq : is_iso q} (p : r ∘ q = x) : r = x ∘ q⁻¹ʰ := + -- sorry -- := sorry --eq_inverse_comp_of_comp_eq p definition comma_object_eq {x y : comma_object S T} (p : ob1 x = ob1 y) (q : ob2 x = ob2 y) (r : T (hom_of_eq q) ∘ mor x ∘ S (inv_of_eq p) = mor y) : x = y := begin cases x with a b f, cases y with a' b' f', cases p, cases q, - have r' : f = f', - begin - rewrite [▸* at r, -r, respect_id, id_left, respect_inv'], - apply eq_comp_inverse_of_comp_eq', - rewrite [respect_id,id_right] - end, - rewrite r' + apply ap (comma_object.mk a' b'), + rewrite [▸* at r, -r, +respect_id, id_leftright] end definition ap_ob1_comma_object_eq' (x y : comma_object S T) (p : ob1 x = ob1 y) (q : ob2 x = ob2 y) diff --git a/hott/algebra/category/constructions/cone.hlean b/hott/algebra/category/constructions/cone.hlean index 5cb0c872f..076132aeb 100644 --- a/hott/algebra/category/constructions/cone.hlean +++ b/hott/algebra/category/constructions/cone.hlean @@ -33,10 +33,6 @@ namespace category cone_hom.mk (cone_hom.f g ∘ cone_hom.f f) abstract λi, by rewrite [assoc, +cone_hom.p] end - definition is_hprop_hom_eq [instance] [priority 1001] {ob : Type} [C : precategory ob] {x y : ob} (f g : x ⟶ y) - : is_hprop (f = g) := - _ - definition cone_obj_eq (p : cone_obj.c x = cone_obj.c y) (q : Πi, cone_obj.η x i = cone_obj.η y i ∘ hom_of_eq p) : x = y := begin diff --git a/hott/algebra/category/constructions/constructions.md b/hott/algebra/category/constructions/constructions.md index 6e741c5e3..77df95b45 100644 --- a/hott/algebra/category/constructions/constructions.md +++ b/hott/algebra/category/constructions/constructions.md @@ -5,7 +5,7 @@ Common categories and constructions on categories. The following files are in th * [functor](functor.hlean) : Functor category * [opposite](opposite.hlean) : Opposite category -* [hset](hset.hlean) : Category of sets. Prove that it is complete and cocomplete +* [hset](hset.hlean) : Category of sets. Includes proof that it is complete and cocomplete * [sum](sum.hlean) : Sum category * [product](product.hlean) : Product category * [comma](comma.hlean) : Comma category diff --git a/hott/algebra/category/constructions/discrete.hlean b/hott/algebra/category/constructions/discrete.hlean index 6c4d8f790..553f1fce0 100644 --- a/hott/algebra/category/constructions/discrete.hlean +++ b/hott/algebra/category/constructions/discrete.hlean @@ -7,9 +7,9 @@ Authors: Floris van Doorn Discrete category -/ -import ..groupoid types.bool ..functor.functor +import ..groupoid types.bool ..nat_trans -open eq is_trunc iso bool functor +open eq is_trunc iso bool functor nat_trans namespace category @@ -44,7 +44,6 @@ namespace category groupoid.Mk _ (discrete_groupoid A) definition c2 [constructor] : Precategory := Discrete_precategory bool - definition c1 [constructor] : Precategory := Discrete_precategory unit definition c2_functor [constructor] (C : Precategory) (x y : C) : c2 ⇒ C := functor.mk (bool.rec x y) @@ -54,4 +53,22 @@ namespace category abstract begin intro b₁ b₂ b₃ g f, induction b₁: induction b₂: induction b₃: esimp at *: try contradiction: exact !id_id⁻¹ end end + definition c2_functor_eta {C : Precategory} (F : c2 ⇒ C) : + c2_functor C (to_fun_ob F ff) (to_fun_ob F tt) = F := + begin + fapply functor_eq: esimp, + { intro b, induction b: reflexivity}, + { intro b₁ b₂ p, induction p, induction b₁: esimp; rewrite [id_leftright]; exact !respect_id⁻¹} + end + + definition c2_nat_trans [constructor] {C : Precategory} {x y u v : C} (f : x ⟶ u) (g : y ⟶ v) : + c2_functor C x y ⟹ c2_functor C u v := + begin + fapply nat_trans.mk: esimp, + { intro b, induction b, exact f, exact g}, + { intro b₁ b₂ p, induction p, induction b₁: esimp: apply id_comp_eq_comp_id}, + end + + + end category diff --git a/hott/algebra/category/constructions/finite_cats.hlean b/hott/algebra/category/constructions/finite_cats.hlean index 99b1f1c24..78a2d339b 100644 --- a/hott/algebra/category/constructions/finite_cats.hlean +++ b/hott/algebra/category/constructions/finite_cats.hlean @@ -7,7 +7,7 @@ Authors: Floris van Doorn Some finite categories which are neither discrete nor indiscrete -/ -import ..functor.functor types.sum +import ..functor.basic types.sum open bool unit is_trunc sum eq functor equiv diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 5b1e91af7..f1d137ba3 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -58,16 +58,16 @@ namespace functor apply is_hset.elim end - definition is_iso_nat_trans [constructor] [instance] : is_iso η := + definition is_natural_iso [constructor] : 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 + definition natural_iso.mk [constructor] : F ≅ G := + iso.mk _ (is_natural_iso η) omit iso - variables (F G) + 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 := @@ -78,8 +78,13 @@ namespace functor {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 + variables {F G} + definition natural_iso.MK [constructor] + (η : Πc, F c ⟶ G c) (p : Π(c c' : C) (f : c ⟶ c'), G f ∘ η c = η c' ∘ F f) + (θ : Πc, G c ⟶ F c) (r : Πc, θ c ∘ η c = id) (q : Πc, η c ∘ θ c = id) : F ≅ G := + iso.mk (nat_trans.mk η p) (@(is_natural_iso _) (λc, is_iso.mk (θ c) (r c) (q c))) + end section /- and conversely, if a natural transformation is an iso, it is componentwise an iso -/ @@ -109,8 +114,8 @@ namespace functor omit isoη definition componentwise_iso (η : F ≅ G) (c : C) : F c ≅ G c := - @iso.mk _ _ _ _ (natural_map (to_hom η) c) - (@componentwise_is_iso _ _ _ _ (to_hom η) (struct η) c) + iso.mk (natural_map (to_hom η) c) + (@componentwise_is_iso _ _ _ _ (to_hom η) (struct η) c) definition componentwise_iso_id (c : C) : componentwise_iso (iso.refl F) c = iso.refl (F c) := iso_eq (idpath (ID (F c))) @@ -207,10 +212,10 @@ namespace functor abstract !n_nf_distrib⁻¹ ⬝ ap (λx, x ∘nf F) (@right_inverse (D ⇒ E) _ _ _ η _) ⬝ !id_nf end definition functor_iso_compose [constructor] (G : D ⇒ E) (η : F ≅ F') : G ∘f F ≅ G ∘f F' := - @(iso.mk _) (is_iso_nf_compose G (to_hom η)) + iso.mk _ (is_iso_nf_compose G (to_hom η)) definition iso_functor_compose [constructor] (η : G ≅ G') (F : C ⇒ D) : G ∘f F ≅ G' ∘f F := - @(iso.mk _) (is_iso_fn_compose (to_hom η) F) + iso.mk _ (is_iso_fn_compose (to_hom η) F) infixr ` ∘fi ` :62 := functor_iso_compose infixr ` ∘if ` :62 := iso_functor_compose @@ -311,10 +316,10 @@ 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) + eq_of_iso (natural_iso.mk η 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_pointwise_iso η iso) = natural_iso.mk η iso := !iso_of_eq_eq_of_iso definition hom_of_eq_eq_of_pointwise_iso (η : F ⟹ G) (iso : Π(c : C), is_iso (η c)) @@ -350,8 +355,6 @@ namespace functor abstract begin intros, apply nat_trans_eq, intro i, esimp, apply respect_id end end abstract begin intros, apply nat_trans_eq, intro i, esimp, apply respect_comp end end - /- evaluation functor -/ - definition eval_functor [constructor] (C D : Precategory) (d : D) : C ^c D ⇒ C := begin fapply functor.mk: esimp, @@ -381,6 +384,15 @@ namespace functor { intro G H I η θ, apply fn_n_distrib}, end + definition constant_diagram [constructor] (C D) : C ⇒ C ^c D := + begin + fapply functor.mk: esimp, + { intro c, exact constant_functor D c}, + { intro c d f, exact constant_nat_trans D f}, + { intro c, fapply nat_trans_eq, reflexivity}, + { intro c d e g f, fapply nat_trans_eq, reflexivity}, + end + end functor diff --git a/hott/algebra/category/constructions/functor2.hlean b/hott/algebra/category/constructions/functor2.hlean index 64e0314b3..7d6b41639 100644 --- a/hott/algebra/category/constructions/functor2.hlean +++ b/hott/algebra/category/constructions/functor2.hlean @@ -15,7 +15,7 @@ namespace category -- preservation of limits variables {D C I : Precategory} - definition limit_functor [constructor] + definition functor_limit_object [constructor] [H : has_limits_of_shape D I] (F : I ⇒ D ^c C) : C ⇒ D := begin assert lem : Π(c d : carrier C) (f : hom c d) ⦃i j : carrier I⦄ (k : i ⟶ j), @@ -34,11 +34,11 @@ namespace category rewrite [respect_comp,assoc,hom_limit_commute,-assoc,hom_limit_commute,assoc]} end - definition limit_functor_cone [constructor] + definition functor_limit_cone [constructor] [H : has_limits_of_shape D I] (F : I ⇒ D ^c C) : cone_obj F := begin fapply cone_obj.mk, - { exact limit_functor F}, + { exact functor_limit_object F}, { fapply nat_trans.mk, { intro i, esimp, fapply nat_trans.mk, { intro c, esimp, apply limit_morphism}, @@ -52,7 +52,7 @@ namespace category : has_limits_of_shape (D ^c C) I := begin intro F, fapply has_terminal_object.mk, - { exact limit_functor_cone F}, + { exact functor_limit_cone F}, { intro c, esimp at *, induction c with G η, induction η with η p, esimp at *, fapply is_contr.mk, { fapply cone_hom.mk, @@ -87,7 +87,7 @@ namespace category -- abstract (λi j k g f, ap010 natural_map !respect_comp c) end -- qed - definition colimit_functor [constructor] + definition functor_colimit_object [constructor] [H : has_colimits_of_shape D I] (F : Iᵒᵖ ⇒ (D ^c C)ᵒᵖ) : C ⇒ D := begin fapply functor.mk, @@ -99,11 +99,11 @@ namespace category rewrite [▸*,respect_comp,-assoc,colimit_hom_commute,assoc,colimit_hom_commute,-assoc]} end - definition colimit_functor_cone [constructor] + definition functor_colimit_cone [constructor] [H : has_colimits_of_shape D I] (F : Iᵒᵖ ⇒ (D ^c C)ᵒᵖ) : cone_obj F := begin fapply cone_obj.mk, - { exact colimit_functor F}, + { exact functor_colimit_object F}, { fapply nat_trans.mk, { intro i, esimp, fapply nat_trans.mk, { intro c, esimp, apply colimit_morphism}, @@ -117,7 +117,7 @@ namespace category : has_colimits_of_shape (D ^c C) I := begin intro F, fapply has_terminal_object.mk, - { exact colimit_functor_cone F}, + { exact functor_colimit_cone F}, { intro c, esimp at *, induction c with G η, induction η with η p, esimp at *, fapply is_contr.mk, { fapply cone_hom.mk, @@ -141,7 +141,8 @@ namespace category local attribute has_limits_of_shape_op_op [instance] [priority 1] universe variables u v - definition is_cocomplete_functor [instance] [H : is_cocomplete.{_ _ u v} D] : is_cocomplete.{_ _ u v} (D ^c C) := + definition is_cocomplete_functor [instance] [H : is_cocomplete.{_ _ u v} D] + : is_cocomplete.{_ _ u v} (D ^c C) := λI, _ end category diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean index e61a25f5f..49977f2b2 100644 --- a/hott/algebra/category/constructions/hset.hlean +++ b/hott/algebra/category/constructions/hset.hlean @@ -167,32 +167,7 @@ namespace category exact exists.intro f idp}} end --- giving the following step explicitly slightly reduces the elaboration time of the next proof - --- definition is_cocomplete_set_cone_hom.{u v w} [constructor] --- (I : Precategory.{v w}) (F : I ⇒ Opposite set.{max u v w}) --- (X : hset.{max u v w}) --- (η : Π (i : carrier I), trunctype.carrier (to_fun_ob F i) → trunctype.carrier X) --- (p : Π {i j : carrier I} (f : hom i j), (λ (x : trunctype.carrier (to_fun_ob F j)), η i (to_fun_hom F f x)) = η j) - --- : --cone_hom (cone_obj.mk X (nat_trans.mk η @p)) (is_cocomplete_set_cone.{u v w} I F) --- @cone_hom I setᵒᵖ F --- (@cone_obj.mk I setᵒᵖ F X --- (@nat_trans.mk I (Opposite set) (@constant_functor I (Opposite set) X) F η @p)) --- (is_cocomplete_set_cone.{u v w} I F) --- := --- begin --- fapply cone_hom.mk, --- { refine set_quotient.elim _ _, --- { intro v, induction v with i x, exact η i x}, --- { intro v w r, induction v with i x, induction w with j y, esimp at *, --- refine trunc.elim_on r _, clear r, --- intro u, induction u with f q, --- exact ap (η i) q⁻¹ ⬝ ap10 (p f) y}}, --- { intro i, reflexivity} --- end - - -- TODO: rewrite after induction tactic for trunc/set_quotient is implemented + -- TODO: change this after induction tactic for trunc/set_quotient is implemented definition is_cocomplete_set.{u v w} [instance] : is_cocomplete.{(max u v w)+1 (max u v w) v w} set := begin diff --git a/hott/algebra/category/constructions/initial.hlean b/hott/algebra/category/constructions/initial.hlean index 1410eb454..0cf3dfcb0 100644 --- a/hott/algebra/category/constructions/initial.hlean +++ b/hott/algebra/category/constructions/initial.hlean @@ -37,7 +37,7 @@ namespace category end definition initial_functor_op (C : Precategory) - : (initial_functor C)ᵒᵖ = initial_functor Cᵒᵖ := + : (initial_functor C)ᵒᵖᶠ = initial_functor Cᵒᵖ := by apply @is_hprop.elim (0 ⇒ Cᵒᵖ) definition initial_functor_comp {C D : Precategory} (F : C ⇒ D) diff --git a/hott/algebra/category/constructions/opposite.hlean b/hott/algebra/category/constructions/opposite.hlean index 7ab41f37d..ef625a6ce 100644 --- a/hott/algebra/category/constructions/opposite.hlean +++ b/hott/algebra/category/constructions/opposite.hlean @@ -6,9 +6,9 @@ Authors: Floris van Doorn, Jakob von Raumer Opposite precategory and (TODO) category -/ -import ..functor.functor ..category +import ..nat_trans ..category -open eq functor iso equiv is_equiv +open eq functor iso equiv is_equiv nat_trans namespace category @@ -29,7 +29,7 @@ namespace category infixr `∘op`:60 := @comp _ (opposite _) _ _ _ postfix `ᵒᵖ`:(max+2) := Opposite - variables {C : Precategory} {a b c : C} + variables {C D : Precategory} {a b c : C} definition compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := by reflexivity @@ -40,23 +40,71 @@ namespace category definition opposite_opposite : (Cᵒᵖ)ᵒᵖ = C := (ap (Precategory.mk C) (opposite_opposite' C)) ⬝ !Precategory.eta - definition opposite_functor [constructor] {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ := + theorem opposite_hom_of_eq {ob : Type} [C : precategory ob] {c c' : ob} (p : c = c') + : @hom_of_eq ob (opposite C) c c' p = inv_of_eq p := + by induction p; reflexivity + + theorem opposite_inv_of_eq {ob : Type} [C : precategory ob] {c c' : ob} (p : c = c') + : @inv_of_eq ob (opposite C) c c' p = hom_of_eq p := + by induction p; reflexivity + + definition opposite_functor [constructor] (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ := begin - apply functor.mk, - intros, apply respect_id F, - intros, apply @respect_comp C D + apply functor.mk, + intros, apply respect_id F, + intros, apply @respect_comp C D end - definition opposite_functor_rev [constructor] {C D : Precategory} (F : Cᵒᵖ ⇒ Dᵒᵖ) : C ⇒ D := + definition opposite_functor_rev [constructor] (F : Cᵒᵖ ⇒ Dᵒᵖ) : C ⇒ D := begin - apply functor.mk, - intros, apply respect_id F, - intros, apply @respect_comp Cᵒᵖ Dᵒᵖ + apply functor.mk, + intros, apply respect_id F, + intros, apply @respect_comp Cᵒᵖ Dᵒᵖ end - postfix `ᵒᵖ`:(max+2) := opposite_functor + postfix `ᵒᵖᶠ`:(max+2) := opposite_functor postfix `ᵒᵖ'`:(max+2) := opposite_functor_rev + definition opposite_rev_opposite_functor (F : Cᵒᵖ ⇒ Dᵒᵖ) : Fᵒᵖ' ᵒᵖᶠ = F := + begin + fapply functor_eq: esimp, + { intro c c' f, esimp, exact !id_right ⬝ !id_left} + end + + definition opposite_opposite_rev_functor (F : C ⇒ D) : Fᵒᵖᶠᵒᵖ' = F := + begin + fapply functor_eq: esimp, + { intro c c' f, esimp, exact !id_leftright} + end + + definition opposite_nat_trans [constructor] {F G : C ⇒ D} (η : F ⟹ G) : Gᵒᵖᶠ ⟹ Fᵒᵖᶠ := + begin + fapply nat_trans.mk: esimp, + { intro c, exact η c}, + { intro c c' f, exact !naturality⁻¹}, + end + + definition opposite_rev_nat_trans [constructor] {F G : Cᵒᵖ ⇒ Dᵒᵖ} (η : F ⟹ G) : Gᵒᵖ' ⟹ Fᵒᵖ' := + begin + fapply nat_trans.mk: esimp, + { intro c, exact η c}, + { intro c c' f, exact !(@naturality Cᵒᵖ Dᵒᵖ)⁻¹}, + end + + definition opposite_nat_trans_rev [constructor] {F G : C ⇒ D} (η : Fᵒᵖᶠ ⟹ Gᵒᵖᶠ) : G ⟹ F := + begin + fapply nat_trans.mk: esimp, + { intro c, exact η c}, + { intro c c' f, exact !(@naturality Cᵒᵖ Dᵒᵖ _ _ η)⁻¹}, + end + + definition opposite_rev_nat_trans_rev [constructor] {F G : Cᵒᵖ ⇒ Dᵒᵖ} (η : Fᵒᵖ' ⟹ Gᵒᵖ') : G ⟹ F := + begin + fapply nat_trans.mk: esimp, + { intro c, exact η c}, + { intro c c' f, exact (naturality η f)⁻¹}, + end + definition opposite_iso [constructor] {ob : Type} [C : precategory ob] {a b : ob} (H : @iso _ C a b) : @iso _ (opposite C) a b := begin diff --git a/hott/algebra/category/constructions/product.hlean b/hott/algebra/category/constructions/product.hlean index 0a3cf8753..9851e60c0 100644 --- a/hott/algebra/category/constructions/product.hlean +++ b/hott/algebra/category/constructions/product.hlean @@ -138,5 +138,4 @@ namespace category apply id_leftright} end - end category diff --git a/hott/algebra/category/constructions/terminal.hlean b/hott/algebra/category/constructions/terminal.hlean index 31ec7e1b7..4449a1b82 100644 --- a/hott/algebra/category/constructions/terminal.hlean +++ b/hott/algebra/category/constructions/terminal.hlean @@ -37,7 +37,7 @@ namespace category end definition terminal_functor_op (C : Precategory) - : (terminal_functor C)ᵒᵖ = terminal_functor Cᵒᵖ := idp + : (terminal_functor C)ᵒᵖᶠ = terminal_functor Cᵒᵖ := idp definition terminal_functor_comp {C D : Precategory} (F : C ⇒ D) : (terminal_functor D) ∘f F = terminal_functor C := idp @@ -49,7 +49,7 @@ namespace category (λx y z g f, !id_id⁻¹) -- we need id_id in the declaration of precategory to make this to hold definitionally - definition point_op (C : Precategory) (c : C) : (point C c)ᵒᵖ = point Cᵒᵖ c := idp + definition point_op (C : Precategory) (c : C) : (point C c)ᵒᵖᶠ = point Cᵒᵖ c := idp definition point_comp {C D : Precategory} (F : C ⇒ D) (c : C) : F ∘f point C c = point D (F c) := idp diff --git a/hott/algebra/category/functor/adjoint.hlean b/hott/algebra/category/functor/adjoint.hlean index 51022da4f..bfc6297f9 100644 --- a/hott/algebra/category/functor/adjoint.hlean +++ b/hott/algebra/category/functor/adjoint.hlean @@ -8,16 +8,22 @@ Adjoint functors import .attributes -open category functor nat_trans eq is_trunc iso equiv prod trunc function pi is_equiv +open functor nat_trans is_trunc eq iso namespace category - -- TODO(?): define a structure "adjoint" and then define + structure adjoint [class] {C D : Precategory} (F : C ⇒ D) (G : D ⇒ C) := + (η : 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)) + + -- TODO(?): define is_left_adjoint in terms of adjoint -- structure is_left_adjoint (F : C ⇒ D) := -- (G : D ⇒ C) -- G -- (is_adjoint : adjoint F G) - -- infix `⊣`:55 := adjoint + infix ` ⊣ `:55 := adjoint structure is_left_adjoint [class] {C D : Precategory} (F : C ⇒ D) := (G : D ⇒ C) diff --git a/hott/algebra/category/functor/adjoint2.hlean b/hott/algebra/category/functor/adjoint2.hlean new file mode 100644 index 000000000..3c0ff5bf0 --- /dev/null +++ b/hott/algebra/category/functor/adjoint2.hlean @@ -0,0 +1,83 @@ +/- +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 + +TODO: move +-/ + +import .adjoint ..yoneda + +open eq functor nat_trans yoneda iso prod is_trunc + +namespace category + + section + universe variables u v + parameters {C D : Precategory.{u v}} {F : C ⇒ D} {G : D ⇒ C} + (θ : hom_functor D ∘f prod_functor_prod Fᵒᵖᶠ 1 ≅ hom_functor C ∘f prod_functor_prod 1 G) + include θ + /- θ : _ ⟹[Cᵒᵖ × D ⇒ set] _-/ + + definition adj_unit [constructor] : 1 ⟹ G ∘f F := + begin + fapply nat_trans.mk: esimp, + { intro c, exact natural_map (to_hom θ) (c, F c) id}, + { intro c c' f, + let H := naturality (to_hom θ) (ID c, F f), + let K := ap10 H id, + rewrite [▸* at K, id_right at K, ▸*, K, respect_id, +id_right], + clear H K, + let H := naturality (to_hom θ) (f, ID (F c')), + let K := ap10 H id, + rewrite [▸* at K, respect_id at K,+id_left at K, K]} + end + + definition adj_counit [constructor] : F ∘f G ⟹ 1 := + begin + fapply nat_trans.mk: esimp, + { intro d, exact natural_map (to_inv θ) (G d, d) id, }, + { intro d d' g, + let H := naturality (to_inv θ) (Gᵒᵖᶠ g, ID d'), + let K := ap10 H id, + rewrite [▸* at K, id_left at K, ▸*, K, respect_id, +id_left], + clear H K, + let H := naturality (to_inv θ) (ID (G d), g), + let K := ap10 H id, + rewrite [▸* at K, respect_id at K,+id_right at K, K]} + end + + theorem adj_eq_unit (c : C) (d : D) (f : F c ⟶ d) + : natural_map (to_hom θ) (c, d) f = G f ∘ adj_unit c := + begin + esimp, + let H := naturality (to_hom θ) (ID c, f), + let K := ap10 H id, + rewrite [▸* at K, id_right at K, K, respect_id, +id_right], + end + + theorem adj_eq_counit (c : C) (d : D) (g : c ⟶ G d) + : natural_map (to_inv θ) (c, d) g = adj_counit d ∘ F g := + begin + esimp, + let H := naturality (to_inv θ) (g, ID d), + let K := ap10 H id, + rewrite [▸* at K, id_left at K, K, respect_id, +id_left], + end + + definition adjoint.mk' [constructor] : F ⊣ G := + begin + fapply adjoint.mk, + { exact adj_unit}, + { exact adj_counit}, + { intro c, esimp, refine (adj_eq_counit c (F c) (adj_unit c))⁻¹ ⬝ _, + apply ap10 (to_left_inverse (componentwise_iso θ (c, F c)))}, + { intro d, esimp, refine (adj_eq_unit (G d) d (adj_counit d))⁻¹ ⬝ _, + apply ap10 (to_right_inverse (componentwise_iso θ (G d, d)))}, + end + + end + + + +end category diff --git a/hott/algebra/category/functor/attributes.hlean b/hott/algebra/category/functor/attributes.hlean index 14aa11142..ac3094752 100644 --- a/hott/algebra/category/functor/attributes.hlean +++ b/hott/algebra/category/functor/attributes.hlean @@ -10,7 +10,7 @@ Adjoint functors, isomorphisms and equivalences have their own file import ..constructions.functor function arity -open category functor nat_trans eq is_trunc iso equiv prod trunc function pi is_equiv +open eq functor trunc prod is_equiv iso equiv function is_trunc namespace category variables {C D E : Precategory} {F : C ⇒ D} {G : D ⇒ C} diff --git a/hott/algebra/category/functor/functor.hlean b/hott/algebra/category/functor/basic.hlean similarity index 99% rename from hott/algebra/category/functor/functor.hlean rename to hott/algebra/category/functor/basic.hlean index f1ca688f2..2231640fc 100644 --- a/hott/algebra/category/functor/functor.hlean +++ b/hott/algebra/category/functor/basic.hlean @@ -6,8 +6,7 @@ Authors: Floris van Doorn, Jakob von Raumer import ..iso types.pi -open function category eq prod prod.ops equiv is_equiv sigma sigma.ops is_trunc funext iso -open pi +open function category eq prod prod.ops equiv is_equiv sigma sigma.ops is_trunc funext iso pi structure functor (C D : Precategory) : Type := (to_fun_ob : C → D) @@ -18,7 +17,7 @@ structure functor (C D : Precategory) : Type := namespace functor - infixl ` ⇒ `:25 := functor + infixl ` ⇒ `:55 := functor variables {A B C D E : Precategory} attribute to_fun_ob [coercion] @@ -109,7 +108,7 @@ namespace functor attribute preserve_is_iso [instance] [priority 100] definition to_fun_iso [constructor] (F : C ⇒ D) {a b : C} (f : a ≅ b) : F a ≅ F b := - iso.mk (F f) + iso.mk (F f) _ theorem respect_inv' (F : C ⇒ D) {a b : C} (f : hom a b) {H : is_iso f} : F (f⁻¹) = (F f)⁻¹ := respect_inv F f diff --git a/hott/algebra/category/functor/default.hlean b/hott/algebra/category/functor/default.hlean index 26b2b4a76..8274c00c1 100644 --- a/hott/algebra/category/functor/default.hlean +++ b/hott/algebra/category/functor/default.hlean @@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ -import .functor +import .basic diff --git a/hott/algebra/category/functor/equivalence.hlean b/hott/algebra/category/functor/equivalence.hlean index 39a2d729d..bc1bde491 100644 --- a/hott/algebra/category/functor/equivalence.hlean +++ b/hott/algebra/category/functor/equivalence.hlean @@ -8,7 +8,7 @@ Functors which are equivalences or isomorphisms import .adjoint -open category functor nat_trans eq is_trunc iso equiv prod trunc function pi is_equiv +open eq functor iso prod nat_trans is_equiv equiv is_trunc namespace category variables {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C} diff --git a/hott/algebra/category/functor/exponential_laws.hlean b/hott/algebra/category/functor/exponential_laws.hlean index 7c325ab8f..5023cca12 100644 --- a/hott/algebra/category/functor/exponential_laws.hlean +++ b/hott/algebra/category/functor/exponential_laws.hlean @@ -6,11 +6,11 @@ Authors: Floris van Doorn, Jakob von Raumer Exponential laws -/ -import .functor.equivalence .functor.curry - .constructions.terminal .constructions.initial .constructions.product .constructions.sum - -open eq category functor is_trunc nat_trans iso unit prod sum prod.ops +import .equivalence .curry + ..constructions.terminal ..constructions.initial ..constructions.product ..constructions.sum + ..constructions.discrete +open eq category functor is_trunc nat_trans iso unit prod sum prod.ops bool namespace category @@ -53,7 +53,6 @@ namespace category { apply empty.elim}}, end - /- C ^ 1 ≅ C -/ definition functor_one_iso [constructor] (C : Precategory) : C ^c 1 ≅c C := @@ -89,6 +88,87 @@ namespace category { intro u v f, apply unit.eta}}, end + /- C ^ 2 ≅ C × C -/ + + definition functor_two_right [constructor] (C : Precategory) + : C ^c c2 ⇒ C ×c C := + begin + fapply functor.mk: esimp, + { intro F, exact (F ff, F tt)}, + { intro F G η, esimp, exact (η ff, η tt)}, + { intro F, reflexivity}, + { intro F G H η θ, reflexivity} + end + + definition functor_two_left [constructor] (C : Precategory) + : C ×c C ⇒ C ^c c2 := + begin + fapply functor.mk: esimp, + { intro v, exact c2_functor C v.1 v.2}, + { intro v w f, exact c2_nat_trans f.1 f.2}, + { intro v, apply nat_trans_eq, esimp, intro b, induction b: reflexivity}, + { intro u v w g f, apply nat_trans_eq, esimp, intro b, induction b: reflexivity} + end + + definition functor_two_iso [constructor] (C : Precategory) + : C ^c c2 ≅c C ×c C := + begin + fapply isomorphism.MK: esimp, + { apply functor_two_right}, + { apply functor_two_left}, + { fapply functor_eq: esimp, + { intro F, apply c2_functor_eta}, + { intro F G η, fapply nat_trans_eq, intro b, esimp, + rewrite [@natural_map_hom_of_eq _ _ _ G, @natural_map_inv_of_eq _ _ _ F, + ↑c2_functor_eta, +@ap010_functor_eq c2 C, ▸*], + induction b: esimp; apply id_leftright}}, + { fapply functor_eq: esimp, + { intro v, apply prod.eta}, + { intro v w f, induction v, induction w, esimp, apply prod_eq: apply id_leftright}}, + end + + /- Cᵒᵖ ^ Dᵒᵖ ≅ (C ^ D)ᵒᵖ -/ + + definition opposite_functor_opposite_right [constructor] (C D : Precategory) + : Cᵒᵖ ^c Dᵒᵖ ⇒ (C ^c D)ᵒᵖ := + begin + fapply functor.mk: esimp, + { exact opposite_functor_rev}, + { apply @opposite_rev_nat_trans}, + { intro F, apply nat_trans_eq, intro d, reflexivity}, + { intro F G H η θ, apply nat_trans_eq, intro d, reflexivity} + end + + definition opposite_functor_opposite_left [constructor] (C D : Precategory) + : (C ^c D)ᵒᵖ ⇒ Cᵒᵖ ^c Dᵒᵖ := + begin + fapply functor.mk: esimp, + { exact opposite_functor}, + { intro F G, exact opposite_nat_trans}, + { intro F, apply nat_trans_eq, reflexivity}, + { intro u v w g f, apply nat_trans_eq, reflexivity} + end + + definition opposite_functor_opposite_iso [constructor] (C D : Precategory) + : Cᵒᵖ ^c Dᵒᵖ ≅c (C ^c D)ᵒᵖ := + begin + fapply isomorphism.MK: esimp, + { apply opposite_functor_opposite_right}, + { apply opposite_functor_opposite_left}, + { fapply functor_eq: esimp, + { exact opposite_rev_opposite_functor}, + { intro F G η, fapply nat_trans_eq, esimp, intro d, + rewrite [@natural_map_hom_of_eq _ _ _ G, @natural_map_inv_of_eq _ _ _ F, + ↑opposite_rev_opposite_functor, +@ap010_functor_eq Dᵒᵖ Cᵒᵖ, ▸*], + exact !id_right ⬝ !id_left}}, + { fapply functor_eq: esimp, + { exact opposite_opposite_rev_functor}, + { intro F G η, fapply nat_trans_eq, esimp, intro d, + rewrite [opposite_hom_of_eq, opposite_inv_of_eq, @natural_map_hom_of_eq _ _ _ F, + @natural_map_inv_of_eq _ _ _ G, ↑opposite_opposite_rev_functor, +@ap010_functor_eq, ▸*], + exact !id_right ⬝ !id_left}}, + end + /- C ^ (D + E) ≅ C ^ D × C ^ E -/ definition functor_sum_right [constructor] (C D E : Precategory) @@ -110,7 +190,6 @@ namespace category -- REPORT: cannot abstract end - /- TODO: optimize -/ definition functor_sum_iso [constructor] (C D E : Precategory) : C ^c (D +c E) ≅c C ^c D ×c C ^c E := begin @@ -172,7 +251,7 @@ namespace category { intro V, apply prod_eq: esimp, apply pr1_functor_prod, apply pr2_functor_prod}, { intro V W ν, rewrite [@pr1_hom_of_eq (C ^c E) (D ^c E), @pr2_hom_of_eq (C ^c E) (D ^c E), @pr1_inv_of_eq (C ^c E) (D ^c E), @pr2_inv_of_eq (C ^c E) (D ^c E)], - apply prod_eq: apply nat_trans_eq: intro v: esimp, + apply prod_eq: apply nat_trans_eq; intro v: esimp, { rewrite [@natural_map_hom_of_eq _ _ _ W.1, @natural_map_inv_of_eq _ _ _ V.1, ▸*, ↑pr1_functor_prod,+ap010_functor_eq, ▸*, id_leftright]}, { rewrite [@natural_map_hom_of_eq _ _ _ W.2, @natural_map_inv_of_eq _ _ _ V.2, ▸*, @@ -222,5 +301,4 @@ namespace category ↑functor_uncurry_functor_curry, +@ap010_functor_eq, ▸*], apply id_leftright}}, end - end category diff --git a/hott/algebra/category/functor/functor.md b/hott/algebra/category/functor/functor.md index 66eca311f..839e68cf7 100644 --- a/hott/algebra/category/functor/functor.md +++ b/hott/algebra/category/functor/functor.md @@ -1,10 +1,11 @@ algebra.category.functor ======================== -* [functor](functor.hlean) : Definition of functors +* [basic](basic.hlean) : Definition and basic properties of functors * [curry](curry.hlean) : Define currying and uncurrying of functors * [attributes](attributes.hlean): Attributes of functors (full, faithful, split essentially surjective, ...) * [adjoint](adjoint.hlean) : Adjoint functors and equivalences * [equivalence](equivalence.hlean) : Equivalences and Isomorphisms +* [exponential_laws](exponential_laws.hlean) Note: the functor category is defined in [constructions.functor](../constructions/functor.hlean). \ No newline at end of file diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index 97578a9ed..e370c5724 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -130,7 +130,7 @@ end iso open iso /- isomorphic objects -/ structure iso {ob : Type} [C : precategory ob] (a b : ob) := (to_hom : hom a b) - [struct : is_iso to_hom] + (struct : is_iso to_hom) infix ` ≅ `:50 := iso notation c ` ≅[`:50 C:0 `] `:0 c':50 := @iso C _ c c' @@ -156,13 +156,13 @@ namespace iso variable [C] protected definition refl [constructor] (a : ob) : a ≅ a := - mk (ID a) + mk (ID a) _ protected definition symm [constructor] ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := - mk (to_hom H)⁻¹ + mk (to_hom H)⁻¹ _ protected definition trans [constructor] ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c := - mk (to_hom H2 ∘ to_hom H1) + mk (to_hom H2 ∘ to_hom H1) _ infixl ` ⬝i `:75 := iso.trans postfix [parsing_only] `⁻¹ⁱ`:(max + 1) := iso.symm @@ -174,7 +174,7 @@ namespace iso iso.MK (to_hom H) g (p ▸ to_left_inverse H) (p ▸ to_right_inverse H) definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f') - : iso.mk f = iso.mk f' := + : iso.mk f _ = iso.mk f' _ := apd011 iso.mk p !is_hprop.elim variable {C} diff --git a/hott/algebra/category/limits.hlean b/hott/algebra/category/limits.hlean index 61e6f2eca..d4217e8d4 100644 --- a/hott/algebra/category/limits.hlean +++ b/hott/algebra/category/limits.hlean @@ -17,10 +17,12 @@ namespace category include C definition is_terminal [class] (c : ob) := Πd, is_contr (d ⟶ c) - definition is_contr_of_is_terminal [instance] (c d : ob) [H : is_terminal d] + definition is_contr_of_is_terminal (c d : ob) [H : is_terminal d] : is_contr (c ⟶ d) := H c + local attribute is_contr_of_is_terminal [instance] + definition terminal_morphism (c c' : ob) [H : is_terminal c'] : c ⟶ c' := !center @@ -171,6 +173,18 @@ namespace category { intro i, apply id_right} end end} end + definition limit_functor [constructor] (D I : Precategory) [H : has_limits_of_shape D I] + : D ^c I ⇒ D := + begin + fapply functor.mk: esimp, + { intro F, exact limit_object F}, + { apply @limit_hom_limit}, + { intro F, unfold limit_hom_limit, refine (eq_hom_limit _ _)⁻¹, intro i, + apply comp_id_eq_id_comp}, + { intro F G H η θ, unfold limit_hom_limit, refine (eq_hom_limit _ _)⁻¹, intro i, + rewrite [assoc, hom_limit_commute, -assoc, hom_limit_commute, assoc]} + end + section bin_products open bool prod.ops definition has_binary_products [reducible] (D : Precategory) := has_limits_of_shape D c2 @@ -180,17 +194,16 @@ namespace category definition product_object : D := limit_object (c2_functor D d d') - infixr `×l`:30 := product_object - local infixr × := product_object + infixr ` ×l `:75 := product_object - definition pr1 : d × d' ⟶ d := + definition pr1 : d ×l d' ⟶ d := limit_morphism (c2_functor D d d') ff - definition pr2 : d × d' ⟶ d' := + definition pr2 : d ×l d' ⟶ d' := limit_morphism (c2_functor D d d') tt variables {d d'} - definition hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : x ⟶ d × d' := + definition hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : x ⟶ d ×l d' := hom_limit (c2_functor D d d') (bool.rec f g) (by intro b₁ b₂ f; induction b₁: induction b₂: esimp at *; try contradiction: apply id_left) @@ -200,16 +213,17 @@ namespace category theorem pr2_hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : !pr2 ∘ hom_product f g = g := hom_limit_commute (c2_functor D d d') (bool.rec f g) _ tt - theorem eq_hom_product {x : D} {f : x ⟶ d} {g : x ⟶ d'} {h : x ⟶ d × d'} + theorem eq_hom_product {x : D} {f : x ⟶ d} {g : x ⟶ d'} {h : x ⟶ d ×l d'} (p : !pr1 ∘ h = f) (q : !pr2 ∘ h = g) : h = hom_product f g := eq_hom_limit _ (bool.rec p q) theorem product_cone_unique {x : D} {f : x ⟶ d} {g : x ⟶ d'} - {h₁ : x ⟶ d × d'} (p₁ : !pr1 ∘ h₁ = f) (q₁ : !pr2 ∘ h₁ = g) - {h₂ : x ⟶ d × d'} (p₂ : !pr1 ∘ h₂ = f) (q₂ : !pr2 ∘ h₂ = g) : h₁ = h₂ := + {h₁ : x ⟶ d ×l d'} (p₁ : !pr1 ∘ h₁ = f) (q₁ : !pr2 ∘ h₁ = g) + {h₂ : x ⟶ d ×l d'} (p₂ : !pr1 ∘ h₂ = f) (q₂ : !pr2 ∘ h₂ = g) : h₁ = h₂ := eq_hom_product p₁ q₁ ⬝ (eq_hom_product p₂ q₂)⁻¹ variable (D) + -- TODO: define this in terms of limit_functor and functor_two_left (in exponential_laws) definition product_functor [constructor] : D ×c D ⇒ D := functor.mk (λx, product_object x.1 x.2) @@ -342,7 +356,7 @@ namespace category end pullbacks namespace ops - infixr × := product_object + infixr ×l := product_object end ops end category diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean index a151f00a8..f6a788804 100644 --- a/hott/algebra/category/nat_trans.hlean +++ b/hott/algebra/category/nat_trans.hlean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Floris van Doorn, Jakob von Raumer -/ -import .functor.functor +import .functor.basic open eq category functor is_trunc equiv sigma.ops sigma is_equiv function pi funext iso structure nat_trans {C : Precategory} {D : Precategory} (F G : C ⇒ D) @@ -43,6 +43,10 @@ namespace nat_trans notation 1 := nat_trans.id + definition constant_nat_trans [constructor] (C : Precategory) {D : Precategory} {d d' : D} + (g : d ⟶ d') : constant_functor C d ⟹ constant_functor C d' := + mk (λc, g) (λc c' f, !id_comp_eq_comp_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) diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean index b3e25029a..1e11ebacb 100644 --- a/hott/algebra/category/precategory.hlean +++ b/hott/algebra/category/precategory.hlean @@ -50,6 +50,10 @@ namespace category abbreviation id_id [unfold 2] := @precategory.id_id abbreviation is_hset_hom [unfold 2] := @precategory.is_hset_hom + definition is_hprop_hom_eq {ob : Type} [C : precategory ob] {x y : ob} (f g : x ⟶ y) + : is_hprop (f = g) := + _ + -- the constructor you want to use in practice protected definition precategory.mk [constructor] {ob : Type} (hom : ob → ob → Type) [hset : Π (a b : ob), is_hset (hom a b)] @@ -256,6 +260,7 @@ namespace category rewrite [↑Precategory_eq, -ap_compose,↑function.compose,ap_constant] end + /- theorem Precategory_eq'_eta {C D : Precategory} (p : C = D) : Precategory_eq (ap carrier p) @@ -265,6 +270,7 @@ namespace category induction p, induction C with X C, unfold Precategory_eq, induction C, unfold precategory_eq, exact sorry end + -/ /- theorem Precategory_eq2 {C D : Precategory} (p q : C = D) diff --git a/hott/algebra/category/strict.hlean b/hott/algebra/category/strict.hlean index 67ac086ff..85ef9d12c 100644 --- a/hott/algebra/category/strict.hlean +++ b/hott/algebra/category/strict.hlean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Jakob von Raumer -/ -import .functor.functor +import .functor.basic open is_trunc eq diff --git a/hott/algebra/category/yoneda.hlean b/hott/algebra/category/yoneda.hlean index c278fd41c..9a86f1ac7 100644 --- a/hott/algebra/category/yoneda.hlean +++ b/hott/algebra/category/yoneda.hlean @@ -21,14 +21,14 @@ namespace yoneda ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : by rewrite -(assoc (f2 ∘ f3) _ _) ... = _ : by rewrite (assoc f2 f3 f4) - definition hom_functor.{u v} [constructor] (C : Precategory.{u v}) : Cᵒᵖ ×c C ⇒ cset.{v} := + definition hom_functor.{u v} [constructor] (C : Precategory.{u v}) : Cᵒᵖ ×c C ⇒ set.{v} := functor.mk (λ (x : Cᵒᵖ ×c C), @homset (Cᵒᵖ) C x.1 x.2) - (λ (x y : Cᵒᵖ ×c C) (f : @category.precategory.hom (Cᵒᵖ ×c C) (Cᵒᵖ ×c C) x y) (h : @homset (Cᵒᵖ) C x.1 x.2), - f.2 ∘[C] (h ∘[C] f.1)) - (λ x, @eq_of_homotopy _ _ _ (ID (@homset Cᵒᵖ C x.1 x.2)) (λ h, concat (by apply @id_left) (by apply @id_right))) - (λ x y z g f, - eq_of_homotopy (by intros; apply @representable_functor_assoc)) + (λ (x y : Cᵒᵖ ×c C) (f : @category.precategory.hom (Cᵒᵖ ×c C) (Cᵒᵖ ×c C) x y) + (h : @homset (Cᵒᵖ) C x.1 x.2), f.2 ∘[C] (h ∘[C] f.1)) + (λ x, abstract @eq_of_homotopy _ _ _ (ID (@homset Cᵒᵖ C x.1 x.2)) + (λ h, concat (by apply @id_left) (by apply @id_right)) end) + (λ x y z g f, abstract eq_of_homotopy (by intros; apply @representable_functor_assoc) end) /- These attributes make sure that the fields of the category "set" reduce to the right things @@ -42,7 +42,7 @@ namespace yoneda functor_curry !hom_functor definition yoneda_embedding (C : Precategory) : C ⇒ cset ^c Cᵒᵖ := - functor_curry (!hom_functor ∘f !functor_prod_flip) + functor_curry (!hom_functor ∘f !prod_flip_functor) notation `ɏ` := yoneda_embedding _ @@ -132,7 +132,7 @@ namespace yoneda begin intro c c', fapply is_equiv_of_equiv_of_homotopy, { exact !eq_equiv_iso ⬝e !iso_equiv_F_iso_F ⬝e !eq_equiv_iso⁻¹ᵉ}, - { intro p, induction p, esimp [equiv.trans, equiv.symm], + { intro p, induction p, esimp [equiv.trans, equiv.symm, to_fun_iso], -- to_fun_iso not unfolded esimp [to_fun_iso], rewrite -eq_of_iso_refl, apply ap eq_of_iso, apply iso_eq, esimp, @@ -143,15 +143,17 @@ namespace yoneda definition is_representable {C : Precategory} (F : Cᵒᵖ ⇒ cset) := Σ(c : C), ɏ c ≅ F - set_option unifier.max_steps 25000 -- TODO: fix this - definition is_hprop_representable {C : Category} (F : Cᵒᵖ ⇒ cset) - : is_hprop (is_representable F) := - begin - fapply is_trunc_equiv_closed, - { transitivity (Σc, ɏ c = F), - { exact fiber.sigma_char ɏ F}, - { apply sigma.sigma_equiv_sigma_id, intro c, apply eq_equiv_iso}}, - { apply function.is_hprop_fiber_of_is_embedding, apply is_embedding_yoneda_embedding} + section + set_option apply.class_instance false + definition is_hprop_representable {C : Category} (F : Cᵒᵖ ⇒ cset) + : is_hprop (is_representable F) := + begin + fapply is_trunc_equiv_closed, + { exact proof fiber.sigma_char ɏ F qed ⬝e sigma.sigma_equiv_sigma_id (λc, !eq_equiv_iso)}, + { apply function.is_hprop_fiber_of_is_embedding, apply is_embedding_yoneda_embedding} + end end + + end yoneda diff --git a/hott/book.md b/hott/book.md index bd202b8a5..828d098c6 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 | - | - | - | - | - | - | | | | | | | | | | @@ -79,7 +79,7 @@ Chapter 3: Sets and logic - 3.8 (The axiom of choice): not formalized - 3.9 (The principle of unique choice): Lemma 9.3.1 in [hit.trunc](hit/trunc.hlean), Lemma 9.3.2 in [types.trunc](types/trunc.hlean) - 3.10 (When are propositions truncated?): no formalizable content -- 3.11 (Contractibility): [init.trunc](init/trunc.hlean) (mostly), [types.pi](types/pi.hlean) (Lemma 3.11.6), [types.trunc](types/trunc.hlean) (Lemma 3.11.7), [types.sigma](types/sigma.hlean) (Lemma 3.11.9) +- 3.11 (Contractibility): [init.trunc](init/trunc.hlean) (mostly), [types.pi](types/pi.hlean) (Lemma 3.11.6), [types.trunc](types/trunc.hlean) (Lemma 3.11.7), [types.sigma](types/sigma.hlean) (Lemma 3.11.9) Chapter 4: Equivalences --------- @@ -131,7 +131,7 @@ Chapter 7: Homotopy n-types - 7.3 (Truncations): [init.hit](init/hit.hlean), [hit.trunc](hit/trunc.hlean) and [types.trunc](types/trunc.hlean) - 7.4 (Colimits of n-types): not formalized - 7.5 (Connectedness): [homotopy.connectedness](homotopy/connectedness.hlean) (just the beginning so far) -- 7.6 (Orthogonal factorization): not formalized +- 7.6 (Orthogonal factorization): not formalized - 7.7 (Modalities): not formalized, and may be unformalizable in general because it's unclear how to define modalities Chapter 8: Homotopy theory @@ -142,13 +142,13 @@ Unless otherwise noted, the files are in the folder [homotopy](homotopy/homotopy - 8.1 (π_1(S^1)): [homotopy.circle](homotopy/circle.hlean) (only one of the proofs) - 8.2 (Connectedness of suspensions): not formalized - 8.3 (πk≤n of an n-connected space and π_{k