From 71f9a5d1d29d9bd3ce39b0f08372900d7f1b3c6d Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 13 Mar 2015 10:32:48 -0400 Subject: [PATCH] feat(hott/algebra/precategory): do lots of stuff with categories --- hott/algebra/category/basic.hlean | 9 +- hott/algebra/category/constructions.hlean | 57 ++++++- hott/algebra/precategory/basic.hlean | 3 +- hott/algebra/precategory/constructions.hlean | 57 ++++++- hott/algebra/precategory/functor.hlean | 166 +++++++++++++++++-- hott/algebra/precategory/iso.hlean | 32 +++- hott/algebra/precategory/yoneda.hlean | 128 +++++++------- hott/init/axioms/funext_of_ua.hlean | 9 +- hott/init/axioms/ua.hlean | 4 + hott/init/path.hlean | 3 + 10 files changed, 373 insertions(+), 95 deletions(-) diff --git a/hott/algebra/category/basic.hlean b/hott/algebra/category/basic.hlean index 1e651688ca..ce7bb5a568 100644 --- a/hott/algebra/category/basic.hlean +++ b/hott/algebra/category/basic.hlean @@ -14,9 +14,11 @@ open iso is_equiv eq is_trunc -- that the function from paths to isomorphisms, -- is an equivalecnce. namespace category + definition is_univalent [reducible] {ob : Type} (C : precategory ob) := + Π(a b : ob), is_equiv (@iso_of_eq ob C a b) structure category [class] (ob : Type) extends parent : precategory ob := - (iso_of_path_equiv : Π (a b : ob), is_equiv (@iso_of_eq ob parent a b)) + (iso_of_path_equiv : is_univalent parent) attribute category [multiple-instances] @@ -34,7 +36,7 @@ namespace category -- TODO: Unsafe class instance? attribute iso_of_path_equiv [instance] - definition eq_of_iso (a b : ob) : a ≅ b → a = b := + definition eq_of_iso {a b : ob} : a ≅ b → a = b := iso_of_eq⁻¹ᵉ set_option apply.class_instance false -- disable class instance resolution in the apply tactic @@ -64,8 +66,7 @@ namespace category definition category.Mk [reducible] := Category.mk definition category.MK [reducible] (C : Precategory) - (H : Π (a b : C), is_equiv (@iso_of_eq C C a b)) : Category := - Category.mk C (category.mk' C C H) + (H : is_univalent C) : Category := Category.mk C (category.mk' C C H) definition Category.eta (C : Category) : Category.mk C C = C := Category.rec (λob c, idp) C diff --git a/hott/algebra/category/constructions.hlean b/hott/algebra/category/constructions.hlean index b04d12ddaf..8115b37df1 100644 --- a/hott/algebra/category/constructions.hlean +++ b/hott/algebra/category/constructions.hlean @@ -59,7 +59,7 @@ namespace category definition equiv_eq_iso (A B : Precategory_hset) : (A ≃ B) = (A ≅ B) := ua !equiv_equiv_iso - definition is_univalent (A B : Precategory_hset) : is_equiv (@iso_of_eq _ _ A B) := + definition is_univalent_hset (A B : Precategory_hset) : is_equiv (@iso_of_eq _ _ A B) := have 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 _ _ _ _ _ @@ -74,7 +74,7 @@ namespace category end set definition category_hset [reducible] [instance] : category hset := - category.mk' hset precategory_hset set.is_univalent + category.mk' hset precategory_hset set.is_univalent_hset definition Category_hset [reducible] : Category := Category.mk hset category_hset @@ -83,4 +83,57 @@ namespace category abbreviation set := Category_hset end ops + section functor + open functor nat_trans + + variables {C : Precategory} {D : Category} {F G : D ^c C} + definition eq_of_iso_functor_ob (η : F ≅ G) (c : C) : F c = G c := + by apply eq_of_iso; apply componentwise_iso; exact η + + + definition eq_of_iso_functor (η : F ≅ G) : F = G := + begin + fapply functor_eq_mk, + {exact (eq_of_iso_functor_ob η)}, + {intros (c, c', f), + apply concat, + {apply (ap (λx, to_hom x ∘ to_fun_hom F f ∘ _)), apply (retr iso_of_eq)}, + apply concat, + {apply (ap (λx, _ ∘ to_fun_hom F f ∘ (to_hom x)⁻¹)), apply (retr iso_of_eq)}, + apply inverse, apply naturality_iso} + end + + --the following error is a bug? + -- definition is_univalent_functor (C : Precategory) (D : Category) : is_univalent (D ^c C) := + -- λ(F G : D ^c C), adjointify _ eq_of_iso_functor sorry sorry + +-- definition iso_of_hom + + definition iso_of_eq_eq_of_iso_functor (η : F ≅ G) : iso_of_eq (eq_of_iso_functor η) = η := + begin + apply iso.eq_mk, + apply nat_trans_eq_mk, + intro c, + apply concat, apply natural_map_hom_of_eq, + apply concat, {apply (ap hom_of_eq), apply ap010_functor_eq_mk}, + apply concat, {apply (ap to_hom), apply (retr iso_of_eq)}, + apply idp + end +--check natural_map_ + definition eq_of_iso_functor_iso_of_eq (p : F = G) : eq_of_iso_functor (iso_of_eq p) = p := + begin + apply sorry + end + + definition is_univalent_functor (C : Precategory) (D : Category) : is_univalent (D ^c C) := + λF G, adjointify _ eq_of_iso_functor + iso_of_eq_eq_of_iso_functor + eq_of_iso_functor_iso_of_eq + + end functor + + + definition category_functor (C : Precategory) (D : Category) : Category := + category.MK (D ^c C) (is_univalent_functor C D) + end category diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean index 27bded3b96..17131420ba 100644 --- a/hott/algebra/precategory/basic.hlean +++ b/hott/algebra/precategory/basic.hlean @@ -47,6 +47,8 @@ namespace category definition id_comp (a : ob) : ID a ∘ ID a = ID a := !id_left + definition id_leftright (f : hom a b) : id ∘ f ∘ id = f := !id_left ⬝ !id_right + definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id := calc i = i ∘ id : by rewrite id_right ... = id : by rewrite H @@ -61,7 +63,6 @@ namespace category definition is_hprop_eq_hom [instance] : is_hprop (f = f') := !is_trunc_eq - end basic_lemmas context squares parameters {ob : Type} [C : precategory ob] diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean index 7f8bcba297..67dd3e3c23 100644 --- a/hott/algebra/precategory/constructions.hlean +++ b/hott/algebra/precategory/constructions.hlean @@ -151,7 +151,7 @@ namespace category definition Precategory_hset [reducible] : Precategory := Precategory.mk hset precategory_hset - section precategory_functor + section open iso functor nat_trans definition precategory_functor [instance] [reducible] (D C : Precategory) : precategory (functor C D) := @@ -168,7 +168,13 @@ namespace category -- definition Precategory_functor_rev [reducible] (C D : Precategory) : Precategory := -- Precategory_functor D C + end + namespace ops + infixr `^c`:35 := Precategory_functor + end ops + section + open iso functor nat_trans /- we prove that if a natural transformation is pointwise an to_fun, then it is an to_fun -/ variables {C D : Precategory} {F G : C ⇒ D} (η : F ⟹ G) [iso : Π(a : C), is_iso (η a)] include iso @@ -199,13 +205,56 @@ namespace category apply is_hset.elim end - definition nat_trans_iso.mk : is_iso η := + definition is_iso_nat_trans : is_iso η := is_iso.mk (nat_trans_left_inverse η) (nat_trans_right_inverse η) - end precategory_functor + omit iso + -- local attribute is_iso_nat_trans [instance] + -- definition functor_iso_functor (H : Π(a : C), F a ≅ G a) : F ≅ G := -- is this true? + -- iso.mk _ + end + + section + open iso functor category.ops nat_trans iso.iso + /- and conversely, if a natural transformation is an iso, it is componentwise an iso -/ + variables {C D : Precategory} {F G : D ^c C} (η : hom F G) [isoη : is_iso η] (c : C) + include isoη + definition componentwise_is_iso : is_iso (η c) := + @is_iso.mk _ _ _ _ _ (natural_map η⁻¹ c) (ap010 natural_map ( left_inverse η) c) + (ap010 natural_map (right_inverse η) c) + + local attribute componentwise_is_iso [instance] + + definition natural_map_inverse : natural_map η⁻¹ c = (η c)⁻¹ := idp + + definition naturality_iso {c c' : C} (f : c ⟶ c') : G f = η c' ∘ F f ∘ (η c)⁻¹ := + calc + G f = (G f ∘ η c) ∘ (η c)⁻¹ : comp_inverse_cancel_right + ... = (η c' ∘ F f) ∘ (η c)⁻¹ : {naturality η f} + ... = η c' ∘ F f ∘ (η c)⁻¹ : assoc + + definition naturality_iso' {c c' : C} (f : c ⟶ c') : (η c')⁻¹ ∘ G f ∘ η c = F f := + calc + (η c')⁻¹ ∘ G f ∘ η c = (η c')⁻¹ ∘ η c' ∘ F f : {naturality η f} + ... = F f : inverse_comp_cancel_left + + 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) + + definition natural_map_hom_of_eq (p : F = G) (c : C) + : natural_map (hom_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c) := + eq.rec_on p idp + + definition natural_map_inv_of_eq (p : F = G) (c : C) + : natural_map (inv_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c)⁻¹ := + eq.rec_on p idp + + end namespace ops - infixr `^c`:35 := Precategory_functor infixr `×f`:30 := product.prod_functor infixr `ᵒᵖᶠ`:(max+1) := opposite.opposite_functor end ops diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean index 0a0d867034..15d1dffab0 100644 --- a/hott/algebra/precategory/functor.hlean +++ b/hott/algebra/precategory/functor.hlean @@ -6,11 +6,96 @@ Module: algebra.precategory.functor Authors: Floris van Doorn, Jakob von Raumer -/ -import .basic types.pi +import .basic types.pi .iso -open function category eq prod equiv is_equiv sigma sigma.ops is_trunc funext +open function category eq prod equiv is_equiv sigma sigma.ops is_trunc funext iso open pi + + + + section + + variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} + + definition homotopy2 [reducible] (f g : Πa b, C a b) : Type := + Πa b, f a b = g a b + + definition homotopy3 [reducible] (f g : Πa b c, D a b c) : Type := + Πa b c, f a b c = g a b c + notation f `∼2`:50 g := homotopy2 f g + notation f `∼3`:50 g := homotopy3 f g + + -- definition apD100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g := + -- λa b, eq.rec_on p idp + + definition apD100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g := + λa b, apD10 (apD10 p a) b + + definition apD1000 {f g : Πa b c, D a b c} (p : f = g) : f ∼3 g := + λa b c, apD100 (apD10 p a) b c + + definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ∼2 g) : f = g := + eq_of_homotopy (λa, eq_of_homotopy (H a)) + + definition eq_of_homotopy3 {f g : Πa b c, D a b c} (H : f ∼3 g) : f = g := + eq_of_homotopy (λa, eq_of_homotopy2 (H a)) + + definition eq_of_homotopy2_id (f : Πa b, C a b) + : eq_of_homotopy2 (λa b, idpath (f a b)) = idpath f := + begin + apply concat, + {apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy_id}, + apply eq_of_homotopy_id + end + + definition eq_of_homotopy3_id (f : Πa b c, D a b c) + : eq_of_homotopy3 (λa b c, idpath (f a b c)) = idpath f := + begin + apply concat, + {apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy2_id}, + apply eq_of_homotopy_id + end + + --TODO: put in namespace funext + definition is_equiv_apD100 [instance] (f g : Πa b, C a b) : is_equiv (@apD100 A B C f g) := + adjointify _ + eq_of_homotopy2 + begin + intro H, esimp {apD100,eq_of_homotopy2, function.compose}, + apply eq_of_homotopy, intro a, + apply concat, apply (ap (λx, @apD10 _ (λb : B a, _) _ _ (x a))), apply (retr apD10), +--TODO: remove implicit argument after #469 is closed + apply (retr apD10) + end + begin + intro p, cases p, apply eq_of_homotopy2_id + end + + definition is_equiv_apD1000 [instance] (f g : Πa b c, D a b c) : is_equiv (@apD1000 A B C D f g) := + adjointify _ + eq_of_homotopy3 + begin + intro H, apply eq_of_homotopy, intro a, + apply concat, {apply (ap (λx, @apD100 _ _ (λ(b : B a)(c : C a b), _) _ _ (x a))), apply (retr apD10)}, +--TODO: remove implicit argument after #469 is closed + apply (@retr _ _ apD100 !is_equiv_apD100) --is explicit argument needed here? + end + begin + intro p, cases p, apply eq_of_homotopy3_id + end + + protected definition homotopy2.rec_on {f g : Πa b, C a b} {P : (f ∼2 g) → Type} + (p : f ∼2 g) (H : Π(q : f = g), P (apD100 q)) : P p := + retr apD100 p ▹ H (eq_of_homotopy2 p) + + protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f ∼3 g) → Type} + (p : f ∼3 g) (H : Π(q : f = g), P (apD1000 q)) : P p := + retr apD1000 p ▹ H (eq_of_homotopy3 p) + end + + + structure functor (C D : Precategory) : Type := (to_fun_ob : C → D) (to_fun_hom : Π ⦃a b : C⦄, hom a b → hom (to_fun_ob a) (to_fun_ob b)) @@ -53,22 +138,23 @@ namespace functor apD01111 functor.mk pF pH !is_hprop.elim !is_hprop.elim definition functor_eq_mk' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)} - {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) - (pF : F₁ ∼ F₂) (pH : Π(a b : C) (f : hom a b), eq_of_homotopy pF ▹ (H₁ a b f) = H₂ a b f) + {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ ∼ F₂) + (pH : Π(a b : C) (f : hom a b), hom_of_eq (pF b) ∘ H₁ a b f ∘ inv_of_eq (pF a) = H₂ a b f) : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ := functor_eq_mk'' id₁ id₂ comp₁ comp₂ (eq_of_homotopy pF) (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (λf, begin - apply concat, rotate_left 1, exact (pH c c' f), - apply concat, rotate_left 1, - exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c c') f), - apply (apD10' f), - apply concat, rotate_left 1, - exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c) c'), - apply (apD10' c'), - apply concat, rotate_left 1, - exact (pi_transport_constant (eq_of_homotopy pF) H₁ c), - apply idp + apply concat, rotate_left 1, exact (pH c c' f), + apply concat, rotate_left 1, apply transport_hom, + apply concat, rotate_left 1, + exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c c') f), + apply (apD10' f), + apply concat, rotate_left 1, + exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c) c'), + apply (apD10' c'), + apply concat, rotate_left 1, + exact (pi_transport_constant (eq_of_homotopy pF) H₁ c), + apply idp end)))) definition functor_eq_mk_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)} @@ -79,8 +165,7 @@ namespace functor (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (pH c c')))) definition functor_eq_mk {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ∼ to_fun_ob F₂), - (Π(a b : C) (f : hom a b), transport (λF, hom (F a) (F b)) (eq_of_homotopy p) (F₁ f) = F₂ f) - → F₁ = F₂ := + (Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) → F₁ = F₂ := functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_eq_mk')) protected definition assoc {A B C D : Precategory} (H : functor C D) (G : functor B C) (F : functor A B) : @@ -136,8 +221,55 @@ namespace functor apply is_trunc_eq, apply is_trunc_succ, apply !homH}, end -end functor + --set_option pp.universes true + -- set_option pp.notation false + -- set_option pp.implicit true + definition functor_eq2' {obF obF' : C → D} {homF homF' idF idF' compF compF'} + (p q : functor.mk obF homF idF compF = functor.mk obF' homF' idF' compF') (r : obF = obF') + : p = q := + begin + cases r, + end + definition functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ∼ ap010 to_fun_ob q) + : p = q := + begin + + end + + -- definition ap010_functor_eq_mk' {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ = to_fun_ob F₂) + -- (q : p ▹ F₁ = F₂) (c : C) : + -- ap to_fun_ob (functor_eq_mk (apD10 p) (λa b f, _)) = p := sorry + -- begin + -- cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros (p, q), + -- cases p, clears (e_1, e_2), + -- end + + -- TODO: remove sorry + -- maybe some lemma "recursion on homotopy (and equiv)" could be useful + definition ap010_functor_eq_mk {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ∼ to_fun_ob F₂) + (q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) ∼3 to_fun_hom F₂) (c : C) : + ap010 to_fun_ob (functor_eq_mk p q) c = p c := + begin + cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros (p, q), + apply sorry, + --cases p, clears (e_1, e_2, p), + + --exact (homotopy3.rec_on q sorry) +-- apply (homotopy3.rec_on q), + end + + -- definition ap010_functor_eq_mk {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ∼ to_fun_ob F₂) + -- (q : Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) (c : C) : + -- ap010 to_fun_ob (functor_eq_mk p q) c = p c := + -- begin + -- cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros (p, q), + -- cases p, clears (e_1, e_2, p), + -- apply (homotopy3.rec_on q), + -- end +-- ⊢ ap010 to_fun_ob (functor_eq_mk rfl q) c = rfl + +end functor namespace category open functor diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean index dbfa64e926..cf946838f5 100644 --- a/hott/algebra/precategory/iso.hlean +++ b/hott/algebra/precategory/iso.hlean @@ -191,7 +191,37 @@ namespace iso end definition iso_of_eq (p : a = b) : a ≅ b := - eq.rec_on p (iso.mk id) + eq.rec_on p (iso.refl a) + + definition hom_of_eq (p : a = b) : a ⟶ b := + iso.to_hom (iso_of_eq p) + + definition inv_of_eq (p : a = b) : b ⟶ a := + iso.to_inv (iso_of_eq p) + + definition iso_of_eq_inv (p : a = b) : iso_of_eq p⁻¹ = iso.symm (iso_of_eq p) := + eq.rec_on p idp + + definition iso_of_eq_con (p : a = b) (q : b = c) + : iso_of_eq (p ⬝ q) = iso.trans (iso_of_eq p) (iso_of_eq q) := + eq.rec_on q (eq.rec_on p (iso.eq_mk !id_comp⁻¹)) + + + section + open funext + variables {X : Type} {x y : X} {F G : X → ob} + definition transport_hom_of_eq (p : F = G) (f : hom (F x) (F y)) + : p ▹ f = hom_of_eq (apD10 p y) ∘ f ∘ inv_of_eq (apD10 p x) := + eq.rec_on p !id_leftright⁻¹ + + definition transport_hom (p : F ∼ G) (f : hom (F x) (F y)) + : eq_of_homotopy p ▹ f = hom_of_eq (p y) ∘ f ∘ inv_of_eq (p x) := + calc + eq_of_homotopy p ▹ f = + hom_of_eq (apD10 (eq_of_homotopy p) y) ∘ f ∘ inv_of_eq (apD10 (eq_of_homotopy p) x) + : transport_hom_of_eq + ... = hom_of_eq (p y) ∘ f ∘ inv_of_eq (p x) : {retr apD10 p} + end structure mono [class] (f : a ⟶ b) := (elim : ∀c (g h : hom c a), f ∘ g = f ∘ h → g = h) diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean index c94a474cb7..0d7a8f3ce8 100644 --- a/hott/algebra/precategory/yoneda.hlean +++ b/hott/algebra/precategory/yoneda.hlean @@ -9,7 +9,7 @@ Authors: Floris van Doorn --note: modify definition in category.set import algebra.category.constructions .iso -open category eq category.ops functor prod.ops is_trunc +open category eq category.ops functor prod.ops is_trunc iso set_option pp.beta true namespace yoneda @@ -67,7 +67,7 @@ namespace functor local abbreviation Fhom := @functor_curry_hom - definition functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) : + 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 := @@ -125,84 +125,88 @@ namespace functor functor.mk (functor_uncurry_ob G) (functor_uncurry_hom G) (functor_uncurry_id G) - (functor_uncurry_comp G) - -- open pi - -- definition functor_eq_mk'1 {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)} - -- {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) - -- (pF : F₁ = F₂) (pH : Π(a b : C) (f : hom a b), pF ▹ (H₁ a b f) = H₂ a b f) - -- : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ := - -- functor_eq_mk'' id₁ id₂ comp₁ comp₂ pF - -- (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (λf, - -- begin - -- apply concat, rotate_left 1, exact (pH c c' f), - -- apply concat, rotate_left 1, - -- exact (pi_transport_constant pF (H₁ c c') f), - -- apply (apD10' f), - -- apply concat, rotate_left 1, - -- exact (pi_transport_constant pF (H₁ c) c'), - -- apply (apD10' c'), - -- apply concat, rotate_left 1, - -- exact (pi_transport_constant pF H₁ c), - -- apply idp - -- end)))) - -- definition functor_eq_mk1 {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ = to_fun_ob F₂), - -- (Π(a b : C) (f : hom a b), transport (λF, hom (F a) (F b)) p (F₁ f) = F₂ f) - -- → F₁ = F₂ := - -- functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_eq_mk'1)) - - --set_option pp.notation false - definition functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := + theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := functor_eq_mk (λp, ap (to_fun_ob F) !prod.eta) begin intros (cd, cd', fg), cases cd with (c,d), cases cd' with (c',d'), cases fg with (f,g), - have H : (functor_uncurry (functor_curry F)) (f, g) = F (f,g), + apply concat, 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) : respect_comp F (id,g) (f,id) - ... = F (f, g ∘ id) : by rewrite id_left - ... = F (f,g) : by rewrite id_right, - rewrite H, - apply sorry - end - --set_option pp.implicit true - definition functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G := - begin - fapply functor_eq_mk, - {intro c, - fapply functor_eq_mk, - {intro d, apply idp}, - {intros (d, d', g), - have H : 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_right, - rewrite H, - -- esimp {idp}, - apply sorry - } - }, - apply sorry + ... = F (f, g ∘ id) : by rewrite id_left + ... = F (f,g) : by rewrite id_right, end - definition equiv_functor_curry : (C ×c D ⇒ E) ≃ (C ⇒ E ^c D) := + definition functor_curry_functor_uncurry_ob (c : C) + : functor_curry (functor_uncurry G) c = G c := + begin + fapply functor_eq_mk, + {intro d, apply idp}, + {intros (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_right} + end + + theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G := + begin + fapply functor_eq_mk, exact (functor_curry_functor_uncurry_ob G), + intros (c, c', f), + fapply nat_trans_eq_mk, + 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_mk}, + 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_mk}, + apply concat, apply id_leftright, + apply concat, apply (ap (λx, x ∘ _)), apply respect_id, + apply id_left + end + + definition prod_functor_equiv_functor_functor (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_ob : C ×c D ⇒ D ×c C := - functor.mk sorry sorry sorry sorry - - - definition contravariant_yoneda_embedding : Cᵒᵖ ⇒ set ^c C := - functor_curry !yoneda.hom_functor + definition functor_prod_flip (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_mk, {intro p, apply prod.eta}, + intros (p, p', h), cases p with (c, d), cases p' with (c', d'), + apply id_leftright, + end end functor +open functor + +namespace yoneda + -- or should this be defined as "yoneda_embedding Cᵒᵖ"? + definition contravariant_yoneda_embedding (C : Precategory) : Cᵒᵖ ⇒ set ^c C := + functor_curry !hom_functor + + definition yoneda_embedding (C : Precategory) : C ⇒ set ^c Cᵒᵖ := + functor_curry (!hom_functor ∘f !functor_prod_flip) + +end yoneda -- Coq uses unit/counit definitions as basic diff --git a/hott/init/axioms/funext_of_ua.hlean b/hott/init/axioms/funext_of_ua.hlean index f0283bb89f..d4095e6d32 100644 --- a/hott/init/axioms/funext_of_ua.hlean +++ b/hott/init/axioms/funext_of_ua.hlean @@ -149,13 +149,14 @@ equiv.mk apD10 _ definition eq_of_homotopy {A : Type} {P : A → Type} {f g : Π x, P x} : f ∼ g → f = g := (@apD10 A P f g)⁻¹ +--rename to eq_of_homotopy_idp definition eq_of_homotopy_id {A : Type} {P : A → Type} (f : Π x, P x) : eq_of_homotopy (λx : A, idpath (f x)) = idpath f := is_equiv.sect apD10 idp -definition eq_of_homotopy2 {A B : Type} {P : A → B → Type} - (f g : Πx y, P x y) : (Πx y, f x y = g x y) → f = g := -λ E, eq_of_homotopy (λx, eq_of_homotopy (E x)) - definition naive_funext_of_ua : naive_funext := λ A P f g h, eq_of_homotopy h + +protected definition homotopy.rec_on {A : Type} {B : A → Type} {f g : Πa, B a} {P : (f ∼ g) → Type} + (p : f ∼ g) (H : Π(q : f = g), P (apD10 q)) : P p := +retr apD10 p ▹ H (eq_of_homotopy p) diff --git a/hott/init/axioms/ua.hlean b/hott/init/axioms/ua.hlean index e3626c3d61..8f5a2f20f6 100644 --- a/hott/init/axioms/ua.hlean +++ b/hott/init/axioms/ua.hlean @@ -44,4 +44,8 @@ namespace equiv -- We can use this for calculation evironments calc_subst transport_of_equiv + definition rec_on_of_equiv_of_eq {A B : Type} {P : (A ≃ B) → Type} + (p : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P p := + retr equiv_of_eq p ▹ H (ua p) + end equiv diff --git a/hott/init/path.hlean b/hott/init/path.hlean index fc3d6eac06..9c74d21769 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -660,6 +660,9 @@ namespace eq definition ap01111 (f : A → B → C → D → E) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') : f a b c d = f a' b' c' d' := eq.rec_on Ha (ap0111 (f a) Hb Hc Hd) + + definition ap010 {C : B → Type} (f : A → Π(b : B), C b) (Ha : a = a') (b : B) : f a b = f a' b := + eq.rec_on Ha idp end section variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}