diff --git a/lakefile.lean b/lakefile.lean
index e47e0d0..00f4307 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,6 +4,8 @@ open Lake DSL
 require batteries from git "https://github.com/leanprover-community/batteries.git" @ "v4.14.0"
 require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.14.0"
 
+require "lens-demo" from git "https://github.com/funexists/lens-demo.git" @ "19c9d9ceed57744a5afd4540593cb943ae407701"
+
 require raylean from git "https://github.com/funexists/raylean.git" @ "3a60f54222e06767daa93e50a8fcbc68975eee4c" with
   NameMap.empty
     |>.insert `bundle "off"
diff --git a/src/Lens.lean b/src/Lens.lean
deleted file mode 100644
index 97c0f3e..0000000
--- a/src/Lens.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-import Lens.Basic
-import Lens.Elab
diff --git a/src/Lens/Basic.lean b/src/Lens/Basic.lean
deleted file mode 100644
index 1e51801..0000000
--- a/src/Lens/Basic.lean
+++ /dev/null
@@ -1,62 +0,0 @@
-import Lens.Const
-open Const
-
-def Lens (s t a b : Type) :=
-  ∀ {f : Type → Type} [Functor f], (a → f b) → s → f t
-
-namespace Lens
-
-def view {s a : Type} (l : Lens s s a a) (x : s) : a :=
-  (l (fun y => (y : Const a a)) x : Const a s)
-
-def set {s t a b : Type} (l : Lens s t a b) (y : b) (x : s) : t :=
-  (l (fun _ => y) x : Id t)
-
-def over {s t a b : Type} (l : Lens s t a b) (f : a → b) (x : s) : t :=
-  (l (fun a => f a) x : Id t)
-
-infixl:50 " ^. " => flip view
-
-end Lens
-
-namespace Example
-open Lens
-
-structure Name where
-  firstname : String
-  surname : String
-
-structure Person where
-  name : Name
-  age : Nat
-
-namespace Example.Lens
-
-def firstname : Lens Name Name String String :=
-  fun {f} [Functor f] g p =>
-    Functor.map (fun newFirstName => { p with firstname := newFirstName }) (g p.firstname)
-
-def name : Lens Person Person Name Name :=
-  fun {f} [Functor f] g p =>
-    Functor.map (fun newName => { p with name := newName }) (g p.name)
-
-end Example.Lens
-
-open Example.Lens
-
-def exampleView : IO Unit :=
-  let person : Person := { name := {firstname := "Alice", surname := "H"}, age := 30 }
-  let personName := person ^. name ∘ firstname
-  IO.println s!"Name: {personName}"
-
-def exampleSet : IO Unit :=
-  let person := { name := { firstname := "Alice", surname := "H"}, age := 30 }
-  let updatedPerson := set (name ∘ firstname) "Bob" person
-  IO.println s!"Updated name: {updatedPerson.name.firstname}"
-
-def exampleOver : IO Unit :=
-  let person := { name := {firstname := "Alice", surname := "H"} , age := 30 }
-  let updatedPerson := over (name ∘ firstname) (String.append · "zzzSmith") person
-  IO.println s!"Modified name: {updatedPerson.name.firstname}"
-
-end Example
diff --git a/src/Lens/Const.lean b/src/Lens/Const.lean
deleted file mode 100644
index 0685c34..0000000
--- a/src/Lens/Const.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-def Const (m : Type u) (_α : Type v) : Type u := m
-
-namespace Const
-
-@[always_inline]
-instance {m : Type u} : Functor (Const m) where
-  map _ x := x
-
-@[always_inline, inline]
-def run (x : Const m α) : m := x
-
-end Const
diff --git a/src/Lens/Elab.lean b/src/Lens/Elab.lean
deleted file mode 100644
index 9d9c1bc..0000000
--- a/src/Lens/Elab.lean
+++ /dev/null
@@ -1,90 +0,0 @@
-import Lens.Basic
-
-import Lean
-
-namespace Lens
-
-/-
-makeLenses T` creates a lens for each field of the structure `T`.
-The name of the lens is the same as the corresponding projection function.
-The lenses are declared in the namespace T.Lens.
--/
-open Lean Elab Command Term Meta in
-elab "makeLenses" structIdent:ident : command => do
-  let name ← resolveGlobalConstNoOverload structIdent
-  let env ← getEnv
-  let some info := getStructureInfo? env name
-    | throwErrorAt structIdent "Not a structure"
-  let mut defs : Array Syntax := #[]
-  let lensNs := mkIdent <| structIdent.raw.getId ++ Name.mkSimple "Lens"
-  for field in info.fieldInfo do
-    let fieldNameIdent := mkIdent field.fieldName
-    let some decl := env.find? (field.projFn)
-      | throwErrorAt structIdent s!"Could not find project function {field.projFn}"
-    let (some fieldTypeName, some fieldTypeArgs) := (← liftTermElabM (liftMetaM (
-             forallTelescope decl.type fun _ body
-               => pure (body.getAppFn.constName?, body.getAppArgs.mapM (·.constName?)))))
-      | throwErrorAt structIdent "Not a structure name"
-    let d ← fieldTypeArgs.mapM fun argName => `($(mkIdent argName))
-    let fieldTypeNameIdent := Syntax.mkCApp fieldTypeName d
-    let lensName := mkIdent field.fieldName
-    let newVal := mkIdent <| Name.mkSimple "newVal"
-    let l ←
-      `(fun {f} [Functor f] g p =>
-        Functor.map
-          (fun $newVal =>
-            { p with $fieldNameIdent:ident := $newVal})
-            (g p.$fieldNameIdent:ident))
-    defs := defs.push
-      (← `(def $lensName : @Lens $(mkIdent name) $(mkIdent name) $fieldTypeNameIdent $fieldTypeNameIdent := $l))
-  elabCommand (← `(namespace $lensNs))
-  for d in defs do
-    elabCommand d
-  elabCommand (← `(end $lensNs))
-
-end Lens
-
-namespace Example
-
-open Lens
-
-structure P where
-  name : Nat
-
-makeLenses P
-
-structure Name' where
-  firstname : String
-  surname : String
-
-structure Person' where
-  name : Name'
-  age : Nat
-
-structure Group where
-  people : List Person'
-
-makeLenses Name'
-makeLenses Person'
-makeLenses Group
-
-open Person'.Lens
-open Name'.Lens
-open Group.Lens
-
-def exampleView' : IO Unit :=
-  let person : Person' := { name := {firstname := "Alice", surname := "H"}, age := 30 }
-  let personName := person ^. name ∘ firstname
-  IO.println s!"Name: {personName}"
-
-def exampleSet' : IO Unit :=
-  let person : Person' := { name := { firstname := "Alice", surname := "H"}, age := 30 }
-  let updatedPerson := set (name ∘ firstname) "Bob" person
-  IO.println s!"Updated name: {updatedPerson.name.firstname}"
-
-def exampleOver' : IO Unit :=
-  let person := { name := {firstname := "Alice", surname := "H"} , age := 30 }
-  let updatedPerson := over (name ∘ firstname) (String.append · "zzzSmith") person
-  IO.println s!"Modified name: {updatedPerson.name.firstname}"
-
-end Example