diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 334aedf..598bbf6 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -34,7 +34,7 @@ mutual
     TYPE : (l : Universe) -> Term d n
 
     ||| function type
-    Pi  : (qty, qtm : Qty) -> (x : Name) ->
+    Pi  : (qtm, qty : Qty) -> (x : Name) ->
           (arg : Term d n) -> (res : Term d (S n)) -> Term d n
     ||| function term
     Lam : (x : Name) -> (body : Term d (S n)) -> Term d n
@@ -126,9 +126,9 @@ mutual
   PrettyHL (Term d n) where
     prettyM (TYPE l) =
       parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
-    prettyM (Pi qty qtm x s t) =
+    prettyM (Pi qtm qty x s t) =
       parensIfM Outer $ hang 2 $
-        !(prettyBinder [qty, qtm] x s) <++> !arrowD
+        !(prettyBinder [qtm, qty] x s) <++> !arrowD
           <//> !(under T x $ prettyM t)
     prettyM (Lam x t) =
       parensIfM Outer $
@@ -320,8 +320,8 @@ mutual
                     Term dfrom from -> NotCloTerm dto to
   pushSubstsTWith th ph (TYPE l) =
     ncloT $ TYPE l
-  pushSubstsTWith th ph (Pi qty qtm x a b) =
-    ncloT $ Pi qty qtm x (subs a th ph) (subs b th (push ph))
+  pushSubstsTWith th ph (Pi qtm qty x a b) =
+    ncloT $ Pi qtm qty x (subs a th ph) (subs b th (push ph))
   pushSubstsTWith th ph (Lam x t) =
     ncloT $ Lam x $ subs t th $ push ph
   pushSubstsTWith th ph (E e) =