feat(hott/algebra/precategory): do lots of stuff with categories

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 :=
+    (H : is_univalent C) : Category := Category.mk C (category.mk' C C H)
-  Category.mk C (category.mk' C C H)
 
   definition Category.eta (C : Category) : Category.mk C C = C :=
   Category.rec (λob c, idp) C

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

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]

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

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₂)
+    {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ ∼ F₂)
-    (pF : F₁ ∼ F₂) (pH : Π(a b : C) (f : hom a b), eq_of_homotopy pF ▹ (H₁ a b f) = H₂ a b 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 (pH c c' f),
-       apply concat, rotate_left 1,
+        apply concat, rotate_left 1, apply transport_hom,
-       exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c c') f),
+        apply concat, rotate_left 1,
-       apply (apD10' f),
+        exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c c') f),
-       apply concat, rotate_left 1,
+        apply (apD10' f),
-       exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c) c'),
+        apply concat, rotate_left 1,
-       apply (apD10' c'),
+        exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c) c'),
-       apply concat, rotate_left 1,
+        apply (apD10' c'),
-       exact (pi_transport_constant (eq_of_homotopy pF) H₁ c),
+        apply concat, rotate_left 1,
-       apply idp
+        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)
+    (Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = 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'))
 
   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

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)

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₂),
+  theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = 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 :=
   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 ∘ id) : by rewrite id_left
-          ... = F (f,g)            : by rewrite id_right,
+          ... = 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
   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 :=
+  definition functor_prod_flip (C D : Precategory) : C ×c D ⇒ D ×c C :=
-  functor.mk sorry sorry sorry sorry
+  functor.mk (λp, (p.2, p.1))
-
+             (λp p' h, (h.2, h.1))
-
+             (λp, idp)
-  definition contravariant_yoneda_embedding : Cᵒᵖ ⇒ set ^c C :=
+             (λp p' p'' h' h, idp)
-  functor_curry !yoneda.hom_functor
 
+  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
 

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)

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

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}