From 6e23305c5d0c41884cb982f1984328051dbdeec2 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 22 Sep 2015 13:11:33 -0400 Subject: [PATCH] feat(category): define terminal, initial, indiscrete and sum category --- hott/algebra/category/adjoint.hlean | 45 +++++++++++--- .../category/constructions/indiscrete.hlean | 31 ++++++++++ .../category/constructions/initial.hlean | 47 ++++++++++++++ .../category/constructions/opposite.hlean | 11 ++-- .../category/constructions/product.hlean | 11 ++-- hott/algebra/category/constructions/sum.hlean | 61 +++++++++++++++++++ .../category/constructions/terminal.hlean | 57 +++++++++++++++++ hott/algebra/category/functor.hlean | 23 +++---- hott/algebra/category/yoneda.hlean | 41 ++++++++++--- 9 files changed, 285 insertions(+), 42 deletions(-) create mode 100644 hott/algebra/category/constructions/indiscrete.hlean create mode 100644 hott/algebra/category/constructions/initial.hlean create mode 100644 hott/algebra/category/constructions/sum.hlean create mode 100644 hott/algebra/category/constructions/terminal.hlean diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean index 4a92ff589..831b9ed72 100644 --- a/hott/algebra/category/adjoint.hlean +++ b/hott/algebra/category/adjoint.hlean @@ -58,10 +58,14 @@ namespace category infix `⋍`:25 := equivalence -- \backsimeq or \equiv infix `≌`:25 := isomorphism -- \backcong or \iso - definition is_equiv_of_fully_faithful [instance] (F : C ⇒ D) [H : fully_faithful F] (c c' : C) - : is_equiv (@(to_fun_hom F) c c') := + definition is_equiv_of_fully_faithful [instance] [reducible] (F : C ⇒ D) [H : fully_faithful F] + (c c' : C) : is_equiv (@(to_fun_hom F) c c') := !H + definition hom_inv [reducible] (F : C ⇒ D) [H : fully_faithful F] (c c' : C) (f : F c ⟶ F c') + : c ⟶ c' := + (to_fun_hom F)⁻¹ᶠ f + definition hom_equiv_F_hom_F [constructor] (F : C ⇒ D) [H : fully_faithful F] (c c' : C) : (c ⟶ c') ≃ (F c ⟶ F c') := equiv.mk _ !H @@ -70,17 +74,17 @@ namespace category [H : fully_faithful F] (c c' : C) (g : F c ≅ F c') : c ≅ c' := begin induction g with g G, induction G with h p q, fapply iso.MK, - { rexact (@(to_fun_hom F) c c')⁻¹ᶠ g}, - { rexact (@(to_fun_hom F) c' c)⁻¹ᶠ h}, + { rexact (to_fun_hom F)⁻¹ᶠ g}, + { rexact (to_fun_hom F)⁻¹ᶠ h}, { exact abstract begin - apply eq_of_fn_eq_fn' (@(to_fun_hom F) c c), + apply eq_of_fn_eq_fn' (to_fun_hom F), rewrite [respect_comp, respect_id, - right_inv (@(to_fun_hom F) c c'), right_inv (@(to_fun_hom F) c' c), p], + right_inv (to_fun_hom F), right_inv (to_fun_hom F), p], end end}, { exact abstract begin - apply eq_of_fn_eq_fn' (@(to_fun_hom F) c' c'), + apply eq_of_fn_eq_fn' (to_fun_hom F), rewrite [respect_comp, respect_id, - right_inv (@(to_fun_hom F) c c'), right_inv (@(to_fun_hom F) c' c), q], + right_inv (to_fun_hom F), right_inv (@(to_fun_hom F) c' c), q], end end} end @@ -197,6 +201,31 @@ namespace category { exact componentwise_iso (@(iso.mk (counit F)) !is_iso_counit) d} end + definition reflect_is_iso [constructor] (F : C ⇒ D) [H : fully_faithful F] {c c' : C} (f : c ⟶ c') + [H : is_iso (F f)] : is_iso f := + begin + fconstructor, + { exact (to_fun_hom F)⁻¹ᶠ (F f)⁻¹}, + { apply eq_of_fn_eq_fn' (to_fun_hom F), + rewrite [respect_comp,right_inv (to_fun_hom F),respect_id,left_inverse]}, + { apply eq_of_fn_eq_fn' (to_fun_hom F), + rewrite [respect_comp,right_inv (to_fun_hom F),respect_id,right_inverse]}, + end + + definition reflect_iso [constructor] (F : C ⇒ D) [H : fully_faithful F] {c c' : C} + (f : F c ≅ F c') : c ≅ c' := + begin + fconstructor, + { exact (to_fun_hom F)⁻¹ᶠ f}, + { assert H : is_iso (F ((to_fun_hom F)⁻¹ᶠ f)), + { have H' : is_iso (to_hom f), from _, exact (right_inv (to_fun_hom F) (to_hom f))⁻¹ ▸ H'}, + exact reflect_is_iso F _}, + end + + theorem reflect_inverse (F : C ⇒ D) [H : fully_faithful F] {c c' : C} (f : c ⟶ c') + [H : is_iso f] : (to_fun_hom F)⁻¹ᶠ (F f)⁻¹ = f⁻¹ := + inverse_eq_inverse (idp : to_hom (@(iso.mk f) (reflect_is_iso F f)) = f) + /- section variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d) -- we need some kind of naturality diff --git a/hott/algebra/category/constructions/indiscrete.hlean b/hott/algebra/category/constructions/indiscrete.hlean new file mode 100644 index 000000000..4d1bcdbca --- /dev/null +++ b/hott/algebra/category/constructions/indiscrete.hlean @@ -0,0 +1,31 @@ +/- +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 + +Indiscrete category +-/ + +import .opposite + +open functor is_trunc unit eq + +namespace category + + variable (X : Type) + + definition indiscrete_precategory [constructor] : precategory X := + precategory.mk (λx y, unit) + (λx y z f g, star) + (λx, star) + (λx y z w f g h, idp) + (λx y f, by induction f; reflexivity) + (λx y f, by induction f; reflexivity) + + definition Indiscrete_precategory [constructor] : Precategory := + precategory.Mk (indiscrete_precategory X) + + definition indiscrete_op : (Indiscrete_precategory X)ᵒᵖ = Indiscrete_precategory X := idp + +end category diff --git a/hott/algebra/category/constructions/initial.hlean b/hott/algebra/category/constructions/initial.hlean new file mode 100644 index 000000000..109e93a9e --- /dev/null +++ b/hott/algebra/category/constructions/initial.hlean @@ -0,0 +1,47 @@ +/- +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 + +Initial category +-/ + +import .indiscrete + +open functor is_trunc eq + +namespace category + + definition initial_precategory [constructor] : precategory empty := + indiscrete_precategory empty + + definition Initial_precategory [constructor] : Precategory := + precategory.Mk initial_precategory + + notation 0 := Initial_precategory + definition zero_op : 0ᵒᵖ = 0 := idp + + definition initial_functor [constructor] (C : Precategory) : 0 ⇒ C := + functor.mk (λx, empty.elim x) + (λx y f, empty.elim x) + (λx, empty.elim x) + (λx y z g f, empty.elim x) + + definition is_contr_zero_functor [instance] (C : Precategory) : is_contr (0 ⇒ C) := + is_contr.mk (initial_functor C) + begin + intro F, fapply functor_eq, + { intro x, exact empty.elim x}, + { intro x y f, exact empty.elim x} + end + + definition initial_functor_op (C : Precategory) + : (initial_functor C)ᵒᵖ = initial_functor Cᵒᵖ := + by apply @is_hprop.elim (0 ⇒ Cᵒᵖ) + + definition initial_functor_comp {C D : Precategory} (F : C ⇒ D) + : F ∘f initial_functor C = initial_functor D := + by apply @is_hprop.elim (0 ⇒ D) + +end category diff --git a/hott/algebra/category/constructions/opposite.hlean b/hott/algebra/category/constructions/opposite.hlean index a83fbb3ac..32ab9f087 100644 --- a/hott/algebra/category/constructions/opposite.hlean +++ b/hott/algebra/category/constructions/opposite.hlean @@ -12,7 +12,7 @@ open eq functor namespace category - definition opposite [reducible] {ob : Type} (C : precategory ob) : precategory ob := + definition opposite [reducible] [constructor] {ob : Type} (C : precategory ob) : precategory ob := precategory.mk' (λ a b, hom b a) (λ a b c f g, g ∘ f) (λ a, id) @@ -23,9 +23,11 @@ namespace category (λ a, !id_id) (λ a b, !is_hset_hom) - definition Opposite [reducible] (C : Precategory) : Precategory := precategory.Mk (opposite C) + definition Opposite [reducible] [constructor] (C : Precategory) : Precategory := + precategory.Mk (opposite C) infixr `∘op`:60 := @comp _ (opposite _) _ _ _ + postfix `ᵒᵖ`:(max+2) := Opposite variables {C : Precategory} {a b c : C} @@ -35,10 +37,9 @@ namespace category definition opposite_opposite' {ob : Type} (C : precategory ob) : opposite (opposite C) = C := by cases C; apply idp - definition opposite_opposite : Opposite (Opposite C) = C := + definition opposite_opposite : (Cᵒᵖ)ᵒᵖ = C := (ap (Precategory.mk C) (opposite_opposite' C)) ⬝ !Precategory.eta - postfix `ᵒᵖ`:(max+2) := Opposite definition opposite_functor [reducible] {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ := begin @@ -47,6 +48,6 @@ namespace category intros, apply (@respect_comp C D) end - infixr `ᵒᵖᶠ`:(max+2) := opposite_functor + postfix `ᵒᵖ`:(max+2) := opposite_functor end category diff --git a/hott/algebra/category/constructions/product.hlean b/hott/algebra/category/constructions/product.hlean index abd279252..98eb38a0d 100644 --- a/hott/algebra/category/constructions/product.hlean +++ b/hott/algebra/category/constructions/product.hlean @@ -11,7 +11,7 @@ import ..category ..functor open eq prod is_trunc functor namespace category - definition precategory_product [reducible] {obC obD : Type} + definition precategory_prod [constructor] [reducible] {obC obD : Type} (C : precategory obC) (D : precategory obD) : precategory (obC × obD) := precategory.mk' (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b)) (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f)) @@ -22,13 +22,12 @@ namespace category (λ a b f, prod_eq !id_right !id_right) (λ a, prod_eq !id_id !id_id) _ + definition Precategory_prod [reducible] [constructor] (C D : Precategory) : Precategory := + precategory.Mk (precategory_prod C D) - definition Precategory_product [reducible] (C D : Precategory) : Precategory := - precategory.Mk (precategory_product C D) + infixr `×c`:30 := Precategory_prod - infixr `×c`:30 := Precategory_product - - definition prod_functor [reducible] {C C' D D' : Precategory} + definition prod_functor [constructor] [reducible] {C C' D D' : Precategory} (F : C ⇒ D) (G : C' ⇒ D') : C ×c C' ⇒ D ×c D' := functor.mk (λ a, pair (F (pr1 a)) (G (pr2 a))) (λ a b f, pair (F (pr1 f)) (G (pr2 f))) diff --git a/hott/algebra/category/constructions/sum.hlean b/hott/algebra/category/constructions/sum.hlean new file mode 100644 index 000000000..20601b815 --- /dev/null +++ b/hott/algebra/category/constructions/sum.hlean @@ -0,0 +1,61 @@ +/- +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 product precategory and (TODO) category +-/ + +import ..category ..functor types.sum + +open eq sum is_trunc functor lift + +namespace category + + --set_option pp.universes true + definition sum_hom.{u v w x} [unfold 5 6] {obC : Type.{u}} {obD : Type.{v}} + (C : precategory.{u w} obC) (D : precategory.{v x} obD) + : obC + obD → obC + obD → Type.{max w x} := + sum.rec (λc, sum.rec (λc', lift (c ⟶ c')) (λd, lift empty)) + (λd, sum.rec (λc, lift empty) (λd', lift (d ⟶ d'))) + + theorem is_hset_sum_hom {obC : Type} {obD : Type} + (C : precategory obC) (D : precategory obD) (x y : obC + obD) + : is_hset (sum_hom C D x y) := + by induction x: induction y: esimp at *: exact _ + + local attribute is_hset_sum_hom [instance] + + definition precategory_sum [constructor] {obC obD : Type} + (C : precategory obC) (D : precategory obD) : precategory (obC + obD) := + precategory.mk (sum_hom C D) + (λ a b c g f, begin induction a: induction b: induction c: esimp at *; + induction f with f; induction g with g; (contradiction | exact up (g ∘ f)) end) + (λ a, by induction a: exact up id) + (λ a b c d h g f, + abstract begin induction a: induction b: induction c: induction d: + esimp at *; induction f with f; induction g with g; induction h with h; + esimp at *; try contradiction: apply ap up !assoc end end) + (λ a b f, abstract begin induction a: induction b: esimp at *; + induction f with f; esimp; try contradiction: exact ap up !id_left end end) + (λ a b f, abstract begin induction a: induction b: esimp at *; + induction f with f; esimp; try contradiction: exact ap up !id_right end end) + + definition Precategory_sum [constructor] (C D : Precategory) : Precategory := + precategory.Mk (precategory_sum C D) + + infixr `+c`:27 := Precategory_sum + + definition sum_functor [constructor] {C C' D D' : Precategory} + (F : C ⇒ D) (G : C' ⇒ D') : C +c C' ⇒ D +c D' := + functor.mk (λ a, by induction a: (exact inl (F a)|exact inr (G a))) + (λ a b f, begin induction a: induction b: esimp at *; + induction f with f; esimp; try contradiction: (exact up (F f)|exact up (G f)) end) + (λ a, abstract by induction a: esimp; exact ap up !respect_id end) + (λ a b c g f, abstract begin induction a: induction b: induction c: esimp at *; + induction f with f; induction g with g; try contradiction: + esimp; exact ap up !respect_comp end end) + + infixr `+f`:27 := sum_functor + +end category diff --git a/hott/algebra/category/constructions/terminal.hlean b/hott/algebra/category/constructions/terminal.hlean new file mode 100644 index 000000000..24a40687a --- /dev/null +++ b/hott/algebra/category/constructions/terminal.hlean @@ -0,0 +1,57 @@ +/- +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 + +Terminal category +-/ + +import .indiscrete + +open functor is_trunc unit eq + +namespace category + + definition terminal_precategory [constructor] : precategory unit := + indiscrete_precategory unit + + definition Terminal_precategory [constructor] : Precategory := + precategory.Mk terminal_precategory + + notation 1 := Terminal_precategory + definition one_op : 1ᵒᵖ = 1 := idp + + definition terminal_functor [constructor] (C : Precategory) : C ⇒ 1 := + functor.mk (λx, star) + (λx y f, star) + (λx, idp) + (λx y z g f, idp) + + definition is_contr_functor_one [instance] (C : Precategory) : is_contr (C ⇒ 1) := + is_contr.mk (terminal_functor C) + begin + intro F, fapply functor_eq, + { intro x, apply @is_hprop.elim unit}, + { intro x y f, apply @is_hprop.elim unit} + end + + definition terminal_functor_op (C : Precategory) + : (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 + + definition point (C : Precategory) (c : C) : 1 ⇒ C := + functor.mk (λx, c) + (λx y f, id) + (λx, idp) + (λ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_comp {C D : Precategory} (F : C ⇒ D) (c : C) + : F ∘f point C c = point D (F c) := idp + +end category diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean index 2ac7ca60b..88e78e03f 100644 --- a/hott/algebra/category/functor.hlean +++ b/hott/algebra/category/functor.hlean @@ -11,7 +11,7 @@ open pi 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)) + (to_fun_hom : Π {a b : C}, hom a b → hom (to_fun_ob a) (to_fun_ob b)) (respect_id : Π (a : C), to_fun_hom (ID a) = ID (to_fun_ob a)) (respect_comp : Π {a b c : C} (g : hom b c) (f : hom a b), to_fun_hom (g ∘ f) = to_fun_hom g ∘ to_fun_hom f) @@ -52,9 +52,8 @@ namespace functor : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ := apd01111 functor.mk pF pH !is_hprop.elim !is_hprop.elim - definition functor_eq' {F₁ F₂ : C ⇒ D} - : Π(p : to_fun_ob F₁ = to_fun_ob F₂), - (transport (λx, Πa b f, hom (x a) (x b)) p (to_fun_hom F₁) = to_fun_hom F₂) → F₁ = F₂ := + definition functor_eq' {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ = to_fun_ob F₂), + (transport (λx, Πa b f, hom (x a) (x b)) p @(to_fun_hom F₁) = @(to_fun_hom F₂)) → F₁ = F₂ := by induction F₁; induction F₂; apply functor_mk_eq' definition functor_mk_eq {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)} @@ -141,13 +140,11 @@ namespace functor to_fun_hom (g ∘ f) = to_fun_hom g ∘ to_fun_hom f)) ≃ (functor C D) := begin fapply equiv.MK, - {intro S, fapply functor.mk, - exact (S.1), exact (S.2.1), - -- TODO(Leo): investigate why we need to use relaxed-exact (rexact) tactic here - exact (pr₁ S.2.2), rexact (pr₂ S.2.2)}, - {intro F, cases F with d1 d2 d3 d4, exact ⟨d1, d2, (d3, @d4)⟩}, - {intro F, cases F, reflexivity}, - {intro S, cases S with d1 S2, cases S2 with d2 P1, cases P1, reflexivity}, + {intro S, induction S with d1 S2, induction S2 with d2 P1, induction P1 with P11 P12, + exact functor.mk d1 d2 P11 @P12}, + {intro F, induction F with d1 d2 d3 d4, exact ⟨d1, @d2, (d3, @d4)⟩}, + {intro F, induction F, reflexivity}, + {intro S, induction S with d1 S2, induction S2 with d2 P1, induction P1, reflexivity}, end section @@ -199,8 +196,8 @@ namespace functor by induction pF; induction pH; induction pid; induction pcomp; reflexivity definition ap010_functor_eq {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 p q) c = p c := + (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 p q) c = p c := begin cases F₁ with F₁o F₁h F₁id F₁comp, cases F₂ with F₂o F₂h F₂id F₂comp, esimp [functor_eq,functor_mk_eq,functor_mk_eq'], diff --git a/hott/algebra/category/yoneda.hlean b/hott/algebra/category/yoneda.hlean index 227eef201..cf56b1a23 100644 --- a/hott/algebra/category/yoneda.hlean +++ b/hott/algebra/category/yoneda.hlean @@ -208,7 +208,7 @@ namespace yoneda local attribute Category.to.precategory category.to_precategory [constructor] -- should this be defined as "yoneda_embedding Cᵒᵖ"? - definition contravariant_yoneda_embedding (C : Precategory) : Cᵒᵖ ⇒ set ^c C := + definition contravariant_yoneda_embedding [reducible] (C : Precategory) : Cᵒᵖ ⇒ set ^c C := functor_curry !hom_functor definition yoneda_embedding (C : Precategory) : C ⇒ set ^c Cᵒᵖ := @@ -226,10 +226,9 @@ namespace yoneda exact ap10 !(@respect_comp Cᵒᵖ set)⁻¹ x} end - definition yoneda_lemma {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ set) : - homset (ɏ c) F ≅ lift_functor (F c) := + definition yoneda_lemma_equiv [constructor] {C : Precategory} (c : C) + (F : Cᵒᵖ ⇒ set) : hom (ɏ c) F ≃ lift (F c) := begin - apply iso_of_equiv, esimp, fapply equiv.MK, { intro η, exact up (η c id)}, { intro x, induction x with x, exact yoneda_lemma_hom c F x}, @@ -242,10 +241,16 @@ 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) : + 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) (η : ɏ c ⟹ F) : to_fun_hom (lift_functor ∘f F) f (to_hom (yoneda_lemma c F) η) = - proof to_hom (yoneda_lemma c' F) (η ∘n to_fun_hom ɏ f) qed := + to_hom (yoneda_lemma c' F) (η ∘n to_fun_hom ɏ f) := begin esimp [yoneda_lemma,yoneda_embedding], apply ap up, transitivity (F f ∘ η c) id, reflexivity, @@ -256,12 +261,29 @@ namespace yoneda rewrite [+id_left,+id_right], end + -- TODO: Investigate what is the bottleneck to type check the next theorem + + -- 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) (θ : F ⟹ F') (η : to_fun_ob ɏ c ⟹ F) : - proof (lift_functor.{v u} ∘fn θ) c (to_hom (yoneda_lemma c F) η) qed = - (to_hom (yoneda_lemma c F') proof (θ ∘n η : (to_fun_ob ɏ c : Cᵒᵖ ⇒ set) ⟹ F') qed) := + (lift_functor.{v u} ∘fn θ) c (to_hom (yoneda_lemma c F) η) = + proof to_hom (yoneda_lemma c F') (θ ∘n η) qed := by reflexivity + -- theorem xx.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ set) + -- (θ : F ⟹ F') (η : to_fun_ob ɏ c ⟹ F) : + -- proof _ qed = + -- to_hom (yoneda_lemma c F') (θ ∘n η) := + -- by reflexivity + + -- theorem yy.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ set) + -- (θ : F ⟹ F') (η : to_fun_ob ɏ c ⟹ F) : + -- (lift_functor.{v u} ∘fn θ) c (to_hom (yoneda_lemma c F) η) = + -- proof _ qed := + -- by reflexivity + definition fully_faithful_yoneda_embedding [instance] (C : Precategory) : fully_faithful (ɏ : C ⇒ set ^c Cᵒᵖ) := begin @@ -275,7 +297,7 @@ namespace yoneda rewrite [id_left,id_right]} end - definition embedding_on_objects_yoneda_embedding (C : Category) : + definition is_embedding_yoneda_embedding (C : Category) : is_embedding (ɏ : C → Cᵒᵖ ⇒ set) := begin intro c c', fapply is_equiv_of_equiv_of_homotopy, @@ -298,8 +320,7 @@ namespace yoneda { transitivity _, rotate 1, { apply sigma.sigma_equiv_sigma_id, intro c, exact !eq_equiv_iso}, { apply fiber.sigma_char}}, - { apply function.is_hprop_fiber_of_is_embedding, - apply embedding_on_objects_yoneda_embedding} + { apply function.is_hprop_fiber_of_is_embedding, apply is_embedding_yoneda_embedding} end end yoneda