diff --git a/src/Algebra/Domain.ard b/src/Algebra/Domain.ard
index a0083809..a45829ce 100644
--- a/src/Algebra/Domain.ard
+++ b/src/Algebra/Domain.ard
@@ -17,10 +17,10 @@
         #0-zro (transport #0 x*y=0 (apartZeroProduct x y x#0 y#0))))))
 
   \lemma nonZero-left (x y : E) (x/=0 : Not (x = zro)) (x*y=0 : x * y = zro) : y = zro =>
-    separatedEq (\lam y/=0 => nonZeroProduct x y x/=0 y/=0 x*y=0)
+    separatedEq (nonZeroProduct x y x/=0 __ x*y=0)
 
   \lemma nonZero-right (x y : E) (y/=0 : Not (y = zro)) (x*y=0 : x * y = zro) : x = zro =>
-    separatedEq (\lam x/=0 => nonZeroProduct x y x/=0 y/=0 x*y=0)
+    separatedEq (nonZeroProduct x y __ y/=0 x*y=0)
 
   \lemma nonZero-cancel-left (x y z : E) (x/=0 : Not (x = zro)) (x*y=x*z : x * y = x * z) : y = z =>
     AddGroup.fromZero y z (nonZero-left x (y - z) x/=0 (ldistr x y (negative z) *> pmap (x * y +) (Ring.negative_*-right x z) *> AddGroup.toZero (x * y) (x * z) x*y=x*z))
@@ -35,8 +35,8 @@
     | ide-left x => SigmaPropExt #0 _ _ (ide-left x.1)
     | ide-right x => SigmaPropExt #0 _ _ (ide-right x.1)
     | *-assoc x y z => SigmaPropExt #0 _ _ (*-assoc x.1 y.1 z.1)
-    | cancel-left x y z x*y=x*z => SigmaPropExt #0 y z (nonZero-cancel-left x.1 y.1 z.1 (\lam x=0 => #0-zro (transport #0 x=0 x.2)) (pmap (\lam t => t.1) x*y=x*z))
-    | cancel-right x y z x*z=y*z => SigmaPropExt #0 x y (nonZero-cancel-right x.1 y.1 z.1 (\lam z=0 => #0-zro (transport #0 z=0 z.2)) (pmap (\lam t => t.1) x*z=y*z))
+    | cancel-left x y z x*y=x*z => SigmaPropExt #0 y z (nonZero-cancel-left x.1 y.1 z.1 (\lam x=0 => #0-zro (transport #0 x=0 x.2)) (pmap (__.1) x*y=x*z))
+    | cancel-right x y z x*z=y*z => SigmaPropExt #0 x y (nonZero-cancel-right x.1 y.1 z.1 (\lam z=0 => #0-zro (transport #0 z=0 z.2)) (pmap (__.1) x*z=y*z))
 } \where {
   \class Dec \extends Domain, Ring.Dec
     \where
diff --git a/src/Algebra/Domain/Bezout.ard b/src/Algebra/Domain/Bezout.ard
index 24e3fdc6..8b310584 100644
--- a/src/Algebra/Domain/Bezout.ard
+++ b/src/Algebra/Domain/Bezout.ard
@@ -17,9 +17,9 @@
       | inv-right =>
         g * (p.1 * g|x.inv + p.2 * g|y.inv)       ==< ldistr g (p.1 * g|x.inv) (p.2 * g|y.inv) >==
         g * (p.1 * g|x.inv) + g * (p.2 * g|y.inv) ==< inv (pmap2 (+) (*-assoc g p.1 g|x.inv) (*-assoc g p.2 g|y.inv)) >==
-        (g * p.1) * g|x.inv + (g * p.2) * g|y.inv ==< pmap2 (\lam t s => t * g|x.inv + s * g|y.inv) (*-comm g p.1) (*-comm g p.2) >==
+        (g * p.1) * g|x.inv + (g * p.2) * g|y.inv ==< pmap2 (__ * g|x.inv + __ * g|y.inv) (*-comm g p.1) (*-comm g p.2) >==
         (p.1 * g) * g|x.inv + (p.2 * g) * g|y.inv ==< pmap2 (+) (*-assoc p.1 g g|x.inv) (*-assoc p.2 g g|y.inv) >==
-        p.1 * (g * g|x.inv) + p.2 * (g * g|y.inv) ==< pmap2 (\lam t s => p.1 * t + p.2 * s) g|x.inv-right g|y.inv-right >==
+        p.1 * (g * g|x.inv) + p.2 * (g * g|y.inv) ==< pmap2 (p.1 * __ + p.2 * __) g|x.inv-right g|y.inv-right >==
         p.1 * x + p.2 * y                         `qed
     }
   })
diff --git a/src/Algebra/Domain/GCD.ard b/src/Algebra/Domain/GCD.ard
index 78e0d750..c3a1c389 100644
--- a/src/Algebra/Domain/GCD.ard
+++ b/src/Algebra/Domain/GCD.ard
@@ -27,8 +27,8 @@
                      | inv-right => SigmaPropExt #0 _ y g.gcd|val2.inv-right
                    }
                    | gcd-univ h (h|x : LDiv h x) (h|y : LDiv h y) =>
-                     \let h|g : LDiv h.1 g.gcd => g.gcd-univ h.1 (\new LDiv h.1 x.1 h|x.inv.1 (pmap (\lam t => t.1) h|x.inv-right))
-                                                                 (\new LDiv h.1 y.1 h|y.inv.1 (pmap (\lam t => t.1) h|y.inv-right))
+                     \let h|g : LDiv h.1 g.gcd => g.gcd-univ h.1 (\new LDiv h.1 x.1 h|x.inv.1 (pmap (__.1) h|x.inv-right))
+                                                                 (\new LDiv h.1 y.1 h|y.inv.1 (pmap (__.1) h|y.inv-right))
                      \in \new LDiv {
                        | inv => (h|g.inv, #0-*-right h.1 h|g.inv (transport #0 (inv h|g.inv-right) g#0))
                        | inv-right => SigmaPropExt #0 _ (g.gcd, g#0) h|g.inv-right
@@ -46,7 +46,7 @@
         | inv => g|x.inv K.* x#0.inv
         | inv-right =>
             g * (g|x.inv * x#0.inv) ==< inv (*-assoc g g|x.inv x#0.inv) >==
-            (g * g|x.inv) * x#0.inv ==< pmap (\lam t => t * x#0.inv) g|x.inv-right >==
+            (g * g|x.inv) * x#0.inv ==< pmap (__ * x#0.inv) g|x.inv-right >==
             x * x#0.inv             ==< x#0.inv-right >==
             ide                     `qed
       }
diff --git a/src/Algebra/Group.ard b/src/Algebra/Group.ard
index 0a18e191..8b3f8c07 100644
--- a/src/Algebra/Group.ard
+++ b/src/Algebra/Group.ard
@@ -49,11 +49,11 @@
           })
     \where {
       \lemma inverse-equality (G H : Group) (p : G = {Monoid} H) : Path (\lam i => p @ i -> p @ i) G.inverse H.inverse
-        => \let | q => pmap (\lam X => Monoid.E {X}) p
-                | f x => coe (\lam i => p @ i) x right
-                | g y => coe (\lam i => inv q @ i) y right
+        => \let | q => pmap (Monoid.E {__}) p
+                | f x => coe (p @ __) x right
+                | g y => coe (inv q @) y right
                 | h' {H' : Monoid} (q : G = {Monoid} H') => transport (\lam (H' : Monoid) => MonoidHom G H') q (MonoidCategory.id G)
-                | h => transport (\lam f' => MonoidHom G H f') (Jl (\lam (H' : Monoid) q => func {h' q} = (\lam x => coe (\lam i => q @ i) x right)) idp p) (h' p)
+                | h => transport (MonoidHom G H __) (Jl (\lam (H' : Monoid) q => func {h' q} = (\lam x => coe (q @ __) x right)) idp p) (h' p)
                 | h-inv (y : H) => MonoidHom.presInvElem h
                                       (\new Inv { | val => g y | inv => G.inverse (g y) | inv-left => G.inverse-left (g y) | inv-right => G.inverse-right (g y) })
                                       (\new Inv { | inv => H.inverse (f (g y)) | inv-left => H.inverse-left (f (g y)) | inv-right => H.inverse-right (f (g y)) })
@@ -86,7 +86,7 @@
     (x + y) - (x + y)          ==< negative-right (x + y) >==
     zro                        ==< inv (negative-right x) >==
     x - x                      ==< pmap (x +) (inv (zro-left (negative x))) >==
-    x + (zro - x)              ==< pmap (\lam t => x + (t - x)) (inv (negative-right y)) >==
+    x + (zro - x)              ==< pmap (x + (__ - x)) (inv (negative-right y)) >==
     x + ((y - y) - x)          ==< pmap (x +) (+-assoc y (negative y) (negative x)) >==
     x + (y + (negative y - x)) ==< inv (+-assoc x y (negative y - x)) >==
     (x + y) + (negative y - x) `qed
@@ -111,7 +111,7 @@
     \use \coerce fromGroup (G : Group) => \new AddGroup G.E G.ide (G.*) G.ide-left G.ide-right G.*-assoc G.inverse G.inverse-left G.inverse-right
     \use \coerce toGroup (G : AddGroup) => \new Group G.E G.zro (G.+) G.zro-left G.zro-right G.+-assoc G.negative G.negative-left G.negative-right
 
-    \func equals (A B : AddGroup) (p : A = {\Set} B) (q : \let f x => coe (\lam i => p @ i) x right \in \Pi (x y : A) -> f (x + y) = f x + f y) : A = B
+    \func equals (A B : AddGroup) (p : A = {\Set} B) (q : \let f x => coe (p @) x right \in \Pi (x y : A) -> f (x + y) = f x + f y) : A = B
       => pmap {Group} {AddGroup} AddGroup.fromGroup (Group.equals A B (Monoid.equals {AddGroup.toGroup A} {AddGroup.toGroup B} p q))
 
   -- | An additive group with a tight apartness relation.
diff --git a/src/Algebra/Group/Category.ard b/src/Algebra/Group/Category.ard
index fd5b7403..c2d162c5 100644
--- a/src/Algebra/Group/Category.ard
+++ b/src/Algebra/Group/Category.ard
@@ -31,7 +31,7 @@
                                          (inv (f.func-+ (zro {f.Dom}) (zro {f.Dom})) *> pmap f.func (zro-right {f.Dom} (zro {f.Dom})) *> inv (zro-right {f.Cod} (f.func (zro {f.Dom}))))
 
     \func equals {A B : AddGroup} {f g : AbGroupHom A B} (p : \Pi (x : A) -> f.func x = g.func x) : f = g
-      => path (\lam i => \new AbGroupHom A B (\lam x => p x @ i) (pathInProp (\lam j => \Pi (x y : A) -> p (x + y) @ j = (p x @ j) + (p y @ j)) f.func-+ g.func-+ @ i))
+      => path (\lam i => \new AbGroupHom A B (p __ @ i) (pathInProp (\lam j => \Pi (x y : A) -> p (x + y) @ j = (p x @ j) + (p y @ j)) f.func-+ g.func-+ @ i))
   }
 
 \instance AddGroupCategory : Cat AddGroup
@@ -46,7 +46,7 @@
   | o-assoc _ _ _ => idp
   | univalence {A B : AddGroup} (f : AbGroupHom A B) (g : AbGroupHom B A) p q =>
     \let A=B => AddGroup.equals A B (path (iso f.func g.func (\lam x => path (\lam i => func {p @ i} x)) (\lam y => path (\lam i => func {q @ i} y)))) f.func-+
-    \in (A=B, AbGroupHom.equals (\lam x => Jl {AddGroup} (\lam C A=C => func {transport (\lam C => AbGroupHom A C) A=C (id A)} x = coe (\lam j => A=C @ j) x right) idp A=B))
+    \in (A=B, AbGroupHom.equals (\lam x => Jl {AddGroup} (\lam C A=C => func {transport (AbGroupHom A __) A=C (id A)} x = coe (A=C @ __) x right) idp A=B))
   \where
     \func id (G : AddGroup) : AbGroupHom G G \cowith
       | func x => x
diff --git a/src/Algebra/Monoid.ard b/src/Algebra/Monoid.ard
index a7d1fd0d..189eda5e 100644
--- a/src/Algebra/Monoid.ard
+++ b/src/Algebra/Monoid.ard
@@ -8,11 +8,11 @@
   | ide-right (x : E) : x * ide = x
   | *-assoc (x y z : E) : (x * y) * z = x * (y * z)
 } \where {
-  \func equals {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (\lam i => p @ i) x right \in \Pi (x y : M) -> f (x * y) = f x * f y) : M = N
-    => \let mp i => prop-equality p q @ i
+  \func equals {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y) : M = N
+    => \let mp => prop-equality p q @ __
        \in path (\lam i => \new Monoid (p @ i) (ide-equality p q @ i) (*-equality p q @ i) (ide-left {mp i}) (ide-right {mp i}) (*-assoc {mp i}))
     \where {
-      \lemma ide-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (\lam i => p @ i) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
+      \lemma ide-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
         : Path (\lam j => p @ j) M.ide N.ide
         => \let | f x => coe (\lam i => p @ i) x right
                 | g y => coe (\lam i => inv p @ i) y right
@@ -25,20 +25,20 @@
                        ide               `qed
            \in pathOver {\lam j => p @ j} r
 
-      \lemma *-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (\lam i => p @ i) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
+      \lemma *-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
         : Path (\lam j => p @ j -> p @ j -> p @ j) (M.*) (N.*)
-        => \let | f x => coe (\lam i => p @ i) x right
-                | g y => coe (\lam i => inv p @ i) y right
+        => \let | f x => coe (p @) x right
+                | g y => coe (inv p @) y right
                 | fg y : f (g y) = y => transport_id_inv (\lam Z => Z) p y
                 | q' (x y : N) =>
-                    coe (\lam i => p @ i -> p @ i -> p @ i) (*) right x y ==< pmap (\lam h => h y) (transport_pi (\lam Z => Z) (\lam Z => Z -> Z) p (*) x) >==
+                    coe (\lam i => p @ i -> p @ i -> p @ i) (*) right x y ==< pmap (__ y) (transport_pi (\lam Z => Z) (\lam Z => Z -> Z) p (*) x) >==
                     coe (\lam i => p @ i -> p @ i) (* (g x)) right y      ==< transport_pi (\lam Z => Z) (\lam Z => Z) p (* (g x)) y >==
                     f (g x * g y)                                         ==< q (g x) (g y) >==
                     f (g x) * f (g y)                                     ==< pmap2 (*) (fg x) (fg y) >==
                     x * y                                                 `qed
            \in pathOver {\lam j => p @ j -> p @ j -> p @ j} (path (\lam j x y => q' x y @ j))
 
-      \lemma prop-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (\lam i => p @ i) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
+      \lemma prop-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
         : Path (\lam j => Monoid (p @ j) (ide-equality p q @ j) (*-equality p q @ j)) M N
         => pathInProp (\lam i => Monoid (p @ i) (ide-equality p q @ i) (*-equality p q @ i)) M N
     }
@@ -94,7 +94,7 @@
       \lemma cancelProp {M : Monoid} (x : M) (q : \Pi (a b : M) -> x * a = x * b -> a = b) (y : M) : isProp (LDiv x y) =>
         \lam (d1 d2 : LDiv x y) =>
             \let p => q d1.inv d2.inv (d1.inv-right *> Paths.inv d2.inv-right)
-            \in path (\lam i => \new LDiv x y (p @ i) (pathInProp (\lam j => x * (p @ j) = y) d1.inv-right d2.inv-right @ i))
+            \in path (\lam i => \new LDiv x y (p @ i) (pathInProp (x * (p @ __) = y) d1.inv-right d2.inv-right @ i))
 
       \use \level levelProp {M : CancelMonoid} (x y : M) : isProp (LDiv x y) => cancelProp x (M.cancel-left x) y
     }
@@ -125,7 +125,7 @@
       \lemma levelProp {M : CancelMonoid} (x y : M) : isProp (RDiv x y) =>
         \lam (d1 d2 : RDiv x y) =>
             \let p => M.cancel-right d1.inv d2.inv x (d1.inv-left *> Paths.inv d2.inv-left)
-            \in path (\lam i => \new RDiv x y (p @ i) (pathInProp (\lam j => (p @ j) * x = y) d1.inv-left d2.inv-left @ i))
+            \in path (\lam i => \new RDiv x y (p @ i) (pathInProp ((p @ __) * x = y) d1.inv-left d2.inv-left @ i))
     }
 
   -- | The type of left inverses of an element
@@ -170,8 +170,8 @@
           j'.inv * ide         ==< ide-right j'.inv >==
           j'.inv               `qed
         \in path (\lam i => \new Inv x (p @ i)
-                                     (pathInProp (\lam j => (p @ j) * x = ide) j.inv-left j'.inv-left @ i)
-                                     (pathInProp (\lam j => x * (p @ j) = ide) j.inv-right j'.inv-right @ i))
+                                     (pathInProp ((p @ __) * x = ide) j.inv-left j'.inv-left @ i)
+                                     (pathInProp (x * (p @ __) = ide) j.inv-right j'.inv-right @ i))
 
       \lemma product {M : Monoid} (i j : Inv {M}) : Inv (i.val * j.val) => func i j
         \where {
@@ -183,7 +183,7 @@
           \lemma lem {M : Monoid} (i j : Inv {M}) : (j.inv * i.inv) * (i.val * j.val) = ide =>
             (j.inv * i.inv) * (i.val * j.val) ==< *-assoc j.inv i.inv (i.val * j.val) >==
             j.inv * (i.inv * (i.val * j.val)) ==< pmap (j.inv *) (Paths.inv (*-assoc i.inv i.val j.val)) >==
-            j.inv * ((i.inv * i.val) * j.val) ==< pmap (\lam t => j.inv * (t * j.val)) i.inv-left >==
+            j.inv * ((i.inv * i.val) * j.val) ==< pmap (j.inv * (__ * j.val)) i.inv-left >==
             j.inv * (ide * j.val)             ==< pmap (j.inv *) (ide-left j.val) >==
             j.inv * j.val                     ==< j.inv-left >==
             ide                               `qed
@@ -198,7 +198,7 @@
           (i.inv * x) * (y * (j.inv * x)) ==< *-assoc i.inv x (y * (j.inv * x)) >==
           i.inv * (x * (y * (j.inv * x))) ==< pmap (i.inv *) (Paths.inv (*-assoc x y (j.inv * x))) >==
           i.inv * ((x * y) * (j.inv * x)) ==< pmap (i.inv *) (Paths.inv (*-assoc (x * y) j.inv x)) >==
-          i.inv * (((x * y) * j.inv) * x) ==< pmap (\lam t => i.inv * (t * x)) j.inv-right >==
+          i.inv * (((x * y) * j.inv) * x) ==< pmap (i.inv * (__ * x)) j.inv-right >==
           i.inv * (ide * x)               ==< pmap (i.inv *) (ide-left x) >==
           i.inv * x                       ==< i.inv-left >==
           ide                             `qed
@@ -227,7 +227,7 @@
         lmake (i.inv * x) (*-assoc i.inv x y *> i.inv-left)
 
       \lemma cfactor-left {M : CMonoid} (x y : M) (i : Inv (x * y)) : Inv x =>
-        cfactor-right y x (transport (\lam t => Inv t) (*-comm x y) i)
+        cfactor-right y x (transport (Inv __) (*-comm x y) i)
     }
 }
 
diff --git a/src/Algebra/Monoid/Category.ard b/src/Algebra/Monoid/Category.ard
index 381e6cc6..657da703 100644
--- a/src/Algebra/Monoid/Category.ard
+++ b/src/Algebra/Monoid/Category.ard
@@ -12,8 +12,8 @@
 }
   \where {
     \func equals {M N : Monoid} {f g : MonoidHom M N} (p : \Pi (x : M) -> f.func x = g.func x) : f = g
-      => path (\lam i => \new MonoidHom M N (\lam x => p x @ i)
-                                            (pathInProp (\lam j => p ide @ j = ide) f.func-ide g.func-ide @ i)
+      => path (\lam i => \new MonoidHom M N (p __ @ i)
+                                            (pathInProp (p ide @ __ = ide) f.func-ide g.func-ide @ i)
                                             (pathInProp (\lam j => \Pi (x y : M) -> p (x * y) @ j = (p x @ j) * (p y @ j)) f.func-* g.func-* @ i))
 
     \open Monoid(Inv)
@@ -44,7 +44,7 @@
   | o-assoc _ _ _ => idp
   | univalence {M N : Monoid} (f : MonoidHom M N) (g : MonoidHom N M) p q =>
     \let M=N => Monoid.equals (path (iso f.func g.func (\lam x => path (\lam i => func {p @ i} x)) (\lam y => path (\lam i => func {q @ i} y)))) f.func-*
-    \in (M=N, MonoidHom.equals (\lam x => Jl {Monoid} (\lam K M=K => func {transport (\lam K => MonoidHom M K) M=K (id M)} x = coe (\lam j => M=K @ j) x right) idp M=N))
+    \in (M=N, MonoidHom.equals (\lam x => Jl {Monoid} (\lam K M=K => func {transport (MonoidHom M __) M=K (id M)} x = coe (M=K @ __) x right) idp M=N))
   \where
     \func id (M : Monoid) : MonoidHom M M \cowith
       | func x => x
diff --git a/src/Algebra/Monoid/Prime.ard b/src/Algebra/Monoid/Prime.ard
index c8ba1831..12ac627d 100644
--- a/src/Algebra/Monoid/Prime.ard
+++ b/src/Algebra/Monoid/Prime.ard
@@ -13,7 +13,7 @@
   | isIrr (x y : M) : e = x * y -> Inv x || Inv y
 
   \func decide (x y : M) (e=x*y : e = x * y) : Inv x `Or` Inv y =>
-    ||.rec (Or.levelProp (\lam (i : Inv x) (j : Inv y) => notInv (transport (\lam x => Inv x) (inv e=x*y) (Inv.product i j)))) inl inr (isIrr x y e=x*y)
+    ||.rec (Or.levelProp (\lam (i : Inv x) (j : Inv y) => notInv (transport (Inv __) (inv e=x*y) (Inv.product i j)))) inl inr (isIrr x y e=x*y)
 }
 
 \lemma Prime-isIrr {M : CancelCMonoid} (p : Prime {M}) : Irr p.e p.notInv \cowith
@@ -79,9 +79,9 @@
             ))
           | byRight (xi : Inv x) => byLeft (\new LDiv p.e a (xi.inv * g|a.inv) (
             p.e * (xi.inv * g|a.inv)     ==< inv (*-assoc _ _ _) >==
-            (p.e * xi.inv) * g|a.inv     ==< pmap (\lam t => (t * xi.inv) * g|a.inv) (inv g|p.inv-right) >==
+            (p.e * xi.inv) * g|a.inv     ==< pmap ((__ * xi.inv) * g|a.inv) (inv g|p.inv-right) >==
             ((g * x) * xi.inv) * g|a.inv ==< pmap (`* g|a.inv) (*-assoc _ _ _) >==
-            (g * (x * xi.inv)) * g|a.inv ==< pmap (\lam t => (g * t) * g|a.inv) xi.inv-right >==
+            (g * (x * xi.inv)) * g|a.inv ==< pmap ((g * __) * g|a.inv) xi.inv-right >==
             (g * ide) * g|a.inv          ==< pmap (`* g|a.inv) (ide-right g) >==
             g * g|a.inv                  ==< g|a.inv-right >==
             a                            `qed
diff --git a/src/Algebra/Ordered.ard b/src/Algebra/Ordered.ard
index e076f051..95f20636 100644
--- a/src/Algebra/Ordered.ard
+++ b/src/Algebra/Ordered.ard
@@ -34,7 +34,7 @@
       (y + z) - (x + z)          ==< pmap ((y + z) +) (negative_+ x z) >==
       (y + z) + (negative z - x) ==< +-assoc _ _ _ >==
       y + (z + (negative z - x)) ==< inv (pmap (y +) (+-assoc _ _ _)) >==
-      y + ((z - z) - x)          ==< pmap (\lam t => y + (t - x)) (negative-right z) >==
+      y + ((z - z) - x)          ==< pmap (y + (__ - x)) (negative-right z) >==
       y + (zro - x)              ==< pmap (y +) (zro-left _) >==
       y - x                      `qed)) x<y
 
@@ -56,7 +56,7 @@
   \lemma diff_+ {A : AddGroup} {x y z : A} : (z - y) + (y - x) = z - x =>
     (z - y) + (y - x)          ==< +-assoc _ _ _ >==
     z + (negative y + (y - x)) ==< inv (pmap (z +) (+-assoc _ _ _)) >==
-    z + ((negative y + y) - x) ==< pmap (\lam t => z + (t - x)) (negative-left y) >==
+    z + ((negative y + y) - x) ==< pmap (z + (__ - x)) (negative-left y) >==
     z + (zro - x)              ==< pmap (z +) (zro-left _) >==
     z - x                      `qed
 }
diff --git a/src/Algebra/Pointed.ard b/src/Algebra/Pointed.ard
index 53e7574d..52450043 100644
--- a/src/Algebra/Pointed.ard
+++ b/src/Algebra/Pointed.ard
@@ -4,8 +4,8 @@
 \class Pointed \extends BaseSet
   | ide : E
   \where {
-    \func equls {X Y : Pointed} (p : X = {\Set} Y) (q : coe (\lam i => p @ i) ide right = ide) : X = Y
-      => path (\lam i => \new Pointed (p @ i) (pathOver {\lam j => p @ j} q @ i))
+    \func equls {X Y : Pointed} (p : X = {\Set} Y) (q : coe (p @) ide right = ide) : X = Y
+      => path (\lam i => \new Pointed (p @ i) (pathOver {p @} q @ i))
   }
 
 \class AddPointed \extends BaseSet
diff --git a/src/Algebra/Pointed/Category.ard b/src/Algebra/Pointed/Category.ard
index 82d77eee..4cbfa339 100644
--- a/src/Algebra/Pointed/Category.ard
+++ b/src/Algebra/Pointed/Category.ard
@@ -9,7 +9,7 @@
   | func-ide : func ide = ide
 } \where
     \func equals {X Y : Pointed} {f g : PointedHom X Y} (p : \Pi (x : X) -> f.func x = g.func x) : f = g
-      => path (\lam i => \new PointedHom X Y (\lam x => p x @ i) (pathInProp (\lam j => p ide @ j = ide) f.func-ide g.func-ide @ i))
+      => path (\lam i => \new PointedHom X Y (p __ @ i) (pathInProp (p ide @ __ = ide) f.func-ide g.func-ide @ i))
 
 \instance PointedSetCat : Cat Pointed
   | Hom X Y => PointedHom X Y
@@ -23,7 +23,7 @@
   | o-assoc _ _ _ => idp
   | univalence {X Y : Pointed} (f : PointedHom X Y) (g : PointedHom Y X) p q =>
     \let X=Y => Pointed.equls (path (iso f.func g.func (\lam x => path (\lam i => func {p @ i} x)) (\lam y => path (\lam i => func {q @ i} y)))) f.func-ide
-    \in (X=Y, PointedHom.equals (\lam x => Jl {Pointed} (\lam Z X=Z => func {transport (\lam Z => PointedHom X Z) X=Z (id X)} x = coe (\lam j => X=Z @ j) x right) idp X=Y))
+    \in (X=Y, PointedHom.equals (\lam x => Jl {Pointed} (\lam Z X=Z => func {transport (PointedHom X __) X=Z (id X)} x = coe (\lam j => X=Z @ j) x right) idp X=Y))
   \where
     \func id (X : Pointed) : PointedHom X X \cowith
       | func x => x
diff --git a/src/Algebra/Ring.ard b/src/Algebra/Ring.ard
index 63125c81..7a46cf3e 100644
--- a/src/Algebra/Ring.ard
+++ b/src/Algebra/Ring.ard
@@ -45,7 +45,7 @@
     | AbGroup => R
     | Semiring => Semiring.op R
 
-  \func equals {R S : Ring} (p : R = {\Set} S) (q : \let f x => coe (\lam i => p @ i) x right \in \Sigma (\Pi (x y : R) -> f (x + y) = f x + f y) (\Pi (x y : R) -> f (x * y) = f x * f y)) : R = S
+  \func equals {R S : Ring} (p : R = {\Set} S) (q : \let f x => coe (p @) x right \in \Sigma (\Pi (x y : R) -> f (x + y) = f x + f y) (\Pi (x y : R) -> f (x * y) = f x * f y)) : R = S
     => \let | gr => AbGroup.equals R S (AddGroup.equals R S p q.1)
             | mon => Monoid.equals p q.2
        \in path (\lam i => \new Ring {
diff --git a/src/Arith/Int.ard b/src/Arith/Int.ard
index f9356dfd..f7d41c85 100644
--- a/src/Arith/Int.ard
+++ b/src/Arith/Int.ard
@@ -135,7 +135,7 @@
     | pos n, pos m, pos k => pmap pos (NatSemiring.ldistr _ _ _)
     | pos n, pos m, neg (suc k) => pos_minus-ldistr
     | pos n, neg (suc m), pos k => pos_minus-ldistr {n} {k} {suc m} *> +-comm _ _
-    | pos 0, neg (suc m), neg (suc k) => pmap neg (zro_*-left (suc m Nat.+ k)) *> inv (pmap2 (\lam t1 t2 => neg t1 + neg t2) (zro_*-left m) (zro_*-left k))
+    | pos 0, neg (suc m), neg (suc k) => pmap neg (zro_*-left (suc m Nat.+ k)) *> inv (pmap2 (neg __ + neg __) (zro_*-left m) (zro_*-left k))
     | pos (suc n), neg (suc m), neg (suc k) => pmap (\lam t => neg (suc t)) (pmap (Nat.`+ n) (NatSemiring.ldistr _ _ _) *> AddMonoid.+-assoc (suc n Nat.* suc m) (suc n Nat.* k) n)
     | neg (suc n), pos m, pos k => pmap neg (NatSemiring.ldistr (suc n) m k) *> inv (neg+neg {suc n Nat.* m} {suc n Nat.* k})
     | neg (suc n), pos m, neg (suc k) => neg_minus-ldistr
diff --git a/src/Arith/Nat.ard b/src/Arith/Nat.ard
index 7172ca77..8f1b81bb 100644
--- a/src/Arith/Nat.ard
+++ b/src/Arith/Nat.ard
@@ -22,7 +22,7 @@
   | suc n => -'id n
 
 \func suc/=0 {n : Nat} (p : suc n = 0) {A : \Type} : A =>
-  coe (\lam i => \case p @ i \with { suc _ => Nat | 0 => A }) 0 right
+  coe (\case p @ __ \with { suc _ => Nat | 0 => A }) 0 right
 
 -- # Properties of <= and <
 
@@ -149,7 +149,7 @@
   }
   | zro<ide => suc<=suc zero<=_
   | <_*_positive-left (n m k : Nat) (p : suc n <= m) (q : 1 <= k) : suc (n * k) <= m * k \elim k, q {
-    | 1, _ => transport2 (\lam t s => suc t <= s) (inv (+-comm _ _)) (inv (+-comm _ _)) p
+    | 1, _ => transport2 (suc __ <= __) (inv (+-comm _ _)) (inv (+-comm _ _)) p
     | suc (suc k), q => <=_+ (<=-transitive _ _ _ <=-suc (<_*_positive-left n m (suc k) p (suc<=suc zero<=_))) p
   }
   | <_*_negative-left x y z x<y z<0 => \case z<0 \with {}
\ No newline at end of file
diff --git a/src/Arith/Rat.ard b/src/Arith/Rat.ard
index 88eb3ef6..9c207086 100644
--- a/src/Arith/Rat.ard
+++ b/src/Arith/Rat.ard
@@ -7,6 +7,6 @@
 \record Rat (extract : LocRing.Type (localization-isOrderedField.positiveSubset IntRing))
 
 \instance RatField : DiscreteOrderedField Rat
-  => transport (\lam X => DiscreteOrderedField X)
-               (path (iso {LocRing.Type (localization-isOrderedField.positiveSubset IntRing)} {Rat} (\lam x => \new Rat x) (\lam r => Rat.extract {r}) idpe idpe))
+  => transport (DiscreteOrderedField __)
+               (path (iso {LocRing.Type (localization-isOrderedField.positiveSubset IntRing)} {Rat} (\lam x => \new Rat x) (Rat.extract {__}) idpe idpe))
                (localization-isDiscreteOrderedField IntRing)
diff --git a/src/Category.ard b/src/Category.ard
index 9b99ec5f..162c99a1 100644
--- a/src/Category.ard
+++ b/src/Category.ard
@@ -82,11 +82,11 @@
                 | f_sec => idpe
               })
               | Eq {x y : C} (e : Iso {C} {x} {y}) (p : x = y)
-                  => Jl (\lam y' p' => \Pi (e' : Iso {C} {x} {y'}) -> Equiv {transport (\lam z => Iso {C} {x} {z}) p' idIso = {Iso {C} {x} {y'}} e'} {transport (Hom x) p' (id x) = e'.f})
+                  => Jl (\lam y' p' => \Pi (e' : Iso {C} {x} {y'}) -> Equiv {transport (Iso {C} {x} {__}) p' idIso = {Iso {C} {x} {y'}} e'} {transport (Hom x) p' (id x) = e'.f})
                         (\lam e' => Embedding.pmap-isEquiv {Emb {x}} {idIso} {e'})
                         p e
               | t (e : Iso) => F e.f e.inv e.f_inv e.inv_f
-              | T-equiv {x y : C} : Equiv (T {x} {y}) => pathEquiv (\lam x y => Iso {C} {x} {y}) (\lam {x} {y} => \new Retraction {
+              | T-equiv {x y : C} : Equiv (T {x} {y}) => pathEquiv (Iso {C} {__} {__}) (\lam {x} {y} => \new Retraction {
                 | f => T {x} {y}
                 | sec (e : Iso) => (t e).1
                 | f_sec (e : Iso) => Equiv.ret {Eq e (t e).1} (t e).2
diff --git a/src/Category/Sub.ard b/src/Category/Sub.ard
index 4d4092a6..4b479996 100644
--- a/src/Category/Sub.ard
+++ b/src/Category/Sub.ard
@@ -14,4 +14,4 @@
   | Precat => subPrecat e.f
   | univalence {x} {y} f g p q =>
     \let (t,r) => univalence f g p q
-    \in (Retraction.sec {e.isEmb x y} t, pmap (\lam s => transport (Hom (e.f x)) s (id (e.f x))) (Retraction.f_sec {e.isEmb x y} t) *> r)
\ No newline at end of file
+    \in (Retraction.sec {e.isEmb x y} t, pmap (transport (Hom (e.f x)) __ (id (e.f x))) (Retraction.f_sec {e.isEmb x y} t) *> r)
\ No newline at end of file
diff --git a/src/Data/SeqColimit.ard b/src/Data/SeqColimit.ard
index 7b32c3fc..fcb7f289 100644
--- a/src/Data/SeqColimit.ard
+++ b/src/Data/SeqColimit.ard
@@ -105,11 +105,11 @@
         \let | t => path (quotSC x) *> pmap inSC ((p n).2 x) *> points s p n
              | h a => (path (quotSC a) *> pmap inSC ((p (suc n)).2 a))
              | q =>
-               coe (\lam i => quotSC x i = inSC (p 0).1) t right                                   ==< coe_path (path (quotSC x)) t idp >==
+               coe (quotSC x __ = inSC (p 0).1) t right                                            ==< coe_path (path (quotSC x)) t idp >==
                inv (path (quotSC x)) *> t                                                          ==< inv (*>-assoc _ _ _) >==
                (inv (path (quotSC x)) *> path (quotSC x)) *> pmap inSC ((p n).2 x) *> points s p n ==< pmap (`*> pmap inSC ((p n).2 x) *> points s p n) (inv_*> (path (quotSC x))) >==
                idp *> pmap inSC ((p n).2 x) *> points s p n                                        ==< idp_*> _ >==
-               pmap inSC ((p n).2 x) *> points s p n                                               ==< pmap (`*> points s p n) (inv (Jl (\lam y q => h (s.f x) *> inv (h y) = pmap inSC q) (*>_inv _) ((p n).2 x))) >==
+               pmap inSC ((p n).2 x) *> points s p n                                               ==< pmap (`*> points s p n) (inv (Jl (\lam y => h (s.f x) *> inv (h y) = pmap inSC __) (*>_inv _) ((p n).2 x))) >==
                (h (s.f x) *> inv (h (p n).1)) *> points s p n                                      ==< *>-assoc _ _ _ >==
                h (s.f x) *> points s p (suc n)                                                     ==< *>-assoc _ _ _ >==
                path (quotSC (s.f x)) *> pmap inSC ((p (suc n)).2 (s.f x)) *> points s p (suc n)    `qed
diff --git a/src/Equiv.ard b/src/Equiv.ard
index fdff3a98..3d271025 100644
--- a/src/Equiv.ard
+++ b/src/Equiv.ard
@@ -13,7 +13,7 @@
 \record Section (ret : B -> A) (ret_f : \Pi (x : A) -> ret (f x) = x) \extends Map
   \where {
     \func =Fiber {A B : \Type} (f : A -> B) : Section f = Fib (-o f) id
-      => path (iso (\lam (s : Section f) => Fib.make (-o f) s.ret (path (\lam i x => s.ret_f x @ i)))
+      => path (iso (\lam (s : Section f) => Fib.make (-o f) s.ret (path (\lam i => s.ret_f __ @ i)))
                    (\lam z => \new Section f z.1 (\lam x => path (\lam i => (z.2 @ i) x)))
                    idpe
                    idpe)
@@ -28,7 +28,7 @@
 \record Retraction (sec : B -> A) (f_sec : \Pi (y : B) -> f (sec y) = y) \extends Map
   \where {
     \func =Fiber {A B : \Type} (f : A -> B) : Retraction f = Fib (f `o-) id
-      => path (iso (\lam (s : Retraction f) => Fib.make (f `o-) s.sec (path (\lam i x => s.f_sec x @ i)))
+      => path (iso (\lam (s : Retraction f) => Fib.make (f `o-) s.sec (path (\lam i => s.f_sec __ @ i)))
                    (\lam z => \new Retraction f z.1 (\lam x => path (\lam i => (z.2 @ i) x)))
                    idpe
                    idpe)
@@ -128,7 +128,7 @@
     })) e3
 
   \lemma parallelEquiv {A B C D : \Type} (ab : A -> B) (cd : C -> D) (ac : Equiv {A} {C}) (bd : Equiv {B} {D}) (h : \Pi (a : A) -> bd.f (ab a) = cd (ac.f a)) : Equiv ab = Equiv cd
-    => propExt (\lam (e : Equiv ab) => leftFactor ac cd (coe (\lam i => QEquiv (\lam a => h a @ i)) (transQEquiv e bd) right))
+    => propExt (\lam (e : Equiv ab) => leftFactor ac cd (coe (\lam i => QEquiv (h __ @ i)) (transQEquiv e bd) right))
                (\lam (e : Equiv cd) => rightFactor ab bd (coe (\lam i => QEquiv (\lam a => inv (h a) @ i)) (transQEquiv ac e) right))
 
   \lemma leftEquiv {A B C : \Type} (e : Equiv {A} {B}) (g : B -> C) : Equiv g = Equiv (g `o` e.f)
@@ -169,20 +169,20 @@
   | A => f = f'
   | B => \Pi (a : A) -> f a = f' a
   | f p a => path (\lam i => (p @ i) a)
-  | ret g => path (\lam i a => g a @ i)
+  | ret g => path (\lam i => g __ @ i)
   | ret_f _ => idp
   | f_sec _ => idp
 
 \func sigmaEquiv {A : \Type} (B : A -> \Type) (p p' : \Sigma (a : A) (B a)) : QEquiv \cowith
   | A => p = p'
   | B => \Sigma (s : p.1 = p'.1) (transport B s p.2 = p'.2)
-  | f q => (pmap (\lam p => p.1) q, pmapd (\lam p => B p.1) (\lam p => p.2) q)
+  | f q => (pmap (\lam p => p.1) q, pmapd (\lam p => B p.1) (__.2) q)
   | ret q => SigmaExt B p p' q.1 q.2
-  | ret_f q => Jl (\lam p'' q' => SigmaExt B p p'' (pmap (\lam p => p.1) q') (pmapd (\lam p => B p.1) (\lam p => p.2) q') = q') idp q
+  | ret_f q => Jl (\lam p'' q' => SigmaExt B p p'' (pmap (__.1) q') (pmapd (\lam p => B p.1) (__.2) q') = q') idp q
   | f_sec q =>
     \let t => \case p'.1 \as p'1        , q.1 \as q1 : p.1 = p'1,
                     p'.2 \as p'2 : B p'1, q.2 \as q2 : transport B q1 p.2 = p'2
-              \return pmapd (\lam p => B p.1) (\lam p => p.2) (SigmaExt {A} B p (p'1,p'2) q1 q2) = q2 \with {
+              \return pmapd (\lam p => B p.1) (__.2) (SigmaExt {A} B p (p'1,p'2) q1 q2) = q2 \with {
                 | p'1, idp, p'2, idp => idp
               }
     \in path (\lam i => (q.1, t @ i))
@@ -208,7 +208,7 @@
 -- # Embeddings and surjections
 
 \record Embedding (isEmb : \Pi (a a' : A) -> Retraction (pmap f {a} {a'})) \extends Map {
-  \func pmap-isEquiv {a a' : A} : QEquiv (pmap f {a} {a'}) => pathEquiv (\lam a a' => f a = f a') (\lam {a} {a'} => isEmb a a')
+  \func pmap-isEquiv {a a' : A} : QEquiv (pmap f {a} {a'}) => pathEquiv (f __ = f __) (\lam {a} {a'} => isEmb a a')
 } \where {
   \use \level levelProp {A B : \Type} {f : A -> B} (e e' : Embedding f) : e = e' =>
     path (\lam i => \new Embedding f (\lam a a' => Retraction.levelProp (pmap-isEquiv {e} {a} {a'}) (e.isEmb a a') (e'.isEmb a a') @ i))
@@ -230,7 +230,7 @@
                 }
     \in transQEquiv q s
 
-  \lemma projection {A : \Type} (B : A -> \Prop) : Embedding {\Sigma (a : A) (B a)} (\lam p => p.1) \cowith
+  \lemma projection {A : \Type} (B : A -> \Prop) : Embedding {\Sigma (a : A) (B a)} (__.1) \cowith
     | isEmb p p' => \new Retraction {
       | sec q => SigmaExt B p p' q (Path.inProp _ _)
       | f_sec => idpe
@@ -264,11 +264,11 @@
     | f_sec p => pmap (pmap e2.f) (Retraction.f_sec {e1.isEmb a a'} (Retraction.sec {e2.isEmb (e1.f a) (e1.f a')} p)) *> Retraction.f_sec {e2.isEmb (e1.f a) (e1.f a')} p
   }
 
-\func \infixr 1 >-> (A B : \Type) => Embedding {A} {B}
+\func \infixr 1 >-> => Embedding {__} {__}
 
 \record Surjection (isSurj : \Pi (y : B) -> TruncP (Fib f y)) \extends Map
 
-\func \infixr 1 ->> (A B : \Type) => Surjection {A} {B}
+\func \infixr 1 ->> => Surjection {__} {__}
 
 \record ESEquiv \extends Embedding, Surjection
   \where {
diff --git a/src/Equiv/Fiber.ard b/src/Equiv/Fiber.ard
index de53a8c8..f8eebef9 100644
--- a/src/Equiv/Fiber.ard
+++ b/src/Equiv/Fiber.ard
@@ -34,7 +34,7 @@
   \let sec y => Contr.center {p y}
   \in \new QEquiv {
     | ret y => (sec y).1
-    | ret_f x => pmap (\lam (r : Fib f (f x)) => r.1) (Contr.contraction {p (f x)} (x,idp))
+    | ret_f x => pmap (__.1) (Contr.contraction {p (f x)} (x,idp))
     | f_sec y => (sec y).2
   }
 
@@ -47,7 +47,7 @@
          -- q0 proves that the second compontents are equal: pmap f p0 *> x.basePath = x0.basePath.
          | q0 =>
             pmap e.f p0 *> x.2                                                 ==< pmap (`*> x.2) (pmap_*>-comm e.f _ _) >==
-            (pmap e.f (pmap p.ret (inv x.2)) *> pmap e.f (p.ret_f x.1)) *> x.2 ==< pmap (\lam r => (pmap e.f (pmap p.ret (inv x.2)) *> r) *> x.2) (p.f_ret_f=f_sec_f x.1) >==
+            (pmap e.f (pmap p.ret (inv x.2)) *> pmap e.f (p.ret_f x.1)) *> x.2 ==< pmap ((pmap e.f (pmap p.ret (inv x.2)) *> __) *> x.2) (p.f_ret_f=f_sec_f x.1) >==
             (pmap e.f (pmap p.ret (inv x.2)) *> p.f_sec (e.f x.1)) *> x.2      ==< pmap (`*> x.2) (homotopy-isNatural (\lam x => e.f (p.ret x)) (\lam x => x) p.f_sec (inv x.2)) >==
             (p.f_sec b0 *> inv x.2) *> x.2                                     ==< *>-assoc _ _ _ >==
             p.f_sec b0 *> (inv x.2 *> x.2)                                     ==< pmap (p.f_sec b0 *>) (inv_*> x.2) >==
diff --git a/src/Equiv/HalfAdjoint.ard b/src/Equiv/HalfAdjoint.ard
index d0417dc7..63629941 100644
--- a/src/Equiv/HalfAdjoint.ard
+++ b/src/Equiv/HalfAdjoint.ard
@@ -11,8 +11,8 @@
       | Section => e
       | f_sec y => inv (e.f_sec (e.f (e.ret y))) *> pmap e.f (e.ret_f (e.ret y)) *> e.f_sec y
       | f_ret_f=f_sec_f x => inv (rotatePathLeft (
-        pmap e.f (e.ret_f (e.ret (e.f x))) *> e.f_sec (e.f x)               ==< pmap (\lam r => pmap e.f r *> e.f_sec (e.f x)) (homotopy_app-comm (\lam x => e.ret (e.f x)) e.ret_f x) >==
-        pmap (\lam x => e.f (e.ret (e.f x))) (e.ret_f x) *> e.f_sec (e.f x) ==< homotopy-isNatural (\lam y => e.f (e.sec y)) (\lam y => y) e.f_sec (pmap e.f (e.ret_f x))              >==
+        pmap e.f (e.ret_f (e.ret (e.f x))) *> e.f_sec (e.f x)               ==< pmap (pmap e.f __ *> e.f_sec (e.f x)) (homotopy_app-comm (\lam x => e.ret (e.f x)) e.ret_f x) >==
+        pmap (\lam x => e.f (e.ret (e.f x))) (e.ret_f x) *> e.f_sec (e.f x) ==< homotopy-isNatural (\lam y => e.f (e.sec y)) (\lam y => y) e.f_sec (pmap e.f (e.ret_f x))     >==
         e.f_sec (e.f (e.ret (e.f x))) *> pmap e.f (e.ret_f x)               `qed
       ))
 
diff --git a/src/Equiv/Path.ard b/src/Equiv/Path.ard
index dc7a3360..e0862cdf 100644
--- a/src/Equiv/Path.ard
+++ b/src/Equiv/Path.ard
@@ -13,14 +13,14 @@
   | f_sec => p.f_sec
 
 -- | If ``f : A -> B`` is an equivalence, then ``pmap f`` is also an equivalence.
-\func pmapEquiv (e : Equiv) {a a' : e.A} : QEquiv {a = a'} => pathEquiv (\lam a a' => e.f a = e.f a') (\lam {a} {a'} => \new Retraction {
+\func pmapEquiv (e : Equiv) {a a' : e.A} : QEquiv {a = a'} => pathEquiv (e.f __ = e.f __) (\lam {a} {a'} => \new Retraction {
   | f => pmap e.f
   | sec p => inv (e.ret_f a) *> pmap e.ret p *> e.ret_f a'
   | f_sec p => \let hae : HAEquiv => e \in
     pmap e.f (inv (e.ret_f a) *> pmap e.ret p *> e.ret_f a')                       ==< pmap_*>-comm e.f (inv (e.ret_f a)) (pmap e.ret p *> e.ret_f a') >==
     pmap e.f (inv (e.ret_f a)) *> pmap e.f (pmap e.ret p *> e.ret_f a')            ==< pmap2 (*>) (pmap_inv-comm e.f (e.ret_f a)) (pmap_*>-comm e.f (pmap e.ret p) (e.ret_f a')) >==
     inv (pmap e.f (e.ret_f a)) *> pmap e.f (pmap e.ret p) *> pmap e.f (e.ret_f a') ==< rotatePathLeft (
-        pmap e.f (pmap e.ret p) *> pmap e.f (e.ret_f a') ==< pmap (\lam r => pmap e.f (pmap e.ret p) *> r) (hae.f_ret_f=f_sec_f a') >==
+        pmap e.f (pmap e.ret p) *> pmap e.f (e.ret_f a') ==< pmap (pmap e.f (pmap e.ret p) *> __) (hae.f_ret_f=f_sec_f a') >==
         pmap e.f (pmap e.ret p) *> (hae.f_sec (e.f a'))  ==< homotopy-isNatural (\lam y => e.f (e.ret y)) (\lam y => y) hae.f_sec p >==
         hae.f_sec (e.f a) *> p                           ==< inv (pmap (`*> p) (hae.f_ret_f=f_sec_f a)) >==
         pmap e.f (e.ret_f a) *> p                        `qed) >==
diff --git a/src/Equiv/Sigma.ard b/src/Equiv/Sigma.ard
index 3c826a23..0d7035ba 100644
--- a/src/Equiv/Sigma.ard
+++ b/src/Equiv/Sigma.ard
@@ -30,13 +30,13 @@
 \func pi-contr-left {A : \Type} (a : A) (B : \Pi (a' : A) -> a = a' -> \Type) : QEquiv {\Pi (a' : A) (p : a = a') -> B a' p} {B a idp} \cowith
   | f h => h a idp
   | ret b a' => Jl B b
-  | ret_f h => path (\lam i a' p => Jl (\lam x q => Jl B (h a idp) q = h x q) idp p @ i)
+  | ret_f h => path (\lam i a' => Jl (\lam x q => Jl B (h a idp) q = h x q) idp __ @ i)
   | f_sec => idpe
 
 \func pi-contr-right {A : \Type} (a' : A) (B : \Pi (a : A) -> a = a' -> \Type) : QEquiv {\Pi (a : A) (p : a = a') -> B a p} {B a' idp} \cowith
   | f h => h a' idp
   | ret b a => Jl.Jr B b
-  | ret_f h => path (\lam i a p => Jl.Jr (\lam x q => Jl.Jr B (h a' idp) q = h x q) idp p @ i)
+  | ret_f h => path (\lam i a => Jl.Jr (\lam x q => Jl.Jr B (h a' idp) q = h x q) idp __ @ i)
   | f_sec => idpe
 
 \lemma sigma-left {A A' : \Type} (B' : A' -> \Type) (p : A = A')
diff --git a/src/Equiv/Univalence.ard b/src/Equiv/Univalence.ard
index 3db09a3e..c8dd28c8 100644
--- a/src/Equiv/Univalence.ard
+++ b/src/Equiv/Univalence.ard
@@ -10,7 +10,7 @@
 \func Equiv-to-= {A B : \Type} (e : Equiv {A} {B}) : A = B => QEquiv-to-= (QEquiv.fromEquiv e)
 
 \func univalence {X Y : \Type} : QEquiv {X = Y} {Equiv {X} {Y}}
-  => pathEquiv (\lam X Y => Equiv {X} {Y}) (\lam {A} {B} =>
+  => pathEquiv (Equiv {__} {__}) (\lam {A} {B} =>
       \new Retraction {
         | f => =-to-Equiv
         | sec => Equiv-to-=
diff --git a/src/HLevel.ard b/src/HLevel.ard
index a9bc7972..827dc838 100644
--- a/src/HLevel.ard
+++ b/src/HLevel.ard
@@ -45,7 +45,7 @@
       })
   }
 
-\func isContr=>isProp {A : \Type} (c : Contr A) : isProp A => \lam a a' => inv (c.contraction a) *> c.contraction a'
+\func isContr=>isProp {A : \Type} (c : Contr A) : isProp A => \lam a => inv (c.contraction a) *> c.contraction __
 
 \func isContr'=>isProp {A : \Type} (c : A -> Contr A) : isProp A => \lam a => isContr=>isProp (c a) a
 
@@ -67,7 +67,7 @@
 
 \func isProp=>HLevel_-2+1 (A : \Type) (p : isProp A) (a a' : A) : Contr (a = a') => \new Contr (a = a') {
   | center => inv (p a a) *> p a a'
-  | contraction => Jl (\lam x q => inv (p a a) *> p a x = q) (inv_*> (p a a))
+  | contraction => Jl (inv (p a a) *> p a __ = __) (inv_*> (p a a))
 }
 
 \lemma HLevel_-1=>HLevel_-2+1 (A : \Type) (n : Nat) (p : A ofHLevel_-1+ n) : A ofHLevel_-2+ suc n \elim n
@@ -106,7 +106,7 @@
 -- | hLevels are closed under sigma-types
 \func HLevels-sigma {A : \Type} (B : A -> \Type) {n : Nat} (pA : A ofHLevel_-1+ n) (pB : \Pi (a : A) -> B a ofHLevel_-1+ n) : (\Sigma (a : A) (B a)) ofHLevel_-1+ n \elim n
   | 0 => \lam p p' => SigmaExt B p p' (pA p.1 p'.1) (pB p'.1 _ _)
-  | suc n => \lam p p' => HLevel-retracts (sigmaEquiv B p p') (HLevels-sigma (\lam s => transport B s p.2 = p'.2) (pA p.1 p'.1) (\lam s => pB _ _ _))
+  | suc n => \lam p p' => HLevel-retracts (sigmaEquiv B p p') (HLevels-sigma (transport B __ p.2 = p'.2) (pA p.1 p'.1) (\lam s => pB _ _ _))
 
 -- | hLevels are closed under embeddings
 \func HLevels-embeddings (e : Embedding) {n : Nat} (p : e.B ofHLevel_-1+ n) : e.A ofHLevel_-1+ n \elim n
@@ -130,4 +130,4 @@
   | 0 => \let | a0 => Contr.center {pA}
               | p0 => ((a0, Contr.center {pB a0}) : \Sigma (a : A) (B a))
          \in Contr.make p0 (\lam p => SigmaExt B p0 p (Contr.contraction {pA} p.1) (isContr=>isProp (pB p.1) _ _))
-  | suc n => \lam p p' => HLevel_-2-retracts (sigmaEquiv B p p') (HLevels_-2-sigma (\lam s => transport B s p.2 = p'.2) (pA p.1 p'.1) (\lam s => pB _ _ _))
\ No newline at end of file
+  | suc n => \lam p p' => HLevel_-2-retracts (sigmaEquiv B p p') (HLevels_-2-sigma (transport B __ p.2 = p'.2) (pA p.1 p'.1) (\lam s => pB _ _ _))
\ No newline at end of file
diff --git a/src/Homotopy/Cube.ard b/src/Homotopy/Cube.ard
index acf5e9d7..0901a1bc 100644
--- a/src/Homotopy/Cube.ard
+++ b/src/Homotopy/Cube.ard
@@ -14,13 +14,13 @@
      -}
     \func equality {A : \Type} {a00 a01 a10 a11 : A} (p_0 : a00 = a10) (p_1 : a01 = a11) (p0_ : a00 = a01) (p1_ : a10 = a11)
       : (p_0 = p0_ <* p_1 *> inv p1_) = Cube2 p_0 p_1 p0_ p1_
-      => path (\lam i => Path (\lam j => p0_ @ I.squeeze i j = p1_ @ I.squeeze i j) p_0 (path (\lam j => p0_ @ I.squeezeR i j) <* p_1 *> inv (path (\lam j => p1_ @ I.squeezeR i j))))
+      => path (\lam i => Path (\lam j => p0_ @ I.squeeze i j = p1_ @ I.squeeze i j) p_0 (path (p0_ @ I.squeezeR i __) <* p_1 *> inv (path (p1_ @ I.squeezeR i __))))
 
     {- | This function satisfies the following equality:
      -   ```map p q idp idp r == r```
      -}
     \func map {A : \Type} {a00 a01 a10 a11 : A} (p_0 : a00 = a10) (p_1 : a01 = a11) (p0_ : a00 = a01) (p1_ : a10 = a11) (r : p_0 = p0_ <* p_1 *> inv p1_) : Cube2 p_0 p_1 p0_ p1_
-      => coe (\lam i => equality p_0 p_1 p0_ p1_ @ i) r right
+      => coe (equality p_0 p_1 p0_ p1_ @) r right
   }
 
 \func Cube3 {A : \Type} {v000 v001 v010 v011 v100 v101 v110 v111 : A}
diff --git a/src/Homotopy/Hopf.ard b/src/Homotopy/Hopf.ard
index 96955db4..724859a2 100644
--- a/src/Homotopy/Hopf.ard
+++ b/src/Homotopy/Hopf.ard
@@ -99,9 +99,9 @@
             \let | e : HAEquiv (`* a) => HSpaceConn-right a
                  | p =>
                    pmap totalJoin (ppglue (e.sec a', a) *> pmap (\lam y => pinr ((),y)) (e.f_sec a')) ==< pmap_*>-comm totalJoin (ppglue (e.sec a', a)) (pmap (\lam y => pinr ((),y)) (e.f_sec a')) >==
-                   jglue a (e.sec a' * a) *> pmap jinr (e.f_sec a')                                   ==< Jl (\lam x p => jglue a (e.sec a' * a) *> pmap jinr p = jglue a x) idp (e.f_sec a') >==
+                   jglue a (e.sec a' * a) *> pmap jinr (e.f_sec a')                                   ==< Jl (\lam x => jglue a (e.sec a' * a) *> pmap jinr __ = jglue a x) idp (e.f_sec a') >==
                    jglue a a'                                                                         `qed
-            \in path (\lam j => p @ j @ i)
+            \in path (p @ __ @ i)
 
         \func totalJoinTotal {A : HSpaceConn} (x : total A) : joinTotal (totalJoin x) = x \elim x
           | pinl (_,a) => idp
@@ -113,7 +113,7 @@
                    s *> pmap (\lam y => pinr ((),y)) (e.f_sec (a * a')) ==< pmap (\lam p => s *> pmap (\lam y => pinr ((),y)) p) (inv (e.f_ret_f=f_sec_f a)) >==
                    s *> pmap (\lam y => pinr ((), y * a')) (e.ret_f a)  ==< Jl (\lam x p => s *> pmap (\lam y => pinr ((), y * a')) p = ppglue (x,a')) idp (e.ret_f a) >==
                    ppglue (a,a')                                        `qed
-            \in path (\lam j => p @ j @ i)
+            \in path (p @ __ @ i)
       }
 
 \func hopfS2 (x : Sphere 2) => hopf x
diff --git a/src/Homotopy/Image.ard b/src/Homotopy/Image.ard
index f7b1d9eb..be71d714 100644
--- a/src/Homotopy/Image.ard
+++ b/src/Homotopy/Image.ard
@@ -12,7 +12,7 @@
 \import Paths
 \import Paths.Meta
 
-\func MJoin {A B : \Type} (R : A -> B -> \Type) => PushoutData {\Sigma (x : A) (y : B) (R x y)} (\lam p => p.1) (\lam p => p.2)
+\func MJoin {A B : \Type} (R : A -> B -> \Type) => PushoutData {\Sigma (x : A) (y : B) (R x y)} (__.1) (__.2)
   \where
     \class MData {A : \Type} {B : \Type (\suc \lp)} (f : A -> B) (R : B -> B -> \Type) (ret : \Pi (b b' : B) -> R b b' -> b = b') {
       \func MImageAppr (n : Nat) : \Sigma (X : \hType) (X -> B) \elim n
@@ -82,5 +82,5 @@
     \lemma cod-map-emb {A B : \Type} (S : A -> B -> \Type) : Embedding (cod-map S)
       => MData.cod-map-emb {data S} (\lam {F} b => idEquiv {F b}) (\lam {F} =>
           \let p b : Equiv-to-= (idEquiv {F b}) = idp => univalence.ret_f idp
-          \in path (\lam i => path (\lam j b => p b @ i @ j)))
+          \in path (\lam i => path (\lam j => p __ @ i @ j)))
   }
diff --git a/src/Homotopy/Join.ard b/src/Homotopy/Join.ard
index 4481f3b1..d52ff492 100644
--- a/src/Homotopy/Join.ard
+++ b/src/Homotopy/Join.ard
@@ -9,10 +9,10 @@
 \import Logic
 \import Paths
 
-\func Join (A B : \Type) => PushoutData {\Sigma A B} (\lam p => p.1) (\lam p => p.2)
+\func Join (A B : \Type) => PushoutData {\Sigma A B} (__.1) (__.2)
   \where {
-    \use \level levelProp {A B : \Prop} : isProp (Join A B) => isContr'=>isProp {Join A B} (\lam x => \case x \with {
-      | pinl a => transport (\lam X => Contr X) (QEquiv-to-= (Join-sym B A)) (Join_Contr B (isProp=>isContr Path.inProp a))
+    \use \level levelProp {A B : \Prop} : isProp (Join A B) => isContr'=>isProp {Join A B} (\case __ \with {
+      | pinl a => transport (Contr __) (QEquiv-to-= (Join-sym B A)) (Join_Contr B (isProp=>isContr Path.inProp a))
       | pinr b => Join_Contr A (isProp=>isContr Path.inProp b)
     })
 
@@ -37,7 +37,7 @@
         (pmap jinr (B.contraction b)) -- bottom edge
         (idpe (jinr B.center))        -- left edge
         (jglue a b)                   -- right edge
-        (Jl (\lam x p => inv (jglue a B.center) = pmap jinr p *> inv (jglue a x)) (inv (idp_*> _)) (B.contraction b)) @ i
+        (Jl (\lam x => inv (jglue a B.center) = pmap jinr __ *> inv (jglue a x)) (inv (idp_*> _)) (B.contraction b)) @ i
   }
 
 \func Join_Sphere0 (A : \Type) : QEquiv {Join (Sphere 0) A} {Susp A} \cowith
@@ -82,7 +82,7 @@
           pmap joinSusp (jglue north a *> inv (jglue south a)) ==< pmap_*>-comm joinSusp (jglue north a) (inv (jglue south a)) >==
           pmerid a *> pmap joinSusp (inv (jglue south a))      ==< pmap (pmerid a *>) (pmap_inv-comm joinSusp (jglue south a)) >==
           pmerid a                                             `qed
-        \in path (\lam j => t @ j @ i)
+        \in path (t @ __ @ i)
   }
 
 \func Join-sym (A B : \Type) : QEquiv {Join A B} {Join B A} \cowith
@@ -101,7 +101,7 @@
       | jinr b => idp
       | pglue (a,b) i =>
         \let p => pmap_inv-comm flip (jglue b a) *> inv_inv (jglue a b)
-        \in path (\lam j => p @ j @ i)
+        \in path (p @ __ @ i)
   }
 
 \func Join-assoc (A B C : \Type) : QEquiv {Join (Join A B) C} {Join A (Join B C)} \cowith
@@ -174,7 +174,7 @@
                      (path (\lam j => path (\lam i => jinl (pglue (a,b) (squeeze (squeezeR j i) n)))))
                      right
                  = path (\lam j => path (\lam i => pglue (pglue (a,b) (squeeze j n), c) i))
-               ) (Jl (\lam y q => Jl.def (\lam x p => Cube2 p p idp idp) idp q = idp) idp (jglue (jinl a) c)) right
+               ) (Jl (\lam y => Jl.def (\lam x p => Cube2 p p idp idp) idp __ = idp) idp (jglue (jinl a) c)) right
         \in path (\lam k => (Jl (\lam y q => s1 q = s2 q) idp (jglue b c) *> proof) @ k @ j @ i)
 
     \func rightLeftRight {A B C : \Type} (j : Join A (Join B C)) : leftToRight (rightToLeft j) = j
@@ -219,7 +219,7 @@
                         idp
                         (jglue a (jinl b)))
                     (jglue b c)
-        \in path (\lam k => (Jl (\lam y q => s1 q = s2 q) idp (jglue a b) *> proof) @ k @ j @ i)
+        \in path ((Jl (\lam y q => s1 q = s2 q) idp (jglue a b) *> proof) @ __ @ j @ i)
   }
 
 \func Join_Susp (A B : \Type) : Join (Susp A) B = Susp (Join A B) =>
diff --git a/src/Homotopy/Localization/Accessible.ard b/src/Homotopy/Localization/Accessible.ard
index 3c6fe799..cdb53ed0 100644
--- a/src/Homotopy/Localization/Accessible.ard
+++ b/src/Homotopy/Localization/Accessible.ard
@@ -21,7 +21,7 @@
             | ret_f g =>
               \let p s => path (isExt {famHat} {A} {inr j} (rec (ext {famHat} {A} {inl j} (g `o` F j)) g (\lam x => path (isExt {famHat} {A} {inl j} (g `o` F j) x))) s)
               \in path (\lam i y => (inv (p (pinl y)) *> p (pinr y)) @ i)
-            | f_sec f => path (\lam i x => isExt {famHat} {A} {inl j} f x i)
+            | f_sec f => path (\lam i => isExt {famHat} {A} {inl j} f __ i)
           }
     }
     | inL => alpha {famHat}
@@ -61,18 +61,18 @@
       | alpha a => K a
       | ext {j} f y =>
         \let p x => path (\lam i => H1 (isExt f x i)) <* dataExt-unique H1 H2 K (f x) *> inv (path (\lam i => H2 (isExt f x i)))
-        \in path (\lam i => (Equiv.sec {pmapEquiv (Z.local j) {H1 `o` ext f} {H2 `o` ext f}} (path (\lam i' x => p x @ i')) @ i) y)
+        \in path (\lam i => (Equiv.sec {pmapEquiv (Z.local j) {H1 `o` ext f} {H2 `o` ext f}} (path (\lam i' => p __ @ i')) @ i) y)
       | isExt {j} f x i =>
         \let | p x => path (\lam i => H1 (isExt f x i)) <* dataExt-unique H1 H2 K (f x) *> inv (path (\lam i => H2 (isExt f x i)))
              | e : Equiv {H1 `o` ext f = H2 `o` ext f} => pmapEquiv (Z.local j)
              | q => path (\lam i => (e.sec (path (\lam i' x => p x @ i')) @ i) (F j x))
-             | s : q = p x => path (\lam k => path (\lam i => (e.f_sec (path (\lam i' x => p x @ i')) @ k @ i) x))
+             | s : q = p x => path (\lam k => path (\lam i => (e.f_sec (path (\lam i' => p __ @ i')) @ k @ i) x))
         \in Cube2.map q (dataExt-unique H1 H2 K (f x)) (path (\lam i' => H1 (isExt f x i'))) (path (\lam i' => H2 (isExt f x i'))) s @ i
 
     \lemma alpha-equiv {fam : Family} {A : \Type} {Z : Local} : Equiv {LData A -> Z} {A -> Z} (-o alpha) =>
       \new QEquiv {
         | ret => dataExt
-        | ret_f h => path (\lam i d => dataExt-unique (dataExt (h `o` alpha)) h (\lam _ => idp) d @ i)
+        | ret_f h => path (\lam i => dataExt-unique (dataExt (h `o` alpha)) h (\lam _ => idp) __ @ i)
         | f_sec _ => idp
       }
 
diff --git a/src/Homotopy/Localization/BlakersMassey.ard b/src/Homotopy/Localization/BlakersMassey.ard
index f913995f..2d66855d 100644
--- a/src/Homotopy/Localization/BlakersMassey.ard
+++ b/src/Homotopy/Localization/BlakersMassey.ard
@@ -66,9 +66,9 @@
       | Y : \hType
       | Q : X -> Y -> \hType
 
-      \func PO => PushoutData {\Sigma (x : X) (y : Y) (Q x y)} (\lam p => p.1) (\lam p => p.2)
+      \func PO => PushoutData {\Sigma (x : X) (y : Y) (Q x y)} (__.1) (__.2)
 
-      \func swap (x : PO) : PushoutData {\Sigma (y : Y) (x : X) (Q x y)} (\lam p => p.1) (\lam p => p.2)
+      \func swap (x : PO) : PushoutData {\Sigma (y : Y) (x : X) (Q x y)} (__.1) (__.2)
         | pinl b => pinr b
         | pinr c => pinl c
         | pglue (x,y,q) i => pglue (y,x,q) (inv (path (\lam j => j)) @ i)
@@ -83,8 +83,7 @@
                           | f => pinr
                           | g => Embedding.projection (\lam y => TruncP (\Sigma (x : X) (Q x y)))
                         }
-                | t => Equiv.ret {EmbeddingPushout.pullback-path-equiv {EP} (pinl x) y} (pmap (\lam w =>
-                        \case w \with {
+                | t => Equiv.ret {EmbeddingPushout.pullback-path-equiv {EP} (pinl x) y} (pmap (\case __ \with {
                            | pinl x => pinl (pinl x)
                            | pinr y => pinr y
                            | pglue (x,y,q) i =>
@@ -231,6 +230,6 @@
       \lemma code-contr {w : PO} (p : pinl x0 = w) : Contr (code p) \cowith
         | center => code-center p
         | contraction => transport (\lam t => \Pi (c : code t.2) -> code-center t.2 = c) (isContr=>isProp (lsigma {PO} (pinl x0)) (pinr y0, pbMap q0) (w, p))
-                                   (\lam c => remove_inL (\lam _ => code-center (pbMap q0)) (\lam c => c) (code-path (pbMap q0)) c)
+                                   (remove_inL (\lam _ => code-center (pbMap q0)) (\lam c => c) (code-path (pbMap q0)))
     }
   }
diff --git a/src/Homotopy/Localization/Connected.ard b/src/Homotopy/Localization/Connected.ard
index 9aca5531..12584a49 100644
--- a/src/Homotopy/Localization/Connected.ard
+++ b/src/Homotopy/Localization/Connected.ard
@@ -21,7 +21,7 @@
   \let c' : Equiv (\lam z _ => z) => propExt.dir (nullTypeUniverse.localDesc X (LType X)) (c (LType X))
   \in \new Contr {
     | center => c'.sec lEta
-    | contraction => remove_inL (\lam _ => c'.sec lEta) (\lam x => x) (\lam a => path (\lam i => (c'.f_sec lEta @ i) a))
+    | contraction => remove_inL (\lam _ => c'.sec lEta) (\lam x => x) (path (\lam i => (c'.f_sec lEta @ i)) __)
   }
 
 -- | If the localization of a type {X} is contractible, then {X} is connected
@@ -53,7 +53,7 @@
               | eq1 => transEquiv (symQEquiv (contr-right (\lam b => lsigma (\lam _ => b))))
                                   (\new QEquiv {\Sigma (b : B) (\Sigma (f : A' -> B) ((\lam _ => b) = f))} {\Sigma (f : A' -> B) (C f)} {
                                     | f p => (p.2.1, (p.1, \lam a => path (\lam i => (p.2.2 @ i) a)))
-                                    | ret p => (p.2.1, (p.1, path (\lam i a => p.2.2 a @ i)))
+                                    | ret p => (p.2.1, (p.1, path (\lam i => p.2.2 __ @ i)))
                                     | ret_f => idpe
                                     | f_sec => idpe
                                   })
diff --git a/src/Homotopy/Localization/Equiv.ard b/src/Homotopy/Localization/Equiv.ard
index e4b9bfa5..f45f375e 100644
--- a/src/Homotopy/Localization/Equiv.ard
+++ b/src/Homotopy/Localization/Equiv.ard
@@ -46,7 +46,7 @@
 
 -- | A map between local types is a local equivalence if and only if it is an equivalence
 \lemma localTypesEquiv {U : Universe} {A B : Local} (f : A -> B) : isLocalEquiv f = Equiv f
-  => propExt (dir f) (\lam (e : Equiv f) C => -o_Equiv {C} e)
+  => propExt (dir f) (\lam (e : Equiv f) => -o_Equiv {__} e)
   \where {
     -- | A local equivalence between local types is an equivalence
     \lemma dir {U : Universe} {A B : Local} (f : A -> B) (p : isLocalEquiv f) : Equiv f
@@ -56,11 +56,11 @@
          \in \new QEquiv {
                | ret => g
                | ret_f a => path (\lam i => (g_f @ i) a)
-               | f_sec b => path (\lam i => ((
+               | f_sec b => path (((
                    f `o` g           ==< inv (Equiv.ret_f {p B} (f `o` g)) >==
                    H (f `o` g `o` f) ==< pmap (\lam t => H (f `o` t)) g_f >==
                    H f               ==< Equiv.ret_f {p B} id >==
-                   id                `qed) @ i) b)
+                   id                `qed) @ __) b)
              }
   }
 
diff --git a/src/Homotopy/Localization/Modality.ard b/src/Homotopy/Localization/Modality.ard
index 84dae980..863277fd 100644
--- a/src/Homotopy/Localization/Modality.ard
+++ b/src/Homotopy/Localization/Modality.ard
@@ -7,4 +7,4 @@
 -- | An elimination principle for the localization in a modality.
 \lemma modality-elim {U : Modality} {A : \Type} (B : LType A -> Local)
   : Equiv {\Pi (x : LType A) -> B x} {\Pi (a : A) -> B (lEta a)} (\lam f a => f (lEta a))
-  => universe-elim (\lam x => B x) (isModality (LType A) B)
+  => universe-elim (B __) (isModality (LType A) B)
diff --git a/src/Homotopy/Localization/Separated.ard b/src/Homotopy/Localization/Separated.ard
index b5d9f586..363a6631 100644
--- a/src/Homotopy/Localization/Separated.ard
+++ b/src/Homotopy/Localization/Separated.ard
@@ -15,7 +15,7 @@
 \func ReflSeparated (U : ReflUniverse \lp \oo) : ReflUniverse \cowith
   | Universe => Separated U
   | localization A =>
-    \let | p (a a' : A) : Local (F a = F a') => transport (\lam X => Local X) (inv (pathEquiv a a')) (LType (a = a'))
+    \let | p (a a' : A) : Local (F a = F a') => transport (Local __) (inv (pathEquiv a a')) (LType (a = a'))
          | q (a a' : A) : LType (a = a') = {\hType \lp} (F a = F a') => inv (pathEquiv a a')
          | r (a a' : A) : Localization (a = a') (p a a') =>
              coe (\lam i => Localization (a = a') (\new Local (q a a' @ i) (pathInProp (\lam j => isLocal (q a a' @ j)) (local {LType (a = a')}) (local {p a a'}) @ i)))
@@ -48,8 +48,8 @@
                 \case f.isSurj b, f.isSurj b' \with {
                   | inP (a,q), inP (a',q') => transport2 (\lam x x' => isLocal (x = x')) q q' (local {(p a a').1})
                 }
-         \in (\new Local { | local => B-local }, \new Localization { | local-univ C => Extension.contr-equiv f.f (\lam g b =>
-            \case f.isSurj b \with {
+         \in (\new Local { | local => B-local }, \new Localization { | local-univ C => Extension.contr-equiv f.f (\lam g =>
+            \case f.isSurj __ \with {
               | inP (a',q) => rewrite1 q (coe (\lam i => Contr (\Sigma (c : C) (\Pi (a : f.A) -> inv (Equiv-to-= (local-univ {(p a a').2} (\new Local (g a = c) (local {C} (g a) c)))) @ i)))
                                              (coe (\lam i => Contr (\Sigma (c : C) (inv (QEquiv-to-= (pi-contr-right a' (\lam x _ => g x = c))) @ i))) (lsigma (g a')) right) right)
             }) })
diff --git a/src/Homotopy/Localization/Universe.ard b/src/Homotopy/Localization/Universe.ard
index 620172ab..88aa8bf9 100644
--- a/src/Homotopy/Localization/Universe.ard
+++ b/src/Homotopy/Localization/Universe.ard
@@ -30,10 +30,10 @@
   \func lift-prop {Z : Local {U}} (f : S -> Z) (x : S) : lift f (inL x) = f x => path (\lam i => (Equiv.f_sec {local-univ Z} f @ i) x)
 
   \func remove_inL {Z : Local {U}} (f g : S' -> Z) (p : \Pi (x : S) -> f (inL x) = g (inL x)) (x : S') : f x = g x
-    => path (\lam i => (Equiv.sec {pmapEquiv (local-univ Z) {f} {g}} (path (\lam i x => p x @ i)) @ i) x)
+    => path (\lam i => (Equiv.sec {pmapEquiv (local-univ Z) {f} {g}} (path (\lam i => p __ @ i)) @ i) x)
 
   \func remove_inL-coh {Z : Local {U}} (f g : S' -> Z) (p : \Pi (x : S) -> f (inL x) = g (inL x)) (x : S) : remove_inL f g p (inL x) = p x
-    => \let t => Equiv.f_sec {pmapEquiv (local-univ Z) {f} {g}} (path (\lam i x => p x @ i))
+    => \let t => Equiv.f_sec {pmapEquiv (local-univ Z) {f} {g}} (path (\lam i => p __ @ i))
        \in pmap (\lam q => path (\lam i => (q @ i) x)) t
 } \where {
   \use \level levelProp {U : Universe} (X : \Type) (l1 l2 : Localization X) : l1 = l2
@@ -50,7 +50,7 @@
             | p2 i => local {pathInProp (\lam j => Local (p1 @ j)) l1.S' l2.S' @ i}
             | q1 : l1.S' = {Local} l2.S' => path (\lam i => \new Local (p1 @ i) (p2 i))
             | q2 x => transport_pi {Local} (\lam _ => X) (\lam Y => Y) q1 l1.inL x *> lift-prop l2.inL x
-            | q2' i => pathOver (path (\lam j x => q2 x @ j)) @ i
+            | q2' i => pathOver (path (\lam j => q2 __ @ j)) @ i
        \in path (\lam i => \new Localization X (q1 @ i) (q2' i) (local-univ {pathInProp (\lam j => Localization X (q1 @ j) (q2' j)) l1 l2 @ i}))
 }
 
@@ -222,7 +222,7 @@
        | F (t : T) => (t.2.1 `o` t.1, t.1 `o` t.2.2)
   \in \new Local { | local =>
     transport isLocal (inv (QEquiv-to-= (\new QEquiv {Equiv {A} {B}} {\Sigma (t : T) (\Sigma) (F t = (id,id))} {
-      | f (e : Equiv) => ((e.f,(e.ret,e.sec)), (), path (\lam i => (\lam a => e.ret_f a @ i, \lam b => e.f_sec b @ i)))
+      | f (e : Equiv) => ((e.f,(e.ret,e.sec)), (), path (\lam i => (e.ret_f __ @ i, e.f_sec __ @ i)))
       | ret p => \new Equiv {
         | f => p.1.1
         | ret => p.1.2.1
diff --git a/src/Homotopy/Loop.ard b/src/Homotopy/Loop.ard
index 2cc2bf61..c7bd2413 100644
--- a/src/Homotopy/Loop.ard
+++ b/src/Homotopy/Loop.ard
@@ -18,14 +18,14 @@
                   (n : Nat)
                   (p : \Pi (x0 : X) -> (x0 = x0) ofHLevel_-1+ n)
   : X ofHLevel_-1+ suc n
-  => \lam x x' => hLevel-inh n (\lam q => rewrite1 q (p x))
+  => \lam x x' => hLevel-inh n (rewrite1 __ (p x))
 
 \lemma loop-level-iter {X : \Type}
                        (n : Nat)
                        (c : \Pi (x0 : X) -> Contr (iterl Loop n (\new Pointed X x0)))
   : X ofHLevel_-1+ n \elim n
   | 0 => isContr'=>isProp c
-  | suc n => \lam x x' => loop-level-iter n (\lam x=x' => Jl (\lam x'' x=x'' => Contr (iterl Loop n (\new Pointed (x = x'') x=x''))) (c x) x=x')
+  | suc n => \lam x x' => loop-level-iter n (Jl (\lam x'' x=x'' => Contr (iterl Loop n (\new Pointed (x = x'') x=x''))) (c x))
 
 \lemma loop-level-iter-inv {X : \Type} (n : Nat) (h : X ofHLevel_-1+ n) (x0 : X)
   : Contr (iterl Loop n (\new Pointed X x0)) \elim n
diff --git a/src/Homotopy/Pointed.ard b/src/Homotopy/Pointed.ard
index 535731b3..3e1416d5 100644
--- a/src/Homotopy/Pointed.ard
+++ b/src/Homotopy/Pointed.ard
@@ -15,8 +15,8 @@
 \func \infixr 1 ->* (A B : Pointed) => \Sigma (f : A -> B) (f base = base)
   \where {
     \func ext {A B : Pointed} {f g : A ->* B} (p : \Pi (x : A) -> f.1 x = g.1 x) (q : p base *> g.2 = f.2) : f = g =>
-      \let | p' => path (\lam i x => p x @ i)
-           | q' => Jl (\lam _ p'' => rewriteF p'' f.2 = inv (pmap (\lam (h : A -> B) => h base) p'') *> f.2)
+      \let | p' => path (\lam i => p __ @ i)
+           | q' => Jl (\lam _ p'' => rewriteF p'' f.2 = inv (pmap (__ base) p'') *> f.2)
                       (inv (idp_*> _)) p' *> rotatePathLeft (inv q)
       \in path (\lam i => (p' @ i, pathOver q' @ i))
   }
diff --git a/src/Homotopy/Pushout.ard b/src/Homotopy/Pushout.ard
index 93d0c5ad..f6b5bdf3 100644
--- a/src/Homotopy/Pushout.ard
+++ b/src/Homotopy/Pushout.ard
@@ -179,7 +179,7 @@
 
   \lemma equiv (b0 : B) (a : A) : Equiv {b0 = f a} {\Sigma (a' : A) (b0 = f a') (g.f a = g.f a')} (\lam p => (a, p, idp)) =>
     (b0 = f a)                                                    ~~< symQEquiv (contr-left (lsigma a) (\lam p => b0 = f p.1)) >~~
-    (\Sigma (p : \Sigma (a' : A) (a = a')) (b0 = f p.1))          ~~< sigma-left (\lam p => b0 = f p.1) (Equiv-to-= (sigma-right (a =) (\lam a' => g.f a = g.f a') (\lam a' => Embedding.pmap-isEquiv {g} {a} {a'}))) >~~
+    (\Sigma (p : \Sigma (a' : A) (a = a')) (b0 = f p.1))          ~~< sigma-left (\lam p => b0 = f p.1) (Equiv-to-= (sigma-right (a =) (g.f a = g.f __) (Embedding.pmap-isEquiv {g} {a} {__}))) >~~
     (\Sigma (p : \Sigma (a' : A) (g.f a = g.f a')) (b0 = f p.1))  ~~< \new QEquiv { | B => \Sigma (a' : A) (b0 = f a') (g.f a = g.f a') | f p => (p.1.1, p.2, p.1.2) | ret q => ((q.1,q.3),q.2) | ret_f => idpe | f_sec => idpe } >~~
     (\Sigma (a' : A) (b0 = f a') (g.f a = g.f a'))                `eqed
     \where \open Equiv.Reasoning
diff --git a/src/Homotopy/Sphere/Circle.ard b/src/Homotopy/Sphere/Circle.ard
index c0816dbd..bd5885cf 100644
--- a/src/Homotopy/Sphere/Circle.ard
+++ b/src/Homotopy/Sphere/Circle.ard
@@ -48,7 +48,7 @@
     \func SuspCircleSusp (x : Sphere 1) : CircleSusp (SuspCircle x) = x
       | north => idp
       | south => pmerid south
-      | pglue north i => path (\lam j => Cube2.map (pmerid north *> inv (pmerid south)) (pmerid north) idp (pmerid south) idp @ j @ i)
+      | pglue north i => path (Cube2.map (pmerid north *> inv (pmerid south)) (pmerid north) idp (pmerid south) idp @ __ @ i)
       | pglue south i => path (\lam j => pglue south (I.squeeze i j))
       | pglue (pglue () _) _
   }
@@ -66,7 +66,7 @@
 
 \func decode (x : Sphere1) : code x -> base1 = x \elim x
   | base1 => wind
-  | loop i => pathOver (path (\lam j x => decode_loop x @ j)) @ i
+  | loop i => pathOver (path (\lam j => decode_loop __ @ j)) @ i
   \where {
     \func wind_loop (n : Int) : wind n *> path loop = wind (isuc n)
       | pos _ => idp
diff --git a/src/Homotopy/Truncation.ard b/src/Homotopy/Truncation.ard
index 29212062..7f8de40c 100644
--- a/src/Homotopy/Truncation.ard
+++ b/src/Homotopy/Truncation.ard
@@ -54,7 +54,7 @@
                               (\lam p => ->*.ext {Sphere.pointed n}
                                                  {Pointed.make t}
                                                  (\lam s => inv p.2 *> path (spokeT p.1 north) *> inv (path (spokeT p.1 s)))
-                                                 (pmap (\lam t => (inv p.2 *> t) *> p.2) (*>_inv (path (spokeT p.1 north))) *> inv_*> p.2))))
+                                                 (pmap ((inv p.2 *> __) *> p.2) (*>_inv (path (spokeT p.1 north))) *> inv_*> p.2))))
 
     \func elim {n : Nat} {A : \hType}
                (P : Trunc_-1+ n A -> Truncated_-1+ n)
@@ -80,10 +80,10 @@
 
     \func equality {n : Nat} {A : \hType} (a a' : A) : QEquiv {inT a = {Trunc_-1+ (suc n) A} inT a'} {Trunc_-1+ n (a = a')} =>
       \let | code => elim2 (\lam _ _ => truncatedTypesLevel n) (\lam a a' => level n (a = a'))
-           | encode (x y : Trunc_-1+ (suc n) A) (p : x = y) => transport (\lam y => code x y) p (elim (\lam x => Truncated_-1+.up (code x x)) (\lam a => inT idp) x)
+           | encode (x y : Trunc_-1+ (suc n) A) (p : x = y) => transport (code x __) p (elim (\lam x => Truncated_-1+.up (code x x)) (\lam a => inT idp) x)
            | decode => elim2 (\lam x y => Truncated_-1+.up (\new Truncated_-1+ n (code x y -> x = y) (HLevels-pi (\lam _ => x = y) (\lam _ => isTruncated {level (suc n) A} x y))))
                              (\lam a a' => elim (\lam _ => \new Truncated_-1+ n (inT a = inT a') (isTruncated {level (suc n) A} (inT a) (inT a'))) (pmap inT))
-      \in pathEquiv (\lam x y => code x y) (\lam {x} {y} => \new Retraction {
+      \in pathEquiv (code __ __) (\lam {x} {y} => \new Retraction {
         | f => encode x y
         | sec => decode x y
         | f_sec => elim2 (\lam x y => Truncated_-1+.up (\new Truncated_-1+ n (\Pi (c : code x y) -> encode x y (decode x y c) = c)
@@ -93,8 +93,8 @@
                          (\lam a a' => elim (\lam c => \new Truncated_-1+ n (encode (inT a) (inT a') (decode (inT a) (inT a') c) = c)
                                                                             (isTruncated {Truncated_-1+.up (level n (a = a'))}
                                                                                          (encode (inT a) (inT a') (decode (inT a) (inT a') c)) c))
-                                            (Jl (\lam _ p => transport (\lam y => elim2 (\lam _ _ => truncatedTypesLevel n)
-                                                                                        (\lam a a' => level n (a = a')) (inT a) y)
+                                            (Jl (\lam _ p => transport (elim2 (\lam _ _ => truncatedTypesLevel n)
+                                                                              (\lam a a' => level n (a = a')) (inT a) __)
                                                                        (pmap inT p)
                                                                        (inT idp) = inT p) idp)) x y
       }) {inT a} {inT a'}
diff --git a/src/Order/LinearOrder.ard b/src/Order/LinearOrder.ard
index 02cdafee..c06ded93 100644
--- a/src/Order/LinearOrder.ard
+++ b/src/Order/LinearOrder.ard
@@ -35,7 +35,7 @@
   \lemma total-distrib {E : Lattice} (totality : \Pi (x y : E) -> x <= y || y <= x) (x y z : E) : meet x (join y z) = join (meet x y) (meet x z) =>
     \case totality y z \with {
       | byLeft y<=z => distrib-x-y totality x y z y<=z
-      | byRight z<=y => transport2 (\lam lj rj => meet x lj = rj) (join-comm z y) (join-comm (meet x z) (meet x y)) (distrib-x-y totality x z y z<=y)
+      | byRight z<=y => transport2 (meet x __ = __) (join-comm z y) (join-comm (meet x z) (meet x y)) (distrib-x-y totality x z y z<=y)
     } \where {
     \lemma distrib-x-y {E : Lattice} (totality : \Pi (x y : E) -> x <= y || y <= x)
                        (x y z : E) (y<=z : y <= z) : meet x (join y z) = join (meet x y) (meet x z) =>
diff --git a/src/Order/PartialOrder.ard b/src/Order/PartialOrder.ard
index 73bea447..ef2639dc 100644
--- a/src/Order/PartialOrder.ard
+++ b/src/Order/PartialOrder.ard
@@ -35,8 +35,8 @@
   \where {
     \func \infix 4 <=C (x y : PreorderC) : \Prop \elim x, y
       | in~ x, in~ y => x <= y
-      | ~-equiv x x' x~x' i, in~ y => propExt (\lam x<=y => <=-transitive x' x y x~x'.2 x<=y) (\lam x'<=y => <=-transitive x x' y x~x'.1 x'<=y) @ i
-      | in~ x, ~-equiv y y' y~y' i => propExt (\lam x<=y => <=-transitive x y y' x<=y y~y'.1) (\lam x<=y' => <=-transitive x y' y x<=y' y~y'.2) @ i
+      | ~-equiv x x' x~x' i, in~ y => propExt (<=-transitive x' x y x~x'.2 __) (<=-transitive x x' y x~x'.1 __) @ i
+      | in~ x, ~-equiv y y' y~y' i => propExt (<=-transitive x y y' __ y~y'.1) (<=-transitive x y' y __ y~y'.2) @ i
 
     \lemma <=C-reflexive {x : PreorderC} : x <=C x \elim x
       | in~ x => <=-reflexive x
diff --git a/src/Paths.ard b/src/Paths.ard
index 01b003fe..2a3eaf4e 100644
--- a/src/Paths.ard
+++ b/src/Paths.ard
@@ -26,7 +26,7 @@
     \func concat {A : I -> \Type} {a a' : A left} {a'' : A right} (p : a = a') (q : Path A a' a'') : Path A a a'' \elim p
       | idp => q
 
-\func psqueeze {A : \Type} {a a' : A} (p : a = a') (i : I) : a = p @ i => path (\lam j => p @ I.squeeze i j)
+\func psqueeze {A : \Type} {a a' : A} (p : a = a') (i : I) : a = p @ i => path (p @ I.squeeze i __)
 
 \func Jl {A : \Type} {a : A} (B : \Pi (a' : A) -> a = a' -> \Type) (b : B a idp) {a' : A} (p : a = a') : B a' p \elim p
   | idp => b
@@ -134,7 +134,7 @@
 
 \func transport_pi2 {A : \Type} (B C : A -> \Type) {a a' : A} (p : a = a') (f : B a -> C a) (g : B a' -> C a') (t : \Pi (x : B a) -> transport C p (f x) = g (transport B p x))
   : transport (\lam y => B y -> C y) p f = g \elim p
-  | idp => path (\lam i x => t x @ i)
+  | idp => path (\lam i => t __ @ i)
 
 \func transport_path-right {A : \Type} {a0 a b : A} (p : a = b) (q : a0 = a)
   : transport (a0 =) p q = q *> p
@@ -157,7 +157,7 @@
   | idp => inv (gf b)
 
 \func funExt {A : \Type} (B : A -> \Type) (f g : \Pi (x : A) -> (B x)) (h : \Pi (x : A) -> (f x = g x)) : f = g =>
-  path (\lam i a => h a @ i)
+  path (\lam i => h __ @ i)
 
 \func SigmaExt {A : \Type} (B : A -> \Type) (x y : \Sigma (a : A) (B a)) (p : x.1 = y.1) (q : transport B p x.2 = y.2) : x = y =>
   path (\lam i => (p @ i, pathOver q @ i))
diff --git a/src/Set.ard b/src/Set.ard
index b260ebca..c8a7b0bc 100644
--- a/src/Set.ard
+++ b/src/Set.ard
@@ -74,4 +74,4 @@
   \in transport isProp (inv (univalence.ret equiv)) Path.inProp
   \where
     \func propPathEquiv {A : \Type} (R : A -> A -> \Prop) (refl : \Pi (a : A) -> R a a) (p : \Pi {a a' : A} -> R a a' -> a = a') {a a' : A} : QEquiv {a = a'} {R a a'}
-      => pathEquiv R (\lam {a} {a'} => \new Retraction (\lam q => transport (R a) q (refl a)) p (\lam _ => Path.inProp _ _))
+      => pathEquiv R (\lam {a} {a'} => \new Retraction (transport (R a) __ (refl a)) p (\lam _ => Path.inProp _ _))