From 448178a045d2fc05e515561eba60b2a1e9c71ab8 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 2 Oct 2015 19:54:27 -0400 Subject: [PATCH] feat(category.functor2): prove that the category of functors is complete and cocomplete if the codomain is --- hott/algebra/category/adjoint.hlean | 2 +- hott/algebra/category/category.hlean | 21 +- hott/algebra/category/category.md | 8 +- hott/algebra/category/colimits.hlean | 15 +- .../category/constructions/constructions.md | 6 +- .../category/constructions/functor.hlean | 25 ++- .../category/constructions/functor2.hlean | 147 ++++++++++++ .../algebra/category/constructions/hset.hlean | 60 ++--- .../category/constructions/initial.hlean | 2 +- .../category/constructions/opposite.hlean | 21 +- hott/algebra/category/curry.hlean | 173 ++++++++++++++ hott/algebra/category/functor.hlean | 1 + hott/algebra/category/limits.hlean | 6 +- hott/algebra/category/nat_trans.hlean | 2 + hott/algebra/category/precategory.hlean | 2 +- hott/algebra/category/strict.hlean | 20 +- hott/algebra/category/yoneda.hlean | 211 ++---------------- hott/function.hlean | 3 +- hott/init/trunc.hlean | 2 +- 19 files changed, 470 insertions(+), 257 deletions(-) create mode 100644 hott/algebra/category/constructions/functor2.hlean create mode 100644 hott/algebra/category/curry.hlean diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean index 9082391de0..ddfd8ba66a 100644 --- a/hott/algebra/category/adjoint.hlean +++ b/hott/algebra/category/adjoint.hlean @@ -8,7 +8,7 @@ Properties of functors such as adjoint functors, equivalences, faithful or full TODO: Split this file in different files -/ -import algebra.category.constructions function arity +import .constructions.functor function arity open category functor nat_trans eq is_trunc iso equiv prod trunc function pi is_equiv diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean index 40a7732120..56fc4840e9 100644 --- a/hott/algebra/category/category.hlean +++ b/hott/algebra/category/category.hlean @@ -8,22 +8,32 @@ import .iso open iso is_equiv equiv eq is_trunc --- A category is a precategory extended by a witness --- that the function from paths to isomorphisms, --- is an equivalecnce. +/- + A category is a precategory extended by a witness + that the function from paths to isomorphisms is an equivalence. +-/ namespace category - definition is_univalent [reducible] {ob : Type} (C : precategory ob) := + /- + TODO: restructure this. is_univalent should probably be a class with as argument + (C : Precategory) + -/ + definition is_univalent [class] {ob : Type} (C : precategory ob) := Π(a b : ob), is_equiv (iso_of_eq : a = b → a ≅ b) + definition is_equiv_of_is_univalent [instance] {ob : Type} [C : precategory ob] + [H : is_univalent C] (a b : ob) : is_equiv (iso_of_eq : a = b → a ≅ b) := + H a b + structure category [class] (ob : Type) extends parent : precategory ob := mk' :: (iso_of_path_equiv : is_univalent parent) attribute category [multiple_instances] abbreviation iso_of_path_equiv := @category.iso_of_path_equiv + attribute category.iso_of_path_equiv [instance] definition category.mk [reducible] [unfold 2] {ob : Type} (C : precategory ob) - (H : Π (a b : ob), is_equiv (iso_of_eq : a = b → a ≅ b)) : category ob := + (H : is_univalent C) : category ob := precategory.rec_on C category.mk' H section basic @@ -31,7 +41,6 @@ namespace category include C -- Make iso_of_path_equiv a class instance - -- TODO: Unsafe class instance? attribute iso_of_path_equiv [instance] definition eq_equiv_iso [constructor] (a b : ob) : (a = b) ≃ (a ≅ b) := diff --git a/hott/algebra/category/category.md b/hott/algebra/category/category.md index 221bac14bc..08f92c9011 100644 --- a/hott/algebra/category/category.md +++ b/hott/algebra/category/category.md @@ -11,7 +11,11 @@ Development of Category Theory. The following files are in this folder (sorted s * [nat_trans](nat_trans.hlean) : Natural transformations * [strict](strict.hlean) : Strict categories * [constructions](constructions/constructions.md) (subfolder) : basic constructions on categories and examples of categories + +The following files depend on some of the files in the folder [constructions](constructions/constructions.md) + +* [curry](curry.hlean) : Define currying and uncurrying of functors +* [limits](limits.hlean) : Limits in a category, defined as terminal object in the cone category +* [colimits](colimits.hlean) : Colimits in a category, defined as the limit of the opposite functor * [adjoint](adjoint.hlean) : Adjoint functors and Equivalences (WIP) * [yoneda](yoneda.hlean) : Yoneda Embedding (WIP) -* [limits](limits.hlean) : Limits in a category, defined as terminal object in the cone category -* [colimits](colimits.hlean) : Colimits in a category, defined as the limit of the opposite functor \ No newline at end of file diff --git a/hott/algebra/category/colimits.hlean b/hott/algebra/category/colimits.hlean index b6a33f1d8a..f7ef6d23e7 100644 --- a/hott/algebra/category/colimits.hlean +++ b/hott/algebra/category/colimits.hlean @@ -59,7 +59,7 @@ namespace category is_hprop_has_terminal_object (Category_opposite D) variable (D) - definition has_colimits_of_shape [reducible] := has_limits_of_shape Dᵒᵖ Iᵒᵖ + abbreviation has_colimits_of_shape := has_limits_of_shape Dᵒᵖ Iᵒᵖ /- The next definitions states that a category is cocomplete with respect to diagrams @@ -67,7 +67,7 @@ namespace category with respect to diagrams of type Precategory.{o₂ h₂} -/ - definition is_cocomplete [reducible] (D : Precategory) := is_complete Dᵒᵖ + abbreviation is_cocomplete (D : Precategory) := is_complete Dᵒᵖ definition has_colimits_of_shape_of_is_cocomplete [instance] [H : is_cocomplete D] (I : Precategory) : has_colimits_of_shape D I := H Iᵒᵖ @@ -85,7 +85,7 @@ namespace category variables {D I} (F : I ⇒ D) [H : has_colimits_of_shape D I] {i j : I} include H - definition cocone [reducible] := (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) := @@ -147,6 +147,11 @@ namespace category {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 + definition colimit_hom_colimit [reducible] {F G : I ⇒ D} (η : F ⟹ G) + : colimit_object F ⟶ colimit_object G := + colimit_hom _ (λi, colimit_morphism G i ∘ η i) + abstract by intro i j f; rewrite [-assoc,-naturality,assoc,colimit_commute] end + omit H variable (F) @@ -308,4 +313,8 @@ namespace category end pushouts + definition has_limits_of_shape_op_op [H : has_limits_of_shape D Iᵒᵖᵒᵖ] + : has_limits_of_shape D I := + by induction I with I Is; induction Is; exact H + end category diff --git a/hott/algebra/category/constructions/constructions.md b/hott/algebra/category/constructions/constructions.md index e70b79903c..6e741c5e37 100644 --- a/hott/algebra/category/constructions/constructions.md +++ b/hott/algebra/category/constructions/constructions.md @@ -5,13 +5,12 @@ 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 +* [hset](hset.hlean) : Category of sets. Prove that it is complete and cocomplete * [sum](sum.hlean) : Sum category * [product](product.hlean) : Product category * [comma](comma.hlean) : Comma category * [cone](cone.hlean) : Cone category - Discrete, indiscrete or finite categories: * [finite_cats](finite_cats.hlean) : Some finite categories, which are diagrams of common limits (the diagram for the pullback or the equalizer). Also contains a general construction of categories where you give some generators for the morphisms, with the condition that you cannot compose two of thosex @@ -19,3 +18,6 @@ Discrete, indiscrete or finite categories: * [indiscrete](indiscrete.hlean) * [terminal](terminal.hlean) * [initial](initial.hlean) + +Non-basic topics: +* [functor2](functor2.hlean) : showing that the functor category has (co)limits if the codomain has them. diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 39260500b9..c27bc4af43 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -8,9 +8,9 @@ Functor precategory and category import ..nat_trans ..category -open eq functor is_trunc nat_trans iso is_equiv +open eq category is_trunc nat_trans iso is_equiv category.hom -namespace category +namespace functor definition precategory_functor [instance] [reducible] [constructor] (D C : Precategory) : precategory (functor C D) := @@ -252,4 +252,23 @@ namespace category end functor -end category + variables {C D I : Precategory} + definition constant2_functor [constructor] (F : I ⇒ D ^c C) (c : C) : I ⇒ D := + functor.mk (λi, to_fun_ob (F i) c) + (λi j f, natural_map (F f) c) + abstract (λi, ap010 natural_map !respect_id c ⬝ proof idp qed) end + abstract (λi j k g f, ap010 natural_map !respect_comp c) end + + definition constant2_functor_natural [constructor] (F : I ⇒ D ^c C) {c d : C} (f : c ⟶ d) + : constant2_functor F c ⟹ constant2_functor F d := + nat_trans.mk (λi, to_fun_hom (F i) f) + (λi j k, (naturality (F k) f)⁻¹) + + definition functor_flip [constructor] (F : I ⇒ D ^c C) : C ⇒ D ^c I := + functor.mk (constant2_functor F) + @(constant2_functor_natural F) + 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 + + +end functor diff --git a/hott/algebra/category/constructions/functor2.hlean b/hott/algebra/category/constructions/functor2.hlean new file mode 100644 index 0000000000..64e0314b3a --- /dev/null +++ b/hott/algebra/category/constructions/functor2.hlean @@ -0,0 +1,147 @@ +/- +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, Jakob von Raumer + +Functor category has (co)limits if the codomain has them +-/ + +import ..colimits + +open functor nat_trans eq is_trunc + +namespace category + + -- preservation of limits + variables {D C I : Precategory} + + definition limit_functor [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), + (constant2_functor F d) k ∘ to_fun_hom (F i) f ∘ limit_morphism (constant2_functor F c) i = + to_fun_hom (F j) f ∘ limit_morphism (constant2_functor F c) j, + { intro c d f i j k, rewrite [-limit_commute _ k,▸*,+assoc,▸*,-naturality (F k) f]}, + + fapply functor.mk, + { intro c, exact limit_object (constant2_functor F c)}, + { intro c d f, fapply hom_limit, + { intro i, refine to_fun_hom (F i) f ∘ !limit_morphism}, + { apply lem}}, + { exact abstract begin intro c, symmetry, apply eq_hom_limit, intro i, + rewrite [id_right,respect_id,▸*,id_left] end end}, + { intro a b c g f, symmetry, apply eq_hom_limit, intro i, -- report: adding abstract fails here + rewrite [respect_comp,assoc,hom_limit_commute,-assoc,hom_limit_commute,assoc]} + end + + definition limit_functor_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}, + { fapply nat_trans.mk, + { intro i, esimp, fapply nat_trans.mk, + { intro c, esimp, apply limit_morphism}, + { intro c d f, rewrite [▸*,hom_limit_commute (constant2_functor F d)]}}, + { intro i j k, apply nat_trans_eq, intro c, + rewrite [▸*,id_right,limit_commute (constant2_functor F c)]}} + end + + variables (D C I) + definition has_limits_of_shape_functor [instance] [H : has_limits_of_shape D I] + : has_limits_of_shape (D ^c C) I := + begin + intro F, fapply has_terminal_object.mk, + { exact limit_functor_cone F}, + { intro c, esimp at *, induction c with G η, induction η with η p, esimp at *, + fapply is_contr.mk, + { fapply cone_hom.mk, + { fapply nat_trans.mk, + { intro c, esimp, fapply hom_limit, + { intro i, esimp, exact η i c}, + { intro i j k, esimp, exact ap010 natural_map (p k) c ⬝ !id_right}}, + { intro c d f, esimp, fapply @limit_cone_unique, + { intro i, esimp, exact to_fun_hom (F i) f ∘ η i c}, + { intro i j k, rewrite [▸*,assoc,-naturality,-assoc,-compose_def,p k,▸*,id_right]}, + { intro i, rewrite [assoc, hom_limit_commute (constant2_functor F d),▸*,-assoc, + hom_limit_commute]}, + { intro i, rewrite [assoc, hom_limit_commute (constant2_functor F d),naturality]}}}, + { intro i, apply nat_trans_eq, intro c, + rewrite [▸*,hom_limit_commute (constant2_functor F c)]}}, + { intro h, induction h with f q, apply cone_hom_eq, + apply nat_trans_eq, intro c, esimp at *, symmetry, + apply eq_hom_limit, intro i, exact ap010 natural_map (q i) c}} + end + + definition is_complete_functor [instance] [H : is_complete D] : is_complete (D ^c C) := + λI, _ + + variables {D C I} + -- preservation of colimits + + -- definition constant2_functor_op [constructor] (F : I ⇒ (D ^c C)ᵒᵖ) (c : C) : I ⇒ D := + -- proof + -- functor.mk (λi, to_fun_ob (F i) c) + -- (λi j f, natural_map (F f) c) + -- abstract (λi, ap010 natural_map !respect_id c ⬝ proof idp qed) end + -- abstract (λi j k g f, ap010 natural_map !respect_comp c) end + -- qed + + definition colimit_functor [constructor] + [H : has_colimits_of_shape D I] (F : Iᵒᵖ ⇒ (D ^c C)ᵒᵖ) : C ⇒ D := + begin + fapply functor.mk, + { intro c, exact colimit_object (constant2_functor Fᵒᵖ' c)}, + { intro c d f, apply colimit_hom_colimit, apply constant2_functor_natural _ f}, + { exact abstract begin intro c, symmetry, apply eq_colimit_hom, intro i, + rewrite [id_left,▸*,respect_id,id_right] end end}, + { intro a b c g f, symmetry, apply eq_colimit_hom, intro i, -- report: adding abstract fails here + rewrite [▸*,respect_comp,-assoc,colimit_hom_commute,assoc,colimit_hom_commute,-assoc]} + end + + definition colimit_functor_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}, + { fapply nat_trans.mk, + { intro i, esimp, fapply nat_trans.mk, + { intro c, esimp, apply colimit_morphism}, + { intro c d f, apply colimit_hom_commute (constant2_functor Fᵒᵖ' c)}}, + { intro i j k, apply nat_trans_eq, intro c, + rewrite [▸*,id_left], apply colimit_commute (constant2_functor Fᵒᵖ' c)}} + end + + variables (D C I) + definition has_colimits_of_shape_functor [instance] [H : has_colimits_of_shape D I] + : has_colimits_of_shape (D ^c C) I := + begin + intro F, fapply has_terminal_object.mk, + { exact colimit_functor_cone F}, + { intro c, esimp at *, induction c with G η, induction η with η p, esimp at *, + fapply is_contr.mk, + { fapply cone_hom.mk, + { fapply nat_trans.mk, + { intro c, esimp, fapply colimit_hom, + { intro i, esimp, exact η i c}, + { intro i j k, esimp, exact ap010 natural_map (p k) c ⬝ !id_left}}, + { intro c d f, esimp, fapply @colimit_cocone_unique, + { intro i, esimp, exact η i d ∘ to_fun_hom (F i) f}, + { intro i j k, rewrite [▸*,-assoc,naturality,assoc,-compose_def,p k,▸*,id_left]}, + { intro i, rewrite [-assoc, colimit_hom_commute (constant2_functor Fᵒᵖ' c), + ▸*, naturality]}, + { intro i, rewrite [-assoc, colimit_hom_commute (constant2_functor Fᵒᵖ' c),▸*,assoc, + colimit_hom_commute (constant2_functor Fᵒᵖ' d)]}}}, + { intro i, apply nat_trans_eq, intro c, + rewrite [▸*,colimit_hom_commute (constant2_functor Fᵒᵖ' c)]}}, + { intro h, induction h with f q, apply cone_hom_eq, + apply nat_trans_eq, intro c, esimp at *, symmetry, + apply eq_colimit_hom, intro i, exact ap010 natural_map (q i) c}} + end + + 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) := + λI, _ + +end category diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean index c9c14d85b6..ec02bb2970 100644 --- a/hott/algebra/category/constructions/hset.hlean +++ b/hott/algebra/category/constructions/hset.hlean @@ -23,24 +23,24 @@ namespace category definition Precategory_hset [reducible] [constructor] : Precategory := Precategory.mk hset precategory_hset - abbreviation pset [constructor] := Precategory_hset + abbreviation set [constructor] := Precategory_hset namespace set local attribute is_equiv_subtype_eq [instance] - definition iso_of_equiv [constructor] {A B : pset} (f : A ≃ B) : A ≅ B := + definition iso_of_equiv [constructor] {A B : set} (f : A ≃ B) : A ≅ B := iso.MK (to_fun f) (to_inv f) (eq_of_homotopy (left_inv (to_fun f))) (eq_of_homotopy (right_inv (to_fun f))) - definition equiv_of_iso [constructor] {A B : pset} (f : A ≅ B) : A ≃ B := + definition equiv_of_iso [constructor] {A B : set} (f : A ≅ B) : A ≃ B := begin apply equiv.MK (to_hom f) (iso.to_inv f), exact ap10 (to_right_inverse f), exact ap10 (to_left_inverse f) end - definition is_equiv_iso_of_equiv [constructor] (A B : pset) + definition is_equiv_iso_of_equiv [constructor] (A B : set) : is_equiv (@iso_of_equiv A B) := adjointify _ (λf, equiv_of_iso f) (λf, proof iso_eq idp qed) @@ -53,7 +53,7 @@ namespace category @ap _ _ (to_fun (trunctype.sigma_char 0)) A B := eq_of_homotopy (λp, eq.rec_on p idp) - definition equiv_equiv_iso (A B : pset) : (A ≃ B) ≃ (A ≅ B) := + definition equiv_equiv_iso (A B : set) : (A ≃ B) ≃ (A ≅ B) := equiv.MK (λf, iso_of_equiv f) (λf, proof equiv.MK (to_hom f) (iso.to_inv f) @@ -62,10 +62,10 @@ namespace category (λf, proof iso_eq idp qed) (λf, proof equiv_eq idp qed) - definition equiv_eq_iso (A B : pset) : (A ≃ B) = (A ≅ B) := + definition equiv_eq_iso (A B : set) : (A ≃ B) = (A ≅ B) := ua !equiv_equiv_iso - definition is_univalent_hset (A B : pset) : is_equiv (iso_of_eq : A = B → A ≅ B) := + definition is_univalent_hset (A B : set) : is_equiv (iso_of_eq : A = B → A ≅ B) := assert H₁ : is_equiv (@iso_of_equiv A B ∘ @equiv_of_eq A B ∘ subtype_eq_inv _ _ ∘ @ap _ _ (to_fun (trunctype.sigma_char 0)) A B), from @is_equiv_compose _ _ _ _ _ @@ -88,10 +88,10 @@ namespace category definition Category_hset [reducible] [constructor] : Category := Category.mk hset category_hset - abbreviation set [constructor] := Category_hset + abbreviation cset [constructor] := Category_hset open functor lift - definition lift_functor.{u v} [constructor] : pset.{u} ⇒ pset.{max u v} := + definition lift_functor.{u v} [constructor] : set.{u} ⇒ set.{max u v} := functor.mk tlift (λa b, lift_functor) (λa, eq_of_homotopy (λx, by induction x; reflexivity)) @@ -102,24 +102,27 @@ namespace category local attribute category.to_precategory [unfold 2] definition is_complete_set_cone.{u v w} [constructor] - (I : Precategory.{v w}) (F : I ⇒ pset.{max u v w}) : cone_obj F := + (I : Precategory.{v w}) (F : I ⇒ set.{max u v w}) : cone_obj F := begin fapply cone_obj.mk, { fapply trunctype.mk, { exact Σ(s : Π(i : I), trunctype.carrier (F i)), Π{i j : I} (f : i ⟶ j), F f (s i) = (s j)}, - { exact sorry /-abstract begin apply is_trunc_sigma, intro s, - apply is_trunc_pi, intro i, - apply is_trunc_pi, intro j, - apply is_trunc_pi, intro f, - apply is_trunc_eq end end-/}}, + { with_options [elaborator.ignore_instances true] -- TODO: fix + ( refine is_trunc_sigma _ _; + ( apply is_trunc_pi); + ( intro s; + refine is_trunc_pi _ _; intro i; + refine is_trunc_pi _ _; intro j; + refine is_trunc_pi _ _; intro f; + apply is_trunc_eq))}}, { fapply nat_trans.mk, { intro i x, esimp at x, exact x.1 i}, { intro i j f, esimp, apply eq_of_homotopy, intro x, esimp at x, induction x with s p, esimp, apply p}} end - definition is_complete_set.{u v w} [instance] : is_complete.{(max u v w)+1 (max u v w) v w} pset := + definition is_complete_set.{u v w} [instance] : is_complete.{(max u v w)+1 (max u v w) v w} set := begin intro I F, fapply has_terminal_object.mk, { exact is_complete_set_cone.{u v w} I F}, @@ -133,15 +136,16 @@ namespace category { esimp, intro h, induction h with f q, apply cone_hom_eq, esimp at *, apply eq_of_homotopy, intro x, fapply sigma_eq: esimp, { apply eq_of_homotopy, intro i, exact (ap10 (q i) x)⁻¹}, - { exact sorry /-apply is_hprop.elimo, - apply is_trunc_pi, intro i, - apply is_trunc_pi, intro j, - apply is_trunc_pi, intro f, - apply is_trunc_eq-/}}} + { with_options [elaborator.ignore_instances true] -- TODO: fix + ( refine is_hprop.elimo _ _ _; + refine is_trunc_pi _ _; intro i; + refine is_trunc_pi _ _; intro j; + refine is_trunc_pi _ _; intro f; + apply is_trunc_eq)}}} end definition is_cocomplete_set_cone_rel.{u v w} [unfold 3 4] - (I : Precategory.{v w}) (F : I ⇒ pset.{max u v w}ᵒᵖ) : (Σ(i : I), trunctype.carrier (F i)) → + (I : Precategory.{v w}) (F : I ⇒ set.{max u v w}ᵒᵖ) : (Σ(i : I), trunctype.carrier (F i)) → (Σ(i : I), trunctype.carrier (F i)) → hprop.{max u v w} := begin intro v w, induction v with i x, induction w with j y, @@ -151,7 +155,7 @@ namespace category end definition is_cocomplete_set_cone.{u v w} [constructor] - (I : Precategory.{v w}) (F : I ⇒ pset.{max u v w}ᵒᵖ) : cone_obj F := + (I : Precategory.{v w}) (F : I ⇒ set.{max u v w}ᵒᵖ) : cone_obj F := begin fapply cone_obj.mk, { fapply trunctype.mk, @@ -163,18 +167,18 @@ namespace category exact exists.intro f idp}} end --- adding the following step explicitly slightly reduces the elaboration time of the next proof +-- 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 pset.{max u v w}) +-- (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 psetᵒᵖ F --- (@cone_obj.mk I psetᵒᵖ F X --- (@nat_trans.mk I (Opposite pset) (@constant_functor I (Opposite pset) X) F η @p)) +-- @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 diff --git a/hott/algebra/category/constructions/initial.hlean b/hott/algebra/category/constructions/initial.hlean index 109e93a9ee..1410eb454e 100644 --- a/hott/algebra/category/constructions/initial.hlean +++ b/hott/algebra/category/constructions/initial.hlean @@ -28,7 +28,7 @@ namespace category (λx, empty.elim x) (λx y z g f, empty.elim x) - definition is_contr_zero_functor [instance] (C : Precategory) : is_contr (0 ⇒ C) := + definition is_contr_initial_functor [instance] (C : Precategory) : is_contr (0 ⇒ C) := is_contr.mk (initial_functor C) begin intro F, fapply functor_eq, diff --git a/hott/algebra/category/constructions/opposite.hlean b/hott/algebra/category/constructions/opposite.hlean index 6b5d193c5a..e9f3e07f4d 100644 --- a/hott/algebra/category/constructions/opposite.hlean +++ b/hott/algebra/category/constructions/opposite.hlean @@ -40,20 +40,27 @@ namespace category definition opposite_opposite : (Cᵒᵖ)ᵒᵖ = C := (ap (Precategory.mk C) (opposite_opposite' C)) ⬝ !Precategory.eta - - definition opposite_functor [reducible] {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ := + definition opposite_functor [constructor] {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ := begin - apply (@functor.mk (Cᵒᵖ) (Dᵒᵖ)), - intro a, 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 := + begin + 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_rev definition opposite_iso [constructor] {ob : Type} [C : precategory ob] {a b : ob} (H : @iso _ C a b) : @iso _ (opposite C) a b := begin - fapply @iso.MK, + fapply @iso.MK _ (opposite C), { exact to_inv H}, { exact to_hom H}, { exact to_left_inverse H}, @@ -84,7 +91,7 @@ namespace category begin intro x y, fapply is_equiv_of_equiv_of_homotopy, - { refine @eq_equiv_iso C C x y ⬝e _, symmetry, apply opposite_iso_equiv}, + { refine @eq_equiv_iso C C x y ⬝e _, symmetry, esimp at *, apply opposite_iso_equiv}, { intro p, induction p, reflexivity} end diff --git a/hott/algebra/category/curry.hlean b/hott/algebra/category/curry.hlean new file mode 100644 index 0000000000..368177e7b3 --- /dev/null +++ b/hott/algebra/category/curry.hlean @@ -0,0 +1,173 @@ +/- +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 + +Definition of currying and uncurrying of functors +-/ + +import .constructions.functor .constructions.product + +open category prod nat_trans eq prod.ops iso equiv + +namespace functor + + variables {C D E : Precategory} (F : C ×c D ⇒ E) (G : C ⇒ E ^c D) + definition functor_curry_ob [reducible] [constructor] (c : C) : E ^c D := + functor.mk (λd, F (c,d)) + (λd d' g, F (id, g)) + (λd, !respect_id) + (λd₁ d₂ d₃ g' g, calc + F (id, g' ∘ g) = F (id ∘ id, g' ∘ g) : by rewrite id_id + ... = F ((id,g') ∘ (id, g)) : by esimp + ... = F (id,g') ∘ F (id, g) : by rewrite respect_comp) + + local abbreviation Fob := @functor_curry_ob + + definition functor_curry_hom [constructor] ⦃c c' : C⦄ (f : c ⟶ c') : Fob F c ⟹ Fob F c' := + begin + fapply @nat_trans.mk, + {intro d, exact F (f, id)}, + {intro d d' g, calc + F (id, g) ∘ F (f, id) = F (id ∘ f, g ∘ id) : respect_comp F + ... = F (f, g ∘ id) : by rewrite id_left + ... = F (f, g) : by rewrite id_right + ... = F (f ∘ id, g) : by rewrite id_right + ... = F (f ∘ id, id ∘ g) : by rewrite id_left + ... = F (f, id) ∘ F (id, g) : (respect_comp F (f, id) (id, g))⁻¹ᵖ + } + end + local abbreviation Fhom := @functor_curry_hom + + theorem functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) : + (Fhom F f) d = to_fun_hom F (f, id) := idp + + theorem functor_curry_id (c : C) : Fhom F (ID c) = nat_trans.id := + nat_trans_eq (λd, respect_id F _) + + theorem functor_curry_comp ⦃c c' c'' : C⦄ (f' : c' ⟶ c'') (f : c ⟶ c') + : Fhom F (f' ∘ f) = Fhom F f' ∘n Fhom F f := + begin + apply @nat_trans_eq, + intro d, calc + natural_map (Fhom F (f' ∘ f)) d = F (f' ∘ f, id) : by rewrite functor_curry_hom_def + ... = F (f' ∘ f, id ∘ id) : by rewrite id_id + ... = F ((f',id) ∘ (f, id)) : by esimp + ... = F (f',id) ∘ F (f, id) : by rewrite [respect_comp F] + ... = natural_map ((Fhom F f') ∘ (Fhom F f)) d : by esimp + end + + definition functor_curry [reducible] [constructor] : C ⇒ E ^c D := + functor.mk (functor_curry_ob F) + (functor_curry_hom F) + (functor_curry_id F) + (functor_curry_comp F) + + definition functor_uncurry_ob [reducible] (p : C ×c D) : E := + to_fun_ob (G p.1) p.2 + local abbreviation Gob := @functor_uncurry_ob + + definition functor_uncurry_hom ⦃p p' : C ×c D⦄ (f : hom p p') : Gob G p ⟶ Gob G p' := + to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2 + local abbreviation Ghom := @functor_uncurry_hom + + theorem functor_uncurry_id (p : C ×c D) : Ghom G (ID p) = id := + calc + Ghom G (ID p) = to_fun_hom (to_fun_ob G p.1) id ∘ natural_map (to_fun_hom G id) p.2 : by esimp + ... = id ∘ natural_map (to_fun_hom G id) p.2 : by rewrite respect_id + ... = id ∘ natural_map nat_trans.id p.2 : by rewrite respect_id + ... = id : id_id + + theorem functor_uncurry_comp ⦃p p' p'' : C ×c D⦄ (f' : p' ⟶ p'') (f : p ⟶ p') + : Ghom G (f' ∘ f) = Ghom G f' ∘ Ghom G f := + calc + Ghom G (f' ∘ f) + = to_fun_hom (to_fun_ob G p''.1) (f'.2 ∘ f.2) ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2 : by esimp + ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2) + ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2 : by rewrite respect_comp + ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2) + ∘ natural_map (to_fun_hom G f'.1 ∘ to_fun_hom G f.1) p.2 : by rewrite respect_comp + ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2) + ∘ (natural_map (to_fun_hom G f'.1) p.2 ∘ natural_map (to_fun_hom G f.1) p.2) : by esimp + ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ natural_map (to_fun_hom G f'.1) p'.2) + ∘ (to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2) : + by rewrite [square_prepostcompose (!naturality⁻¹ᵖ) _ _] + ... = Ghom G f' ∘ Ghom G f : by esimp + + definition functor_uncurry [reducible] [constructor] : C ×c D ⇒ E := + functor.mk (functor_uncurry_ob G) + (functor_uncurry_hom G) + (functor_uncurry_id G) + (functor_uncurry_comp G) + + theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := + functor_eq (λp, ap (to_fun_ob F) !prod.eta) + begin + intro cd cd' fg, + cases cd with c d, cases cd' with c' d', cases fg with f g, + transitivity to_fun_hom (functor_uncurry (functor_curry F)) (f, g), + apply id_leftright, + show (functor_uncurry (functor_curry F)) (f, g) = F (f,g), + from calc + (functor_uncurry (functor_curry F)) (f, g) = to_fun_hom F (id, g) ∘ to_fun_hom F (f, id) : by esimp + ... = F (id ∘ f, g ∘ id) : by krewrite [-respect_comp F (id,g) (f,id)] + ... = F (f, g ∘ id) : by rewrite id_left + ... = F (f,g) : by rewrite id_right, + end + + definition functor_curry_functor_uncurry_ob (c : C) + : functor_curry (functor_uncurry G) c = G c := + begin + fapply functor_eq, + {intro d, reflexivity}, + {intro d d' g, + apply concat, apply id_leftright, + show to_fun_hom (functor_curry (functor_uncurry G) c) g = to_fun_hom (G c) g, + from calc + to_fun_hom (functor_curry (functor_uncurry G) c) g + = to_fun_hom (G c) g ∘ natural_map (to_fun_hom G (ID c)) d : by esimp + ... = to_fun_hom (G c) g ∘ natural_map (ID (G c)) d : by rewrite respect_id + ... = to_fun_hom (G c) g ∘ id : by reflexivity + ... = to_fun_hom (G c) g : by rewrite id_right} + end + + theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G := + begin + fapply functor_eq, exact (functor_curry_functor_uncurry_ob G), + intro c c' f, + fapply nat_trans_eq, + intro d, + apply concat, + {apply (ap (λx, x ∘ _)), + apply concat, apply natural_map_hom_of_eq, apply (ap hom_of_eq), apply ap010_functor_eq}, + apply concat, + {apply (ap (λx, _ ∘ x)), apply (ap (λx, _ ∘ x)), + apply concat, apply natural_map_inv_of_eq, + apply (ap (λx, hom_of_eq x⁻¹)), apply ap010_functor_eq}, + apply concat, apply id_leftright, + apply concat, apply (ap (λx, x ∘ _)), apply respect_id, + apply id_left + end + + definition prod_functor_equiv_functor_functor [constructor] (C D E : Precategory) + : (C ×c D ⇒ E) ≃ (C ⇒ E ^c D) := + equiv.MK functor_curry + functor_uncurry + functor_curry_functor_uncurry + functor_uncurry_functor_curry + + + definition functor_prod_flip [constructor] (C D : Precategory) : C ×c D ⇒ D ×c C := + functor.mk (λp, (p.2, p.1)) + (λp p' h, (h.2, h.1)) + (λp, idp) + (λp p' p'' h' h, idp) + + definition functor_prod_flip_functor_prod_flip (C D : Precategory) + : functor_prod_flip D C ∘f (functor_prod_flip C D) = functor.id := + begin + fapply functor_eq, {intro p, apply prod.eta}, + intro p p' h, cases p with c d, cases p' with c' d', + apply id_leftright, + end +end functor diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean index 649b69b637..8dc3d72828 100644 --- a/hott/algebra/category/functor.hlean +++ b/hott/algebra/category/functor.hlean @@ -155,6 +155,7 @@ namespace functor section local attribute precategory.is_hset_hom [priority 1001] + local attribute trunctype.struct [priority 1] -- remove after #842 is closed protected theorem is_hset_functor [instance] [HD : is_hset D] : is_hset (functor C D) := by apply is_trunc_equiv_closed; apply functor.sigma_char diff --git a/hott/algebra/category/limits.hlean b/hott/algebra/category/limits.hlean index a8d02104c4..c17256a8b1 100644 --- a/hott/algebra/category/limits.hlean +++ b/hott/algebra/category/limits.hlean @@ -7,7 +7,7 @@ Limits in a category -/ import .constructions.cone .constructions.discrete .constructions.product - .constructions.finite_cats .category + .constructions.finite_cats .category .constructions.functor open is_trunc functor nat_trans eq @@ -145,6 +145,10 @@ namespace category {h₂ : d ⟶ limit_object F} (q₂ : Πi, limit_morphism F i ∘ h₂ = η i): h₁ = h₂ := eq_hom_limit p q₁ ⬝ (eq_hom_limit p q₂)⁻¹ + definition limit_hom_limit {F G : I ⇒ D} (η : F ⟹ G) : limit_object F ⟶ limit_object G := + hom_limit _ (λi, η i ∘ limit_morphism F i) + abstract by intro i j f; rewrite [assoc,naturality,-assoc,limit_commute] end + omit H -- notation `noinstances` t:max := by+ with_options [elaborator.ignore_instances true] (exact t) diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean index 858554db28..3130cb2614 100644 --- a/hott/algebra/category/nat_trans.hlean +++ b/hott/algebra/category/nat_trans.hlean @@ -32,6 +32,8 @@ namespace nat_trans infixr ` ∘n `:60 := nat_trans.compose + definition compose_def (η : G ⟹ H) (θ : F ⟹ G) (c : C) : (η ∘n θ) c = η c ∘ θ c := idp + protected definition id [reducible] [constructor] {F : C ⇒ D} : nat_trans F F := mk (λa, id) (λa b f, !id_right ⬝ !id_left⁻¹) diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean index 4ad5a356ec..ee90e564f3 100644 --- a/hott/algebra/category/precategory.hlean +++ b/hott/algebra/category/precategory.hlean @@ -30,7 +30,7 @@ namespace category (id_id : Π (a : ob), comp !ID !ID = ID a) (is_hset_hom : Π(a b : ob), is_hset (hom a b)) - attribute precategory [multiple_instances] + -- attribute precategory [multiple-instances] --this is not used anywhere attribute precategory.is_hset_hom [instance] infixr ∘ := precategory.comp diff --git a/hott/algebra/category/strict.hlean b/hott/algebra/category/strict.hlean index 10941d3776..8446f0b52e 100644 --- a/hott/algebra/category/strict.hlean +++ b/hott/algebra/category/strict.hlean @@ -30,19 +30,19 @@ namespace category open functor - definition precat_strict_precat : precategory Strict_precategory := - precategory.mk (λ a b, functor a b) - (λ a b c g f, functor.compose g f) - (λ a, functor.id) - (λ a b c d h g f, !functor.assoc) - (λ a b f, !functor.id_left) - (λ a b f, !functor.id_right) + -- TODO: move to constructions.cat? + definition precategory_strict_precategory [constructor] : precategory Strict_precategory := + precategory.mk (λ A B, A ⇒ B) + (λ A B C G F, G ∘f F) + (λ A, 1) + (λ A B C D, functor.assoc) + (λ A B, functor.id_left) + (λ A B, functor.id_right) - definition Precat_of_strict_precats := precategory.Mk precat_strict_precat + definition Precategory_strict_precategory [constructor] := precategory.Mk precategory_strict_precategory namespace ops - abbreviation SPreCat := Precat_of_strict_precats - --attribute precat_strict_precat [instance] + abbreviation Cat := Precategory_strict_precategory end ops end category diff --git a/hott/algebra/category/yoneda.hlean b/hott/algebra/category/yoneda.hlean index 00152c60ec..bad454cf6c 100644 --- a/hott/algebra/category/yoneda.hlean +++ b/hott/algebra/category/yoneda.hlean @@ -2,16 +2,15 @@ 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 + +Yoneda embedding and Yoneda lemma -/ ---note: modify definition in category.set -import .constructions.functor .constructions.hset .constructions.product .constructions.opposite - .adjoint +import .curry .constructions.hset .constructions.opposite .adjoint -open category eq category.ops functor prod.ops is_trunc iso +open category eq functor prod.ops is_trunc iso is_equiv equiv category.set nat_trans lift namespace yoneda --- set_option class.conservative false definition representable_functor_assoc [C : Precategory] {a1 a2 a3 a4 a5 a6 : C} (f1 : hom a5 a6) (f2 : hom a4 a5) (f3 : hom a3 a4) (f4 : hom a2 a3) (f5 : hom a1 a2) @@ -22,7 +21,7 @@ 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 ⇒ set.{v} := + definition hom_functor.{u v} [constructor] (C : Precategory.{u v}) : Cᵒᵖ ×c C ⇒ cset.{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), @@ -30,175 +29,6 @@ namespace yoneda (λ 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)) -end yoneda - -open is_equiv equiv - -namespace functor - open prod nat_trans - variables {C D E : Precategory} (F : C ×c D ⇒ E) (G : C ⇒ E ^c D) - definition functor_curry_ob [reducible] [constructor] (c : C) : E ^c D := - functor.mk (λd, F (c,d)) - (λd d' g, F (id, g)) - (λd, !respect_id) - (λd₁ d₂ d₃ g' g, calc - F (id, g' ∘ g) = F (id ∘ id, g' ∘ g) : by rewrite id_id - ... = F ((id,g') ∘ (id, g)) : by esimp - ... = F (id,g') ∘ F (id, g) : by rewrite respect_comp) - - local abbreviation Fob := @functor_curry_ob - - definition functor_curry_hom [constructor] ⦃c c' : C⦄ (f : c ⟶ c') : Fob F c ⟹ Fob F c' := - begin - fapply @nat_trans.mk, - {intro d, exact F (f, id)}, - {intro d d' g, calc - F (id, g) ∘ F (f, id) = F (id ∘ f, g ∘ id) : respect_comp F - ... = F (f, g ∘ id) : by rewrite id_left - ... = F (f, g) : by rewrite id_right - ... = F (f ∘ id, g) : by rewrite id_right - ... = F (f ∘ id, id ∘ g) : by rewrite id_left - ... = F (f, id) ∘ F (id, g) : (respect_comp F (f, id) (id, g))⁻¹ᵖ - } - end - local abbreviation Fhom := @functor_curry_hom - - theorem functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) : - (Fhom F f) d = to_fun_hom F (f, id) := idp - - theorem functor_curry_id (c : C) : Fhom F (ID c) = nat_trans.id := - nat_trans_eq (λd, respect_id F _) - - theorem functor_curry_comp ⦃c c' c'' : C⦄ (f' : c' ⟶ c'') (f : c ⟶ c') - : Fhom F (f' ∘ f) = Fhom F f' ∘n Fhom F f := - begin - apply @nat_trans_eq, - intro d, calc - natural_map (Fhom F (f' ∘ f)) d = F (f' ∘ f, id) : by rewrite functor_curry_hom_def - ... = F (f' ∘ f, id ∘ id) : by rewrite id_id - ... = F ((f',id) ∘ (f, id)) : by esimp - ... = F (f',id) ∘ F (f, id) : by rewrite [respect_comp F] - ... = natural_map ((Fhom F f') ∘ (Fhom F f)) d : by esimp - end - - definition functor_curry [reducible] [constructor] : C ⇒ E ^c D := - functor.mk (functor_curry_ob F) - (functor_curry_hom F) - (functor_curry_id F) - (functor_curry_comp F) - - definition functor_uncurry_ob [reducible] (p : C ×c D) : E := - to_fun_ob (G p.1) p.2 - local abbreviation Gob := @functor_uncurry_ob - - definition functor_uncurry_hom ⦃p p' : C ×c D⦄ (f : hom p p') : Gob G p ⟶ Gob G p' := - to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2 - local abbreviation Ghom := @functor_uncurry_hom - - theorem functor_uncurry_id (p : C ×c D) : Ghom G (ID p) = id := - calc - Ghom G (ID p) = to_fun_hom (to_fun_ob G p.1) id ∘ natural_map (to_fun_hom G id) p.2 : by esimp - ... = id ∘ natural_map (to_fun_hom G id) p.2 : by rewrite respect_id - ... = id ∘ natural_map nat_trans.id p.2 : by rewrite respect_id - ... = id : id_id - - theorem functor_uncurry_comp ⦃p p' p'' : C ×c D⦄ (f' : p' ⟶ p'') (f : p ⟶ p') - : Ghom G (f' ∘ f) = Ghom G f' ∘ Ghom G f := - calc - Ghom G (f' ∘ f) - = to_fun_hom (to_fun_ob G p''.1) (f'.2 ∘ f.2) ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2 : by esimp - ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2) - ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2 : by rewrite respect_comp - ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2) - ∘ natural_map (to_fun_hom G f'.1 ∘ to_fun_hom G f.1) p.2 : by rewrite respect_comp - ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2) - ∘ (natural_map (to_fun_hom G f'.1) p.2 ∘ natural_map (to_fun_hom G f.1) p.2) : by esimp - ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ natural_map (to_fun_hom G f'.1) p'.2) - ∘ (to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2) : - by rewrite [square_prepostcompose (!naturality⁻¹ᵖ) _ _] - ... = Ghom G f' ∘ Ghom G f : by esimp - - definition functor_uncurry [reducible] [constructor] : C ×c D ⇒ E := - functor.mk (functor_uncurry_ob G) - (functor_uncurry_hom G) - (functor_uncurry_id G) - (functor_uncurry_comp G) - - theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := - functor_eq (λp, ap (to_fun_ob F) !prod.eta) - begin - intro cd cd' fg, - cases cd with c d, cases cd' with c' d', cases fg with f g, - transitivity to_fun_hom (functor_uncurry (functor_curry F)) (f, g), - apply id_leftright, - show (functor_uncurry (functor_curry F)) (f, g) = F (f,g), - from calc - (functor_uncurry (functor_curry F)) (f, g) = to_fun_hom F (id, g) ∘ to_fun_hom F (f, id) : by esimp - ... = F (id ∘ f, g ∘ id) : by krewrite [-respect_comp F (id,g) (f,id)] - ... = F (f, g ∘ id) : by rewrite id_left - ... = F (f,g) : by rewrite id_right, - end - - definition functor_curry_functor_uncurry_ob (c : C) - : functor_curry (functor_uncurry G) c = G c := - begin - fapply functor_eq, - {intro d, reflexivity}, - {intro d d' g, - apply concat, apply id_leftright, - show to_fun_hom (functor_curry (functor_uncurry G) c) g = to_fun_hom (G c) g, - from calc - to_fun_hom (functor_curry (functor_uncurry G) c) g - = to_fun_hom (G c) g ∘ natural_map (to_fun_hom G (ID c)) d : by esimp - ... = to_fun_hom (G c) g ∘ natural_map (ID (G c)) d : by rewrite respect_id - ... = to_fun_hom (G c) g ∘ id : by reflexivity - ... = to_fun_hom (G c) g : by rewrite id_right} - end - - theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G := - begin - fapply functor_eq, exact (functor_curry_functor_uncurry_ob G), - intro c c' f, - fapply nat_trans_eq, - intro d, - apply concat, - {apply (ap (λx, x ∘ _)), - apply concat, apply natural_map_hom_of_eq, apply (ap hom_of_eq), apply ap010_functor_eq}, - apply concat, - {apply (ap (λx, _ ∘ x)), apply (ap (λx, _ ∘ x)), - apply concat, apply natural_map_inv_of_eq, - apply (ap (λx, hom_of_eq x⁻¹)), apply ap010_functor_eq}, - apply concat, apply id_leftright, - apply concat, apply (ap (λx, x ∘ _)), apply respect_id, - apply id_left - end - - definition prod_functor_equiv_functor_functor [constructor] (C D E : Precategory) - : (C ×c D ⇒ E) ≃ (C ⇒ E ^c D) := - equiv.MK functor_curry - functor_uncurry - functor_curry_functor_uncurry - functor_uncurry_functor_curry - - - definition functor_prod_flip [constructor] (C D : Precategory) : C ×c D ⇒ D ×c C := - functor.mk (λp, (p.2, p.1)) - (λp p' h, (h.2, h.1)) - (λp, idp) - (λp p' p'' h' h, idp) - - definition functor_prod_flip_functor_prod_flip (C D : Precategory) - : functor_prod_flip D C ∘f (functor_prod_flip C D) = functor.id := - begin - fapply functor_eq, {intro p, apply prod.eta}, - intro p p' h, cases p with c d, cases p' with c' d', - apply id_leftright, - end -end functor -open functor - -namespace yoneda - open category.set nat_trans lift /- These attributes make sure that the fields of the category "set" reduce to the right things @@ -208,26 +38,26 @@ namespace yoneda local attribute Category.to.precategory category.to_precategory [constructor] -- should this be defined as "yoneda_embedding Cᵒᵖ"? - definition contravariant_yoneda_embedding [reducible] (C : Precategory) : Cᵒᵖ ⇒ set ^c C := + definition contravariant_yoneda_embedding [reducible] (C : Precategory) : Cᵒᵖ ⇒ cset ^c C := functor_curry !hom_functor - definition yoneda_embedding (C : Precategory) : C ⇒ set ^c Cᵒᵖ := + definition yoneda_embedding (C : Precategory) : C ⇒ cset ^c Cᵒᵖ := functor_curry (!hom_functor ∘f !functor_prod_flip) notation `ɏ` := yoneda_embedding _ - definition yoneda_lemma_hom [constructor] {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ set) + definition yoneda_lemma_hom [constructor] {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ cset) (x : trunctype.carrier (F c)) : ɏ c ⟹ F := begin fapply nat_trans.mk, { intro c', esimp [yoneda_embedding], intro f, exact F f x}, { intro c' c'' f, esimp [yoneda_embedding], apply eq_of_homotopy, intro f', refine _ ⬝ ap (λy, to_fun_hom F y x) !(@id_left _ C)⁻¹, - exact ap10 !(@respect_comp Cᵒᵖ set)⁻¹ x} + exact ap10 !(@respect_comp Cᵒᵖ cset)⁻¹ x} end definition yoneda_lemma_equiv [constructor] {C : Precategory} (c : C) - (F : Cᵒᵖ ⇒ set) : hom (ɏ c) F ≃ lift (F c) := + (F : Cᵒᵖ ⇒ cset) : hom (ɏ c) F ≃ lift (F c) := begin fapply equiv.MK, { intro η, exact up (η c id)}, @@ -241,13 +71,13 @@ namespace yoneda rewrite naturality, esimp [yoneda_embedding], rewrite [id_left], apply ap _ !id_left end end}, end - definition yoneda_lemma {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ set) : + definition yoneda_lemma {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ cset) : homset (ɏ c) F ≅ lift_functor (F c) := begin apply iso_of_equiv, esimp, apply yoneda_lemma_equiv, end - theorem yoneda_lemma_natural_ob {C : Precategory} (F : Cᵒᵖ ⇒ set) {c c' : C} (f : c' ⟶ c) + theorem yoneda_lemma_natural_ob {C : Precategory} (F : Cᵒᵖ ⇒ cset) {c c' : C} (f : c' ⟶ c) (η : ɏ c ⟹ F) : to_fun_hom (lift_functor ∘f F) f (to_hom (yoneda_lemma c F) η) = to_hom (yoneda_lemma c' F) (η ∘n to_fun_hom ɏ f) := @@ -266,7 +96,7 @@ namespace yoneda -- attribute yoneda_lemma lift_functor Precategory_hset precategory_hset homset -- yoneda_embedding nat_trans.compose functor_nat_trans_compose [reducible] -- attribute tlift functor.compose [reducible] - theorem yoneda_lemma_natural_functor.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ set) + theorem yoneda_lemma_natural_functor.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ cset) (θ : F ⟹ F') (η : to_fun_ob ɏ c ⟹ F) : (lift_functor.{v u} ∘fn θ) c (to_hom (yoneda_lemma c F) η) = proof to_hom (yoneda_lemma c F') (θ ∘n η) qed := @@ -285,7 +115,7 @@ namespace yoneda -- by reflexivity definition fully_faithful_yoneda_embedding [instance] (C : Precategory) : - fully_faithful (ɏ : C ⇒ set ^c Cᵒᵖ) := + fully_faithful (ɏ : C ⇒ cset ^c Cᵒᵖ) := begin intro c c', fapply is_equiv_of_equiv_of_homotopy, @@ -298,7 +128,7 @@ namespace yoneda end definition is_embedding_yoneda_embedding (C : Category) : - is_embedding (ɏ : C → Cᵒᵖ ⇒ set) := + is_embedding (ɏ : C → Cᵒᵖ ⇒ cset) := 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⁻¹ᵉ}, @@ -311,15 +141,16 @@ namespace yoneda rewrite [category.category.id_left], apply id_right} end - definition is_representable {C : Precategory} (F : Cᵒᵖ ⇒ set) := Σ(c : C), ɏ c ≅ F + definition is_representable {C : Precategory} (F : Cᵒᵖ ⇒ cset) := Σ(c : C), ɏ c ≅ F - definition is_hprop_representable {C : Category} (F : Cᵒᵖ ⇒ set) + 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 _, rotate 1, - { apply sigma.sigma_equiv_sigma_id, intro c, exact !eq_equiv_iso}, - { apply fiber.sigma_char}}, + { 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} end diff --git a/hott/function.hlean b/hott/function.hlean index 2def10b9a5..acb45aaae1 100644 --- a/hott/function.hlean +++ b/hott/function.hlean @@ -225,7 +225,8 @@ namespace function ... = a : left_inverse) section - local attribute is_equiv_of_is_section_of_is_retraction [instance] + local attribute is_equiv_of_is_section_of_is_retraction [instance] [priority 10000] + local attribute trunctype.struct [priority 1] -- remove after #842 is closed variable (f) definition is_hprop_is_retraction_prod_is_section : is_hprop (is_retraction f × is_section f) := begin diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 05bd6e85d0..ae23aa3ed0 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -308,7 +308,7 @@ namespace is_trunc structure trunctype (n : trunc_index) := (carrier : Type) (struct : is_trunc n carrier) attribute trunctype.carrier [coercion] - attribute trunctype.struct [instance] + attribute trunctype.struct [instance] [priority 1400] notation n `-Type` := trunctype n abbreviation hprop := -1-Type