Delete useless commented out Yoneda garbage

Changes

1 changed files (+0/-15)

• Dao.lean
  • @@ -144,14 +144,6 @@ end Ch18
    namespace Yoneda - -- inductive Natural f g [Functor f] [Functor g] - -- | mk : (f a → g a) → Natural f g - - -- def Hom (a : Type u) := fun (x : Type u) ↦ x → a - - -- instance : Functor (Hom a) where - -- map f a := - class ContraFunctor (f : Type → Type) where contramap : (β → α) → f α → f β id_contramap (x : f α) : contramap id x = x
  • @@ -186,13 +178,6 @@ instance : Natural Option List OptionToList where
    simp [OptionToList] grind - -- abbrev Natural (f : Type → Type) [Functor f] [LawfulFunctor f] (g : Type → Type) [Functor g] [LawfulFunctor g] := - -- ∀ α, f α → g α - - -- example (f : Type → Type) [Functor f] [LawfulFunctor f] (g : Type → Type) [Functor g] [LawfulFunctor g] (η : Natural f g) (x : f α) (h : α → β) - -- : Functor.map (f := g) h (η α x) = η β (Functor.map (f := f) h x) := by - -- simp - -- OK time to do Yoneda part 2 /-- Hom-functor in enriched category -/