feat(category.limits): prove that yoneda preserves limits

hott/algebra/category/functor/basic.hlean

@@ -170,6 +170,16 @@ namespace functor
       {intro S, induction S with d1 S2, induction S2 with d2 P1, induction P1, reflexivity},
   end
 
+  definition change_fun [constructor] (F : C ⇒ D) (Fob : C → D)
+    (Fhom : Π⦃c c' : C⦄ (f : c ⟶ c'), Fob c ⟶ Fob c') (p : F = Fob) (q : F =[p] Fhom) : C ⇒ D :=
+  functor.mk
+    Fob
+    Fhom
+    proof abstract λa, transporto (λFo (Fh : Π⦃c c'⦄, _), Fh (ID a) = ID (Fo a))
+      q (respect_id F a) end qed
+    proof abstract λa b c g f, transporto (λFo (Fh : Π⦃c c'⦄, _), Fh (g ∘ f) = Fh g ∘ Fh f)
+      q (respect_comp F g f) end qed
+
   section
     local attribute precategory.is_hset_hom [priority 1001]
     local attribute trunctype.struct [priority 1] -- remove after #842 is closed

hott/algebra/category/functor/examples.hlean

@@ -26,13 +26,13 @@ namespace functor
 
   local abbreviation Fhom [constructor] := @functor_curry_hom
 
-  theorem functor_curry_id (c : C) : Fhom F (ID c) = nat_trans.id :=
-  nat_trans_eq (λd, respect_id F _)
+  theorem functor_curry_id (c : C) : Fhom F (ID c) = 1 :=
+  nat_trans_eq (λd, respect_id F (c, d))
 
   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,
+    apply nat_trans_eq,
     intro d, calc
     natural_map (Fhom F (f' ∘ f)) d = F (f' ∘ f, id) : by esimp
       ... = F (f' ∘ f, id ∘ id)                      : by rewrite id_id
@@ -41,12 +41,36 @@ namespace functor
       ... = natural_map ((Fhom F f') ∘ (Fhom F f)) d : by esimp
   end
 
-  definition functor_curry [reducible] [constructor] : C ⇒ E ^c D :=
+  definition functor_curry [constructor] : C ⇒ E ^c D :=
   functor.mk (functor_curry_ob F)
              (functor_curry_hom F)
              (functor_curry_id F)
              (functor_curry_comp F)
 
+  /- currying a functor, flipping the arguments -/
+  definition functor_curry_rev_ob [reducible] [constructor] (d : D) : C ⇒ E :=
+  F ∘f (1 ×f constant_functor C d)
+
+  definition functor_curry_rev_hom [constructor] ⦃d d' : D⦄ (g : d ⟶ d')
+    : functor_curry_rev_ob F d ⟹ functor_curry_rev_ob F d' :=
+  F ∘fn (1 ×n constant_nat_trans C g)
+
+  local abbreviation Fhomr [constructor] := @functor_curry_rev_hom
+  theorem functor_curry_rev_id (d : D) : Fhomr F (ID d) = nat_trans.id :=
+  nat_trans_eq (λc, respect_id F (c, d))
+
+  theorem functor_curry_rev_comp ⦃d d' d'' : D⦄ (g' : d' ⟶ d'') (g : d ⟶ d')
+    : Fhomr F (g' ∘ g) = Fhomr F g' ∘n Fhomr F g :=
+  begin
+    apply nat_trans_eq, esimp, intro c, rewrite [-id_id at {1}], apply respect_comp F
+  end
+
+  definition functor_curry_rev [constructor] : D ⇒ E ^c C :=
+  functor.mk (functor_curry_rev_ob F)
+             (functor_curry_rev_hom F)
+             (functor_curry_rev_id F)
+             (functor_curry_rev_comp F)
+
   /- uncurrying a functor -/
 
   definition functor_uncurry_ob [reducible] (p : C ×c D) : E :=
@@ -80,7 +104,7 @@ namespace functor
                   by rewrite [square_prepostcompose (!naturality⁻¹ᵖ) _ _]
       ... = Ghom G f' ∘ Ghom G f : by esimp
 
-  definition functor_uncurry [reducible] [constructor] : C ×c D ⇒ E :=
+  definition functor_uncurry [constructor] : C ×c D ⇒ E :=
   functor.mk (functor_uncurry_ob G)
              (functor_uncurry_hom G)
              (functor_uncurry_id G)
@@ -191,16 +215,20 @@ namespace functor
     (λ x y z g f, abstract eq_of_homotopy (by intros; apply @hom_functor_assoc) end)
 
   -- the functor hom(-, c)
-  definition hom_functor_left.{u v} [constructor] (C : Precategory.{u v}) (c : C)
+  definition hom_functor_left.{u v} [constructor] {C : Precategory.{u v}} (c : C)
     : Cᵒᵖ ⇒ set.{v} :=
-  hom_functor C ∘f (1 ×f constant_functor Cᵒᵖ c)
+  functor_curry_rev_ob !hom_functor c
 
   -- the functor hom(c, -)
-  definition hom_functor_right.{u v} [constructor] (C : Precategory.{u v}) (c : C)
+  definition hom_functor_right.{u v} [constructor] {C : Precategory.{u v}} (c : C)
     : C ⇒ set.{v} :=
-  hom_functor C ∘f (constant_functor C c ×f 1)
+  functor_curry_ob !hom_functor c
 
+  definition nat_trans_hom_functor_left [constructor] {C : Precategory}
+    ⦃c c' : C⦄ (f : c ⟶ c') : hom_functor_left c ⟹ hom_functor_left c' :=
+  functor_curry_rev_hom !hom_functor f
 
+  -- the yoneda embedding itself is defined in [yoneda].
   end
 
 

hott/algebra/category/functor/yoneda.hlean

@@ -24,9 +24,18 @@ namespace yoneda
     (C : Precategory) : Cᵒᵖ ⇒ cset ^c C :=
   functor_curry !hom_functor
 
+  /-
+    we use (change_fun) to make sure that (to_fun_ob (yoneda_embedding C) c) will reduce to
+    (hom_functor_left c) instead of (functor_curry_rev_ob (hom_functor C) c)
+  -/
   definition yoneda_embedding [constructor] (C : Precategory) : C ⇒ cset ^c Cᵒᵖ :=
-  functor_curry (!hom_functor ∘f !prod_flip_functor)
-
+--(functor_curry_rev !hom_functor)
+  change_fun
+    (functor_curry_rev !hom_functor)
+    hom_functor_left
+    nat_trans_hom_functor_left
+    idp
+    idpo
 
   notation `ɏ` := yoneda_embedding _
 

hott/algebra/category/limits/functor_preserve.hlean

@@ -8,7 +8,7 @@ Functors preserving limits
 
 import .colimits ..functor.yoneda
 
-open functor yoneda is_trunc nat_trans
+open eq functor yoneda is_trunc nat_trans
 
 namespace category
 
@@ -50,33 +50,45 @@ namespace category
 
   /- yoneda preserves existing limits -/
 
-  definition preserves_existing_limits_yoneda_embedding_lemma [constructor] (x : cone_obj F)
-    [H : is_terminal x] {G : Cᵒᵖ ⇒ cset} (η : constant_functor I G ⟹ ɏ ∘f F) :
-    G ⟹ to_fun_ob ɏ (cone_to_obj x) :=
+  local attribute Category.to.precategory category.to_precategory [constructor]
+
+  definition preserves_existing_limits_yoneda_embedding_lemma [constructor] (y : cone_obj F)
+    [H : is_terminal y] {G : Cᵒᵖ ⇒ cset} (η : constant_functor I G ⟹ ɏ ∘f F) :
+    G ⟹ hom_functor_left (cone_to_obj y) :=
   begin
     fapply nat_trans.mk: esimp,
     { intro c x, fapply to_hom_limit,
       { intro i, exact η i c x},
-      { intro i j k, exact sorry}},
-    { intro c c' f, apply eq_of_homotopy, intro x, exact sorry}
+      { exact abstract begin
+        intro i j k,
+        exact !id_right⁻¹ ⬝ !assoc⁻¹ ⬝ ap0100 natural_map (naturality η k) c x end end
+        }},
+      -- [BUG] abstracting here creates multiple lemmas proving this fact
+    { intro c c' f, apply eq_of_homotopy, intro x,
+      rewrite [id_left], apply to_eq_hom_limit, intro i,
+      refine !assoc ⬝ _, rewrite to_hom_limit_commute,
+      refine _ ⬝ ap10 (naturality (η i) f) x, rewrite [▸*, id_left]}
+      -- abstracting here fails
   end
+--  print preserves_existing_limits_yoneda_embedding_lemma_11
 
   theorem preserves_existing_limits_yoneda_embedding (C : Precategory)
     : preserves_existing_limits (yoneda_embedding C) :=
   begin
-    intro I F H Gη, induction H with x H, induction Gη with G η, esimp at *,
+    intro I F H Gη, induction H with y H, induction Gη with G η, esimp at *,
+    assert lem : Π (i : carrier I),
+    nat_trans_hom_functor_left (natural_map (cone_to_nat y) i)
+      ∘n preserves_existing_limits_yoneda_embedding_lemma y η = natural_map η i,
+    { intro i, apply nat_trans_eq, intro c, apply eq_of_homotopy, intro x,
+        esimp, refine !assoc ⬝ !id_right ⬝ !to_hom_limit_commute},
     fapply is_contr.mk,
-    { fapply cone_hom.mk: esimp,
-      { exact sorry
-        -- fapply nat_trans.mk: esimp,
-        -- { intro c x, esimp [yoneda_embedding], fapply to_hom_limit,
-        --   { apply has_terminal_object.is_terminal}, --this should be solved by type class res.
-        --   { intro i, induction dη with d η, esimp at *, },
-        --   {  intro i j k, }},
-        -- { }
-  },
-      { exact sorry}},
-    { exact sorry}
+    { fapply cone_hom.mk,
+      { exact preserves_existing_limits_yoneda_embedding_lemma y η},
+      { exact lem}},
+    { intro v, apply cone_hom_eq, esimp, apply nat_trans_eq, esimp, intro c,
+      apply eq_of_homotopy, intro x, refine (to_eq_hom_limit _ _)⁻¹,
+      intro i, refine !id_right⁻¹ ⬝ !assoc⁻¹ ⬝ _,
+      exact ap0100 natural_map (cone_to_eq v i) c x}
   end
 
 end category

hott/init/pathover.hlean

@@ -226,7 +226,7 @@ namespace eq
   variable (C)
   definition transporto (r : b =[p] b₂) (c : C b) : C b₂ :=
   by induction r;exact c
-  infix `▸o`:75 := transporto _
+  infix ` ▸o `:75 := transporto _
 
   definition fn_tro_eq_tro_fn (C' : Π ⦃a : A⦄, B a → Type) (q : b =[p] b₂)
     (f : Π(b : B a), C b → C' b) (c : C b) : f b (q ▸o c) = (q ▸o (f b c)) :=
@@ -316,7 +316,7 @@ namespace eq
     (s : r = r') (s₂ : r₂ = r₂') : r ⬝o r₂ = r' ⬝o r₂' :=
   by induction s; induction s₂; reflexivity
 
-  infixl `◾o`:75 := concato2
+  infixl ` ◾o `:75 := concato2
   postfix [parsing_only] `⁻²ᵒ`:(max+10) := inverseo2 --this notation is abusive, should we use it?
 
 end eq