diff --git a/src/thesis/motivation.agda b/src/thesis/motivation.agda
new file mode 100644
index 0000000..c6f15bf
--- /dev/null
+++ b/src/thesis/motivation.agda
@@ -0,0 +1,75 @@
+{-# OPTIONS --guardedness #-}
+
+-- Take this example as motivation:
+-- https://stackoverflow.com/questions/21808186/agda-reading-a-line-of-standard-input-as-a-string-instead-of-a-costring
+
+open import Level
+open import Agda.Builtin.Coinduction
+module thesis.motivation where
+
+module old-delay where
+  private
+    variable
+      a : Level
+  data _⊥ (A : Set a) : Set a where
+    now : A → A ⊥
+    later : ∞ (A ⊥) → A ⊥
+
+  never : ∀ {A : Set a} → A ⊥
+  never = later (♯ never)
+
+module ReverseInput where
+  open import Data.Char
+  open import Data.Nat
+  open import Data.List using (List; []; _∷_)
+  open import Data.String
+  open import Data.Unit.Polymorphic
+  open import Codata.Musical.Costring
+  open import Codata.Musical.Colist using ([]; _∷_)
+  -- open import IO using (IO; seq; bind; return; Main; run; putStrLn)
+  open import IO.Primitive
+  open import IO.Primitive.Infinite using (getContents)
+  open import Agda.Builtin.IO using ()
+
+  open old-delay
+  -- IDEA: start in haskell, then motivate in agda and define delay type
+  -- next talk about bisimilarity.
+  -- idea for slide title: dlrowolleh.hs and dlrowolleh.agda
+
+  private
+    variable
+      a : Level
+
+  -- reverse : Costring → String ⊥
+  -- reverse = go []
+  --   where
+  --   go : List Char → Costring → String ⊥
+  --   go acc []       = now (fromList acc)
+  --   go acc (x ∷ xs) = later (♯ go (x ∷ acc) (♭ xs))
+
+  -- putStrLn⊥ : String ⊥ → IO {a} ⊤
+  -- putStrLn⊥ (now   s) = putStrLn s
+  -- putStrLn⊥ (later s) = seq (♯ return tt) (♯ putStrLn⊥ (♭ s))
+
+  -- main : Main
+  -- main = run (bind (♯ {!  getContents !}) {!   !}) --(λ c → ♯ putStrLn⊥ (reverse c)))
+
+-- NOTE: This is not very understandable... Better stick to the outdated syntax
+module delay where
+  mutual
+    data _⊥ (A : Set) : Set where
+      now : A → A ⊥
+      later : A ⊥' → A ⊥
+    
+    record _⊥' (A : Set) : Set where
+      coinductive
+      field
+        force : A ⊥
+  open _⊥'
+
+  mutual
+    never : ∀ {A : Set} → A ⊥
+    never = later never'
+
+    never' : ∀ {A : Set} → A ⊥'
+    force never' = never