From fd89aa77a3a2a12c98df3b05035f465b03198f06 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 2 Sep 2015 19:41:19 -0400
Subject: [PATCH] feat(hott): prove Yoneda lemma

---
 hott/algebra/category/category.hlean          | 10 +--
 .../category/constructions/functor.hlean      |  2 +-
 .../algebra/category/constructions/hset.hlean | 22 ++++---
 hott/algebra/category/nat_trans.hlean         |  3 +-
 hott/algebra/category/precategory.hlean       | 22 +++----
 hott/algebra/category/yoneda.hlean            | 62 ++++++++++++++-----
 hott/hit/trunc.hlean                          |  2 +-
 hott/init/trunc.hlean                         | 55 ++++++++--------
 src/emacs/lean-input.el                       |  2 +
 9 files changed, 113 insertions(+), 67 deletions(-)

diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean
index f055789a7..9f8e80eb6 100644
--- a/hott/algebra/category/category.hlean
+++ b/hott/algebra/category/category.hlean
@@ -22,7 +22,7 @@ namespace category
 
   abbreviation iso_of_path_equiv := @category.iso_of_path_equiv
 
-  definition category.mk [reducible] {ob : Type} (C : precategory ob)
+  definition category.mk [reducible] [unfold 2] {ob : Type} (C : precategory ob)
     (H : Π (a b : ob), is_equiv (iso_of_eq : a = b → a ≅ b)) : category ob :=
   precategory.rec_on C category.mk' H
 
@@ -62,12 +62,14 @@ namespace category
     (struct : category carrier)
 
   attribute Category.struct [instance] [coercion]
+  attribute Category.to.precategory category.to_precategory [constructor]
 
-  definition Category.to_Precategory [coercion] [reducible] (C : Category) : Precategory :=
+  definition Category.to_Precategory [constructor] [coercion] [reducible] (C : Category)
+    : Precategory :=
   Precategory.mk (Category.carrier C) C
 
-  definition category.Mk [reducible] := Category.mk
-  definition category.MK [reducible] (C : Precategory)
+  definition category.Mk [constructor] [reducible] := Category.mk
+  definition category.MK [constructor] [reducible] (C : Precategory)
     (H : is_univalent C) : Category := Category.mk C (category.mk C H)
 
   definition Category.eta (C : Category) : Category.mk C C = C :=
diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean
index f2aceee50..9a346f968 100644
--- a/hott/algebra/category/constructions/functor.hlean
+++ b/hott/algebra/category/constructions/functor.hlean
@@ -21,7 +21,7 @@ namespace category
                  (λ a b f, !nat_trans.id_left)
                  (λ a b f, !nat_trans.id_right)
 
-  definition Precategory_functor [reducible] (D C : Precategory) : Precategory :=
+  definition Precategory_functor [reducible] [constructor] (D C : Precategory) : Precategory :=
   precategory.Mk (precategory_functor D C)
 
   infixr `^c`:35 := Precategory_functor
diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean
index 56b094f2e..662729042 100644
--- a/hott/algebra/category/constructions/hset.hlean
+++ b/hott/algebra/category/constructions/hset.hlean
@@ -6,14 +6,13 @@ Authors: Floris van Doorn, Jakob von Raumer
 Category of hsets
 -/
 
-import ..category types.equiv
+import ..category types.equiv ..functor types.lift
 
---open eq is_trunc sigma equiv iso is_equiv
 open eq category equiv iso is_equiv is_trunc function sigma
 
 namespace category
 
-  definition precategory_hset [reducible] : precategory hset :=
+  definition precategory_hset.{u} [reducible] [constructor] : precategory hset.{u} :=
   precategory.mk (λx y : hset, x → y)
                  (λx y z g f a, g (f a))
                  (λx a, a)
@@ -21,14 +20,14 @@ namespace category
                  (λx y f, eq_of_homotopy (λa, idp))
                  (λx y f, eq_of_homotopy (λa, idp))
 
-  definition Precategory_hset [reducible] : Precategory :=
+  definition Precategory_hset [reducible] [constructor] : Precategory :=
   Precategory.mk hset precategory_hset
 
   namespace set
     local attribute is_equiv_subtype_eq [instance]
     definition iso_of_equiv {A B : Precategory_hset} (f : A ≃ B) : A ≅ B :=
     iso.MK (to_fun f)
-           (equiv.to_inv f)
+           (to_inv f)
            (eq_of_homotopy (left_inv (to_fun f)))
            (eq_of_homotopy (right_inv (to_fun f)))
 
@@ -89,11 +88,18 @@ namespace category
     end
   end set
 
-  definition category_hset [instance] : category hset :=
+  definition category_hset [instance] [constructor] : category hset :=
   category.mk precategory_hset set.is_univalent_hset
 
-  definition Category_hset [reducible] : Category :=
+  definition Category_hset [reducible] [constructor] : Category :=
   Category.mk hset category_hset
 
-  abbreviation set := Category_hset
+  abbreviation set [constructor] := Category_hset
+
+  open functor lift
+  definition lift_functor.{u v} [constructor] : set.{u} ⇒ set.{max u v} :=
+  functor.mk tlift
+             (λa b, lift_functor)
+             (λa, eq_of_homotopy (λx, by induction x; reflexivity))
+             (λa b c g f, eq_of_homotopy (λx, by induction x; reflexivity))
 end category
diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean
index 8a3a8d0b1..104d71f0b 100644
--- a/hott/algebra/category/nat_trans.hlean
+++ b/hott/algebra/category/nat_trans.hlean
@@ -6,7 +6,8 @@ Author: Floris van Doorn, Jakob von Raumer
 import .functor .iso
 open eq category functor is_trunc equiv sigma.ops sigma is_equiv function pi funext iso
 
-structure nat_trans {C D : Precategory} (F G : C ⇒ D) :=
+structure nat_trans {C : Precategory} {D : Precategory} (F G : C ⇒ D)
+  : Type :=
  (natural_map : Π (a : C), hom (F a) (G a))
  (naturality : Π {a b : C} (f : hom a b), G f ∘ natural_map a = natural_map b ∘ F f)
 
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index 656e7cf6b..67a7091e2 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/hott/algebra/category/precategory.hlean
@@ -40,15 +40,15 @@ namespace category
     infixl `⟶`:25 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
   end hom
 
-  abbreviation hom         := @precategory.hom
-  abbreviation comp        := @precategory.comp
-  abbreviation ID          := @precategory.ID
-  abbreviation assoc       := @precategory.assoc
-  abbreviation assoc'      := @precategory.assoc'
-  abbreviation id_left     := @precategory.id_left
-  abbreviation id_right    := @precategory.id_right
-  abbreviation id_id       := @precategory.id_id
-  abbreviation is_hset_hom := @precategory.is_hset_hom
+  abbreviation hom         [unfold 2] := @precategory.hom
+  abbreviation comp        [unfold 2] := @precategory.comp
+  abbreviation ID          [unfold 2] := @precategory.ID
+  abbreviation assoc       [unfold 2] := @precategory.assoc
+  abbreviation assoc'      [unfold 2] := @precategory.assoc'
+  abbreviation id_left     [unfold 2] := @precategory.id_left
+  abbreviation id_right    [unfold 2] := @precategory.id_right
+  abbreviation id_id       [unfold 2] := @precategory.id_id
+  abbreviation is_hset_hom [unfold 2] := @precategory.is_hset_hom
 
   -- the constructor you want to use in practice
   protected definition precategory.mk [constructor] {ob : Type} (hom : ob → ob → Type)
@@ -80,7 +80,7 @@ namespace category
     calc i = id ∘ i : by rewrite id_left
        ... = id     : by rewrite H
 
-    definition homset [reducible] (x y : ob) : hset :=
+    definition homset [reducible] [constructor] (x y : ob) : hset :=
     hset.mk (hom x y) _
 
   end basic_lemmas
@@ -150,7 +150,7 @@ namespace category
   attribute Precategory.struct [instance] [priority 10000] [coercion]
   -- definition precategory.carrier [coercion] [reducible] := Precategory.carrier
   -- definition precategory.struct [instance] [coercion] [reducible] := Precategory.struct
-  notation g `∘⁅`:60 C:0 `⁆`:0 f:60 :=
+  notation g `∘[`:60 C:0 `]`:0 f:60 :=
   @comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f
   -- TODO: make this left associative
   -- TODO: change this notation?
diff --git a/hott/algebra/category/yoneda.hlean b/hott/algebra/category/yoneda.hlean
index 2fdb50d06..f2f837c64 100644
--- a/hott/algebra/category/yoneda.hlean
+++ b/hott/algebra/category/yoneda.hlean
@@ -10,7 +10,7 @@ import .constructions.functor .constructions.hset .constructions.product .constr
 open category eq category.ops functor prod.ops is_trunc iso
 
 namespace yoneda
-  set_option class.conservative false
+--  set_option class.conservative false
 
   definition representable_functor_assoc [C : Precategory] {a1 a2 a3 a4 a5 a6 : C}
     (f1 : hom a5 a6) (f2 : hom a4 a5) (f3 : hom a3 a4) (f4 : hom a2 a3) (f5 : hom a1 a2)
@@ -21,11 +21,11 @@ namespace yoneda
       ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : by rewrite -(assoc (f2 ∘ f3) _ _)
       ... = _                          : by rewrite (assoc f2 f3 f4)
 
-  definition hom_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set :=
+  definition hom_functor.{u v} [constructor] (C : Precategory.{u v}) : Cᵒᵖ ×c C ⇒ set.{v} :=
   functor.mk
     (λ (x : Cᵒᵖ ×c C), @homset (Cᵒᵖ) C x.1 x.2)
     (λ (x y : Cᵒᵖ ×c C) (f : @category.precategory.hom (Cᵒᵖ ×c C) (Cᵒᵖ ×c C) x y) (h : @homset (Cᵒᵖ) C x.1 x.2),
-       f.2 ∘⁅ C ⁆ (h ∘⁅ C ⁆ f.1))
+       f.2 ∘[C] (h ∘[C] f.1))
     (λ x, @eq_of_homotopy _ _ _ (ID (@homset Cᵒᵖ C x.1 x.2)) (λ h, concat (by apply @id_left) (by apply @id_right)))
     (λ x y z g f,
        eq_of_homotopy (by intros; apply @representable_functor_assoc))
@@ -36,7 +36,7 @@ open is_equiv equiv
 namespace functor
   open prod nat_trans
   variables {C D E : Precategory} (F : C ×c D ⇒ E) (G : C ⇒ E ^c D)
-  definition functor_curry_ob [reducible] (c : C) : E ^c D :=
+  definition functor_curry_ob [reducible] [constructor] (c : C) : E ^c D :=
   functor.mk (λd, F (c,d))
              (λd d' g, F (id, g))
              (λd, !respect_id)
@@ -47,7 +47,7 @@ namespace functor
 
   local abbreviation Fob := @functor_curry_ob
 
-  definition functor_curry_hom ⦃c c' : C⦄ (f : c ⟶ c') : Fob F c ⟹ Fob F c' :=
+  definition functor_curry_hom [constructor] ⦃c c' : C⦄ (f : c ⟶ c') : Fob F c ⟹ Fob F c' :=
   begin
     fapply @nat_trans.mk,
       {intro d, exact F (f, id)},
@@ -80,7 +80,7 @@ namespace functor
       ... = natural_map ((Fhom F f') ∘ (Fhom F f)) d : by esimp
   end
 
-  definition functor_curry [reducible] : C ⇒ E ^c D :=
+  definition functor_curry [reducible] [constructor] : C ⇒ E ^c D :=
   functor.mk (functor_curry_ob F)
              (functor_curry_hom F)
              (functor_curry_id F)
@@ -107,19 +107,17 @@ namespace functor
     Ghom G (f' ∘ f)
           = to_fun_hom (to_fun_ob G p''.1) (f'.2 ∘ f.2) ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2 : by esimp
       ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
-              ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2                   : by rewrite respect_comp
+              ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2                : by rewrite respect_comp
       ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
-              ∘ natural_map (to_fun_hom G f'.1 ∘ to_fun_hom G f.1) p.2        : by rewrite respect_comp
+              ∘ natural_map (to_fun_hom G f'.1 ∘ to_fun_hom G f.1) p.2     : by rewrite respect_comp
       ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
-              ∘ (natural_map (to_fun_hom G f'.1) p.2 ∘ natural_map (to_fun_hom G f.1) p.2) : by esimp
-      ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
-              ∘ (natural_map (to_fun_hom G f'.1) p.2 ∘ natural_map (to_fun_hom G f.1) p.2) : by esimp
+             ∘ (natural_map (to_fun_hom G f'.1) p.2 ∘ natural_map (to_fun_hom G f.1) p.2) : by esimp
       ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ natural_map (to_fun_hom G f'.1) p'.2)
               ∘ (to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2) :
                   by rewrite [square_prepostcompose (!naturality⁻¹ᵖ) _ _]
       ... = Ghom G f' ∘ Ghom G f : by esimp
 
-  definition functor_uncurry [reducible] : C ×c D ⇒ E :=
+  definition functor_uncurry [reducible] [constructor] : C ×c D ⇒ E :=
   functor.mk (functor_uncurry_ob G)
              (functor_uncurry_hom G)
              (functor_uncurry_id G)
@@ -174,7 +172,7 @@ namespace functor
   apply id_left
   end
 
-  definition prod_functor_equiv_functor_functor (C D E : Precategory)
+  definition prod_functor_equiv_functor_functor [constructor] (C D E : Precategory)
     : (C ×c D ⇒ E) ≃ (C ⇒ E ^c D) :=
   equiv.MK functor_curry
            functor_uncurry
@@ -182,7 +180,7 @@ namespace functor
            functor_uncurry_functor_curry
 
 
-  definition functor_prod_flip (C D : Precategory) : C ×c D ⇒ D ×c C :=
+  definition functor_prod_flip [constructor] (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)
@@ -199,6 +197,7 @@ end functor
 open functor
 
 namespace yoneda
+  open category.set nat_trans lift
   --should this be defined as "yoneda_embedding Cᵒᵖ"?
   definition contravariant_yoneda_embedding (C : Precategory) : Cᵒᵖ ⇒ set ^c C :=
   functor_curry !hom_functor
@@ -206,4 +205,39 @@ namespace yoneda
   definition yoneda_embedding (C : Precategory) : C ⇒ set ^c Cᵒᵖ :=
   functor_curry (!hom_functor ∘f !functor_prod_flip)
 
+  notation `ɏ` := yoneda_embedding _
+
+  -- set_option pp.implicit true
+  -- set_option pp.notation false
+  -- -- -- set_option pp.full_names true
+  -- set_option pp.coercions true -- [constructor]
+
+  set_option formatter.hide_full_terms false
+  definition yoneda_lemma_hom [constructor] {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ set)
+    (x : trunctype.carrier (F c)) : ɏ c ⟹ F :=
+  begin
+    fapply nat_trans.mk,
+    { intro c', esimp [yoneda_embedding], intro f, exact F f x},
+    { intro c' c'' f, esimp [yoneda_embedding], apply eq_of_homotopy, intro f',
+      refine _ ⬝ ap (λy, to_fun_hom F y x) !(@id_left _ C)⁻¹,
+      exact ap10 !(@respect_comp Cᵒᵖ set)⁻¹ x}
+  end
+
+  -- set_option pp.implicit true
+  definition yoneda_lemma {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ set) :
+    homset (ɏ c) F ≅ lift_functor (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},
+    { intro x, induction x with x, esimp, apply ap up,
+      exact ap10 !respect_id x},
+    { intro η, esimp, apply nat_trans_eq,
+      intro c', esimp, apply eq_of_homotopy,
+      intro f, esimp [yoneda_embedding] at f,
+      transitivity (F f ∘ η c) id, reflexivity,
+      rewrite naturality, esimp [yoneda_embedding], rewrite [id_left], apply ap _ !id_left},
+  end
+
 end yoneda
diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean
index b6fb91fa3..406912b9d 100644
--- a/hott/hit/trunc.hlean
+++ b/hott/hit/trunc.hlean
@@ -26,7 +26,7 @@ namespace trunc
 
   /-
     there are no theorems to eliminate to the universe here,
-    because the universe is generally not a set
+    because the universe is not a set
   -/
 
   --export is_trunc
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 0662499c1..c9450d4c1 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -213,25 +213,6 @@ namespace is_trunc
   definition is_trunc_empty [instance] (n : trunc_index) : is_trunc (n.+1) empty :=
   !is_trunc_succ_of_is_hprop
 
-  /- truncated universe -/
-
-  -- TODO: move to root namespace?
-  structure trunctype (n : trunc_index) :=
-  (carrier : Type) (struct : is_trunc n carrier)
-  attribute trunctype.carrier [coercion]
-  attribute trunctype.struct [instance]
-
-  notation n `-Type` := trunctype n
-  abbreviation hprop := -1-Type
-  abbreviation hset := 0-Type
-
-  protected abbreviation hprop.mk := @trunctype.mk -1
-  protected abbreviation hset.mk := @trunctype.mk (-1.+1)
-
-  protected abbreviation trunctype.mk' [parsing-only] (n : trunc_index) (A : Type)
-    [H : is_trunc n A] : n-Type :=
-  trunctype.mk A H
-
   /- interaction with equivalences -/
 
   section
@@ -282,6 +263,11 @@ namespace is_trunc
   definition equiv_of_iff_of_is_hprop [unfold 5] [HA : is_hprop A] [HB : is_hprop B] (H : A ↔ B) : A ≃ B :=
   equiv_of_is_hprop (iff.elim_left H) (iff.elim_right H)
 
+  /- truncatedness of lift -/
+  definition is_trunc_lift [instance] [priority 1450] (A : Type) (n : trunc_index)
+    [H : is_trunc n A] : is_trunc n (lift A) :=
+  is_trunc_equiv_closed _ !equiv_lift
+
   end
 
   /- interaction with the Unit type -/
@@ -312,12 +298,27 @@ namespace is_trunc
 
   -- TODO: port "Truncated morphisms"
 
-end is_trunc
+  /- truncated universe -/
 
-/- truncatedness of lift -/
-namespace lift
-  open is_trunc equiv
-  definition is_trunc_lift [instance] [priority 1450] (A : Type) (n : trunc_index)
-    [H : is_trunc n A] : is_trunc n (lift A) :=
-  is_trunc_equiv_closed _ !equiv_lift
-end lift
+  -- TODO: move to root namespace?
+  structure trunctype (n : trunc_index) :=
+  (carrier : Type) (struct : is_trunc n carrier)
+  attribute trunctype.carrier [coercion]
+  attribute trunctype.struct [instance]
+
+  notation n `-Type` := trunctype n
+  abbreviation hprop := -1-Type
+  abbreviation hset := 0-Type
+
+  protected abbreviation hprop.mk := @trunctype.mk -1
+  protected abbreviation hset.mk := @trunctype.mk (-1.+1)
+
+  protected abbreviation trunctype.mk' [parsing-only] (n : trunc_index) (A : Type)
+    [H : is_trunc n A] : n-Type :=
+  trunctype.mk A H
+
+  definition tlift.{u v} [constructor] {n : trunc_index} (A : trunctype.{u} n)
+    : trunctype.{max u v} n :=
+  trunctype.mk (lift A) (is_trunc_lift _ _)
+
+end is_trunc
diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el
index 077c93b51..8bf2fe091 100644
--- a/src/emacs/lean-input.el
+++ b/src/emacs/lean-input.el
@@ -991,6 +991,8 @@ order for the change to take effect."
   ("(x)"  . ,(lean-input-to-string-list "⒳Ⓧⓧ"))
   ("(y)"  . ,(lean-input-to-string-list "⒴Ⓨⓨ"))
   ("(z)"  . ,(lean-input-to-string-list "⒵Ⓩⓩ"))
+  ("y"    . ("ɏ"))
+
 
   ))
   "A list of translations specific to the Lean input method.