diff --git a/thesis/agda/motivation.agda b/thesis/agda/motivation.agda
deleted file mode 100644
index c6f15bf..0000000
--- a/thesis/agda/motivation.agda
+++ /dev/null
@@ -1,75 +0,0 @@
-{-# 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
diff --git a/thesis/agda/setoids.agda b/thesis/agda/setoids.agda
new file mode 100644
index 0000000..46a9e70
--- /dev/null
+++ b/thesis/agda/setoids.agda
@@ -0,0 +1,47 @@
+module Foo where
+  open import Level
+
+  record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+    constructor _,_
+    field
+      fst : A
+      snd : B
+  open _×_
+
+  <_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
+          → (A → B) → (A → C) → A → (B × C)
+  < f , g > x = (f x , g x)
+
+  record ⊤ {l} : Set l where
+    constructor tt
+  
+  ! : ∀ {l} {X : Set l} → X → ⊤ {l}
+  ! _ = tt
+
+  data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+    i₁ : A → A + B
+    i₂ : B → A + B 
+
+  [_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+          → (A → C) → (B → C) → (A + B) → C
+  [ f , g ] (i₁ x) = f x
+  [ f , g ] (i₂ x) = g x
+
+  data ⊥ {l} : Set l where
+
+  ¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
+  ¡ ()
+
+  distributeˡ⁻¹ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A × B) + (A × C) → A × (B + C)
+  distributeˡ⁻¹ (i₁ (x , y)) = (x , i₁ y)
+  distributeˡ⁻¹ (i₂ (x , y)) = (x , i₂ y)
+
+  distributeˡ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → A × (B + C) → (A × B) + (A × C)
+  distributeˡ (x , i₁ y) = i₁ (x , y)
+  distributeˡ (x , i₂ y) = i₂ (x , y) 
+
+  curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (C × A → B) → C → A → B
+  curry f x y = f (x , y)
+
+  eval : ∀ {a b} {A : Set a} {B : Set b} → ((A → B) × A) → B
+  eval (f , x) = f x