Use partially applied syntax extensively

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

src/Data/SeqColimit.ard

@@ -109,7 +109,7 @@
                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

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 ((z.2 @ __) 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 ((z.2 @ __) x)))
                    idpe
                    idpe)
@@ -159,7 +159,7 @@
   | A => f = f'
   | B => \Pi (a : A) -> f a = f' a
   | f p a => path ((p @ __) a)
-  | ret g => path (\lam i a => g a @ i)
+  | ret g => path (\lam i => g __ @ i)
   | ret_f _ => idp
   | f_sec _ => idp
 
@@ -254,11 +254,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 {

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
   }
 

src/Equiv/HalfAdjoint.ard

@@ -12,7 +12,7 @@
       | 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 (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))              >==
+        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
       ))
 

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')

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 __
 
 \lemma 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

src/Homotopy/Hopf.ard

@@ -99,7 +99,7 @@
             \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 (p @ __ @ i)
 

src/Homotopy/Image.ard

@@ -82,5 +82,5 @@
     \lemma cod-map-emb {A B : \Type} (S : A -> B -> \Type) : Embedding (cod-map S)
       => MData.cod-map-emb (\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)))
   }

src/Homotopy/Join.ard

@@ -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
@@ -174,7 +174,7 @@
                      (path (\lam j => path (\lam i => jinl (pglue (a,b) (squeeze (squeezeR j i) n)))))
                      right
                  = path (\lam j => path (pglue (pglue (a,b) (squeeze j n), c)))
-               ) (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 ((Jl (\lam y q => s1 q = s2 q) idp (jglue b c) *> proof) @ __ @ j @ i)
 
     \func rightLeftRight {A B C : \Type} (j : Join A (Join B C)) : leftToRight (rightToLeft j) = j

src/Homotopy/Localization/Accessible.ard

@@ -22,7 +22,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}
@@ -62,18 +62,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
       }
 

src/Homotopy/Localization/BlakersMassey.ard

@@ -231,6 +231,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)))
     }
   }

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 ((g_f @ __) 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)
              }
   }
 

src/Homotopy/Localization/Separated.ard

@@ -49,8 +49,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) => later rewriteI 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)
             }) })

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 ((q @ __) 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}))
 }
 

src/Homotopy/Loop.ard

@@ -26,7 +26,7 @@
                        (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

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))
   }

src/Homotopy/Sphere/Circle.ard

@@ -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

src/Paths.ard

@@ -1,3 +1,5 @@
+\import Function
+
 \func idpe {A : \Type} (a : A) : a = a => idp
 
 \func pmap {A B : \Type} (f : A -> B) {a a' : A} (p : a = a') : f a = f a' => path (\lam i => f (p @ i))
@@ -114,7 +116,7 @@
 \func homotopy_app-comm {A : \Type} (f : A -> A) (h : \Pi (a : A) -> f a = a) (a : A) : h (f a) = pmap f (h a) =>
   h (f a)                             ==< pmap (h (f a) *>) (inv (*>_inv (h a))) >==
   h (f a) *> (h a *> inv (h a))       ==< inv (*>-assoc (h (f a)) (h a) (inv (h a))) >==
-  (h (f a) *> h a) *> inv (h a)       ==< pmap (`*> inv (h a)) (inv (homotopy-isNatural f (\lam a => a) h (h a))) >==
+  (h (f a) *> h a) *> inv (h a)       ==< pmap (`*> inv (h a)) (inv (homotopy-isNatural f id h (h a))) >==
   (pmap f (h a) *> h a) *> inv (h a)  ==< *>-assoc (pmap f (h a)) (h a) (inv (h a)) >==
   pmap f (h a) *> (h a *> inv (h a))  ==< pmap (pmap f (h a) *>) (*>_inv (h a)) >==
   pmap f (h a)                        `qed
@@ -137,7 +139,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
@@ -160,7 +162,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))