feat(category): prove Theorem 9.5.9 from the HoTT book

hott/algebra/category/yoneda.hlean

@@ -134,7 +134,7 @@ namespace functor
     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 (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
@@ -267,7 +267,7 @@ namespace yoneda
       rewrite [id_left,id_right]}
   end
 
-  definition injective_on_objects_yoneda_embedding (C : Category) :
+  definition embedding_on_objects_yoneda_embedding (C : Category) :
     is_embedding (ɏ : C → Cᵒᵖ ⇒ set) :=
   begin
     apply is_embedding.mk, intro c c', fapply is_equiv_of_equiv_of_homotopy,
@@ -281,4 +281,17 @@ 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_hprop_representable {C : Category} (F : Cᵒᵖ ⇒ set)
+    : 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}},
+    { apply function.is_hprop_fiber_of_is_embedding,
+      apply embedding_on_objects_yoneda_embedding}
+  end
+
 end yoneda

hott/book.md

@@ -23,7 +23,7 @@ The rows indicate the chapters, the columns the sections.
 | Ch 6  | . | + | + | + | + | ½ | ½ | ¼ | ¼ | ¼  | ¾  | -  | .  |    |    |
 | Ch 7  | + | + | + | - | - | - | - |   |   |    |    |    |    |    |    |
 | Ch 8  | ¾ | - | - | - | - | - | - | - | - | -  |    |    |    |    |    |
-| Ch 9  | ¾ | + | + | ¼ | ½ | ½ | - | - | - |    |    |    |    |    |    |
+| Ch 9  | ¾ | + | + | ¼ | ¾ | ½ | - | - | - |    |    |    |    |    |    |
 | Ch 10 | - | - | - | - | - |   |   |   |   |    |    |    |    |    |    |
 | Ch 11 | - | - | - | - | - | - |   |   |   |    |    |    |    |    |    |
 
@@ -157,7 +157,7 @@ Every file is in the folder [algebra.category](algebra/category/category.md)
 - 9.2 (Functors and transformations): [functor](algebra/category/functor.hlean), [nat_trans](algebra/category/nat_trans.hlean), [constructions.functor](algebra/category/constructions/functor.hlean)
 - 9.3 (Adjunctions): [adjoint](algebra/category/adjoint.hlean)
 - 9.4 (Equivalences): [adjoint](algebra/category/adjoint.hlean) (only definitions)
-- 9.5 (The Yoneda lemma): [constructions.opposite](algebra/category/constructions/opposite.hlean), [constructions.product](algebra/category/constructions/product.hlean), [yoneda](algebra/category/yoneda.hlean) (up to definition of Yoneda embedding)
+- 9.5 (The Yoneda lemma): [constructions.opposite](algebra/category/constructions/opposite.hlean), [constructions.product](algebra/category/constructions/product.hlean), [yoneda](algebra/category/yoneda.hlean) (up to Theorem 9.5.9)
 - 9.6 (Strict categories): [strict](algebra/category/strict.hlean) (only definition)
 - 9.7 (†-categories): not formalized
 - 9.8 (The structure identity principle): not formalized

hott/function.hlean

@@ -40,14 +40,6 @@ namespace function
 
   attribute is_embedding.elim [instance]
 
-  definition is_surjective_rec_on {P : Type} (H : is_surjective f) (b : B) [Pt : is_hprop P]
-    (IH : fiber f b → P) : P :=
-  trunc.rec_on (is_surjective.elim f b) IH
-
-  definition is_surjective_of_is_split_surjective [instance] [H : is_split_surjective f]
-    : is_surjective f :=
-  is_surjective.mk (λb, tr (is_split_surjective.elim f b))
-
   definition is_injective_of_is_embedding [reducible] [H : is_embedding f] {a a' : A}
     : f a = f a' → a = a' :=
   (ap f)⁻¹
@@ -77,6 +69,24 @@ namespace function
     exact H,
   end
 
+  definition is_hprop_fiber_of_is_embedding (f : A → B) [H : is_embedding f] (b : B) :
+    is_hprop (fiber f b) :=
+  begin
+    apply is_hprop.mk, intro v w,
+    induction v with a p, induction w with a' q, induction q,
+    fapply fiber_eq,
+    { esimp, apply is_injective_of_is_embedding p},
+    { esimp [is_injective_of_is_embedding], symmetry, apply right_inv}
+  end
+
+  definition is_surjective_rec_on {P : Type} (H : is_surjective f) (b : B) [Pt : is_hprop P]
+    (IH : fiber f b → P) : P :=
+  trunc.rec_on (is_surjective.elim f b) IH
+
+  definition is_surjective_of_is_split_surjective [instance] [H : is_split_surjective f]
+    : is_surjective f :=
+  is_surjective.mk (λb, tr (is_split_surjective.elim f b))
+
   definition is_hprop_is_surjective [instance] (f : A → B) : is_hprop (is_surjective f) :=
   begin
     have H : (Π(b : B), merely (fiber f b)) ≃ is_surjective f,

hott/types/equiv.hlean

@@ -91,10 +91,6 @@ namespace is_equiv
 
   definition is_hprop_is_contr_fun (f : A → B) : is_hprop (is_contr_fun f) := _
 
-  /-
-    we cannot make the next theorem an instance, because it loops together with
-    is_contr_fiber_of_is_equiv
-  -/
   definition is_equiv_of_is_contr_fun [H : is_contr_fun f] : is_equiv f :=
   adjointify _ (λb, point (center (fiber f b)))
                (λb, point_eq (center (fiber f b)))