diff --git a/GenerateEverything.hs b/GenerateEverything.hs
index b4356c6bf0..4327bf3ba0 100644
--- a/GenerateEverything.hs
+++ b/GenerateEverything.hs
@@ -50,6 +50,9 @@ unsafeModules = map modToFile
   , "Data.Bytestring.IO"
   , "Data.Bytestring.IO.Primitive"
   , "Data.Bytestring.Primitive"
+  , "Data.List.Unsafe.Instances"
+  , "Data.Maybe.Unsafe.Instances"
+  , "Data.Nat.Unsafe.Instances"
   , "Data.Word8.Base"
   , "Data.Word8.Literals"
   , "Data.Word8.Primitive"
@@ -109,6 +112,9 @@ isUnsafeModule fp =
 withKModules :: [FilePath]
 withKModules = map modToFile
   [ "Axiom.Extensionality.Heterogeneous"
+  , "Data.List.Unsafe.Instances"
+  , "Data.Maybe.Unsafe.Instances"
+  , "Data.Nat.Unsafe.Instances"
   , "Data.Star.BoundedVec"
   , "Data.Star.Decoration"
   , "Data.Star.Environment"
diff --git a/src/Data/Integer/Instances.agda b/src/Data/Integer/Instances.agda
index b43ad23e66..683668138e 100644
--- a/src/Data/Integer/Instances.agda
+++ b/src/Data/Integer/Instances.agda
@@ -8,10 +8,21 @@
 
 module Data.Integer.Instances where
 
+open import Data.Integer.Base using (ℤ)
 open import Data.Integer.Properties using (_≡?_; ≤-isDecTotalOrder)
+open import Data.Integer.Show using () renaming (show to showℤ)
+open import Data.List.Base using (_++_)
+open import Data.String.Base using (toList)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 
+open import Text.Write using (Write)
+
 instance
   ℤ-≡-isDecEquivalence = isDecEquivalence _≡?_
   ℤ-≤-isDecTotalOrder = ≤-isDecTotalOrder
+
+instance
+  open Write
+  IntWrite : Write ℤ
+  IntWrite .writesPrecList _ i str = toList (showℤ i) ++ str
diff --git a/src/Data/List/Instances.agda b/src/Data/List/Instances.agda
index 3f28c89185..cba8597ebc 100644
--- a/src/Data/List/Instances.agda
+++ b/src/Data/List/Instances.agda
@@ -8,7 +8,7 @@
 
 module Data.List.Instances where
 
-open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Base using (List; []; _∷_; foldr)
 open import Data.List.Effectful
   using (functor; applicative; applicativeZero; alternative; monad
         ; monadZero; monadPlus)
@@ -22,6 +22,7 @@ open import Data.List.Relation.Binary.Pointwise
   using (Pointwise)
 open import Data.List.Relation.Binary.Lex.NonStrict
   using (Lex-≤; ≤-isDecTotalOrder)
+open import Data.Nat.Instances using (NatWrite)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
@@ -29,6 +30,7 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 open import Relation.Binary.TypeClasses
   using (IsDecTotalOrder; IsDecEquivalence; _≈?_)
+open import Text.Write
 
 private
   variable
@@ -58,3 +60,22 @@ instance
                              → {{IsDecTotalOrder _≈_ _≼_}}
                              → IsDecTotalOrder (Pointwise _≈_) (Lex-≤ _≈_ _≼_)
   List-Lex-≤-isDecTotalOrder {{≼-isDecTotalOrder}} = ≤-isDecTotalOrder ≼-isDecTotalOrder
+
+------------------------------------------------------------------------
+-- List write
+
+open Write {{...}}
+
+instance
+  ListWrite : {{ Write A }} → Write (List A)
+  ListWrite .writesPrecList prec [] str = '[' ∷ (']' ∷ str)
+  ListWrite .writesPrecList prec (x ∷ xs) str = '[' ∷ writesPrecList prec x (listWrite' prec str xs)
+    where
+      -- after the first call, don't prepend '['
+      listWrite' : {{ Write A }} → Precedence → List Char → List A → List Char
+      listWrite' prec str = foldr (λ x str → ',' ∷ writesPrecList prec x str) (']' ∷ str)
+
+-- some examples to write the instances working
+private
+  test[ℕ] : String
+  test[ℕ] = write (5 ∷ 2 ∷ 12 ∷ 42 ∷ [])
diff --git a/src/Data/List/Unsafe/Instances.agda b/src/Data/List/Unsafe/Instances.agda
new file mode 100644
index 0000000000..39ee0cacd1
--- /dev/null
+++ b/src/Data/List/Unsafe/Instances.agda
@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe instances for List
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K #-}
+
+module Data.List.Unsafe.Instances where
+
+open import Data.List.Base
+open import Data.Nat.Base
+open import Data.Nat.Instances
+open import Level using (Level)
+open import Text.Write
+open import Text.Pretty 80
+
+private
+  variable
+    a : Level
+    A : Set a
+
+open Pretty {{...}}
+
+instance
+  ListPretty : {{ Pretty A }} → Pretty (List A)
+  ListPretty .pPrintPrec prec xs = parens (commaSep (map (pPrintPrec prec) xs))
diff --git a/src/Data/Maybe/Unsafe/Instances.agda b/src/Data/Maybe/Unsafe/Instances.agda
new file mode 100644
index 0000000000..1011efa9ef
--- /dev/null
+++ b/src/Data/Maybe/Unsafe/Instances.agda
@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe instances for Maybe
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K #-}
+
+module Data.Maybe.Unsafe.Instances where
+
+open import Data.Maybe.Base
+open import Text.Pretty 80
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+instance
+  open Pretty {{...}}
+  MaybePretty : {{ Pretty A }} → Pretty (Maybe A)
+  MaybePretty .pPrintPrec prec (just x) = (text "just") <+> pPrintPrec prec x
+  MaybePretty .pPrintPrec prec nothing = text "nothing"
diff --git a/src/Data/Nat/Instances.agda b/src/Data/Nat/Instances.agda
index efe7e48d3e..245151f83d 100644
--- a/src/Data/Nat/Instances.agda
+++ b/src/Data/Nat/Instances.agda
@@ -8,10 +8,32 @@
 
 module Data.Nat.Instances where
 
+open import Data.Char using (isDigit)
+open import Data.List.Base using (_++_; spanᵇ)
+open import Data.Maybe using (_>>=_; just)
+open import Data.Nat.Base using (ℕ; _≤ᵇ_)
 open import Data.Nat.Properties using (≤-isDecTotalOrder; _≡?_)
+open import Data.Nat.Show using (readMaybe) renaming (show to showℕ)
+open import Data.Product using (_,_)
+open import Data.String.Base using (toList; fromList)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
+open import Text.Read using (Read)
+open import Text.Write using (Write)
 
 instance
   ℕ-≡-isDecEquivalence = isDecEquivalence _≡?_
   ℕ-≤-isDecTotalOrder = ≤-isDecTotalOrder
+
+instance
+  open Write
+  NatWrite : Write ℕ
+  NatWrite .writesPrecList _ n str = (toList (showℕ n)) ++ str
+
+instance
+  open Read {{...}}
+  NatRead : Read ℕ
+  NatRead .readsPrecList prec str = do
+    let (digits , leftover) = spanᵇ isDigit str
+    num ← readMaybe 10 (fromList digits)
+    just (num , leftover)
diff --git a/src/Data/Nat/Unsafe/Instances.agda b/src/Data/Nat/Unsafe/Instances.agda
new file mode 100644
index 0000000000..1b0f89f14f
--- /dev/null
+++ b/src/Data/Nat/Unsafe/Instances.agda
@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe instances for Nat
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K #-}
+
+module Data.Nat.Unsafe.Instances where
+
+open import Data.Nat.Base
+open import Data.Nat.Show using (show)
+open import Text.Pretty 80
+
+instance
+  open Pretty {{...}}
+  ℕPretty : Pretty ℕ
+  ℕPretty .pPrintPrec prec n = text (show n)
diff --git a/src/Text/Pretty.agda b/src/Text/Pretty.agda
index a9202b1f82..f305a3f4ec 100644
--- a/src/Text/Pretty.agda
+++ b/src/Text/Pretty.agda
@@ -12,6 +12,7 @@ open import Data.Nat.Base using (ℕ)
 
 module Text.Pretty (width : ℕ) where
 
+open import Agda.Builtin.Reflection using (Precedence) public
 import Level
 open import Data.Char.Base using (Char)
 open import Data.List.Base
@@ -137,3 +138,20 @@ commaSep = foldDoc (λ d e → d <> comma <+> e)
 
 newline : Doc
 newline = flush empty
+
+------------------------------------------------------------------------
+-- Pretty class
+
+private
+  variable
+    a : Level.Level
+
+record Pretty (A : Set a) : Set a where
+  field
+    pPrintPrec : Precedence → A → Doc
+
+  pPrint : A → Doc
+  pPrint = pPrintPrec Precedence.unrelated
+
+  pretty : A → String
+  pretty = render ∘ pPrint
diff --git a/src/Text/Read.agda b/src/Text/Read.agda
new file mode 100644
index 0000000000..99bcde109e
--- /dev/null
+++ b/src/Text/Read.agda
@@ -0,0 +1,41 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Read class
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe  #-}
+
+module Text.Read where
+
+-- should builtin be used?
+open import Agda.Builtin.Reflection using (Precedence) public
+open import Data.Char.Base using (Char) public
+open import Data.List.Base using (List; []; _++_; _∷_)
+open import Data.Maybe.Base using (Maybe; just; nothing; map)
+open import Data.Product.Base using (_×_; _,_; proj₁) renaming (map to map×)
+open import Data.String.Base using (String) public
+open import Data.String.Base using (fromList; toList)
+open import Function.Base using (_∘_; const; _$_; id)
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record Read (A : Set a) : Set a where
+  field
+    readsPrecList : Precedence → List Char → Maybe (A × List Char)
+
+  readPrecList : Precedence → List Char → Maybe A
+  readPrecList prec str = map proj₁ (readsPrecList prec str)
+
+  readsPrec : Precedence → String → Maybe (A × String)
+  readsPrec prec str = map (map× id fromList) (readsPrecList prec (toList str))
+
+  readPrec : Precedence → String → Maybe A
+  readPrec prec = (readPrecList prec) ∘ toList
+
+  read : String → Maybe A
+  read = readPrec Precedence.unrelated
diff --git a/src/Text/ReadWrite.agda b/src/Text/ReadWrite.agda
new file mode 100644
index 0000000000..da8fff8cfb
--- /dev/null
+++ b/src/Text/ReadWrite.agda
@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- ReadWrite class
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe  #-}
+
+module Text.ReadWrite where
+
+-- should builtin be used?
+open import Agda.Builtin.Reflection using (Precedence) public
+open import Data.Char.Base using (Char) public
+open import Data.List.Base using (List; []; _++_; _∷_)
+open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.Maybe.Base using (just)
+open import Data.String.Base using (String) public
+open import Data.String.Base using (fromList; toList)
+open import Function.Base using (_∘_; const; _$_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Text.Write using (Write)
+open import Text.Read using (Read)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record ReadWrite (A : Set a) :  Set a where
+  open Read
+  open Write
+
+  field
+    reader : Read A
+    writer : Write A
+
+    readWrite : ∀ {x : A} → read reader (write writer x) ≡ (just x)
+    writeRead : ∀ {x : A} {s : String} → (read reader s) ≡ (just x) → writeMaybe writer (read reader s) ≡ s
+
diff --git a/src/Text/Write.agda b/src/Text/Write.agda
new file mode 100644
index 0000000000..a117c1fbab
--- /dev/null
+++ b/src/Text/Write.agda
@@ -0,0 +1,45 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Write class
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe  #-}
+
+module Text.Write where
+
+-- should builtin be used?
+open import Agda.Builtin.Reflection using (Precedence) public
+open import Data.Char.Base using (Char) public
+open import Data.List.Base using (List; []; _++_; _∷_)
+open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.String.Base using (String) public
+open import Data.String.Base using (fromList; toList)
+open import Function.Base using (_∘_; const; _$_)
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record Write (A : Set a) :  Set a where
+  field
+    writesPrecList :  Precedence → A → List Char → List Char
+
+  writePrecList : Precedence → A → List Char
+  writePrecList prec x =  writesPrecList prec x []
+
+  writesPrec : Precedence → A → String → String
+  writesPrec prec x str = fromList (writesPrecList prec x (toList str))
+
+  writePrec : Precedence → A → String
+  writePrec prec x = fromList (writesPrecList prec x [])
+
+  write : A → String
+  write = writePrec Precedence.unrelated
+
+  writeMaybe : Maybe A → String
+  writeMaybe nothing = ""
+  writeMaybe (just x) = write x
diff --git a/src/Text/Write/Deriving.agda b/src/Text/Write/Deriving.agda
new file mode 100644
index 0000000000..40335fbe53
--- /dev/null
+++ b/src/Text/Write/Deriving.agda
@@ -0,0 +1,203 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Macro for deriving instances of Write
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+-- NOTE: still figuring things out, just pushing to get over to other device
+
+module Text.Write.Deriving where
+
+-- Much understanding and structure taken from
+--   ∙ https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda
+--   ∙ https://github.com/alhassy/gentle-intro-to-reflection
+
+open import Data.List.Base using (_∷_; []; List; concat; _++_; zip)
+open import Data.List.Effectful
+open import Data.Nat.Base using (ℕ; _+_)
+open import Data.Nat.Instances using (NatWrite)
+open TraversableM using (mapM)
+open import Data.Unit using (⊤)
+open import Data.Product.Base using (_×_; _,_; uncurry; proj₁; proj₂)
+open import Reflection
+open import Reflection.AST.Term using (Telescope; Clause)
+open import Reflection.TCM
+open import Reflection.TCM.Effectful using () renaming (monad to monadTCM)
+open import Text.Write using (Write; Char; Precedence)
+
+data Test : Set where
+  a : ℕ → (x : ℕ) → ℕ → Test
+
+{-
+Should this be placed in Tactic.DerivingWrite?
+
+For now, some notes on design:
+
+Should print syntactically correct Agda that can be read by
+an also derived Read instance.
+
+Steps:
+1. Check term is actually a data/record definition, if not throw typecheck error?
+2. Get all parameters and attach required instances to the resulting function type
+
+   only need instances for types within constructors, e.g.
+
+   data {a : Level} {A : Set} → MyData A : Set a where
+     c : A → A → MyData A
+
+   needs to have
+
+   {a : Level} {A : Set} {{ Write A }} → Write (List A)
+
+   NOT
+
+   {a : Level} {A : Set} {{ Write a }} {{ Write A }} → Write (List A)
+
+
+3. For records, print in record syntax (record { x = y, ... }), recursively
+   calling write on fields
+4. For data, get fixity of constructor and recursively call write, intertwining
+   parts of the constructors name in a way that properly aligns with fixity
+
+   (e.g. print x ∷ [] as "x ∷ []", not "_∷_ x []")
+
+Reflection notes:
+- Prelude has a lot of machinery that should be moved over
+- Should derive *own* type so we know the exact order things are in
+- Instance arguments MUST be included in telescope and argument patterns, and must be provided
+  to calls to writesPrecList, as opposed to say instance resolution within the definition.
+  (at least I think)
+- Clause takes telescope of arguments (i.e. the type of the given function without the return value)
+  AND a list of patterns applied to those arguments. If no pattern matching is applied, just the
+  deBruijin index within a var pattern should be given.
+
+-}
+
+------------------------------------------------------------------------
+-- Machinery for deriving things
+
+telView : Type → Telescope × Type
+telView (pi x (abs y b)) = ((y , x) ∷ (proj₁ telVb)) , proj₂ telVb
+  where
+    telVb : Telescope × Type
+    telVb = telView b
+{-# CATCHALL #-}
+telView x                = [] , x
+
+-- Construct a Type out of a Telescope and Core Type
+telToType : Telescope → Type → Type
+telToType tel core = {!!}
+
+-- Return a list of all types that appear in the constructors
+-- or fields of a data or record type that aren't the type itself
+-- in order of appearance
+--
+-- e.g. for
+-- data X : Set where
+--   c₁ : ℕ → X
+--   c₂ : Bool → X → X
+--
+-- This should return ℕ, Bool
+consArgTypes : Type → List Type
+consArgTypes = {!!}
+
+instanceArg : Arg Name
+instanceArg = arg (arg-info instance′ defaultModality) (quote Write)
+
+-- Derive the telescope for the type of an instance,
+--
+-- e.g. for Write List this returns
+--      {a : Level} {A : Set a} {{ Write A }}
+instanceTel : Name → Name → TC Telescope
+instanceTel = {!!}
+
+-- Derive the type of an instance for a given record type,
+-- prepending all required instances to the telescope
+--
+-- e.g. for Write (List), will give
+--      : {{ Write A }} → Write (List A)
+instanceType : Name → Name → TC Type
+instanceType cls inst = do
+  clsT ← getType cls
+  instT ← getType inst
+  tel ← instanceTel cls inst
+  pure (telToType tel {!!})
+
+telStr : Telescope → List ErrorPart
+telStr [] = strErr "[]" ∷ []
+telStr ((nm , arg i t) ∷ xs) = strErr nm ∷ termErr t ∷ (telStr xs)
+
+vra : {A : Set} → A → Arg A
+vra = arg (arg-info visible (modality relevant quantity-0))
+
+vrv :  ℕ → List (Arg Term) → Arg Term
+vrv n args = arg (arg-info visible (modality relevant quantity-0)) (var n args)
+
+vri : ℕ → Arg Term
+vri n = arg (arg-info instance′ (modality relevant quantity-0)) (var n [])
+
+vrv' : ℕ → Arg Term
+vrv' n = vrv n []
+
+------------------------------------------------------------------------
+-- Machinery specific to Write
+
+-- TODO: doc comment can be better
+-- given the telescope for a constructor, produce the whole telescope for
+-- its clause
+-- Precedence → A → List Char → List Char
+conTel : Telescope → Telescope
+conTel tel =  ("str" , (vra (quoteTerm (List Char)))) ∷ (tel ++ ("prec" , (vra (quoteTerm Precedence))) ∷ [])
+
+------------------------------------------------------------------------
+-- Derive macro for Write
+
+-- test implementation, no bracketing
+
+-- concat write calls to each argument in a telescope for Write
+-- suc suc N is used because we have Prec → A → List Char → List Char, so everything is one more away
+-- because of the List Char taken as an argument
+
+telWrite : ℕ → Term
+telWrite ℕ.zero = con (quote List.[]) []
+telWrite (ℕ.suc n) = def (quote _++_) (vra (def (quote Write.writesPrecList) (vri 5 ∷ vrv' 0 ∷ vrv' (1 + n) ∷ vrv' 4 ∷ [])) ∷ (vra (telWrite n)) ∷ [])
+-- telWrite 0 = con (quote (List.[])) []
+-- telWrite (suc n) = def (quote _++_) ({!!} ∷ {!!})
+
+varPat : ℕ → Arg Pattern
+varPat n = vra (Pattern.var n)
+
+telToVarPat : ℕ → List (Arg Pattern)
+telToVarPat 0 = []
+telToVarPat (ℕ.suc n) = telToVarPat n ++ (varPat (1 + n)) ∷ []
+
+-- derive the clause for a single constructor
+consClause : Name → Type → Clause
+consClause nm t with telView t
+... | tel , _ = Clause.clause (conTel tel) (varPat 0 ∷ (vra (Pattern.con nm (telToVarPat (Data.List.Base.length tel)))) ∷ varPat 4 ∷ []) (telWrite (Data.List.Base.length tel))
+
+deriveWriteFun : Name → Definition → Definition
+deriveWriteFun nm (Reflection.data-type pars cs) = function (Data.List.Base.map (uncurry consClause) {!!})
+deriveWriteFun nm (Reflection.record-type c fs) = {!!}
+{-# CATCHALL #-}
+deriveWriteFun _ _ = function []
+-- cs in data-type contains actual constructor names
+-- 'name' in data-cons is just name of data type itself
+deriveWrite' : Definition → Term → TC ⊤
+deriveWrite' (Reflection.record-type c fs) met = {!!}
+deriveWrite' (data-type p cs) met = do
+  ts ← mapM monadTCM getType cs
+  let clauses = (Data.List.Base.map (uncurry consClause) (zip cs ts))
+      term = telWrite 5
+  typeError (termErr (pat-lam clauses []) ∷ [])
+-- unify met (pat-lam clauses [])
+{-# CATCHALL #-}
+deriveWrite' _ _  = typeError (strErr "Write instances can only be derived for data and record types" ∷ [])
+
+macro
+  deriveWrite : Name → Term → TC ⊤
+  deriveWrite nm met = do
+    d ← getDefinition nm
+    deriveWrite' d met