diff --git a/app/Repl.hs b/app/Repl.hs
index ce0d9b4..7ddf142 100644
--- a/app/Repl.hs
+++ b/app/Repl.hs
@@ -51,7 +51,7 @@ actOnParse :: String -> (Expr -> InputT IO ()) -> InputT IO ()
 actOnParse input action = either outputStrLn (action . elaborate) $ parseExpr "repl" (pack input)
 
 printErrorOrResult :: Env -> (Expr -> ReaderT Env Result Expr) -> Expr -> InputT IO ()
-printErrorOrResult env action expr = putTextLn $ either toText pretty $ runReaderT (action expr) env
+printErrorOrResult env action expr = putTextLn $ either toText prettyT $ runReaderT (action expr) env
 
 parseActPrint :: Env -> String -> (Expr -> ReaderT Env Result Expr) -> InputT IO ()
 parseActPrint env input action = actOnParse input (printErrorOrResult env action)
@@ -75,7 +75,7 @@ repl = do
             Just Quit -> pure env
             Just DumpEnv -> lift (dumpEnv env) >> loop env
             Just (TypeQuery input) -> parseActPrint env input (findType []) >> loop env
-            Just (ValueQuery input) -> lookupAct env input (putTextLn . pretty . _val) >> loop env
+            Just (ValueQuery input) -> lookupAct env input (putTextLn . prettyT . _val) >> loop env
             Just (Normalize input) -> parseActPrint env input normalize >> loop env
             Just (WeakNormalize input) -> parseActPrint env input whnf >> loop env
             Just (DumpDebug input) -> either outputStrLn (outputStrLn . show) (parseDef "repl" (pack input)) >> loop env
diff --git a/examples/peano.pg b/examples/peano.pg
index f1561e1..c7de3f5 100644
--- a/examples/peano.pg
+++ b/examples/peano.pg
@@ -3,10 +3,6 @@
 -- import basic logic definitions from <logic.pg>
 
 @include logic.pg
-@include algebra.pg
-
-def comp (A B C : *) (g : B -> C) (f : A -> B) (x : A) : C :=
-  g (f x);
 
 -- }}}
 
@@ -473,7 +469,8 @@ def one_plus_one_two : eq nat (plus one one) two :=
 -- We will now prove a couple standard properties of addition.
 
 -- First, associativity, namely that n + (m + p) = (n + m) + p.
-def plus_assoc : assoc nat plus := fun (n m : nat) =>
+def plus_assoc : forall (n m p : nat), eq nat (plus n (plus m p)) (plus (plus n m) p)
+  := fun (n m : nat) =>
   -- We prove this via induction on p for any fixed n and m.
   nat_ind
     (fun (p : nat) => eq nat (plus n (plus m p)) (plus (plus n m) p))
diff --git a/lib/Check.hs b/lib/Check.hs
index 0259790..01a8e87 100644
--- a/lib/Check.hs
+++ b/lib/Check.hs
@@ -22,7 +22,7 @@ findLevel g a = do
     whnf s >>= \case
         Level i -> pure i
         Star -> pure $ -1 -- HACK: but works, so...
-        _ -> throwError $ NotASort a s
+        _ -> throwError $ NotASort a
 
 validateType :: Context -> Expr -> ReaderT Env Result ()
 validateType g a = void $ findLevel g a
@@ -39,9 +39,9 @@ compSort _ _ (Level i) Star
     | i == 0 = pure Star
     | otherwise = pure $ Level i
 compSort _ _ (Level i) (Level j) = pure $ Level $ max i j
-compSort a b left right
-    | isSort left = throwError $ NotASort b right
-    | otherwise = throwError $ NotASort a left
+compSort a b left _
+    | isSort left = throwError $ NotASort b
+    | otherwise = throwError $ NotASort a
 
 findType :: Context -> Expr -> ReaderT Env Result Expr
 findType _ Star = pure $ Level 0
diff --git a/lib/Errors.hs b/lib/Errors.hs
index 97629ff..bc93410 100644
--- a/lib/Errors.hs
+++ b/lib/Errors.hs
@@ -1,25 +1,35 @@
 module Errors where
 
 import Expr
+import Prettyprinter
+import Prettyprinter.Render.Text
+import Prelude hiding (group)
 
 data Error
     = UnboundVariable Text
-    | NotASort Expr Expr
+    | NotASort Expr
     | ExpectedPiType Expr Expr
     | NotEquivalent Expr Expr Expr
     | PNMissingType Text
     | DuplicateDefinition Text
-    | EmptySection Text
     deriving (Eq, Ord)
 
+instance Pretty Error where
+    pretty (UnboundVariable x) = "Unbound variable: '" <> pretty x <> "'"
+    pretty (NotASort x) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> "is not a type"
+    pretty (ExpectedPiType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> hang 4 ("is not a function, instead is type" <> line <> pretty t)
+    pretty (NotEquivalent a a' e) =
+        group $
+            hang 4 ("Cannot unify" <> line <> pretty a)
+                <> line
+                <> hang 4 ("with" <> line <> pretty a')
+                <> line
+                <> hang 4 ("when evaluating" <> line <> pretty e)
+    pretty (PNMissingType x) = "Axiom '" <> pretty x <> "' missing type ascription"
+    pretty (DuplicateDefinition n) = "'" <> pretty n <> "' already defined"
+
 instance ToText Error where
-    toText (UnboundVariable x) = "Unbound variable: '" <> x <> "'"
-    toText (NotASort x t) = "Expected '" <> pretty x <> "' to have type * or □, instead found '" <> pretty t <> "'"
-    toText (ExpectedPiType x t) = "'" <> pretty x <> "' : '" <> pretty t <> "' is not a function"
-    toText (NotEquivalent a a' e) = "Cannot unify '" <> pretty a <> "' with '" <> pretty a' <> "' when evaluating '" <> pretty e <> "'"
-    toText (PNMissingType x) = "Axiom '" <> x <> "' missing type ascription"
-    toText (DuplicateDefinition n) = "'" <> n <> "' already defined"
-    toText (EmptySection var) = "Tried to declare variable " <> var <> " without a section"
+    toText = renderStrict . layoutSmart (LayoutOptions (AvailablePerLine 100 1.0)) . pretty
 
 instance ToString Error where
     toString = toString . toText
diff --git a/lib/Eval.hs b/lib/Eval.hs
index daa1b5a..25994fb 100644
--- a/lib/Eval.hs
+++ b/lib/Eval.hs
@@ -26,7 +26,7 @@ emptyEnv :: Env
 emptyEnv = M.empty
 
 showEnvEntry :: Text -> Definition -> Text
-showEnvEntry k Def{_ty = t} = k <> " : " <> pretty t
+showEnvEntry k Def{_ty = t} = k <> " : " <> prettyT t
 
 dumpEnv :: Env -> IO ()
 dumpEnv = void . M.traverseWithKey ((putTextLn .) . showEnvEntry)
diff --git a/lib/Expr.hs b/lib/Expr.hs
index 28beb76..cef3632 100644
--- a/lib/Expr.hs
+++ b/lib/Expr.hs
@@ -1,5 +1,10 @@
 module Expr where
 
+import qualified Data.List.NonEmpty as NE
+import Prettyprinter
+import Prettyprinter.Render.Text
+import Prelude hiding (group)
+
 data Expr where
     Var :: Text -> Integer -> Expr
     Free :: Text -> Expr
@@ -12,6 +17,9 @@ data Expr where
     Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr
     deriving (Show, Ord)
 
+instance Pretty Expr where
+    pretty = prettyExpr 0 . cleanNames
+
 instance Eq Expr where
     (Var _ n) == (Var _ m) = n == m
     (Free s) == (Free t) = s == t
@@ -53,21 +61,28 @@ incIndices = shiftIndices 1 0
 
 {- --------------------- PRETTY PRINTING ----------------------------- -}
 
-parenthesize :: Text -> Text
-parenthesize s = "(" <> s <> ")"
+data Param = Param Text Expr
+data ParamGroup = ParamGroup [Text] Expr
+data Binding = Binding Text [ParamGroup] Expr
 
-type Param = (Text, Expr)
-type ParamGroup = ([Text], Expr)
-type Binding = (Text, [ParamGroup], Expr)
+instance Pretty Param where
+    pretty (Param x ty) = group $ parens $ pretty x <+> ":" <+> pretty ty
+
+instance Pretty ParamGroup where
+    pretty (ParamGroup vars ty) = group $ parens $ align (sep (map pretty vars)) <+> ":" <+> pretty ty
+
+instance Pretty Binding where
+    pretty (Binding var [] body) = group $ parens $ pretty var <+> ":=" <+> pretty body
+    pretty (Binding var params body) = group $ parens $ pretty var <+> align (sep (map pretty params)) <+> ":=" <+> pretty body
 
 collectLambdas :: Expr -> ([Param], Expr)
-collectLambdas (Abs x ty _ body) = ((x, ty) : params, final)
+collectLambdas (Abs x ty _ body) = (Param x ty : params, final)
   where
     (params, final) = collectLambdas body
 collectLambdas e = ([], e)
 
 collectLets :: Expr -> ([Binding], Expr)
-collectLets (Let x _ val body) = ((x, params', val') : bindings, final)
+collectLets (Let x _ val body) = (Binding x params' val' : bindings, final)
   where
     (bindings, final) = collectLets body
     (params, val') = collectLambdas val
@@ -76,11 +91,17 @@ collectLets e = ([], e)
 
 collectPis :: Expr -> ([Param], Expr)
 collectPis p@(Pi "" _ _ _) = ([], p)
-collectPis (Pi x ty _ body) = ((x, ty) : params, final)
+collectPis (Pi x ty _ body) = (Param x ty : params, final)
   where
     (params, final) = collectPis body
 collectPis e = ([], e)
 
+collectApps :: Expr -> NonEmpty Expr
+collectApps (App e1 e2) = e2 :| toList rest
+  where
+    rest = collectApps e1
+collectApps e = pure e
+
 cleanNames :: Expr -> Expr
 cleanNames (App m n) = App (cleanNames m) (cleanNames n)
 cleanNames (Abs x ty a body) = Abs x (cleanNames ty) a (cleanNames body)
@@ -92,25 +113,13 @@ cleanNames e = e
 groupParams :: [Param] -> [ParamGroup]
 groupParams = foldr addParam []
   where
-    addParam :: (Text, Expr) -> [([Text], Expr)] -> [([Text], Expr)]
-    addParam (x, t) [] = [([x], t)]
-    addParam (x, t) l@((xs, s) : rest)
-        | incIndices t == s = (x : xs, t) : rest
-        | otherwise = ([x], t) : l
+    addParam :: Param -> [ParamGroup] -> [ParamGroup]
+    addParam (Param x t) [] = [ParamGroup [x] t]
+    addParam (Param x t) l@(ParamGroup xs s : rest)
+        | incIndices t == s = ParamGroup (x : xs) t : rest
+        | otherwise = ParamGroup [x] t : l
 
-showParamGroup :: ParamGroup -> Text
-showParamGroup (ids, ty) = parenthesize $ unwords ids <> " : " <> pretty ty
-
-showBinding :: Binding -> Text
-showBinding (ident, params, val) =
-    parenthesize $
-        ident
-            <> " "
-            <> unwords (map showParamGroup params)
-            <> " := "
-            <> pretty val
-
-printLevel :: Integer -> Text
+printLevel :: Integer -> Doc ann
 printLevel k
     | k == 0 = "₀"
     | k == 1 = "₁"
@@ -122,40 +131,54 @@ printLevel k
     | k == 7 = "₇"
     | k == 8 = "₈"
     | k == 9 = "₉"
-    | k < 0 = show k
+    | k < 0 = pretty k
     | otherwise = printLevel (k `div` 10) <> printLevel (k `mod` 10)
 
-helper :: Integer -> Expr -> Text
-helper _ (Var s _) = s
-helper _ (Free s) = s
-helper _ (Axiom s) = s
-helper _ Star = "*"
-helper _ (Level i)
-    | i == 0 = "□"
-    | otherwise = "□" <> printLevel i
-helper k (App e1 e2) = if k > 3 then parenthesize res else res
-  where
-    res = helper 3 e1 <> " " <> helper 4 e2
-helper k (Pi "" t1 _ t2) = if k > 2 then parenthesize res else res
-  where
-    res = helper 3 t1 <> " -> " <> helper 2 t2
-helper k e@(Pi{}) = if k > 2 then parenthesize res else res
-  where
-    (params, body) = collectPis e
-    grouped = showParamGroup <$> groupParams params
-    res = "∏ " <> unwords grouped <> " , " <> pretty body
-helper k e@(Abs{}) = if k >= 1 then parenthesize res else res
-  where
-    (params, body) = collectLambdas e
-    grouped = showParamGroup <$> groupParams params
-    res = "λ " <> unwords grouped <> " => " <> pretty body
-helper _ e@(Let{}) = res
-  where
-    (binds, body) = collectLets e
-    res = "let " <> unwords (map showBinding binds) <> " in " <> pretty body <> " end"
+prettyExpr :: Integer -> Expr -> Doc ann
+prettyExpr k expr = case expr of
+    Var s _ -> pretty s
+    Free s -> pretty s
+    Axiom s -> pretty s
+    Star -> "*"
+    Level i
+        | i == 0 -> "□"
+        | otherwise -> "□" <> printLevel i
+    App{}
+        | k > 3 -> parens application
+        | otherwise -> application
+      where
+        (top :| rest) = NE.reverse $ collectApps expr
+        application = group $ hang 4 $ prettyExpr 3 top <> line <> align (sep $ map (prettyExpr 4) rest)
+    Pi "" t1 _ t2
+        | k > 2 -> parens piType
+        | otherwise -> piType
+      where
+        piType = group $ prettyExpr 3 t1 <+> "->" <+> align (prettyExpr 2 t2)
+    Pi{} -> group $ hang 4 $ "∏" <+> align (sep grouped) <> "," <> line <> align (prettyExpr 0 body)
+      where
+        (params, body) = collectPis expr
+        grouped = pretty <$> groupParams params
+    Abs{} ->
+        if k >= 1
+            then parens lambdaForm
+            else lambdaForm
+      where
+        (params, body) = collectLambdas expr
+        grouped = pretty <$> groupParams params
+        lambdaForm = group $ hang 4 $ "λ" <+> align (sep grouped) <+> "=>" <> line <> align (prettyExpr 0 body)
+    Let{} ->
+        group $
+            vsep
+                [ "let" <+> align bindings
+                , "in" <+> align (prettyExpr 0 body)
+                , "end"
+                ]
+      where
+        (binds, body) = collectLets expr
+        bindings = sep $ map pretty binds
 
-pretty :: Expr -> Text
-pretty = helper 0 . cleanNames
+prettyT :: Expr -> Text
+prettyT = renderStrict . layoutSmart defaultLayoutOptions . pretty
 
 prettyS :: Expr -> String
-prettyS = toString . pretty
+prettyS = toString . prettyT
diff --git a/perga.cabal b/perga.cabal
index 7e806a4..b3bcf64 100644
--- a/perga.cabal
+++ b/perga.cabal
@@ -42,6 +42,7 @@ library perga-lib
                       , megaparsec
                       , mtl
                       , parser-combinators
+                      , prettyprinter
     mixins:             base hiding (Prelude)
                       , relude (Relude as Prelude)
                       , relude