diff --git a/examples/algebra.pg b/examples/algebra.pg
index 1d1f744..6ff2f33 100644
--- a/examples/algebra.pg
+++ b/examples/algebra.pg
@@ -15,42 +15,44 @@ section BasicDefinitions
     -- I'd always strongly recommend including the type ascriptions for theorems
 
     -- Fix some set A
-    variable (A : *);
+    variable (A : ★);
 
-    -- a unary operation is a function `A -> A`
-    def unop := A -> A;
+    -- a unary operation is a function `A → A`
+    def unop := A → A;
 
-    -- a binary operation is a function `A -> A -> A`
-    def binop := A -> A -> A;
+    -- a binary operation is a function `A → A → A`
+    def binop := A → A → A;
 
     -- fix some binary operation `op`
-    variable (op : binop);
+    variable (* : binop);
+
+    infixl 20 *;
 
     -- it is associative if ...
-    def assoc := forall (a b c : A), eq A (op a (op b c)) (op (op a b) c);
+    def assoc := forall (a b c : A), eq A (a * (b * c)) ((a * b) * c);
 
     -- fix some element `e`
     variable (e : A);
 
     -- it is a left identity with respect to binop `op` if `∀ a, e * a = a`
-    def id_l := forall (a : A), eq A (op e a) a;
+    def id_l := forall (a : A), eq A (e * a) a;
 
     -- likewise for right identity
-    def id_r := forall (a : A), eq A (op a e) a;
+    def id_r := forall (a : A), eq A (a * e) a;
 
     -- an element is an identity element if it is both a left and right identity
-    def id := and id_l id_r;
+    def id := id_l ∧ id_r;
 
     -- b is a left inverse for a if `b * a = e`
     -- NOTE: we don't require `e` to be an identity in this definition.
     --       this definition is purely for convenience's sake
-    def inv_l (a b : A) := eq A (op b a) e;
+    def inv_l (a b : A) := eq A (b * a) e;
 
     -- likewise for right inverse
-    def inv_r (a b : A) := eq A (op a b) e;
+    def inv_r (a b : A) := eq A (a * b) e;
 
     -- and full-on inverse
-    def inv (a b : A) := and (inv_l a b) (inv_r a b);
+    def inv (a b : A) := inv_l a b ∧ inv_r a b;
 
 end BasicDefinitions
 
@@ -59,15 +61,21 @@ end BasicDefinitions
 -- --------------------------------------------------------------------------------------------------------------
 
 -- a set `S` with binary operation `op` is a semigroup if its operation is associative
-def semigroup (S : *) (op : binop S) : * := assoc S op;
+def semigroup (S : ★) (op : binop S) : ★ := assoc S op;
 
 section Monoid
 
-    variable (M : *) (op : binop M) (e : M);
+    -- Let `M` be a set with binary operation `op` and element `e`.
+    variable (M : ★) (op : binop M) (e : M);
+
+    -- We'll use `*` as an infix shorthand for `op`
+    def * (a b : M) := op a b;
+    infixl 50 *;
 
     -- a set `M` with binary operation `op` and element `e` is a monoid 
-    def monoid : * := and (semigroup M op) (id M op e);
+    def monoid : ★ := (semigroup M op) ∧ (id M op e);
 
+    -- Suppose `(M, *, e)` is a monoid
     hypothesis (Hmonoid : monoid);
 
     -- some "getters" for `monoid` so we don't have to do a bunch of very verbose
@@ -87,10 +95,10 @@ section Monoid
     def monoid_id_l_implies_identity (a : M) (H : id_l M op a) : eq M a e :=
             -- WTS a = a * e = e
             -- we can use `eq_trans` to glue proofs of `a = a * e` and `a * e = e` together
-            eq_trans M a (op a e) e
+            eq_trans M a (a * e) e
 
                 -- first, `a = a * e`, but we'll use `eq_sym` to flip it around
-                (eq_sym M (op a e) a
+                (eq_sym M (a * e) a
                     -- now the goal is to show `a * e = a`, which follows immediately from `id_r`
                     (id_rm a))
 
@@ -100,10 +108,10 @@ section Monoid
     -- the analogous result for right identities
     def monoid_id_r_implies_identity (a : M) (H : id_r M op a) : eq M a e :=
             -- this time, we'll show `a = e * a = e`
-            eq_trans M a (op e a) e
+            eq_trans M a (e * a) e
 
                 -- first, `a = e * a`
-                (eq_sym M (op e a) a
+                (eq_sym M (e * a) a
                     -- this time, it immediately follows from `id_l`
                     (id_lm a))
 
@@ -114,12 +122,15 @@ end Monoid
 
 section Group
 
-    variable (G : *) (op : binop G) (e : G) (i : unop G);
+    variable (G : ★) (op : binop G) (e : G) (i : unop G);
+
+    def * (a b : G) := op a b;
+    infixl 50 *;
 
     -- groups are just monoids with inverses
-    def has_inverses : * := forall (a : G), inv G op e a (i a);
+    def has_inverses : ★ := forall (a : G), inv G op e a (i a);
 
-    def group : * := and (monoid G op e) has_inverses;
+    def group : ★ := (monoid G op e) ∧ has_inverses;
 
     hypothesis (Hgroup : group);
 
@@ -141,23 +152,23 @@ section Group
         --   = (b * a) * a^-1
         --   = e * a^-1
         --   = a^-1
-        eq_trans G b (op b e) (i a)
+        eq_trans G b (b * e) (i a)
         -- b = b * e
-        (eq_sym G (op b e) b (id_rg b))
+        (eq_sym G (b * e) b (id_rg b))
         -- b * e = a^-1
-        (eq_trans G (op b e) (op b (op a (i a))) (i a)
+        (eq_trans G (b * e) (b * (a * i a)) (i a)
             --b * e = b * (a * a^-1)
-            (eq_cong G G e (op a (i a)) (op b)
+            (eq_cong G G e (a * i a) (op b)
                 -- e = a * a^-1
-                (eq_sym G (op a (i a)) e (inv_rg a)))
+                (eq_sym G (a * i a) e (inv_rg a)))
             -- b * (a * a^-1) = a^-1
-            (eq_trans G (op b (op a (i a))) (op (op b a) (i a)) (i a)
+            (eq_trans G (b * (a * i a)) (b * a * i a) (i a)
                 -- b * (a * a^-1) = (b * a) * a^-1
                 (assoc_g b a (i a))
                 -- (b * a) * a^-1 = a^-1
-                (eq_trans G (op (op b a) (i a)) (op e (i a)) (i a)
+                (eq_trans G (b * a * i a) (e * i a) (i a)
                     -- (b * a) * a^-1 = e * a^-1
-                    (eq_cong G G (op b a) e (fun (x : G) => op x (i a)) h)
+                    (eq_cong G G (b * a) e (fun (x : G) => x * i a) h)
                     -- e * a^-1 = a^-1
                     (id_lg (i a)))));
 
@@ -168,66 +179,60 @@ section Group
         --   = a^-1 * (a * b)
         --   = a^-1 * e
         --   = a^-1
-        eq_trans G b (op e b) (i a)
+        eq_trans G b (e * b) (i a)
         -- b = e * b
-        (eq_sym G (op e b) b (id_lg b))
+        (eq_sym G (e * b) b (id_lg b))
         -- e * b = a^-1
-        (eq_trans G (op e b) (op (op (i a) a) b) (i a)
+        (eq_trans G (e * b) (i a * a * b) (i a)
             -- e * b = (a^-1 * a) * b
-            (eq_cong G G e (op (i a) a) (fun (x : G) => op x b)
+            (eq_cong G G e (i a * a) (fun (x : G) => x * b)
                 -- e = (a^-1 * a)
-                (eq_sym G (op (i a) a) e (inv_lg a)))
+                (eq_sym G (i a * a) e (inv_lg a)))
 
             -- (a^-1 * a) * b = a^-1
-            (eq_trans G (op (op (i a) a) b) (op (i a) (op a b)) (i a)
+            (eq_trans G (i a * a * b) (i a * (a * b)) (i a)
                 -- (a^-1 * a) * b = a^-1 * (a * b)
-                (eq_sym G (op (i a) (op a b)) (op (op (i a) a) b) (assoc_g (i a) a b))
+                (eq_sym G (i a * (a * b)) (i a * a * b) (assoc_g (i a) a b))
 
                 -- a^-1 * (a * b) = a^-1
-                (eq_trans G (op (i a) (op a b)) (op (i a) e) (i a)
+                (eq_trans G (i a * (a * b)) (i a * e) (i a)
                     -- a^-1 * (a * b) = a^-1 * e
-                    (eq_cong G G (op a b) e (op (i a)) h)
+                    (eq_cong G G (a * b) e (op (i a)) h)
 
                     -- a^-1 * e = a^-1
                     (id_rg (i a)))));
 
     -- the classic shoes and socks theorem, namely that (a * b)^-1 = b^-1 * a^-1
-    def shoes_and_socks (a b : G) : eq G (i (op a b)) (op (i b) (i a)) :=
-        eq_sym G (op (i b) (i a)) (i (op a b))
-        (right_inv_unique (op a b) (op (i b) (i a))
+    def shoes_and_socks (a b : G) : eq G (i (a * b)) (i b * i a) :=
+        eq_sym G (i b * i a) (i (a * b))
+        (right_inv_unique (a * b) (i b * i a)
         -- WTS: (a * b) * (b^-1 * a^-1) = e
         (let
-            -- some abbreviations for common terms
-            (ab := op a b)
-            (biai := op (i b) (i a))
-            (ab_bi := op (op a b) (i b))
-            (a_bbi := op a (op b (i b)))
-
             -- helper function to prove that x * a^-1 = y * a^-1 given x = y
-            (under_ai (x y : G) (h : eq G x y) := eq_cong G G x y (fun (z : G) => op z (i a)) h)
+            (under_ai (x y : G) (h : eq G x y) := eq_cong G G x y (fun (z : G) => z * (i a)) h)
          in
             -- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1
             --                         = (a * (b * b^-1)) * a^-1
             --                         = (a * e) * a^-1
             --                         = a * a^-1
             --                         = e
-            eq_trans G (op ab biai) (op ab_bi (i a)) e
+            eq_trans G (a * b * (i b * i a)) (a * b * i b * i a) e
             -- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1
-            (assoc_g ab (i b) (i a))
+            (assoc_g (a * b) (i b) (i a))
             -- ((a * b) * b^-1) * a^-1 = e
-            (eq_trans G (op ab_bi (i a)) (op a_bbi (i a)) e
+            (eq_trans G (a * b * i b * i a) (a * (b * i b) * i a) e
                 -- ((a * b) * b^-1) * a^-1 = (a * (b * b^-1)) * a^-1
-                (under_ai ab_bi a_bbi (eq_sym G a_bbi ab_bi (assoc_g a b (i b))))
+                (under_ai (a * b * i b) (a * (b * i b)) (eq_sym G (a * (b * i b)) (a * b * i b) (assoc_g a b (i b))))
 
                 -- (a * (b * b^-1)) * a^-1 = e
-                (eq_trans G (op a_bbi (i a)) (op (op a e) (i a)) e
+                (eq_trans G (a * (b * i b) * i a) (a * e * i a) e
                     -- (a * (b * b^-1)) * a^-1 = (a * e) * a^-1
-                    (eq_cong G G (op b (i b)) e (fun (x : G) => (op (op a x) (i a))) (inv_rg b))
+                    (eq_cong G G (b * i b) e (fun (x : G) => (a * x * i a)) (inv_rg b))
 
                     -- (a * e) * a^-1 = e
-                    (eq_trans G (op (op a e) (i a)) (op a (i a)) e
+                    (eq_trans G (a * e * i a) (a * i a) e
                         -- (a * e) * a^-1 = a * a^-1
-                        (under_ai (op a e) a (id_rg a))
+                        (under_ai (a * e) a (id_rg a))
 
                         -- a * a^-1 = e
                         (inv_rg a))))
diff --git a/examples/category.pg b/examples/category.pg
index c95a458..eddab4c 100644
--- a/examples/category.pg
+++ b/examples/category.pg
@@ -2,71 +2,77 @@
 
 section Category
     variable
-        (Obj  : *)
-        (Hom  : Obj -> Obj -> *)
-        (id   : forall (A     : Obj), Hom A A)
-        (comp : forall (A B C : Obj), Hom A B -> Hom B C -> Hom A C);
+        (Obj  : ★)
+        (~>   : Obj -> Obj -> ★);
+
+    infixr 10 ~>;
+
+    variable
+        (id   : forall (A     : Obj), A ~> A)
+        (comp : forall (A B C : Obj), A ~> B -> B ~> C -> A ~> C);
 
     hypothesis
-        (id_l  : forall (A B     : Obj) (f : Hom A B), eq (Hom A B) (comp A A B (id A) f) f)
-        (id_r  : forall (A B     : Obj) (f : Hom B A), eq (Hom A B) (comp B A A f (id A)) f)
-        (assoc : forall (A B C D : Obj) (f : Hom A B) (g : Hom B C) (h : Hom C D),
-            eq (Hom A D)
+        (id_l  : forall (A B     : Obj) (f : A ~> B), eq (A ~> B) (comp A A B (id A) f) f)
+        (id_r  : forall (A B     : Obj) (f : B ~> A), eq (A ~> B) (comp B A A f (id A)) f)
+        (assoc : forall (A B C D : Obj) (f : A ~> B) (g : B ~> C) (h : C ~> D),
+            eq (A ~> D)
                 (comp A B D f (comp B C D g h))
                 (comp A C D (comp A B C f g) h));
 
-    def initial  (A : Obj) := forall (B : Obj), exists_uniq_t (Hom A B);
-    def terminal (A : Obj) := forall (B : Obj), exists_uniq_t (Hom B A);
+    def initial  (A : Obj) := forall (B : Obj), exists_uniq_t (A ~> B);
+    def terminal (A : Obj) := forall (B : Obj), exists_uniq_t (B ~> A);
 
-    def product (A B C : Obj) (piA : Hom C A) (piB : Hom C B) :=
-        forall (D : Obj) (f : Hom D A) (g : Hom D B),
-            exists_uniq (Hom D C) (fun (fxg : Hom D C) =>
-                and (eq (Hom D A) (comp D C A fxg piA) f)
-                    (eq (Hom D B) (comp D C B fxg piB) g));
+    def × (A B C : Obj) (piA : C ~> A) (piB : C ~> B) :=
+        forall (D : Obj) (f : D ~> A) (g : D ~> B),
+            exists_uniq (D ~> C) (fun (fxg : D ~> C) =>
+                (eq (D ~> A) (comp D C A fxg piA) f)
+                ∧ (eq (D ~> B) (comp D C B fxg piB) g));
 
     section Inverses
         variable
             (A B : Obj)
-            (f : Hom A B)
-            (g : Hom B A);
+            (f : A ~> B)
+            (g : B ~> A);
 
-        def inv_l := eq (Hom A A) (comp A B A f g) (id A);
-        def inv_r := eq (Hom B B) (comp B A B g f) (id B);
+        def inv_l := eq (A ~> A) (comp A B A f g) (id A);
+        def inv_r := eq (B ~> B) (comp B A B g f) (id B);
 
-        def inv := and inv_l inv_r;
+        def inv := inv_l ∧ inv_r;
     end Inverses
 
-    def isomorphic (A B : Obj) :=
-        exists (Hom A B) (fun (f : Hom A B) =>
-            exists (Hom B A) (inv A B f));
+    def ≅ (A B : Obj) :=
+        exists (A ~> B) (fun (f : A ~> B) =>
+            exists (B ~> A) (inv A B f));
 
-    def initial_uniq (A B : Obj) (hA : initial A) (hB : initial B) : isomorphic A B :=
-        exists_uniq_t_elim (Hom A B) (isomorphic A B) (hA B) (fun (f : Hom A B) (f_uniq : forall (y : Hom A B), eq (Hom A B) f y) =>
-        exists_uniq_t_elim (Hom B A) (isomorphic A B) (hB A) (fun (g : Hom B A) (g_uniq : forall (y : Hom B A), eq (Hom B A) g y) =>
-        exists_uniq_t_elim (Hom A A) (isomorphic A B) (hA A) (fun (a : Hom A A) (a_uniq : forall (y : Hom A A), eq (Hom A A) a y) =>
-        exists_uniq_t_elim (Hom B B) (isomorphic A B) (hB B) (fun (b : Hom B B) (b_uniq : forall (y : Hom B B), eq (Hom B B) b y) =>
-            exists_intro (Hom A B) (fun (f : Hom A B) => exists (Hom B A) (inv A B f)) f
-                (exists_intro (Hom B A) (inv A B f) g
+    infixl 20 ≅;
+
+    def initial_uniq (A B : Obj) (hA : initial A) (hB : initial B) : A ≅ B :=
+        exists_uniq_t_elim (A ~> B) (A ≅ B) (hA B) (fun (f : A ~> B) (f_uniq : forall (y : A ~> B), eq (A ~> B) f y) =>
+        exists_uniq_t_elim (B ~> A) (A ≅ B) (hB A) (fun (g : B ~> A) (g_uniq : forall (y : B ~> A), eq (B ~> A) g y) =>
+        exists_uniq_t_elim (A ~> A) (A ≅ B) (hA A) (fun (a : A ~> A) (a_uniq : forall (y : A ~> A), eq (A ~> A) a y) =>
+        exists_uniq_t_elim (B ~> B) (A ≅ B) (hB B) (fun (b : B ~> B) (b_uniq : forall (y : B ~> B), eq (B ~> B) b y) =>
+            exists_intro (A ~> B) (fun (f : A ~> B) => exists (B ~> A) (inv A B f)) f
+                (exists_intro (B ~> A) (inv A B f) g
                     (and_intro (inv_l A B f g) (inv_r A B f g)
-                        (eq_trans (Hom A A) (comp A B A f g) a (id A)
-                            (eq_sym (Hom A A) a (comp A B A f g) (a_uniq (comp A B A f g)))
+                        (eq_trans (A ~> A) (comp A B A f g) a (id A)
+                            (eq_sym (A ~> A) a (comp A B A f g) (a_uniq (comp A B A f g)))
                             (a_uniq (id A)))
-                        (eq_trans (Hom B B) (comp B A B g f) b (id B)
-                            (eq_sym (Hom B B) b (comp B A B g f) (b_uniq (comp B A B g f)))
+                        (eq_trans (B ~> B) (comp B A B g f) b (id B)
+                            (eq_sym (B ~> B) b (comp B A B g f) (b_uniq (comp B A B g f)))
                             (b_uniq (id B)))))))));
 
-    def terminal_uniq (A B : Obj) (hA : terminal A) (hB : terminal B) : isomorphic A B :=
-        exists_uniq_t_elim (Hom A B) (isomorphic A B) (hB A) (fun (f : Hom A B) (f_uniq : forall (y : Hom A B), eq (Hom A B) f y) =>
-        exists_uniq_t_elim (Hom B A) (isomorphic A B) (hA B) (fun (g : Hom B A) (g_uniq : forall (y : Hom B A), eq (Hom B A) g y) =>
-        exists_uniq_t_elim (Hom A A) (isomorphic A B) (hA A) (fun (a : Hom A A) (a_uniq : forall (y : Hom A A), eq (Hom A A) a y) =>
-        exists_uniq_t_elim (Hom B B) (isomorphic A B) (hB B) (fun (b : Hom B B) (b_uniq : forall (y : Hom B B), eq (Hom B B) b y) =>
-            exists_intro (Hom A B) (fun (f : Hom A B) => exists (Hom B A) (inv A B f)) f
-                (exists_intro (Hom B A) (inv A B f) g
+    def terminal_uniq (A B : Obj) (hA : terminal A) (hB : terminal B) : A ≅ B :=
+        exists_uniq_t_elim (A ~> B) (A ≅ B) (hB A) (fun (f : A ~> B) (f_uniq : forall (y : A ~> B), eq (A ~> B) f y) =>
+        exists_uniq_t_elim (B ~> A) (A ≅ B) (hA B) (fun (g : B ~> A) (g_uniq : forall (y : B ~> A), eq (B ~> A) g y) =>
+        exists_uniq_t_elim (A ~> A) (A ≅ B) (hA A) (fun (a : A ~> A) (a_uniq : forall (y : A ~> A), eq (A ~> A) a y) =>
+        exists_uniq_t_elim (B ~> B) (A ≅ B) (hB B) (fun (b : B ~> B) (b_uniq : forall (y : B ~> B), eq (B ~> B) b y) =>
+            exists_intro (A ~> B) (fun (f : A ~> B) => exists (B ~> A) (inv A B f)) f
+                (exists_intro (B ~> A) (inv A B f) g
                     (and_intro (inv_l A B f g) (inv_r A B f g)
-                        (eq_trans (Hom A A) (comp A B A f g) a (id A)
-                            (eq_sym (Hom A A) a (comp A B A f g) (a_uniq (comp A B A f g)))
+                        (eq_trans (A ~> A) (comp A B A f g) a (id A)
+                            (eq_sym (A ~> A) a (comp A B A f g) (a_uniq (comp A B A f g)))
                             (a_uniq (id A)))
-                        (eq_trans (Hom B B) (comp B A B g f) b (id B)
-                            (eq_sym (Hom B B) b (comp B A B g f) (b_uniq (comp B A B g f)))
+                        (eq_trans (B ~> B) (comp B A B g f) b (id B)
+                            (eq_sym (B ~> B) b (comp B A B g f) (b_uniq (comp B A B g f)))
                             (b_uniq (id B)))))))));
 end Category
diff --git a/examples/classical.pg b/examples/classical.pg
index 63b04c7..ef853ab 100644
--- a/examples/classical.pg
+++ b/examples/classical.pg
@@ -2,26 +2,26 @@
 
 -- excluded middle!
 -- P ∨ ~P
-axiom em (P : *) : or P (not P);
+axiom em (P : ★) : P ∨ not P;
 
 -- ~~P => P
-def dne (P : *) (nnp : not (not P)) : P :=
+def dne (P : ★) (nnp : not (not P)) : P :=
     or_elim P (not P) P (em P)
         (fun (p : P) => p)
         (fun (np : not P) => nnp np P);
 
 -- ((P => Q) => P) => P
-def peirce (P Q : *) (h : (P -> Q) -> P) : P :=
+def peirce (P Q : ★) (h : (P -> Q) -> P) : P :=
     or_elim P (not P) P (em P)
         (fun (p : P) => p)
         (fun (np : not P) => h (fun (p : P) => np p Q));
 
 
 -- ~(A ∧ B) => ~A ∨ ~B
-def de_morgan4 (A B : *) (h : not (and A B)) : or (not A) (not B) :=
-    or_elim A (not A) (or (not A) (not B)) (em A)
+def de_morgan4 (A B : ★) (h : not (A ∧ B)) : not A ∨ not B :=
+    or_elim A (not A) (not A ∨ not B) (em A)
         (fun (a : A) =>
-            or_elim B (not B) (or (not A) (not B)) (em B)
-                (fun (b : B) => h (and_intro A B a b) (or (not A) (not B)))
+            or_elim B (not B) (not A ∨ not B) (em B)
+                (fun (b : B) => h (and_intro A B a b) (not A ∨ not B))
                 (fun (nb : not B) => or_intro_r (not A) (not B) nb))
         (fun (na : not A) => or_intro_l (not A) (not B) na);
diff --git a/examples/computation.pg b/examples/computation.pg
index e565e7f..c5717c4 100644
--- a/examples/computation.pg
+++ b/examples/computation.pg
@@ -6,19 +6,21 @@
 
 -- the natural number `n` is encoded as the function taking any function
 -- `A -> A` and repeating it `n` times
-def nat : * := forall (A : *), (A -> A) -> A -> A;
+def nat : ★ := forall (A : ★), (A -> A) -> A -> A;
 
 -- zero is the constant function
-def zero : nat := fun (A : *) (f : A -> A) (x : A) => x;
+def zero : nat := fun (A : ★) (f : A -> A) (x : A) => x;
 
 -- `suc n` composes one more `f` than `n`
-def suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x);
+def suc : nat -> nat := fun (n : nat) (A : ★) (f : A -> A) (x : A) => f ((n A f) x);
 
 -- addition can be encoded as usual
-def plus : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x);
+def + : nat -> nat -> nat := fun (n m : nat) (A : ★) (f : A -> A) (x : A) => (m A f) (n A f x);
+infixl 20 +;
 
 -- likewise for multiplication
-def times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x;
+def * : nat -> nat -> nat := fun (n m : nat) (A : ★) (f : A -> A) (x : A) => (m A (n A f)) x;
+infixl 30 *;
 
 -- unforunately, it is impossible to prove induction on Church numerals,
 -- which makes it really hard to prove standard theorems, or do anything really.
@@ -37,19 +39,25 @@ def eight : nat := suc seven;
 def nine  : nat := suc eight;
 def ten   : nat := suc nine;
 
+def = (n m : nat) := eq nat n m;
+infixl 1 =;
+
 -- now we can do a bunch of computations, even at the type level
 -- the way we can do this is by defining equality (see <examples/logic.pg> for
 -- more details on how this works) and proving a bunch of theorems like
--- `plus one one = two` (how exciting!)
+-- `one + one = two` (how exciting!)
 -- then perga will only accept our proof if `plus one one` and `two` are beta
 -- equivalent
 
 -- since `plus one one` and `two` are beta-equivalent, `eq_refl nat two` is a
 -- proof that `1 + 1 = 2`
-def one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two;
+def one_plus_one_is_two : one + one = two := eq_refl nat two;
 
 -- we can likewise compute 2 + 2
-def two_plus_two_is_four : eq nat (plus two two) four := eq_refl nat four;
+def two_plus_two_is_four : two + two = four := eq_refl nat four;
 
 -- even multiplication works
-def two_times_five_is_ten : eq nat (times two five) ten := eq_refl nat ten;
+def two_times_five_is_ten : two * five = ten := eq_refl nat ten;
+
+-- this is just to kind of show off the parser
+def mixed : two + four * two = ten := eq_refl nat ten;
diff --git a/examples/logic.pg b/examples/logic.pg
index c549769..ffde90c 100644
--- a/examples/logic.pg
+++ b/examples/logic.pg
@@ -1,52 +1,53 @@
 -- False
 
-def false : * := forall (A : *), A;
+def false : ★ := forall (A : ★), A;
 
 -- no introduction rule
 
 -- elimination rule
-def false_elim (A : *) (contra : false) : A := contra A;
+def false_elim (A : ★) (contra : false) : A := contra A;
 
 -- --------------------------------------------------------------------------------------------------------------
 
 -- True
 
-def true : * := forall (A : *), A -> A;
+def true : ★ := forall (A : ★), A → A;
 
-def true_intro : true := fun (A : *) (x : A) => x;
+def true_intro : true := fun (A : ★) (x : A) => x;
 
 -- --------------------------------------------------------------------------------------------------------------
 
 -- Negation
 
-def not (A : *) : * := A -> false;
+def not (A : ★) : ★ := A → false;
 
 -- introduction rule (kinda just the definition)
-def not_intro (A : *) (h : A -> false) : not A := h;
+def not_intro (A : ★) (h : A → false) : not A := h;
 
 -- elimination rule
-def not_elim (A B : *) (a : A) (na : not A) : B := na a B;
+def not_elim (A B : ★) (a : A) (na : not A) : B := na a B;
 
 -- can introduce double negation (can't eliminate it as that isn't constructive)
-def double_neg_intro (A : *) (a : A) : not (not A) :=
+def double_neg_intro (A : ★) (a : A) : not (not A) :=
     fun (notA : not A) => notA a;
 
 -- --------------------------------------------------------------------------------------------------------------
 
 -- Conjunction
 
-def and (A B : *) : * := forall (C : *), (A -> B -> C) -> C;
+def ∧ (A B : ★) : ★ := forall (C : ★), (A → B → C) → C;
+infixl 10 ∧;
 
 -- introduction rule
-def and_intro (A B : *) (a : A) (b : B) : and A B :=
-    fun (C : *) (H : A -> B -> C) => H a b;
+def and_intro (A B : ★) (a : A) (b : B) : A ∧ B :=
+    fun (C : ★) (H : A → B → C) => H a b;
 
 -- left elimination rule
-def and_elim_l (A B : *) (ab : and A B) : A :=
+def and_elim_l (A B : ★) (ab : A ∧ B) : A :=
     ab A (fun (a : A) (b : B) => a);
 
 -- right elimination rule
-def and_elim_r (A B : *) (ab : and A B) : B :=
+def and_elim_r (A B : ★) (ab : A ∧ B) : B :=
     ab B (fun (a : A) (b : B) => b);
 
 -- --------------------------------------------------------------------------------------------------------------
@@ -54,18 +55,19 @@ def and_elim_r (A B : *) (ab : and A B) : B :=
 -- Disjunction
 
 -- 2nd order disjunction
-def or (A B : *) : * := forall (C : *), (A -> C) -> (B -> C) -> C;
+def ∨ (A B : ★) : ★ := forall (C : ★), (A → C) → (B → C) → C;
+infixl 5 ∨;
 
 -- left introduction rule
-def or_intro_l (A B : *) (a : A) : or A B :=
-    fun (C : *) (ha : A -> C) (hb : B -> C) => ha a;
+def or_intro_l (A B : ★) (a : A) : A ∨ B :=
+    fun (C : ★) (ha : A → C) (hb : B → C) => ha a;
 
 -- right introduction rule
-def or_intro_r (A B : *) (b : B) : or A B :=
-    fun (C : *) (ha : A -> C) (hb : B -> C) => hb b;
+def or_intro_r (A B : ★) (b : B) : A ∨ B :=
+    fun (C : ★) (ha : A → C) (hb : B → C) => hb b;
 
 -- elimination rule (kinda just the definition)
-def or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
+def or_elim (A B C : ★) (ab : A ∨ B) (ha : A → C) (hb : B → C) : C :=
     ab C ha hb;
 
 -- --------------------------------------------------------------------------------------------------------------
@@ -73,14 +75,14 @@ def or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
 -- Existential
 
 -- 2nd order existential
-def exists (A : *) (P : A -> *) : * := forall (C : *), (forall (x : A), P x -> C) -> C;
+def exists (A : ★) (P : A → ★) : ★ := forall (C : ★), (forall (x : A), P x → C) → C;
 
 -- introduction rule
-def exists_intro (A : *) (P : A -> *) (a : A) (h : P a) : exists A P :=
-    fun (C : *) (g : forall (x : A), P x -> C) => g a h;
+def exists_intro (A : ★) (P : A → ★) (a : A) (h : P a) : exists A P :=
+    fun (C : ★) (g : forall (x : A), P x → C) => g a h;
 
 -- elimination rule (kinda just the definition)
-def exists_elim (A B : *) (P : A -> *) (ex_a : exists A P) (h : forall (a : A), P a -> B) : B :=
+def exists_elim (A B : ★) (P : A → ★) (ex_a : exists A P) (h : forall (a : A), P a → B) : B :=
     ex_a B h;
 
 -- --------------------------------------------------------------------------------------------------------------
@@ -88,53 +90,53 @@ def exists_elim (A B : *) (P : A -> *) (ex_a : exists A P) (h : forall (a : A),
 -- Universal
 
 -- 2nd order universal (just ∏, including it for completeness)
-def all (A : *) (P : A -> *) : * := forall (a : A), P a;
+def all (A : ★) (P : A → ★) : ★ := forall (a : A), P a;
 
 -- introduction rule
-def all_intro (A : *) (P : A -> *) (h : forall (a : A), P a) : all A P := h;
+def all_intro (A : ★) (P : A → ★) (h : forall (a : A), P a) : all A P := h;
 
 -- elimination rule
-def all_elim (A : *) (P : A -> *) (h_all : all A P) (a : A) : P a := h_all a;
+def all_elim (A : ★) (P : A → ★) (h_all : all A P) (a : A) : P a := h_all a;
 
 -- --------------------------------------------------------------------------------------------------------------
 
 -- Equality
 
 -- 2nd order Leibniz equality
-def eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
+def eq (A : ★) (x y : A) := forall (P : A → ★), P x → P y;
 
 -- equality is reflexive
-def eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
+def eq_refl (A : ★) (x : A) : eq A x x := fun (P : A → ★) (Hx : P x) => Hx;
 
 -- equality is symmetric
-def eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
-    Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
+def eq_sym (A : ★) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A → ★) (Hy : P y) =>
+    Hxy (fun (z : A) => P z → P x) (fun (Hx : P x) => Hx) Hy;
 
 -- equality is transitive
-def eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
+def eq_trans (A : ★) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A → ★) (Hx : P x) =>
     Hyz P (Hxy P Hx);
 
 -- equality is a universal congruence
-def eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
-  fun (P : B -> *) (Hfx : P (f x)) =>
+def eq_cong (A B : ★) (x y : A) (f : A → B) (H : eq A x y) : eq B (f x) (f y) :=
+  fun (P : B → ★) (Hfx : P (f x)) =>
       H (fun (a : A) => P (f a)) Hfx;
 
 -- --------------------------------------------------------------------------------------------------------------
 
 -- unique existence
-def exists_uniq (A : *) (P : A -> *) : * :=
-    exists A (fun (x : A) => and (P x) (forall (y : A), P y -> eq A x y));
+def exists_uniq (A : ★) (P : A → ★) : ★ :=
+    exists A (fun (x : A) => P x ∧ (forall (y : A), P y → eq A x y));
 
-def exists_uniq_elim (A B : *) (P : A -> *) (ex_a : exists_uniq A P) (h : forall (a : A), P a -> (forall (y : A), P y -> eq A a y) -> B) : B :=
-    exists_elim A B (fun (x : A) => and (P x) (forall (y : A), P y -> eq A x y)) ex_a
-    (fun (a : A) (h2 : and (P a) (forall (y : A), P y -> eq A a y)) =>
-        h a (and_elim_l (P a) (forall (y : A), P y -> eq A a y) h2)
-            (and_elim_r (P a) (forall (y : A), P y -> eq A a y) h2));
+def exists_uniq_elim (A B : ★) (P : A → ★) (ex_a : exists_uniq A P) (h : forall (a : A), P a → (forall (y : A), P y → eq A a y) → B) : B :=
+    exists_elim A B (fun (x : A) => P x ∧ (forall (y : A), P y → eq A x y)) ex_a
+    (fun (a : A) (h2 : P a ∧ (forall (y : A), P y → eq A a y)) =>
+        h a (and_elim_l (P a) (forall (y : A), P y → eq A a y) h2)
+            (and_elim_r (P a) (forall (y : A), P y → eq A a y) h2));
 
-def exists_uniq_t (A : *) : * :=
+def exists_uniq_t (A : ★) : ★ :=
     exists A (fun (x : A) => forall (y : A), eq A x y);
 
-def exists_uniq_t_elim (A B : *) (ex_a : exists_uniq_t A) (h : forall (a : A), (forall (y : A), eq A a y) -> B) : B :=
+def exists_uniq_t_elim (A B : ★) (ex_a : exists_uniq_t A) (h : forall (a : A), (forall (y : A), eq A a y) → B) : B :=
     exists_elim A B (fun (x : A) => forall (y : A), eq A x y) ex_a (fun (a : A) (h2 : forall (y : A), eq A a y) => h a h2);
 
 -- --------------------------------------------------------------------------------------------------------------
@@ -143,24 +145,24 @@ def exists_uniq_t_elim (A B : *) (ex_a : exists_uniq_t A) (h : forall (a : A), (
 
 section Theorems
 
-    variable (A B C : *);
+    variable (A B C : ★);
 
     -- ~(A ∨ B) => ~A ∧ ~B
-    def de_morgan1 (h : not (or A B)) : and (not A) (not B) :=
+    def de_morgan1 (h : not (A ∨ B)) : not A ∧ not B :=
         and_intro (not A) (not B)
             (fun (a : A) => h (or_intro_l A B a))
             (fun (b : B) => h (or_intro_r A B b));
 
     -- ~A ∧ ~B => ~(A ∨ B)
-    def de_morgan2 (h : and (not A) (not B)) : not (or A B) :=
-        fun (contra : or A B) => 
+    def de_morgan2 (h : not A ∧ not B) : not (A ∨ B) :=
+        fun (contra : A ∨ B) => 
             or_elim A B false contra
                 (and_elim_l (not A) (not B) h)
                 (and_elim_r (not A) (not B) h);
 
     -- ~A ∨ ~B => ~(A ∧ B)
-    def de_morgan3 (h : or (not A) (not B)) : not (and A B) :=
-        fun (contra : and A B) =>
+    def de_morgan3 (h : not A ∨ not B) : not (A ∧ B) :=
+        fun (contra : A ∧ B) =>
             or_elim (not A) (not B) false h
                 (fun (na : not A) => na (and_elim_l A B contra))
                 (fun (nb : not B) => nb (and_elim_r A B contra));
@@ -168,80 +170,80 @@ section Theorems
     -- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
 
     -- A ∧ B => B ∧ A
-    def and_comm (h : and A B) : and B A :=
+    def and_comm (h : A ∧ B) : B ∧ A :=
         and_intro B A
             (and_elim_r A B h)
             (and_elim_l A B h);
 
     -- A ∨ B => B ∨ A
-    def or_comm (h : or A B) : or B A :=
-        or_elim A B (or B A) h
+    def or_comm (h : A ∨ B) : B ∨ A :=
+        or_elim A B (B ∨ A) h
             (fun (a : A) => or_intro_r B A a)
             (fun (b : B) => or_intro_l B A b);
 
     -- A ∧ (B ∧ C) => (A ∧ B) ∧ C
-    def and_assoc_l (h : and A (and B C)) : and (and A B) C :=
-        let (a := (and_elim_l A (and B C) h))
-            (bc := (and_elim_r A (and B C) h))
+    def and_assoc_l (h : A ∧ (B ∧ C)) : (A ∧ B) ∧ C :=
+        let (a := (and_elim_l A (B ∧ C) h))
+            (bc := (and_elim_r A (B ∧ C) h))
             (b := (and_elim_l B C bc))
             (c := (and_elim_r B C bc))
         in
-            and_intro (and A B) C (and_intro A B a b) c
+            and_intro (A ∧ B) C (and_intro A B a b) c
         end;
 
     -- (A ∧ B) ∧ C => A ∧ (B ∧ C)
-    def and_assoc_r (h : and (and A B) C) : and A (and B C) :=
-        let (ab := and_elim_l (and A B) C h)
+    def and_assoc_r (h : (A ∧ B) ∧ C) : A ∧ (B ∧ C) :=
+        let (ab := and_elim_l (A ∧ B) C h)
             (a := and_elim_l A B ab)
             (b := and_elim_r A B ab)
-            (c := and_elim_r (and A B) C h)
+            (c := and_elim_r (A ∧ B) C h)
         in
-            and_intro A (and B C) a (and_intro B C b c)
+            and_intro A (B ∧ C) a (and_intro B C b c)
         end;
 
     -- A ∨ (B ∨ C) => (A ∨ B) ∨ C
-    def or_assoc_l (h : or A (or B C)) : or (or A B) C :=
-        or_elim A (or B C) (or (or A B) C) h
-            (fun (a : A) => or_intro_l (or A B) C (or_intro_l A B a))
-            (fun (g : or B C) =>
-                or_elim B C (or (or A B) C) g
-                    (fun (b : B) => or_intro_l (or A B) C (or_intro_r A B b))
-                    (fun (c : C) => or_intro_r (or A B) C c));
+    def or_assoc_l (h : A ∨ (B ∨ C)) : (A ∨ B) ∨ C :=
+        or_elim A (B ∨ C) (A ∨ B ∨ C) h
+            (fun (a : A) => or_intro_l (A ∨ B) C (or_intro_l A B a))
+            (fun (g : B ∨ C) =>
+                or_elim B C (A ∨ B ∨ C) g
+                    (fun (b : B) => or_intro_l (A ∨ B) C (or_intro_r A B b))
+                    (fun (c : C) => or_intro_r (A ∨ B) C c));
 
     -- (A ∨ B) ∨ C => A ∨ (B ∨ C)
-    def or_assoc_r (h : or (or A B) C) : or A (or B C) :=
-        or_elim (or A B) C (or A (or B C)) h
-            (fun (g : or A B) => 
-                or_elim A B (or A (or B C)) g
-                    (fun (a : A) => or_intro_l A (or B C) a)
-                    (fun (b : B) => or_intro_r A (or B C) (or_intro_l B C b)))
-            (fun (c : C) => or_intro_r A (or B C) (or_intro_r B C c));
+    def or_assoc_r (h : (A ∨ B) ∨ C) : A ∨ (B ∨ C) :=
+        or_elim (A ∨ B) C (A ∨ (B ∨ C)) h
+            (fun (g : A ∨ B) => 
+                or_elim A B (A ∨ (B ∨ C)) g
+                    (fun (a : A) => or_intro_l A (B ∨ C) a)
+                    (fun (b : B) => or_intro_r A (B ∨ C) (or_intro_l B C b)))
+            (fun (c : C) => or_intro_r A (B ∨ C) (or_intro_r B C c));
 
     -- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
-    def and_distrib_l_or (h : and A (or B C)) : or (and A B) (and A C) :=
-        or_elim B C (or (and A B) (and A C)) (and_elim_r A (or B C) h)
-            (fun (b : B) => or_intro_l (and A B) (and A C)
-                (and_intro A B (and_elim_l A (or B C) h) b))
-            (fun (c : C) => or_intro_r (and A B) (and A C)
-                (and_intro A C (and_elim_l A (or B C) h) c));
+    def and_distrib_l_or (h : A ∧ (B ∨ C)) : A ∧ B ∨ A ∧ C :=
+        or_elim B C (A ∧ B ∨ A ∧ C) (and_elim_r A (B ∨ C) h)
+            (fun (b : B) => or_intro_l (A ∧ B) (A ∧ C)
+                (and_intro A B (and_elim_l A (B ∨ C) h) b))
+            (fun (c : C) => or_intro_r (A ∧ B) (A ∧ C)
+                (and_intro A C (and_elim_l A (B ∨ C) h) c));
 
     -- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
-    def and_factor_l_or (h : or (and A B) (and A C)) : and A (or B C) :=
-        or_elim (and A B) (and A C) (and A (or B C)) h
-            (fun (ab : and A B) => and_intro A (or B C)
+    def and_factor_l_or (h : A ∧ B ∨ A ∧ C) : A ∧ (B ∨ C) :=
+        or_elim (A ∧ B) (A ∧ C) (A ∧ (B ∨ C)) h
+            (fun (ab : A ∧ B) => and_intro A (B ∨ C)
                 (and_elim_l A B ab)
                 (or_intro_l B C (and_elim_r A B ab)))
-            (fun (ac : and A C) => and_intro A (or B C)
+            (fun (ac : A ∧ C) => and_intro A (B ∨ C)
                 (and_elim_l A C ac)
                 (or_intro_r B C (and_elim_r A C ac)));
 
     -- Thanks Quinn!
     -- A ∨ B => ~B => A
-    def disj_syllog (nb : not B) (hor : or A B) : A :=
+    def disj_syllog (nb : not B) (hor : A ∨ B) : A :=
         or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A);
 
     -- (A => B) => ~B => ~A
-    def contrapositive (f : A -> B) (nb : not B) : not A :=
+    def contrapositive (f : A → B) (nb : not B) : not A :=
         fun (a : A) => nb (f a);
 
 end Theorems
diff --git a/examples/peano.pg b/examples/peano.pg
index 2646597..f186953 100644
--- a/examples/peano.pg
+++ b/examples/peano.pg
@@ -12,7 +12,7 @@
 -- powerful enough to construct the natural numbers (or at least to prove the
 -- Peano axioms as theorems from a definition constructible in perga). However,
 -- working with axioms is extremely common in math. As such, perga has a system
--- for doing just that, namely the *axiom* system.
+-- for doing just that, namely the ★axiom★ system.
 -- 
 -- In a definition, rather than give a value for the term, we can give it the
 -- value axiom, in which case a type ascription is mandatory. Perga will then
@@ -20,7 +20,7 @@
 -- defined is a value of the asserted type. For example, we will use the axiom
 -- system to assert the existence of a type of natural numbers
 
-axiom nat : *;
+axiom nat : ★;
 
 -- As you can imagine, this can be risky. For instance, there's nothing stopping
 -- us from saying
@@ -56,7 +56,7 @@ axiom suc_nonzero : forall (n : nat), not (eq nat (suc n) zero);
 
 -- axiom 9: Induction! For any proposition P on natural numbers, if P(0) holds,
 -- and if for every natural number n, P(n) ⇒ P(S n), then P holds for all n.
-axiom nat_ind : forall (P : nat -> *), P zero -> (forall (n : nat), P n -> P (suc n))
+axiom nat_ind : forall (P : nat -> ★), P zero -> (forall (n : nat), P n -> P (suc n))
     -> forall (n : nat), P n;
 
 -- }}}
@@ -80,7 +80,7 @@ def four  : nat := suc three;
 def five  : nat := suc four;
 
 -- First, the predecessor of n is m if n = suc m.
-def pred (n m : nat) : * := eq nat n (suc m);
+def pred (n m : nat) : ★ := eq nat n (suc m);
 
 -- Our claim is a disjunction, whose first option is that n = 0.
 def szc_l (n : nat) := eq nat n zero;
@@ -90,7 +90,7 @@ def szc_r (n : nat) := exists nat (pred n);
 
 -- So the claim we are trying to prove is that either one of the above options
 -- holds for every n.
-def szc (n : nat) := or (szc_l n) (szc_r n);
+def szc (n : nat) := szc_l n ∨ szc_r n;
 
 -- And here's our proof!
 def suc_or_zero : forall (n : nat), szc n :=
@@ -142,8 +142,8 @@ def suc_or_zero : forall (n : nat), szc n :=
 -- more used to perga. As such, I will go into a lot less detail on each of
 -- these proofs than in the later sections.
 --
--- Here's our game plan. We will define a relation R : nat -> A -> * such that
--- R x y iff for every relation Q : nat -> A -> * satisfying
+-- Here's our game plan. We will define a relation R : nat -> A -> ★ such that
+-- R x y iff for every relation Q : nat -> A -> ★ satisfying
 -- 1) Q 0 z and
 -- 2) forall (x : nat) (y : A), Q x y -> Q (suc x) (fS x y),
 -- Q x y.
@@ -154,30 +154,30 @@ def suc_or_zero : forall (n : nat), szc n :=
 section RecursiveDefs
 
 -- First, fix an A, z : A, and fS : nat -> A -> A
-variable (A : *) (z : A) (fS : nat -> A -> A);
+variable (A : ★) (z : A) (fS : nat -> A -> A);
 
 -- {{{ Defining R
 -- Here is condition 1 formally expressed in perga.
-def cond1 (Q : nat -> A -> *) := Q zero z;
+def cond1 (Q : nat -> A -> ★) := Q zero z;
 
 -- Likewise for condition 2.
-def cond2 (Q : nat -> A -> *) :=
+def cond2 (Q : nat -> A -> ★) :=
     forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);
 
 -- From here we can define R.
 def rec_rel (x : nat) (y : A) :=
-    forall (Q : nat -> A -> *), cond1 Q -> cond2 Q -> Q x y;
+    forall (Q : nat -> A -> ★), cond1 Q -> cond2 Q -> Q x y;
 -- }}}
 
 -- {{{ R is total
-def total (A B : *) (R : A -> B -> *) := forall (a : A), exists B (R a);
+def total (A B : ★) (R : A -> B -> ★) := forall (a : A), exists B (R a);
 
 def rec_rel_cond1 : cond1 rec_rel :=
-    fun (Q : nat -> A -> *) (h1 : cond1 Q) (h2 : cond2 Q) => h1;
+    fun (Q : nat -> A -> ★) (h1 : cond1 Q) (h2 : cond2 Q) => h1;
 
 def rec_rel_cond2 : cond2 rec_rel :=
     fun (n : nat) (y : A) (h : rec_rel n y)
-        (Q : nat -> A -> *) (h1 : cond1 Q) (h2 : cond2 Q) =>
+        (Q : nat -> A -> ★) (h1 : cond1 Q) (h2 : cond2 Q) =>
         h2 n y (h Q h1 h2);
 
 def rec_rel_total : total nat A rec_rel :=
@@ -194,18 +194,18 @@ def rec_rel_total : total nat A rec_rel :=
 
 -- {{{ Defining R2
 def alt_cond1 (x : nat) (y : A) :=
-    and (eq nat x zero) (eq A y z);
+    eq nat x zero ∧ eq A y z;
 
 def cond_y2 (x : nat) (y : A)
     (x2 : nat) (y2 : A) :=
-        and (eq A y (fS x2 y2)) (rec_rel x2 y2);
+        (eq A y (fS x2 y2)) ∧ (rec_rel x2 y2);
 
 def cond_x2 (x : nat) (y : A) (x2 : nat) :=
-    and (pred x x2) (exists A (cond_y2 x y x2));
+    pred x x2 ∧ exists A (cond_y2 x y x2);
 
 def alt_cond2 (x : nat) (y : A) := exists nat (cond_x2 x y);
 
-def rec_rel_alt (x : nat) (y : A) := or (alt_cond1 x y) (alt_cond2 x y);
+def rec_rel_alt (x : nat) (y : A) := alt_cond1 x y ∨ alt_cond2 x y;
 -- }}}
 
 -- {{{ R = R2
@@ -282,10 +282,10 @@ def R_sub_R2 (x : nat) (y : A) : rec_rel x y -> rec_rel_alt x y :=
 
 -- {{{ R2 (hence R) is functional
 
-def fl_in (A B : *) (R : A -> B -> *) (x : A) := forall (y1 y2 : B),
+def fl_in (A B : ★) (R : A -> B -> ★) (x : A) := forall (y1 y2 : B),
     R x y1 -> R x y2 -> eq B y1 y2;
 
-def fl (A B : *) (R : A -> B -> *) := forall (x : A), fl_in A B R x;
+def fl (A B : ★) (R : A -> B -> ★) := forall (x : A), fl_in A B R x;
 
 def R2_zero (y : A) : rec_rel_alt zero y -> eq A y z :=
     let (cx2 := cond_x2 zero y)
@@ -382,7 +382,7 @@ def rec_def (x : nat) : A :=
 -- existential, it still satisfies the property it definitionally is supposed
 -- to satisfy. This annoying problem would be subverted with proper Σ-types,
 -- provided they had η-equality.
-axiom definite_description (A : *) (P : A -> *) (h : exists A P) :
+axiom definite_description (A : ★) (P : A -> ★) (h : exists A P) :
     P (exists_elim A A P h (fun (x : A) (_ : P x) => x));
 
 -- Now we can use this axiom to prove that R n (rec_def n).
@@ -440,27 +440,31 @@ def psuc (_ r : nat) := suc r;
 -- And here's plus!
 def plus (n : nat) : nat -> nat := rec_def nat n psuc;
 
+-- And here's an infix version of it
+def + (n m : nat) : nat := plus n m;
+infixl 20 +;
+
 -- The first equation manifests itself as the familiar
 --      n + 0 = 0.
-def plus_0_r (n : nat) : eq nat (plus n zero) n :=
+def plus_0_r (n : nat) : eq nat (n + zero) n :=
   rec_def_sat_zero nat n psuc;
 
 -- The second equation, after a bit of massaging, manifests itself as the
 -- likewise familiar
 --      n + suc m = suc (n + m).
-def plus_s_r (n m : nat) : eq nat (plus n (suc m)) (suc (plus n m)) :=
+def plus_s_r (n m : nat) : eq nat (n + suc m) (suc (n + m)) :=
   rec_def_sat_suc nat n psuc m;
 
 -- -- We can now prove 1 + 1 = 2!
-def one_plus_one_two : eq nat (plus one one) two :=
+def one_plus_one_two : eq nat (one + one) two :=
   -- 1 + (suc zero) = suc (1 + zero) = suc one
-  eq_trans nat (plus one one) (suc (plus one zero)) two
+  eq_trans nat (one + one) (suc (one + zero)) two
 
   -- 1 + (suc zero) = suc (1 + zero)
   (plus_s_r one zero)
 
   -- suc (1 + zero) = suc one
-  (eq_cong nat nat (plus one zero) one suc (plus_0_r one));
+  (eq_cong nat nat (one + zero) one suc (plus_0_r one));
 
 -- We have successfully defined addition! Note that evaluating 1 + 1 to 2
 -- requires a proof, unfortunately, since this computation isn't visible to
@@ -469,133 +473,133 @@ 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 : forall (n m p : nat), eq nat (plus n (plus m p)) (plus (plus n m) p)
+def plus_assoc : forall (n m p : nat), eq nat (n + (m + p)) (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))
+    (fun (p : nat) => eq nat (n + (m + p)) (n + m + p))
 
     -- Base case: p = 0
     -- WTS n + (m + 0) = (n + m) + 0
     -- n + (m + 0) = n + m = (n + m) + 0
-    (eq_trans nat (plus n (plus m zero)) (plus n m) (plus (plus n m) zero)
+    (eq_trans nat (n + (m + zero)) (n + m) (n + m + zero)
       -- n + (m + 0) = n + m
-      (eq_cong nat nat (plus m zero) m (fun (p : nat) => plus n p) (plus_0_r m))
+      (eq_cong nat nat (m + zero) m (fun (p : nat) => n + p) (plus_0_r m))
 
       -- n + m = (n + m) + 0
-      (eq_sym nat (plus (plus n m) zero) (plus n m) (plus_0_r (plus n m))))
+      (eq_sym nat (n + m + zero) (n + m) (plus_0_r (n + m))))
 
     -- Inductive step: IH = n + (m + p) = (n + m) + p
-    (fun (p : nat) (IH : eq nat (plus n (plus m p)) (plus (plus n m) p)) =>
+    (fun (p : nat) (IH : eq nat (n + (m + p)) (n + m + p)) =>
       -- WTS n + (m + suc p) = (n + m) + suc p
       -- n + (m + suc p) = n + suc (m + p)
       --                 = suc (n + (m + p))
       --                 = suc ((n + m) + p)
       --                 = (n + m) + suc p
-      eq_trans nat (plus n (plus m (suc p))) (plus n (suc (plus m p))) (plus (plus n m) (suc p))
+      eq_trans nat (n + (m + suc p)) (n + (suc (m + p))) (n + m + suc p)
 
       -- n + (m + suc p) = n + suc (m + p)
-      (eq_cong nat nat (plus m (suc p)) (suc (plus m p)) (fun (a : nat) => (plus n a)) (plus_s_r m p))
+      (eq_cong nat nat (m + suc p) (suc (m + p)) (fun (a : nat) => (n + a)) (plus_s_r m p))
 
       -- n + suc (m + p) = (n + m) + suc p
-      (eq_trans nat (plus n (suc (plus m p))) (suc (plus n (plus m p))) (plus (plus n m) (suc p))
+      (eq_trans nat (n + suc (m + p)) (suc (n + (m + p))) (n + m + suc p)
         -- n + suc (m + p) = suc (n + (m + p))
-        (plus_s_r n (plus m p))
+        (plus_s_r n (m + p))
 
         -- suc (n + (m + p)) = (n + m) + suc p
-        (eq_trans nat (suc (plus n (plus m p))) (suc (plus (plus n m) p)) (plus (plus n m) (suc p))
+        (eq_trans nat (suc (n + (m + p))) (suc (n + m + p)) (n + m + suc p)
           -- suc (n + (m + p)) = suc ((n + m) + p)
-          (eq_cong nat nat (plus n (plus m p)) (plus (plus n m) p) suc IH)
+          (eq_cong nat nat (n + (m + p)) (n + m + p) suc IH)
 
           -- suc ((n + m) + p) = (n + m) + suc p
-          (eq_sym nat (plus (plus n m) (suc p)) (suc (plus (plus n m) p))
-            (plus_s_r (plus n m) p)))));
+          (eq_sym nat (n + m + suc p) (suc (n + m + p))
+            (plus_s_r (n + m) p)))));
 
 -- Up next is commutativity, but we will need a couple lemmas first.
 
 -- First, we will show that 0 + n = n.
-def plus_0_l : forall (n : nat), eq nat (plus zero n) n :=
+def plus_0_l : forall (n : nat), eq nat (zero + n) n :=
   -- We prove this by induction on n.
-  nat_ind (fun (n : nat) => eq nat (plus zero n) n)
+  nat_ind (fun (n : nat) => eq nat (zero + n) n)
     -- base case: WTS 0 + 0 = 0
     -- This is just plus_0_r 0
     (plus_0_r zero)
 
     -- inductive case
-    (fun (n : nat) (IH : eq nat (plus zero n) n) =>
+    (fun (n : nat) (IH : eq nat (zero + n) n) =>
       -- WTS 0 + (suc n) = suc n
       -- 0 + (suc n) = suc (0 + n) = suc n
-      eq_trans nat (plus zero (suc n)) (suc (plus zero n)) (suc n)
+      eq_trans nat (zero + suc n) (suc (zero + n)) (suc n)
       -- 0 + (suc n) = suc (0 + n)
       (plus_s_r zero n)
 
       -- suc (0 + n) = suc n
-      (eq_cong nat nat (plus zero n) n suc IH));
+      (eq_cong nat nat (zero + n) n suc IH));
 
 -- Next, we will show that (suc n) + m = suc (n + m).
-def plus_s_l (n : nat) : forall (m : nat), eq nat (plus (suc n) m) (suc (plus n m)) :=
+def plus_s_l (n : nat) : forall (m : nat), eq nat (suc n + m) (suc (n + m)) :=
   -- We proceed by induction on m.
-  nat_ind (fun (m : nat) => eq nat (plus (suc n) m) (suc (plus n m)))
+  nat_ind (fun (m : nat) => eq nat (suc n + m) (suc (n + m)))
     -- base case: (suc n) + 0 = suc (n + 0)
     -- (suc n) + 0 = suc n = suc (n + 0)
-    (eq_trans nat (plus (suc n) zero) (suc n) (suc (plus n zero))
+    (eq_trans nat (suc n + zero) (suc n) (suc (n + zero))
       -- (suc n) + 0 = suc n
       (plus_0_r (suc n))
 
       -- suc n = suc (n + 0)
-      (eq_cong nat nat n (plus n zero) suc
+      (eq_cong nat nat n (n + zero) suc
         -- n = n + 0
-        (eq_sym nat (plus n zero) n (plus_0_r n))))
+        (eq_sym nat (n + zero) n (plus_0_r n))))
 
     -- inductive case
     -- IH = suc n + m = suc (n + m)
-    (fun (m : nat) (IH : eq nat (plus (suc n) m) (suc (plus n m))) =>
+    (fun (m : nat) (IH : eq nat (suc n + m) (suc (n + m))) =>
         -- WTS suc n + suc m = suc (n + suc m)
         -- suc n + suc m = suc (suc n + m)
         --               = suc (suc (n + m))
         --               = suc (n + suc m)
-        (eq_trans nat (plus (suc n) (suc m)) (suc (plus (suc n) m)) (suc (plus n (suc m)))
+        (eq_trans nat (suc n + suc m) (suc (suc n + m)) (suc (n + suc m))
           -- suc n + suc m = suc (suc n + m)
           (plus_s_r (suc n) m)
 
           -- suc (suc n + m) = suc (n + suc m)
-          (eq_trans nat (suc (plus (suc n) m)) (suc (suc (plus n m))) (suc (plus n (suc m)))
+          (eq_trans nat (suc (suc n + m)) (suc (suc (n + m))) (suc (n + suc m))
             -- suc (suc n + m) = suc (suc (n + m))
-            (eq_cong nat nat (plus (suc n) m) (suc (plus n m)) suc IH)
+            (eq_cong nat nat (suc n + m) (suc (n + m)) suc IH)
 
             -- suc (suc (n + m)) = suc (n + suc m)
-            (eq_cong nat nat (suc (plus n m)) (plus n (suc m)) suc
+            (eq_cong nat nat (suc (n + m)) (n + suc m) suc
               -- suc (n + m) = n + suc m
-              (eq_sym nat (plus n (suc m)) (suc (plus n m)) (plus_s_r n m))))));
+              (eq_sym nat (n + suc m) (suc (n + m)) (plus_s_r n m))))));
 
 -- Finally, we can prove commutativity.
-def plus_comm (n : nat) : forall (m : nat), eq nat (plus n m) (plus m n) :=
+def plus_comm (n : nat) : forall (m : nat), eq nat (n + m) (m + n) :=
   -- As usual, we proceed by induction.
-  nat_ind (fun (m : nat) => eq nat (plus n m) (plus m n))
+  nat_ind (fun (m : nat) => eq nat (n + m) (m + n))
 
   -- Base case: WTS n + 0 = 0 + n
   -- n + 0 = n = 0 + n
-  (eq_trans nat (plus n zero) n (plus zero n)
+  (eq_trans nat (n + zero) n (zero + n)
     -- n + 0 = n
     (plus_0_r n)
 
     -- n = 0 + n
-    (eq_sym nat (plus zero n) n (plus_0_l n)))
+    (eq_sym nat (zero + n) n (plus_0_l n)))
 
   -- Inductive step:
-  (fun (m : nat) (IH : eq nat (plus n m) (plus m n)) =>
+  (fun (m : nat) (IH : eq nat (n + m) (m + n)) =>
     -- WTS n + suc m = suc m + n
     -- n + suc m = suc (n + m)
     --           = suc (m + n)
     --           = suc m + n
-    (eq_trans nat (plus n (suc m)) (suc (plus n m)) (plus (suc m) n)
+    (eq_trans nat (n + suc m) (suc (n + m)) (suc m + n)
       -- n + suc m = suc (n + m)
       (plus_s_r n m)
 
       -- suc (n + m) = suc m + n
-      (eq_trans nat (suc (plus n m)) (suc (plus m n)) (plus (suc m) n)
+      (eq_trans nat (suc (n + m)) (suc (m + n)) (suc m + n)
         -- suc (n + m) = suc (m + n)
-        (eq_cong nat nat (plus n m) (plus m n) suc IH)
+        (eq_cong nat nat (n + m) (m + n) suc IH)
 
         -- suc (m + n) = suc m + n
-        (eq_sym nat (plus (suc m) n) (suc (plus m n)) (plus_s_l m n)))));
+        (eq_sym nat (suc m + n) (suc (m + n)) (plus_s_l m n)))));
diff --git a/lib/Parser.hs b/lib/Parser.hs
index c41a26b..7203f92 100644
--- a/lib/Parser.hs
+++ b/lib/Parser.hs
@@ -5,18 +5,26 @@ module Parser where
 import Control.Monad.Combinators (option)
 import Control.Monad.Except
 import Data.List (foldl, foldl1)
+import qualified Data.Map.Strict as M
 import qualified Data.Text as T
 import Errors (Error (..))
 import IR
 import Preprocessor
-import Text.Megaparsec (MonadParsec (..), Parsec, ShowErrorComponent (..), between, choice, errorBundlePretty, label, runParser, try)
+import Text.Megaparsec (MonadParsec (..), ParsecT, ShowErrorComponent (..), between, choice, errorBundlePretty, label, runParserT, try)
 import Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer as L
 
 newtype TypeError = TE Error
     deriving (Eq, Ord)
 
-type Parser = Parsec TypeError Text
+data Fixity
+    = InfixL Int
+    | InfixR Int
+    deriving (Eq, Show)
+
+type Operators = Map Text Fixity
+
+type Parser = ParsecT TypeError Text (State Operators)
 
 instance ShowErrorComponent TypeError where
     showErrorComponent (TE e) = toString e
@@ -34,6 +42,9 @@ lexeme = L.lexeme skipSpace
 symbol :: Text -> Parser ()
 symbol = void . L.symbol skipSpace
 
+symbols :: String
+symbols = "!@#$%^&*-+=<>,./?[]{}\\|`~'\"∧∨⊙×≅"
+
 pKeyword :: Text -> Parser ()
 pKeyword keyword = void $ lexeme (string keyword <* notFollowedBy alphaNumChar)
 
@@ -46,21 +57,24 @@ pIdentifier = try $ label "identifier" $ lexeme $ do
     guard $ ident `notElem` keywords
     pure ident
 
+pSymbol :: Parser Text
+pSymbol = lexeme $ takeWhile1P (Just "symbol") (`elem` symbols)
+
 pVar :: Parser IRExpr
 pVar = label "variable" $ lexeme $ Var <$> pIdentifier
 
-pParamGroup :: Parser [Param]
-pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do
-    idents <- some pIdentifier
+pParamGroup :: Parser Text -> Parser [Param]
+pParamGroup ident = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do
+    idents <- some ident
     symbol ":"
     ty <- pIRExpr
     pure $ map (,ty) idents
 
-pSomeParams :: Parser [Param]
-pSomeParams = lexeme $ concat <$> some pParamGroup
+pSomeParams :: Parser Text -> Parser [Param]
+pSomeParams ident = lexeme $ concat <$> some (pParamGroup ident)
 
-pManyParams :: Parser [Param]
-pManyParams = lexeme $ concat <$> many pParamGroup
+pManyParams :: Parser Text -> Parser [Param]
+pManyParams ident = lexeme $ concat <$> many (pParamGroup ident)
 
 mkAbs :: Maybe IRExpr -> (Text, IRExpr) -> IRExpr -> IRExpr
 mkAbs ascription (param, typ) = Abs param typ ascription
@@ -71,7 +85,7 @@ mkPi ascription (param, typ) = Pi param typ ascription
 pLAbs :: Parser IRExpr
 pLAbs = lexeme $ label "λ-abstraction" $ do
     _ <- pKeyword "fun" <|> symbol "λ"
-    params <- pSomeParams
+    params <- pSomeParams pIdentifier
     ascription <- optional pAscription
     _ <- symbol "=>" <|> symbol "⇒"
     body <- pIRExpr
@@ -80,7 +94,7 @@ pLAbs = lexeme $ label "λ-abstraction" $ do
 pPAbs :: Parser IRExpr
 pPAbs = lexeme $ label "Π-abstraction" $ do
     _ <- pKeyword "forall" <|> symbol "∏" <|> symbol "∀"
-    params <- pSomeParams
+    params <- pSomeParams pIdentifier
     ascription <- optional pAscription
     symbol ","
     body <- pIRExpr
@@ -90,7 +104,7 @@ pBinding :: Parser (Text, Maybe IRExpr, IRExpr)
 pBinding = lexeme $ label "binding" $ do
     symbol "("
     ident <- pIdentifier
-    params <- pManyParams
+    params <- pManyParams pIdentifier
     ascription <- optional pAscription
     symbol ":="
     value <- pIRExpr
@@ -117,7 +131,7 @@ pApp :: Parser IRExpr
 pApp = lexeme $ foldl1 App <$> some pTerm
 
 pStar :: Parser IRExpr
-pStar = lexeme $ Star <$ symbol "*"
+pStar = lexeme $ Star <$ symbol "★"
 
 subscriptDigit :: Parser Integer
 subscriptDigit =
@@ -146,8 +160,31 @@ pSort = lexeme $ pStar <|> pSquare
 pTerm :: Parser IRExpr
 pTerm = lexeme $ label "term" $ choice [pSort, pVar, between (char '(') (char ')') pIRExpr]
 
+pInfix :: Parser IRExpr
+pInfix = parseWithPrec 0
+  where
+    parseWithPrec :: Int -> Parser IRExpr
+    parseWithPrec prec = pApp >>= continue prec
+
+    continue :: Int -> IRExpr -> Parser IRExpr
+    continue prec lhs = option lhs $ do
+        op <- lookAhead pSymbol
+        operators <- get
+        case M.lookup op operators of
+            Just fixity -> do
+                let (opPrec, nextPrec) = case fixity of
+                        InfixL p -> (p, p)
+                        InfixR p -> (p, p + 1)
+                if opPrec <= prec
+                    then pure lhs
+                    else do
+                        _ <- pSymbol
+                        rhs <- parseWithPrec nextPrec
+                        continue prec (App (App (Var op) lhs) rhs)
+            Nothing -> fail $ "unknown operator '" ++ toString op ++ "'"
+
 pAppTerm :: Parser IRExpr
-pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pApp]
+pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pInfix]
 
 pIRExpr :: Parser IRExpr
 pIRExpr = lexeme $ do
@@ -161,7 +198,7 @@ pAxiom :: Parser IRDef
 pAxiom = lexeme $ label "axiom" $ do
     pKeyword "axiom"
     ident <- pIdentifier
-    params <- pManyParams
+    params <- pManyParams (pIdentifier <|> pSymbol)
     ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription
     symbol ";"
     pure $ Axiom ident ascription
@@ -169,21 +206,33 @@ pAxiom = lexeme $ label "axiom" $ do
 pVariable :: Parser [IRSectionDef]
 pVariable = lexeme $ label "variable declaration" $ do
     pKeyword "variable" <|> pKeyword "hypothesis"
-    vars <- pManyParams
+    vars <- pManyParams (pIdentifier <|> pSymbol)
     symbol ";"
     pure $ uncurry Variable <$> vars
 
 pDef :: Parser IRDef
 pDef = lexeme $ label "definition" $ do
     pKeyword "def"
-    ident <- pIdentifier
-    params <- pManyParams
+    ident <- pIdentifier <|> pSymbol
+    params <- pManyParams pIdentifier
     ascription <- fmap (flip (foldr (mkPi Nothing)) params) <$> optional pAscription
     symbol ":="
     body <- pIRExpr
     symbol ";"
     pure $ Def ident ascription $ foldr (mkAbs Nothing) body params
 
+pFixityDec :: Parser ()
+pFixityDec = do
+    _ <- string "infix"
+    fixity <-
+        choice
+            [ InfixL <$> (lexeme (char 'l') >> lexeme L.decimal)
+            , InfixR <$> (lexeme (char 'r') >> lexeme L.decimal)
+            ]
+    ident <- pSymbol
+    modify (M.insert ident fixity)
+    symbol ";"
+
 pSection :: Parser IRSectionDef
 pSection = lexeme $ label "section" $ do
     pKeyword "section"
@@ -194,13 +243,13 @@ pSection = lexeme $ label "section" $ do
     pure $ Section secLabel body
 
 pIRDef :: Parser [IRSectionDef]
-pIRDef = (pure . IRDef <$> pAxiom) <|> (pure . IRDef <$> pDef) <|> pVariable <|> (pure <$> pSection)
+pIRDef = (pure . IRDef <$> pAxiom) <|> (pure . IRDef <$> pDef) <|> pVariable <|> (pure <$> pSection) <|> ([] <$ pFixityDec)
 
 pIRProgram :: Parser IRProgram
 pIRProgram = skipSpace >> concat <$> some pIRDef
 
 parserWrapper :: Parser a -> String -> Text -> Either String a
-parserWrapper p filename input = first errorBundlePretty $ runParser p filename input
+parserWrapper p filename input = first errorBundlePretty $ evalState (runParserT p filename input) M.empty
 
 parseProgram :: String -> Text -> Either String IRProgram
 parseProgram = parserWrapper pIRProgram