diff --git a/.github/workflows/ghc.yml b/.github/workflows/ghc.yml
index 6f03698e3..5fac24356 100644
--- a/.github/workflows/ghc.yml
+++ b/.github/workflows/ghc.yml
@@ -36,14 +36,14 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [ubuntu-latest, windows-latest, macos-latest]
+        os: [ubuntu-latest, windows-latest, macos-12]
 
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: 🧰 Setup Stack
-        uses: freckle/stack-action@v4
+        uses: freckle/stack-action@v5
 
       - name: Tar and strip the binary
         run: |
@@ -53,7 +53,7 @@ jobs:
         shell: bash
 
       - name: Upload rzk binary as Artifact
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           path: rzk-bin.tar.gz
           name: rzk-${{ runner.os }}-${{ runner.arch }}.tar.gz
@@ -67,10 +67,10 @@ jobs:
 
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: 🧰 Setup Stack
-        uses: freckle/stack-action@v4
+        uses: freckle/stack-action@v5
 
       - name: 🔨 Build Haddock Documentation (with Stack)
         run: |
@@ -93,11 +93,11 @@ jobs:
 
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: 📥 Download rzk
         id: download
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
           name: rzk-${{ runner.os }}-${{ runner.arch }}.tar.gz
 
diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml
index b45b88c16..768726e25 100644
--- a/.github/workflows/ghcjs.yml
+++ b/.github/workflows/ghcjs.yml
@@ -35,7 +35,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: ❄️ Install Nix
-        uses: nixbuild/nix-quick-install-action@v25
+        uses: nixbuild/nix-quick-install-action@v27
         with:
           nix_conf: |
             substituters = https://cache.nixos.org/ https://cache.iog.io https://nix-community.cachix.org https://miso-haskell.cachix.org
diff --git a/.github/workflows/mkdocs.yml b/.github/workflows/mkdocs.yml
index 21e6a7176..79a027b6e 100644
--- a/.github/workflows/mkdocs.yml
+++ b/.github/workflows/mkdocs.yml
@@ -2,7 +2,7 @@ name: MKDocs
 
 on:
   push:
-    branches: [develop,mkdocs-*]
+    branches: [develop, mkdocs-*]
     tags: [v*]
     paths:
       - .github/workflows/mkdocs.yml
@@ -19,12 +19,12 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
 
       - name: 🧰 Set up Python
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: "3.9"
           cache: "pip" # caching pip dependencies
@@ -38,15 +38,13 @@ jobs:
           chmod: 0755
 
       - name: Check Rzk files for each language
-        run:
-          for lang_dir in $(ls -d docs/docs/*/); do
-            pushd ${lang_dir} && rzk typecheck; popd ;
+        run: for lang_dir in $(ls -d docs/docs/*/); do
+          pushd ${lang_dir} && rzk typecheck; popd ;
           done
 
       - name: Check Rzk formatting for each language
-        run:
-          for lang_dir in $(ls -d docs/docs/*/); do
-            pushd ${lang_dir} && rzk format --check; popd ;
+        run: for lang_dir in $(ls -d docs/docs/*/); do
+          pushd ${lang_dir} && rzk format --check; popd ;
           done
 
       - name: 🔨 Install MkDocs Material and mike
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 3be2af0fb..7e15152ad 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -12,10 +12,10 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: 🧰 Setup Stack
-        uses: freckle/stack-action@v4
+        uses: freckle/stack-action@v5
         with:
           fast: false
 
@@ -37,10 +37,10 @@ jobs:
 
     steps:
       - name: 📥 Checkout repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: 🧰 Setup Stack
-        uses: freckle/stack-action@v4
+        uses: freckle/stack-action@v5
         with:
           fast: false
 
diff --git a/CITATION.cff b/CITATION.cff
index 6b01db532..ae6a75486 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -8,5 +8,5 @@ authors:
   - family-names: Danko
     given-names: Danila
 title: "Rzk: a  proof assistant for synthetic $\\infty$-categories"
-version: 0.7.4
+version: 0.7.5
 url: "https://github.com/rzk-lang/rzk"
diff --git a/docs/docs/en/related.md b/docs/docs/en/related.md
index 8e01fb8aa..ed045f723 100644
--- a/docs/docs/en/related.md
+++ b/docs/docs/en/related.md
@@ -39,13 +39,13 @@ Aya is implemented in Java.
 
     I do not know of existing formalization libraries in Aya.
 
-## The <b><span style="color: red">red</span>*</b> family
+## The <b><span style="color: red">red</span>\*</b> family
 
 [<b><span style="color: #135cb7;">cool</span>tt</b>](https://github.com/redprl/cooltt), [<b><span style="color: red">red</span>tt</b>](https://github.com/redprl/redtt), and [<b><span style="color: red">Red</span>PRL</b>](https://redprl.readthedocs.io/en/latest/) are a family of experimental proof assistants developed by the [<b><span style="color: red">Red</span>PRL</b> Development Team](https://redprl.org).
 
 There is a [<b><span style="color: red">red</span>tt</b> mathematical library](https://github.com/RedPRL/redtt/tree/master/library)
 
-The <b><span style="color: red">red</span>*</b> family of proof assistants is implemented in OCaml.
+The <b><span style="color: red">red</span>\*</b> family of proof assistants is implemented in OCaml.
 The developers also have a related [<b><span style="color: rgb(133, 177, 96);">A.L.G.A.E.<span></b> project](https://redprl.org/#algae),
 which aims to provide composable (OCaml) libraries that facilitate the construction of a usable proof assistant from a core type checker.
 
@@ -60,6 +60,7 @@ Other notable formalizations of HoTT in Coq include [Coq-HoTT](https://github.co
 Coq is implemented in OCaml.
 
 ## Cubical Agda
+
 [Cubical Agda](https://agda.readthedocs.io/en/latest/language/cubical.html) is a mode extending Agda with a variety of features from Cubical Type Theory[^1] [^2].
 
 Although technical a mode within Agda, it is probably best seen as a separate language.
@@ -89,7 +90,11 @@ Hence, a formalization of [HoTT in Lean 2](https://github.com/leanprover/lean2/t
 However, since Lean 2 is not supported anymore, the formalization is also unmantained.
 
 Lean 3 and 4 has dropped the mode that allowed (direct) HoTT formalization.
-There is, however, an unmaintained [port of Lean 2 HoTT Library to Lean 3](https://github.com/gebner/hott3).
+However, the [Ground Zero](https://github.com/forked-from-1kasper/ground_zero) project
+attempts to formalize HoTT in Lean 4. The project makes use of the [large elimination checker](https://github.com/forked-from-1kasper/ground_zero/blob/d8c41ea2910d81d3c1bf6c2762663473368016ab/GroundZero/Meta/HottTheory.lean),
+ported from an unmaintained [port of Lean 2 HoTT Library to Lean 3](https://github.com/gebner/hott3),
+which enables HoTT and non-HoTT scopes to coexist consistently (as the project authors believe).
+In particular, attempting to show UIP results in a type error under HoTT scope in the Ground Zero project.
 
 Lean 2 and 3 are implemented in C++.
 Lean 4 is implemented in itself (and a bit of C++)!
@@ -102,22 +107,19 @@ Lean 4 is implemented in itself (and a bit of C++)!
     <https://doi.org/10.4230/LIPIcs.TYPES.2015.5>
 
 [^2]:
-    Thierry Coquand, Simon Huber, and Anders Mörtberg.
-    2018. _On Higher Inductive Types in Cubical Type Theory_.
+    Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. _On Higher Inductive Types in Cubical Type Theory_.
     In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18).
     Association for Computing Machinery, New York, NY, USA, 255–264.
     <https://doi.org/10.1145/3209108.3209197>
 
 [^3]:
-    Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters.
-    2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
+    Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. 2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
     In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017).
     Association for Computing Machinery, New York, NY, USA, 164–172.
     <https://doi.org/10.1145/3018610.3018615>
 
 [^4]:
-    Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz.
-    2017. _Homotopy Type Theory in Lean_.
+    Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz. 2017. _Homotopy Type Theory in Lean_.
     In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017.
     Lecture Notes in Computer Science(), vol 10499. Springer, Cham.
     <https://doi.org/10.1007/978-3-319-66107-0_30>
diff --git a/docs/docs/ru/related.md b/docs/docs/ru/related.md
index 81dd4a28d..05d5619ea 100644
--- a/docs/docs/ru/related.md
+++ b/docs/docs/ru/related.md
@@ -44,7 +44,7 @@ Aya реализована на Java.
 
     Мне неизвестны библиотеки формализации на Aya.
 
-## Семейство <b><span style="color: red">red</span>*</b>
+## Семейство <b><span style="color: red">red</span>\*</b>
 
 [<b><span style="color: #135cb7;">cool</span>tt</b>](https://github.com/redprl/cooltt),
 [<b><span style="color: red">red</span>tt</b>](https://github.com/redprl/redtt),
@@ -54,8 +54,8 @@ Aya реализована на Java.
 
 Существует формализация [математической библиотеки <b><span style="color: red">red</span>tt</b>](https://github.com/RedPRL/redtt/tree/master/library)
 
-Семейство решателей <b><span style="color: red">red</span>*</b> реализовано на языке программирования OCaml.
-Создатели семества решателей также работают над  [проектом <b><span style="color: rgb(133, 177, 96);">A.L.G.A.E.<span></b>](https://redprl.org/#algae),
+Семейство решателей <b><span style="color: red">red</span>\*</b> реализовано на языке программирования OCaml.
+Создатели семества решателей также работают над [проектом <b><span style="color: rgb(133, 177, 96);">A.L.G.A.E.<span></b>](https://redprl.org/#algae),
 который нацелен на реализацию ряда удобных библиотек (для OCaml) для помощи в реализации
 решателей теорем на основе проверки типов для ядра решателя.
 
@@ -70,6 +70,7 @@ Coq — это зрелый решатель теорем, основанный
 Coq реализован на OCaml.
 
 ## Cubical Agda
+
 [Cubical Agda](https://agda.readthedocs.io/en/latest/language/cubical.html) (кубическая Агда)
 — это расширение Agda набором возможностей кубической теории типов[^1] [^2].
 
@@ -102,7 +103,12 @@ Lean 2, как и Agda, поддерживал режим без уникаль
 Однако, Lean 2 больше не поддерживается и формализация, соответственно, тоже.
 
 Lean 3 и 4 убрали режим, допускающий (прямую) формализацию гомотопической теории типов.
-Однако, существует ныне неподдерживаемый [проект по переносу библиотеки HoTT с Lean 2 на Lean 3](https://github.com/gebner/hott3).
+Несмотря на это проект [Ground Zero](https://github.com/forked-from-1kasper/ground_zero)
+продолжает формализацию HoTT на Lean 4. Проект использует [проверку элиминации](https://github.com/forked-from-1kasper/ground_zero/blob/d8c41ea2910d81d3c1bf6c2762663473368016ab/GroundZero/Meta/HottTheory.lean),
+портированную из неподдерживаемого [проекта по переносу библиотеки HoTT с Lean 2 на Lean 3](https://github.com/gebner/hott3).
+Эта проверка позволяет поддерживать окружение HoTT, совместимое со стандартным окружением Lean (по крайней мере по убеждениям авторов проекта).
+В частности, попытка (напрямую) доказать принцип неразличимости доказательств равенства (Uniqueness of Identity Proofs)
+приводит к ошибки типизации в рамках проекта Ground Zero.
 
 Lean 2 и 3 реализованы на C++.
 Lean 4 реализован в основном на самом себе (и немного на C++)!
@@ -115,22 +121,19 @@ Lean 4 реализован в основном на самом себе (и н
     <https://doi.org/10.4230/LIPIcs.TYPES.2015.5>
 
 [^2]:
-    Thierry Coquand, Simon Huber, and Anders Mörtberg.
-    2018. _On Higher Inductive Types in Cubical Type Theory_.
+    Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. _On Higher Inductive Types in Cubical Type Theory_.
     In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18).
     Association for Computing Machinery, New York, NY, USA, 255–264.
     <https://doi.org/10.1145/3209108.3209197>
 
 [^3]:
-    Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters.
-    2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
+    Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. 2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
     In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017).
     Association for Computing Machinery, New York, NY, USA, 164–172.
     <https://doi.org/10.1145/3018610.3018615>
 
 [^4]:
-    Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz.
-    2017. _Homotopy Type Theory in Lean_.
+    Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz. 2017. _Homotopy Type Theory in Lean_.
     In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017.
     Lecture Notes in Computer Science(), vol 10499. Springer, Cham.
     <https://doi.org/10.1007/978-3-319-66107-0_30>
diff --git a/flake.lock b/flake.lock
index 597cef8b0..ac3dc6343 100644
--- a/flake.lock
+++ b/flake.lock
@@ -53,17 +53,17 @@
     "miso": {
       "flake": false,
       "locked": {
-        "lastModified": 1691794309,
-        "narHash": "sha256-TQ6SRXDOit24jWnlNAh10FF5NQu8V6tbrY7ry56Cu7w=",
+        "lastModified": 1712007677,
+        "narHash": "sha256-6Ewu/T+VyeQ93lrN6bcpyCcoinwtO/X8HJrJp7hLSEQ=",
         "owner": "dmjio",
         "repo": "miso",
-        "rev": "49edf0677253bbcdd473422b5dd5b4beffd83910",
+        "rev": "8277ac79941825abaf50b917e074e3df7ef6d213",
         "type": "github"
       },
       "original": {
         "owner": "dmjio",
         "repo": "miso",
-        "rev": "49edf0677253bbcdd473422b5dd5b4beffd83910",
+        "rev": "8277ac79941825abaf50b917e074e3df7ef6d213",
         "type": "github"
       }
     },
@@ -84,17 +84,17 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1701842937,
-        "narHash": "sha256-xIhu/49t/xQaHQu/XyOI1HkK7Lva1dMosD1TM4P+iWc=",
+        "lastModified": 1713187215,
+        "narHash": "sha256-3WqIvGM8G5mgF9sabP7eAG+lW0n6RaN/xUdjk15lqP4=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "d1c3a8112f9d5d4840e0669727222e5fd9243451",
+        "rev": "2436aaf8fad634ee66a6280fb82a19c1771c173f",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "d1c3a8112f9d5d4840e0669727222e5fd9243451",
+        "rev": "2436aaf8fad634ee66a6280fb82a19c1771c173f",
         "type": "github"
       }
     },
diff --git a/flake.nix b/flake.nix
index 14ab88ce5..b83429a23 100644
--- a/flake.nix
+++ b/flake.nix
@@ -1,9 +1,9 @@
 {
   inputs = {
     flake-utils.url = "github:numtide/flake-utils";
-    nixpkgs.url = "github:NixOS/nixpkgs/d1c3a8112f9d5d4840e0669727222e5fd9243451";
+    nixpkgs.url = "github:NixOS/nixpkgs/2436aaf8fad634ee66a6280fb82a19c1771c173f";
     miso = {
-      url = "github:dmjio/miso/49edf0677253bbcdd473422b5dd5b4beffd83910";
+      url = "github:dmjio/miso/8277ac79941825abaf50b917e074e3df7ef6d213";
       flake = false;
     };
     flake-compat = {
@@ -22,7 +22,7 @@
 
       rzk = "rzk";
       rzk-js = "rzk-js";
-      ghcVersion = "ghc962";
+      ghcVersion = "ghc963";
       rzk-src = (inputs.nix-filter {
         root = ./${rzk};
         include = [ "app" "src" "test" "package.yaml" ];
diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md
index 99618aaf3..ec2a6e72d 100644
--- a/rzk/ChangeLog.md
+++ b/rzk/ChangeLog.md
@@ -6,9 +6,24 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.7.5 — 2024-08-18
+
+Minor changes:
+
+- Suport syntax sugar for nested Σ-types (see [#183](https://github.com/rzk-lang/rzk/pull/183))
+- Improve error reporting (see [#176](https://github.com/rzk-lang/rzk/pull/176) and [#179](https://github.com/rzk-lang/rzk/pull/179))
+
+Fixes:
+
+- Support newer `lsp` (specifically, `lsp-2.7.0.0`, see [#188](https://github.com/rzk-lang/rzk/pull/188))
+- Fix CI (see [#184](https://github.com/rzk-lang/rzk/pull/184))
+- Fix build of nix flake on aarch64-darwin (see [#181](https://github.com/rzk-lang/rzk/pull/181))
+- Small documentation fixes (see [#178](https://github.com/rzk-lang/rzk/pull/178))
+
 ## v0.7.4 — 2024-04-01
 
 Fixes:
+
 - Fix caching in Rzk Language Server, especially in presence of errors (see [#167](https://github.com/rzk-lang/rzk/pull/167))
 - Fix CI for the Rzk Playground (see [#174](https://github.com/rzk-lang/rzk/pull/174))
 
@@ -18,33 +33,37 @@ and a typo fix (see [#171](https://github.com/rzk-lang/rzk/pull/171)).
 ## v0.7.3 — 2023-12-16
 
 Fixes:
+
 - Fix overlapping edits in the formatter, hopefully making it idempotent (see [#160](https://github.com/rzk-lang/rzk/pull/160));
 - Fix formatter crashing the language server (see [#161](https://github.com/rzk-lang/rzk/pull/161));
 - Avoid unnecessary typechecking when semantics of a file has not changed (see [#159](https://github.com/rzk-lang/rzk/pull/159));
 - Stop typechecking after the first parse error (avoid invalid cache) (see [`68ab0b4`](https://github.com/rzk-lang/rzk/commit/68ab0b4dd3d627756e10adb55cb16845b08d09d9));
 
 Other:
+
 - Add unit tests for the formatter (see [#157](https://github.com/rzk-lang/rzk/pull/157));
 
 ## v0.7.2 — 2023-12-12
 
 Fixes:
+
 - Fixes for `rzk format`:
-    - Fix extra space after open parens in formatter (see [#155](https://github.com/rzk-lang/rzk/pull/155));
-    - Replace line string content with tokens when checking open parens (see [#156](https://github.com/rzk-lang/rzk/pull/156));
+  - Fix extra space after open parens in formatter (see [#155](https://github.com/rzk-lang/rzk/pull/155));
+  - Replace line string content with tokens when checking open parens (see [#156](https://github.com/rzk-lang/rzk/pull/156));
 - Throw an error when `rzk.yaml`'s `include` is empty (see [#154](https://github.com/rzk-lang/rzk/pull/154));
 
 Changes to the Rzk website:
-  - Support multiple languages in the documentation (see [#150](https://github.com/rzk-lang/rzk/pull/150));
-      - English is the default;
-      - Russian documentation is partially translated and is available at <http://rzk-lang.github.io/rzk/ru/>;
-  - Add a blog (see [#153](https://github.com/rzk-lang/rzk/pull/153) and [`e438820`](https://github.com/rzk-lang/rzk/commit/e4388202cea59531903c4c24b939841b2771ceb7));
-      - The blog is not versioned and is always available at <https://rzk-lang.github.io/rzk/en/blog/>;
-  - Add a new [Other proof assistants for HoTT](https://rzk-lang.github.io/rzk/en/v0.7.2/related/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/related/));
-  - Add a new [Introduction to Dependent Types](https://rzk-lang.github.io/rzk/en/v0.7.2/getting-started/dependent-types.rzk/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/getting-started/dependent-types.rzk/))
-  - Add (default) social cards
-  - Integrate ToC on the left
-  - Use Inria Sans for English, PT Sans for Russian
+
+- Support multiple languages in the documentation (see [#150](https://github.com/rzk-lang/rzk/pull/150));
+  - English is the default;
+  - Russian documentation is partially translated and is available at <http://rzk-lang.github.io/rzk/ru/>;
+- Add a blog (see [#153](https://github.com/rzk-lang/rzk/pull/153) and [`e438820`](https://github.com/rzk-lang/rzk/commit/e4388202cea59531903c4c24b939841b2771ceb7));
+  - The blog is not versioned and is always available at <https://rzk-lang.github.io/rzk/en/blog/>;
+- Add a new [Other proof assistants for HoTT](https://rzk-lang.github.io/rzk/en/v0.7.2/related/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/related/));
+- Add a new [Introduction to Dependent Types](https://rzk-lang.github.io/rzk/en/v0.7.2/getting-started/dependent-types.rzk/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/getting-started/dependent-types.rzk/))
+- Add (default) social cards
+- Integrate ToC on the left
+- Use Inria Sans for English, PT Sans for Russian
 
 ## v0.7.1 — 2023-12-08
 
diff --git a/rzk/app/Main.hs b/rzk/app/Main.hs
index d2f6c4c40..47d290e4c 100644
--- a/rzk/app/Main.hs
+++ b/rzk/app/Main.hs
@@ -16,7 +16,7 @@ import           Control.Monad           (forM, forM_, unless, when,
                                           (>=>))
 import           Data.Version            (showVersion)
 
-#ifdef LSP
+#ifdef LSP_ENABLED
 import           Language.Rzk.VSCode.Lsp (runLsp)
 #endif
 
@@ -66,7 +66,7 @@ main = do
         Right _decls -> putStrLn "Everything is ok!"
 
     Lsp ->
-#ifdef LSP
+#ifdef LSP_ENABLED
       void runLsp
 #else
       error "rzk lsp is not supported with this build"
diff --git a/rzk/grammar/Syntax.cf b/rzk/grammar/Syntax.cf
index 2c3ce32f6..14dbd2518 100644
--- a/rzk/grammar/Syntax.cf
+++ b/rzk/grammar/Syntax.cf
@@ -60,6 +60,7 @@ SomeSectionName.  SectionName ::= VarIdent ;
 PatternUnit.      Pattern ::= "unit" ;
 PatternVar.       Pattern ::= VarIdent ;
 PatternPair.      Pattern ::= "(" Pattern "," Pattern ")" ;
+PatternTuple.     Pattern ::= "(" Pattern "," Pattern "," [Pattern] ")" ;
 separator nonempty Pattern "" ;
 
 -- Parameter introduction (for lambda abstractions)
@@ -78,6 +79,10 @@ ParamVarShapeDeprecated. ParamDecl ::= "{" "(" Pattern ":" Term ")" "|" Term "}"
 paramVarShapeDeprecated. ParamDecl ::= "{" Pattern ":" Term "|" Term "}" ;
 define paramVarShapeDeprecated pat cube tope = ParamVarShapeDeprecated pat cube tope ;
 
+-- Parameter declaration for Sigma types
+SigmaParam. SigmaParam ::= Pattern ":" Term ;
+separator nonempty SigmaParam "," ;
+
 Restriction. Restriction ::= Term "↦" Term ;
 separator nonempty Restriction "," ;
 
@@ -106,6 +111,7 @@ RecOrDeprecated.  Term7 ::= "recOR" "(" Term "," Term "," Term "," Term ")" ;
 -- Types
 TypeFun.        Term1 ::= ParamDecl "→" Term1 ;
 TypeSigma.      Term1 ::= "Σ" "(" Pattern ":" Term ")" "," Term1 ;
+TypeSigmaTuple. Term1 ::= "Σ" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
 TypeUnit.       Term7 ::= "Unit" ;
 TypeId.         Term1 ::= Term2 "=_{" Term "}" Term2 ;
 TypeIdSimple.   Term1 ::= Term2 "=" Term2 ;
@@ -115,6 +121,7 @@ TypeExtensionDeprecated.  Term7 ::= "<" ParamDecl "→" Term ">" ;
 App.            Term6 ::= Term6 Term7 ;
 Lambda.         Term1 ::= "\\" [Param] "→" Term1 ;
 Pair.           Term7 ::= "(" Term "," Term ")" ;
+Tuple.          Term7 ::= "(" Term "," Term "," [Term] ")" ;
 First.          Term6 ::= "π₁" Term7 ;
 Second.         Term6 ::= "π₂" Term7 ;
 Unit.           Term7 ::= "unit" ;
@@ -149,6 +156,7 @@ ASCII_TopeOr.         Term2 ::= Term3 "\\/" Term2 ;
 
 ASCII_TypeFun.        Term1 ::= ParamDecl "->" Term1 ;
 ASCII_TypeSigma.      Term1 ::= "Sigma" "(" Pattern ":" Term ")" "," Term1 ;
+ASCII_TypeSigmaTuple. Term1 ::= "Sigma" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
 
 ASCII_Lambda.         Term1 ::= "\\" [Param] "->" Term1 ;
 ASCII_Restriction. Restriction ::= Term "|->" Term ;
@@ -161,4 +169,6 @@ ASCII_Second.         Term6 ::= "second" Term7 ;
 -- Alternative Unicode syntax rules
 
 unicode_TypeSigmaAlt.   Term1 ::= "∑" "(" Pattern ":" Term ")" "," Term1 ;    -- \sum
+unicode_TypeSigmaTupleAlt. Term1 ::= "∑" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
 define unicode_TypeSigmaAlt pat fst snd = TypeSigma pat fst snd ;
+define unicode_TypeSigmaTupleAlt par pars t = TypeSigmaTuple par pars t ;
diff --git a/rzk/package.yaml b/rzk/package.yaml
index dcc75ae77..bdce72e8b 100644
--- a/rzk/package.yaml
+++ b/rzk/package.yaml
@@ -1,10 +1,10 @@
 name: rzk
-version: 0.7.4
+version: 0.7.5
 github: "rzk-lang/rzk"
 license: BSD3
 author: "Nikolai Kudasov"
 maintainer: "nickolay.kudasov@gmail.com"
-copyright: "2023 Nikolai Kudasov"
+copyright: "2023-2024 Nikolai Kudasov"
 
 extra-source-files:
   - README.md
@@ -28,7 +28,7 @@ flags:
 
 when:
   - condition: flag(lsp) && !impl(ghcjs)
-    cpp-options: -DLSP
+    cpp-options: -DLSP_ENABLED
 
 custom-setup:
   dependencies:
diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
index 803f863b7..55fc7ceab 100644
--- a/rzk/rzk.cabal
+++ b/rzk/rzk.cabal
@@ -5,7 +5,7 @@ cabal-version: 1.24
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.7.4
+version:        0.7.5
 synopsis:       An experimental proof assistant for synthetic ∞-categories
 description:    Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 category:       Dependent Types
@@ -13,7 +13,7 @@ homepage:       https://github.com/rzk-lang/rzk#readme
 bug-reports:    https://github.com/rzk-lang/rzk/issues
 author:         Nikolai Kudasov
 maintainer:     nickolay.kudasov@gmail.com
-copyright:      2023 Nikolai Kudasov
+copyright:      2023-2024 Nikolai Kudasov
 license:        BSD3
 license-file:   LICENSE
 build-type:     Custom
@@ -76,7 +76,7 @@ library
     , yaml >=0.11.0.0
   default-language: Haskell2010
   if flag(lsp) && !impl(ghcjs)
-    cpp-options: -DLSP
+    cpp-options: -DLSP_ENABLED
   if flag(lsp) && !impl(ghcjs)
     exposed-modules:
         Language.Rzk.VSCode.Config
@@ -121,7 +121,7 @@ executable rzk
     , yaml >=0.11.0.0
   default-language: Haskell2010
   if flag(lsp) && !impl(ghcjs)
-    cpp-options: -DLSP
+    cpp-options: -DLSP_ENABLED
   if !impl(ghcjs)
     build-depends:
         optparse-generic >=1.4.0
@@ -153,7 +153,7 @@ test-suite doctests
     , yaml >=0.11.0.0
   default-language: Haskell2010
   if flag(lsp) && !impl(ghcjs)
-    cpp-options: -DLSP
+    cpp-options: -DLSP_ENABLED
 
 test-suite rzk-test
   type: exitcode-stdio-1.0
@@ -185,4 +185,4 @@ test-suite rzk-test
     , yaml >=0.11.0.0
   default-language: Haskell2010
   if flag(lsp) && !impl(ghcjs)
-    cpp-options: -DLSP
+    cpp-options: -DLSP_ENABLED
diff --git a/rzk/src/Language/Rzk/Free/Syntax.hs b/rzk/src/Language/Rzk/Free/Syntax.hs
index 786b17b6b..ad716ed38 100644
--- a/rzk/src/Language/Rzk/Free/Syntax.hs
+++ b/rzk/src/Language/Rzk/Free/Syntax.hs
@@ -173,6 +173,12 @@ toScopePattern pat bvars = toTerm $ \z ->
     bindings (Rzk.PatternVar _loc (Rzk.VarIdent _ "_")) _ = []
     bindings (Rzk.PatternVar _loc x)    t = [(varIdent x, t)]
     bindings (Rzk.PatternPair _loc l r) t = bindings l (First t) <> bindings r (Second t)
+    bindings (Rzk.PatternTuple loc p1 p2 ps) t = bindings (desugarTuple loc (reverse ps) p2 p1) t
+
+desugarTuple loc ps p2 p1 =
+  case ps of
+    []          -> Rzk.PatternPair loc p1 p2
+    pLast : ps' -> Rzk.PatternPair loc (desugarTuple loc ps' p2 p1) pLast
 
 toTerm :: (VarIdent -> Term a) -> Rzk.Term -> Term a
 toTerm bvars = go
@@ -209,7 +215,6 @@ toTerm bvars = go
         (Rzk.TypeFun loc (Rzk.ParamTermShape loc' (patternToTerm pat) cube tope) ret)
       t@(Rzk.Lambda loc ((Rzk.ParamPatternShapeDeprecated loc' pat cube tope):params) body) -> deprecated t
         (Rzk.Lambda loc ((Rzk.ParamPatternShape loc' [pat] cube tope):params) body)
-
       -- ASCII versions
       Rzk.ASCII_CubeUnitStar loc -> go (Rzk.CubeUnitStar loc)
       Rzk.ASCII_Cube2_0 loc -> go (Rzk.Cube2_0 loc)
@@ -223,6 +228,7 @@ toTerm bvars = go
 
       Rzk.ASCII_TypeFun loc param ret -> go (Rzk.TypeFun loc param ret)
       Rzk.ASCII_TypeSigma loc pat ty ret -> go (Rzk.TypeSigma loc pat ty ret)
+      Rzk.ASCII_TypeSigmaTuple loc p ps tN -> go (Rzk.TypeSigmaTuple loc p ps tN)
       Rzk.ASCII_Lambda loc pat ret -> go (Rzk.Lambda loc pat ret)
       Rzk.ASCII_TypeExtensionDeprecated loc shape type_ -> go (Rzk.TypeExtensionDeprecated loc shape type_)
       Rzk.ASCII_First loc term -> go (Rzk.First loc term)
@@ -256,6 +262,8 @@ toTerm bvars = go
       Rzk.Unit _loc -> Unit
       Rzk.App _loc f x -> App (go f) (go x)
       Rzk.Pair _loc l r -> Pair (go l) (go r)
+      Rzk.Tuple _loc p1 p2 (p:ps) -> go (Rzk.Tuple _loc (Rzk.Pair _loc p1 p2) p ps)
+      Rzk.Tuple _loc p1 p2 [] -> go (Rzk.Pair _loc p1 p2)
       Rzk.First _loc term -> First (go term)
       Rzk.Second _loc term -> Second (go term)
       Rzk.Refl _loc -> Refl Nothing
@@ -280,11 +288,18 @@ toTerm bvars = go
       Rzk.TypeSigma _loc pat tA tB ->
         TypeSigma (patternVar pat) (go tA) (toScopePattern pat bvars tB)
 
+      Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ patA tA) ((Rzk.SigmaParam _ patB tB) : ps) tN -> 
+        go (Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _loc patX tX) ps tN)
+        where
+          patX = Rzk.PatternPair _loc patA patB
+          tX = Rzk.TypeSigma _loc patA tA tB
+      Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ pat tA) [] tB -> go (Rzk.TypeSigma _loc pat tA tB)
+
       Rzk.Lambda _loc [] body -> go body
       Rzk.Lambda _loc (Rzk.ParamPattern _ pat : params) body ->
         Lambda (patternVar pat) Nothing (toScopePattern pat bvars (Rzk.Lambda _loc params body))
       Rzk.Lambda _loc (Rzk.ParamPatternType _ [] _ty : params) body ->
-        go (Rzk.Lambda _loc params body)
+        go (Rzk.Lambda _loc params body)                        
       Rzk.Lambda _loc (Rzk.ParamPatternType _ (pat:pats) ty : params) body ->
         Lambda (patternVar pat) (Just (go ty, Nothing))
           (toScopePattern pat bvars (Rzk.Lambda _loc (Rzk.ParamPatternType _loc pats ty : params) body))
@@ -317,6 +332,7 @@ patternToTerm = ptt
       Rzk.PatternVar loc x    -> Rzk.Var loc x
       Rzk.PatternPair loc l r -> Rzk.Pair loc (ptt l) (ptt r)
       Rzk.PatternUnit loc     -> Rzk.Unit loc
+      Rzk.PatternTuple loc p1 p2 ps -> patternToTerm (desugarTuple loc (reverse ps) p2 p1)
 
 unsafeTermToPattern :: Rzk.Term -> Rzk.Pattern
 unsafeTermToPattern = ttp
diff --git a/rzk/src/Language/Rzk/Syntax/Abs.hs b/rzk/src/Language/Rzk/Syntax/Abs.hs
index ad4c07fbe..57bd7ad0e 100644
--- a/rzk/src/Language/Rzk/Syntax/Abs.hs
+++ b/rzk/src/Language/Rzk/Syntax/Abs.hs
@@ -72,6 +72,7 @@ data Pattern' a
     = PatternUnit a
     | PatternVar a (VarIdent' a)
     | PatternPair a (Pattern' a) (Pattern' a)
+    | PatternTuple a (Pattern' a) (Pattern' a) [Pattern' a]
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
 
 type Param = Param' BNFC'Position
@@ -91,6 +92,10 @@ data ParamDecl' a
     | ParamVarShapeDeprecated a (Pattern' a) (Term' a) (Term' a)
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
 
+type SigmaParam = SigmaParam' BNFC'Position
+data SigmaParam' a = SigmaParam a (Pattern' a) (Term' a)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+
 type Restriction = Restriction' BNFC'Position
 data Restriction' a
     = Restriction a (Term' a) (Term' a)
@@ -119,6 +124,7 @@ data Term' a
     | RecOrDeprecated a (Term' a) (Term' a) (Term' a) (Term' a)
     | TypeFun a (ParamDecl' a) (Term' a)
     | TypeSigma a (Pattern' a) (Term' a) (Term' a)
+    | TypeSigmaTuple a (SigmaParam' a) [SigmaParam' a] (Term' a)
     | TypeUnit a
     | TypeId a (Term' a) (Term' a) (Term' a)
     | TypeIdSimple a (Term' a) (Term' a)
@@ -127,6 +133,7 @@ data Term' a
     | App a (Term' a) (Term' a)
     | Lambda a [Param' a] (Term' a)
     | Pair a (Term' a) (Term' a)
+    | Tuple a (Term' a) (Term' a) [Term' a]
     | First a (Term' a)
     | Second a (Term' a)
     | Unit a
@@ -148,6 +155,7 @@ data Term' a
     | ASCII_TopeOr a (Term' a) (Term' a)
     | ASCII_TypeFun a (ParamDecl' a) (Term' a)
     | ASCII_TypeSigma a (Pattern' a) (Term' a) (Term' a)
+    | ASCII_TypeSigmaTuple a (SigmaParam' a) [SigmaParam' a] (Term' a)
     | ASCII_Lambda a [Param' a] (Term' a)
     | ASCII_TypeExtensionDeprecated a (ParamDecl' a) (Term' a)
     | ASCII_First a (Term' a)
@@ -184,6 +192,9 @@ ascii_CubeProduct = \ _a l r -> CubeProduct _a l r
 unicode_TypeSigmaAlt :: a -> Pattern' a -> Term' a -> Term' a -> Term' a
 unicode_TypeSigmaAlt = \ _a pat fst snd -> TypeSigma _a pat fst snd
 
+unicode_TypeSigmaTupleAlt :: a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
+unicode_TypeSigmaTupleAlt = \ _a par pars t -> TypeSigmaTuple _a par pars t
+
 newtype VarIdentToken = VarIdentToken String
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)
 
@@ -253,6 +264,7 @@ instance HasPosition Pattern where
     PatternUnit p -> p
     PatternVar p _ -> p
     PatternPair p _ _ -> p
+    PatternTuple p _ _ _ -> p
 
 instance HasPosition Param where
   hasPosition = \case
@@ -269,6 +281,10 @@ instance HasPosition ParamDecl where
     ParamTermTypeDeprecated p _ _ -> p
     ParamVarShapeDeprecated p _ _ _ -> p
 
+instance HasPosition SigmaParam where
+  hasPosition = \case
+    SigmaParam p _ _ -> p
+
 instance HasPosition Restriction where
   hasPosition = \case
     Restriction p _ _ -> p
@@ -296,6 +312,7 @@ instance HasPosition Term where
     RecOrDeprecated p _ _ _ _ -> p
     TypeFun p _ _ -> p
     TypeSigma p _ _ _ -> p
+    TypeSigmaTuple p _ _ _ -> p
     TypeUnit p -> p
     TypeId p _ _ _ -> p
     TypeIdSimple p _ _ -> p
@@ -304,6 +321,7 @@ instance HasPosition Term where
     App p _ _ -> p
     Lambda p _ _ -> p
     Pair p _ _ -> p
+    Tuple p _ _ _ -> p
     First p _ -> p
     Second p _ -> p
     Unit p -> p
@@ -325,6 +343,7 @@ instance HasPosition Term where
     ASCII_TopeOr p _ _ -> p
     ASCII_TypeFun p _ _ -> p
     ASCII_TypeSigma p _ _ _ -> p
+    ASCII_TypeSigmaTuple p _ _ _ -> p
     ASCII_Lambda p _ _ -> p
     ASCII_TypeExtensionDeprecated p _ _ -> p
     ASCII_First p _ -> p
diff --git a/rzk/src/Language/Rzk/Syntax/Doc.txt b/rzk/src/Language/Rzk/Syntax/Doc.txt
index ea571c2c7..f8adc1639 100644
--- a/rzk/src/Language/Rzk/Syntax/Doc.txt
+++ b/rzk/src/Language/Rzk/Syntax/Doc.txt
@@ -97,6 +97,7 @@ All other symbols are terminals.
   | //Pattern// | -> | ``unit``
   |  |  **|**  | //VarIdent//
   |  |  **|**  | ``(`` //Pattern// ``,`` //Pattern// ``)``
+  |  |  **|**  | ``(`` //Pattern// ``,`` //Pattern// ``,`` //[Pattern]// ``)``
   | //[Pattern]// | -> | //Pattern//
   |  |  **|**  | //Pattern// //[Pattern]//
   | //Param// | -> | //Pattern//
@@ -111,6 +112,9 @@ All other symbols are terminals.
   |  |  **|**  | ``{`` //Pattern// ``:`` //Term// ``}``
   |  |  **|**  | ``{`` ``(`` //Pattern// ``:`` //Term// ``)`` ``|`` //Term// ``}``
   |  |  **|**  | ``{`` //Pattern// ``:`` //Term// ``|`` //Term// ``}``
+  | //SigmaParam// | -> | //Pattern// ``:`` //Term//
+  | //[SigmaParam]// | -> | //SigmaParam//
+  |  |  **|**  | //SigmaParam// ``,`` //[SigmaParam]//
   | //Restriction// | -> | //Term// ``↦`` //Term//
   |  |  **|**  | //Term// ``|->`` //Term//
   | //[Restriction]// | -> | //Restriction//
@@ -131,6 +135,7 @@ All other symbols are terminals.
   |  |  **|**  | ``Unit``
   |  |  **|**  | ``<`` //ParamDecl// ``→`` //Term// ``>``
   |  |  **|**  | ``(`` //Term// ``,`` //Term// ``)``
+  |  |  **|**  | ``(`` //Term// ``,`` //Term// ``,`` //[Term]// ``)``
   |  |  **|**  | ``unit``
   |  |  **|**  | ``refl``
   |  |  **|**  | ``refl_{`` //Term// ``}``
@@ -161,14 +166,17 @@ All other symbols are terminals.
   |  |  **|**  | //Term3// ``\/`` //Term2//
   | //Term1// | -> | //ParamDecl// ``→`` //Term1//
   |  |  **|**  | ``Σ`` ``(`` //Pattern// ``:`` //Term// ``)`` ``,`` //Term1//
+  |  |  **|**  | ``Σ`` ``(`` //SigmaParam// ``,`` //[SigmaParam]// ``)`` ``,`` //Term1//
   |  |  **|**  | //Term2// ``=_{`` //Term// ``}`` //Term2//
   |  |  **|**  | //Term2// ``=`` //Term2//
   |  |  **|**  | ``\`` //[Param]// ``→`` //Term1//
   |  |  **|**  | //Term2//
   |  |  **|**  | //ParamDecl// ``->`` //Term1//
   |  |  **|**  | ``Sigma`` ``(`` //Pattern// ``:`` //Term// ``)`` ``,`` //Term1//
+  |  |  **|**  | ``Sigma`` ``(`` //SigmaParam// ``,`` //[SigmaParam]// ``)`` ``,`` //Term1//
   |  |  **|**  | ``\`` //[Param]// ``->`` //Term1//
   |  |  **|**  | ``∑`` ``(`` //Pattern// ``:`` //Term// ``)`` ``,`` //Term1//
+  |  |  **|**  | ``∑`` ``(`` //SigmaParam// ``,`` //[SigmaParam]// ``)`` ``,`` //Term1//
   | //Term6// | -> | //Term6// ``[`` //[Restriction]// ``]``
   |  |  **|**  | //Term6// //Term7//
   |  |  **|**  | ``π₁`` //Term7//
diff --git a/rzk/src/Language/Rzk/Syntax/Par.y b/rzk/src/Language/Rzk/Syntax/Par.y
index f2967f020..9089984c0 100644
--- a/rzk/src/Language/Rzk/Syntax/Par.y
+++ b/rzk/src/Language/Rzk/Syntax/Par.y
@@ -23,6 +23,8 @@ module Language.Rzk.Syntax.Par
   , pParam
   , pListParam
   , pParamDecl
+  , pSigmaParam
+  , pListSigmaParam
   , pRestriction
   , pListRestriction
   , pTerm7
@@ -58,6 +60,8 @@ import Language.Rzk.Syntax.Lex
 %name pParam_internal Param
 %name pListParam_internal ListParam
 %name pParamDecl_internal ParamDecl
+%name pSigmaParam_internal SigmaParam
+%name pListSigmaParam_internal ListSigmaParam
 %name pRestriction_internal Restriction
 %name pListRestriction_internal ListRestriction
 %name pTerm7_internal Term7
@@ -230,6 +234,7 @@ Pattern
   : 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
   | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.PatternVar (fst $1) (snd $1)) }
   | '(' Pattern ',' Pattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternPair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '(' Pattern ',' Pattern ',' ListPattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternTuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
 
 ListPattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Pattern]) }
 ListPattern
@@ -257,6 +262,15 @@ ParamDecl
   | '{' '(' Pattern ':' Term ')' '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
   | '{' Pattern ':' Term '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.paramVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
 
+SigmaParam :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.SigmaParam) }
+SigmaParam
+  : Pattern ':' Term { (fst $1, Language.Rzk.Syntax.Abs.SigmaParam (fst $1) (snd $1) (snd $3)) }
+
+ListSigmaParam :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.SigmaParam]) }
+ListSigmaParam
+  : SigmaParam { (fst $1, (:[]) (snd $1)) }
+  | SigmaParam ',' ListSigmaParam { (fst $1, (:) (snd $1) (snd $3)) }
+
 Restriction :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Restriction) }
 Restriction
   : Term '↦' Term { (fst $1, Language.Rzk.Syntax.Abs.Restriction (fst $1) (snd $1) (snd $3)) }
@@ -285,6 +299,7 @@ Term7
   | 'Unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
   | '<' ParamDecl '→' Term '>' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeExtensionDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
   | '(' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Pair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '(' Term ',' Term ',' ListTerm ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Tuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
   | 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Unit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
   | 'refl' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Refl (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
   | 'refl_{' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ReflTerm (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
@@ -330,14 +345,17 @@ Term1 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term)
 Term1
   : ParamDecl '→' Term1 { (fst $1, Language.Rzk.Syntax.Abs.TypeFun (fst $1) (snd $1) (snd $3)) }
   | 'Σ' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | 'Σ' '(' SigmaParam ',' ListSigmaParam ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeSigmaTuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
   | Term2 '=_{' Term '}' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeId (fst $1) (snd $1) (snd $3) (snd $5)) }
   | Term2 '=' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeIdSimple (fst $1) (snd $1) (snd $3)) }
   | '\\' ListParam '→' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
   | Term2 { (fst $1, (snd $1)) }
   | ParamDecl '->' Term1 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TypeFun (fst $1) (snd $1) (snd $3)) }
   | 'Sigma' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | 'Sigma' '(' SigmaParam ',' ListSigmaParam ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeSigmaTuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
   | '\\' ListParam '->' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
   | '∑' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.unicode_TypeSigmaAlt (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | '∑' '(' SigmaParam ',' ListSigmaParam ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.unicode_TypeSigmaTupleAlt (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
 
 Term6 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
 Term6
@@ -421,6 +439,12 @@ pListParam = fmap snd . pListParam_internal
 pParamDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.ParamDecl
 pParamDecl = fmap snd . pParamDecl_internal
 
+pSigmaParam :: [Token] -> Err Language.Rzk.Syntax.Abs.SigmaParam
+pSigmaParam = fmap snd . pSigmaParam_internal
+
+pListSigmaParam :: [Token] -> Err [Language.Rzk.Syntax.Abs.SigmaParam]
+pListSigmaParam = fmap snd . pListSigmaParam_internal
+
 pRestriction :: [Token] -> Err Language.Rzk.Syntax.Abs.Restriction
 pRestriction = fmap snd . pRestriction_internal
 
diff --git a/rzk/src/Language/Rzk/Syntax/Print.hs b/rzk/src/Language/Rzk/Syntax/Print.hs
index c31b45a6e..ae973872f 100644
--- a/rzk/src/Language/Rzk/Syntax/Print.hs
+++ b/rzk/src/Language/Rzk/Syntax/Print.hs
@@ -198,6 +198,7 @@ instance Print (Language.Rzk.Syntax.Abs.Pattern' a) where
     Language.Rzk.Syntax.Abs.PatternUnit _ -> prPrec i 0 (concatD [doc (showString "unit")])
     Language.Rzk.Syntax.Abs.PatternVar _ varident -> prPrec i 0 (concatD [prt 0 varident])
     Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")])
+    Language.Rzk.Syntax.Abs.PatternTuple _ pattern_1 pattern_2 patterns -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ","), prt 0 patterns, doc (showString ")")])
 
 instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where
   prt _ [] = concatD []
@@ -224,6 +225,15 @@ instance Print (Language.Rzk.Syntax.Abs.ParamDecl' a) where
     Language.Rzk.Syntax.Abs.ParamTermTypeDeprecated _ pattern_ term -> prPrec i 0 (concatD [doc (showString "{"), prt 0 pattern_, doc (showString ":"), prt 0 term, doc (showString "}")])
     Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated _ pattern_ term1 term2 -> prPrec i 0 (concatD [doc (showString "{"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString ")"), doc (showString "|"), prt 0 term2, doc (showString "}")])
 
+instance Print (Language.Rzk.Syntax.Abs.SigmaParam' a) where
+  prt i = \case
+    Language.Rzk.Syntax.Abs.SigmaParam _ pattern_ term -> prPrec i 0 (concatD [prt 0 pattern_, doc (showString ":"), prt 0 term])
+
+instance Print [Language.Rzk.Syntax.Abs.SigmaParam' a] where
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
+  prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
+
 instance Print (Language.Rzk.Syntax.Abs.Restriction' a) where
   prt i = \case
     Language.Rzk.Syntax.Abs.Restriction _ term1 term2 -> prPrec i 0 (concatD [prt 0 term1, doc (showString "\8614"), prt 0 term2])
@@ -256,6 +266,7 @@ instance Print (Language.Rzk.Syntax.Abs.Term' a) where
     Language.Rzk.Syntax.Abs.RecOrDeprecated _ term1 term2 term3 term4 -> prPrec i 7 (concatD [doc (showString "recOR"), doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ","), prt 0 term3, doc (showString ","), prt 0 term4, doc (showString ")")])
     Language.Rzk.Syntax.Abs.TypeFun _ paramdecl term -> prPrec i 1 (concatD [prt 0 paramdecl, doc (showString "\8594"), prt 1 term])
     Language.Rzk.Syntax.Abs.TypeSigma _ pattern_ term1 term2 -> prPrec i 1 (concatD [doc (showString "\931"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString ")"), doc (showString ","), prt 1 term2])
+    Language.Rzk.Syntax.Abs.TypeSigmaTuple _ sigmaparam sigmaparams term -> prPrec i 1 (concatD [doc (showString "\931"), doc (showString "("), prt 0 sigmaparam, doc (showString ","), prt 0 sigmaparams, doc (showString ")"), doc (showString ","), prt 1 term])
     Language.Rzk.Syntax.Abs.TypeUnit _ -> prPrec i 7 (concatD [doc (showString "Unit")])
     Language.Rzk.Syntax.Abs.TypeId _ term1 term2 term3 -> prPrec i 1 (concatD [prt 2 term1, doc (showString "=_{"), prt 0 term2, doc (showString "}"), prt 2 term3])
     Language.Rzk.Syntax.Abs.TypeIdSimple _ term1 term2 -> prPrec i 1 (concatD [prt 2 term1, doc (showString "="), prt 2 term2])
@@ -264,6 +275,7 @@ instance Print (Language.Rzk.Syntax.Abs.Term' a) where
     Language.Rzk.Syntax.Abs.App _ term1 term2 -> prPrec i 6 (concatD [prt 6 term1, prt 7 term2])
     Language.Rzk.Syntax.Abs.Lambda _ params term -> prPrec i 1 (concatD [doc (showString "\\"), prt 0 params, doc (showString "\8594"), prt 1 term])
     Language.Rzk.Syntax.Abs.Pair _ term1 term2 -> prPrec i 7 (concatD [doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ")")])
+    Language.Rzk.Syntax.Abs.Tuple _ term1 term2 terms -> prPrec i 7 (concatD [doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ","), prt 0 terms, doc (showString ")")])
     Language.Rzk.Syntax.Abs.First _ term -> prPrec i 6 (concatD [doc (showString "\960\8321"), prt 7 term])
     Language.Rzk.Syntax.Abs.Second _ term -> prPrec i 6 (concatD [doc (showString "\960\8322"), prt 7 term])
     Language.Rzk.Syntax.Abs.Unit _ -> prPrec i 7 (concatD [doc (showString "unit")])
@@ -285,6 +297,7 @@ instance Print (Language.Rzk.Syntax.Abs.Term' a) where
     Language.Rzk.Syntax.Abs.ASCII_TopeOr _ term1 term2 -> prPrec i 2 (concatD [prt 3 term1, doc (showString "\\/"), prt 2 term2])
     Language.Rzk.Syntax.Abs.ASCII_TypeFun _ paramdecl term -> prPrec i 1 (concatD [prt 0 paramdecl, doc (showString "->"), prt 1 term])
     Language.Rzk.Syntax.Abs.ASCII_TypeSigma _ pattern_ term1 term2 -> prPrec i 1 (concatD [doc (showString "Sigma"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString ")"), doc (showString ","), prt 1 term2])
+    Language.Rzk.Syntax.Abs.ASCII_TypeSigmaTuple _ sigmaparam sigmaparams term -> prPrec i 1 (concatD [doc (showString "Sigma"), doc (showString "("), prt 0 sigmaparam, doc (showString ","), prt 0 sigmaparams, doc (showString ")"), doc (showString ","), prt 1 term])
     Language.Rzk.Syntax.Abs.ASCII_Lambda _ params term -> prPrec i 1 (concatD [doc (showString "\\"), prt 0 params, doc (showString "->"), prt 1 term])
     Language.Rzk.Syntax.Abs.ASCII_TypeExtensionDeprecated _ paramdecl term -> prPrec i 7 (concatD [doc (showString "<"), prt 0 paramdecl, doc (showString "->"), prt 0 term, doc (showString ">")])
     Language.Rzk.Syntax.Abs.ASCII_First _ term -> prPrec i 6 (concatD [doc (showString "first"), prt 7 term])
diff --git a/rzk/src/Language/Rzk/Syntax/Skel.hs b/rzk/src/Language/Rzk/Syntax/Skel.hs
index f563fd074..fb485cc56 100644
--- a/rzk/src/Language/Rzk/Syntax/Skel.hs
+++ b/rzk/src/Language/Rzk/Syntax/Skel.hs
@@ -71,6 +71,7 @@ transPattern x = case x of
   Language.Rzk.Syntax.Abs.PatternUnit _ -> failure x
   Language.Rzk.Syntax.Abs.PatternVar _ varident -> failure x
   Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> failure x
+  Language.Rzk.Syntax.Abs.PatternTuple _ pattern_1 pattern_2 patterns -> failure x
 
 transParam :: Show a => Language.Rzk.Syntax.Abs.Param' a -> Result
 transParam x = case x of
@@ -87,6 +88,10 @@ transParamDecl x = case x of
   Language.Rzk.Syntax.Abs.ParamTermTypeDeprecated _ pattern_ term -> failure x
   Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated _ pattern_ term1 term2 -> failure x
 
+transSigmaParam :: Show a => Language.Rzk.Syntax.Abs.SigmaParam' a -> Result
+transSigmaParam x = case x of
+  Language.Rzk.Syntax.Abs.SigmaParam _ pattern_ term -> failure x
+
 transRestriction :: Show a => Language.Rzk.Syntax.Abs.Restriction' a -> Result
 transRestriction x = case x of
   Language.Rzk.Syntax.Abs.Restriction _ term1 term2 -> failure x
@@ -114,6 +119,7 @@ transTerm x = case x of
   Language.Rzk.Syntax.Abs.RecOrDeprecated _ term1 term2 term3 term4 -> failure x
   Language.Rzk.Syntax.Abs.TypeFun _ paramdecl term -> failure x
   Language.Rzk.Syntax.Abs.TypeSigma _ pattern_ term1 term2 -> failure x
+  Language.Rzk.Syntax.Abs.TypeSigmaTuple _ sigmaparam sigmaparams term -> failure x
   Language.Rzk.Syntax.Abs.TypeUnit _ -> failure x
   Language.Rzk.Syntax.Abs.TypeId _ term1 term2 term3 -> failure x
   Language.Rzk.Syntax.Abs.TypeIdSimple _ term1 term2 -> failure x
@@ -122,6 +128,7 @@ transTerm x = case x of
   Language.Rzk.Syntax.Abs.App _ term1 term2 -> failure x
   Language.Rzk.Syntax.Abs.Lambda _ params term -> failure x
   Language.Rzk.Syntax.Abs.Pair _ term1 term2 -> failure x
+  Language.Rzk.Syntax.Abs.Tuple _ term1 term2 terms -> failure x
   Language.Rzk.Syntax.Abs.First _ term -> failure x
   Language.Rzk.Syntax.Abs.Second _ term -> failure x
   Language.Rzk.Syntax.Abs.Unit _ -> failure x
@@ -143,6 +150,7 @@ transTerm x = case x of
   Language.Rzk.Syntax.Abs.ASCII_TopeOr _ term1 term2 -> failure x
   Language.Rzk.Syntax.Abs.ASCII_TypeFun _ paramdecl term -> failure x
   Language.Rzk.Syntax.Abs.ASCII_TypeSigma _ pattern_ term1 term2 -> failure x
+  Language.Rzk.Syntax.Abs.ASCII_TypeSigmaTuple _ sigmaparam sigmaparams term -> failure x
   Language.Rzk.Syntax.Abs.ASCII_Lambda _ params term -> failure x
   Language.Rzk.Syntax.Abs.ASCII_TypeExtensionDeprecated _ paramdecl term -> failure x
   Language.Rzk.Syntax.Abs.ASCII_First _ term -> failure x
diff --git a/rzk/src/Language/Rzk/VSCode/Handlers.hs b/rzk/src/Language/Rzk/VSCode/Handlers.hs
index 49ecdf329..7cefeea7b 100644
--- a/rzk/src/Language/Rzk/VSCode/Handlers.hs
+++ b/rzk/src/Language/Rzk/VSCode/Handlers.hs
@@ -1,10 +1,12 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# LANGUAGE CPP           #-}
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications    #-}
-{-# OPTIONS_GHC -Wno-orphans #-}
-{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns        #-}
+{-# LANGUAGE RecordWildCards     #-}
 
 module Language.Rzk.VSCode.Handlers (
   typecheckFromConfigFile,
@@ -40,6 +42,7 @@ import           Language.LSP.VFS              (virtualFileText)
 import           System.FilePath               (makeRelative, (</>))
 import           System.FilePath.Glob          (compile, globDir)
 
+import           Data.Char                     (isDigit)
 import           Language.Rzk.Free.Syntax      (RzkPosition (RzkPosition),
                                                 VarIdent (getVarIdent))
 import           Language.Rzk.Syntax           (Module, VarIdent' (VarIdent),
@@ -53,6 +56,7 @@ import           Rzk.Format                    (FormattingEdit (..),
                                                 formatTextEdits)
 import           Rzk.Project.Config            (ProjectConfig (include))
 import           Rzk.TypeCheck
+import           Text.Read                     (readMaybe)
 
 -- | Given a list of file paths, reads them and parses them as Rzk modules,
 --   returning the same list of file paths but with the parsed module (or parse error)
@@ -181,7 +185,7 @@ typecheckFromConfigFile = do
         line = fromIntegral $ fromMaybe 0 $ extractLineNumber err
 
     diagnosticOfParseError :: String -> Diagnostic
-    diagnosticOfParseError err = Diagnostic (Range (Position 0 0) (Position 0 0))
+    diagnosticOfParseError err = Diagnostic (Range (Position errLine errColumnStart) (Position errLine errColumnEnd))
                       (Just DiagnosticSeverity_Error)
                       (Just $ InR "parse-error")
                       Nothing
@@ -190,6 +194,27 @@ typecheckFromConfigFile = do
                       Nothing
                       (Just [])
                       Nothing
+      where
+        (errLine, errColumnStart, errColumnEnd) = fromMaybe (0, 0, 0) $
+          case words err of
+            -- Happy parse error
+            (take 9 -> ["syntax", "error", "at", "line", lineStr, "column", columnStr, "before", token]) -> do
+              line <- readMaybe (takeWhile isDigit lineStr)
+              columnStart <- readMaybe (takeWhile isDigit columnStr)
+              return (line - 1, columnStart - 1, columnStart + fromIntegral (length token) - 3)
+            -- Happy parse error due to lexer error
+            (take 7 -> ["syntax", "error", "at", "line", lineStr, "column", columnStr]) -> do
+              line <- readMaybe (takeWhile isDigit lineStr)
+              columnStart <- readMaybe (takeWhile isDigit columnStr)
+              return (line - 1, columnStart - 1, columnStart - 1)
+            -- BNFC layout resolver error
+            (take 14 -> ["Layout", "error", "at", "line", _lineStr, "column", _columnStr, "found", token, "at", "line", lineStr', "column", columnStr']) -> do
+              -- line <- readMaybe (takeWhile isDigit lineStr)
+              -- columnStart <- readMaybe (takeWhile isDigit columnStr)
+              line' <- readMaybe (takeWhile isDigit lineStr')
+              columnStart' <- readMaybe (takeWhile isDigit columnStr')
+              return (line' - 1, columnStart', columnStart' + fromIntegral (length token) - 2)
+            _ -> Nothing
 
 instance Default T.Text where def = ""
 instance Default CompletionItem
@@ -220,7 +245,7 @@ provideCompletions req res = do
     declsToItems :: FilePath -> (FilePath, [Decl']) -> [CompletionItem]
     declsToItems root (path, decls) = map (declToItem root path) decls
     declToItem :: FilePath -> FilePath -> Decl' -> CompletionItem
-    declToItem rootDir path (Decl name type' _ _ _) = def
+    declToItem rootDir path (Decl name type' _ _ _ _loc) = def
       & label .~ T.pack (printTree $ getVarIdent name)
       & detail ?~ T.pack (show type')
       & documentation ?~ InR (MarkupContent MarkupKind_Markdown $ T.pack $
@@ -255,7 +280,11 @@ formatDocument req res = do
         let edits = formatTextEdits (filter (/= '\r') $ T.unpack sourceCode)
         return (Right $ map formattingEditToTextEdit edits)
     case possibleEdits of
+#if MIN_VERSION_lsp(2,7,0)
+      Left err    -> res $ Left $ TResponseError (InR ErrorCodes_InternalError) err Nothing
+#else
       Left err    -> res $ Left $ ResponseError (InR ErrorCodes_InternalError) err Nothing
+#endif
       Right edits -> do
         res $ Right $ InL edits
   else do
diff --git a/rzk/src/Language/Rzk/VSCode/Tokenize.hs b/rzk/src/Language/Rzk/VSCode/Tokenize.hs
index 0a60bdee1..5de819e4b 100644
--- a/rzk/src/Language/Rzk/VSCode/Tokenize.hs
+++ b/rzk/src/Language/Rzk/VSCode/Tokenize.hs
@@ -63,6 +63,7 @@ tokenizePattern = \case
   PatternVar _loc var    -> mkToken var SemanticTokenTypes_Parameter [SemanticTokenModifiers_Declaration]
   PatternPair _loc l r   -> foldMap tokenizePattern [l, r]
   pat@(PatternUnit _loc) -> mkToken pat SemanticTokenTypes_EnumMember [SemanticTokenModifiers_Declaration]
+  PatternTuple _loc p1 p2 ps -> foldMap tokenizePattern (p1 : p2 : ps)
 
 tokenizeTope :: Term -> [SemanticTokenAbsolute]
 tokenizeTope = tokenizeTerm' (Just SemanticTokenTypes_String)
@@ -125,8 +126,17 @@ tokenizeTerm' varTokenType = go
         [ mkToken (VarIdent loc "Sigma") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]
         , tokenizePattern pat
         , foldMap go [a, b] ]
+      TypeSigmaTuple loc p ps tN -> concat 
+        [ mkToken (VarIdent loc "∑") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]
+        , foldMap tokenizeSigmaParam (p : ps)
+        , go tN ]
+      ASCII_TypeSigmaTuple loc p ps tN -> concat 
+        [ mkToken (VarIdent loc "Sigma") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]
+        , foldMap tokenizeSigmaParam (p : ps)
+        , go tN ]
       TypeId _loc x a y -> foldMap go [x, a, y]
       TypeIdSimple _loc x y -> foldMap go [x, y]
+        
 
       TypeRestricted _loc type_ rs -> concat
         [ go type_
@@ -139,6 +149,7 @@ tokenizeTerm' varTokenType = go
       ASCII_Lambda loc params body -> go (Lambda loc params body)
 
       Pair _loc l r -> foldMap go [l, r]
+      Tuple _loc p1 p2 ps -> foldMap go (p1:p2:ps)
       First loc t -> concat
         [ mkToken (VarIdent loc "π₁") SemanticTokenTypes_Function [SemanticTokenModifiers_DefaultLibrary]
         , go t ]
@@ -201,6 +212,11 @@ tokenizeParamDecl = \case
     , tokenizeTope tope
     ]
 
+tokenizeSigmaParam :: SigmaParam -> [SemanticTokenAbsolute]
+tokenizeSigmaParam (SigmaParam _loc pat type_) = concat 
+  [ tokenizePattern pat 
+  , tokenizeTerm type_ ]
+
 mkToken :: (HasPosition a, Print a) => a -> SemanticTokenTypes -> [SemanticTokenModifiers] -> [SemanticTokenAbsolute]
 mkToken x tokenType tokenModifiers =
   case hasPosition x of
diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs
index 027c1acd7..14d00c5e1 100644
--- a/rzk/src/Rzk/TypeCheck.hs
+++ b/rzk/src/Rzk/TypeCheck.hs
@@ -1,10 +1,10 @@
 {-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-}
-{-# LANGUAGE DeriveFoldable       #-}
-{-# LANGUAGE DeriveFunctor        #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE LambdaCase           #-}
-{-# LANGUAGE OverloadedStrings    #-}
-{-# LANGUAGE RecordWildCards      #-}
+{-# LANGUAGE DeriveFoldable    #-}
+{-# LANGUAGE DeriveFunctor     #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards   #-}
 module Rzk.TypeCheck where
 
 import           Control.Applicative      ((<|>))
@@ -45,6 +45,7 @@ data Decl var = Decl
   , declValue        :: Maybe (TermT var)
   , declIsAssumption :: Bool
   , declUsedVars     :: [var]
+  , declLocation     :: Maybe LocationInfo
   } deriving Eq
 
 type Decl' = Decl VarIdent
@@ -135,7 +136,8 @@ typecheckModule path (Rzk.Module _moduleLoc _lang commands) =
           paramDecls <- concat <$> mapM paramToParamDecl params
           ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT
           term' <- typecheck (toTerm' (addParams params term)) ty' >>= whnfT
-          let decl = Decl (varIdentAt path name) ty' (Just term') False (varIdentAt path <$> vars)
+          loc <- asks location
+          let decl = Decl (varIdentAt path name) ty' (Just term') False (varIdentAt path <$> vars) loc
           fmap (first (decl :)) $
             localDeclPrepared decl $ do
               Context{..} <- ask
@@ -154,7 +156,8 @@ typecheckModule path (Rzk.Module _moduleLoc _lang commands) =
           mapM_ checkDefinedVar (varIdentAt path <$> vars)
           paramDecls <- concat <$> mapM paramToParamDecl params
           ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT
-          let decl = Decl (varIdentAt path name) ty' Nothing False (varIdentAt path <$> vars)
+          loc <- asks location
+          let decl = Decl (varIdentAt path name) ty' Nothing False (varIdentAt path <$> vars) loc
           fmap (first (decl :)) $
             localDeclPrepared decl $
               go (i + 1) moreCommands
@@ -191,7 +194,8 @@ typecheckModule path (Rzk.Module _moduleLoc _lang commands) =
           <> " Checking #assume " <> intercalate " " [ Rzk.printTree name | name <- names ] ) $ do
         withCommand command $ do
           ty' <- typecheck (toTerm' ty) universeT
-          let decls = [ Decl (varIdentAt path name) ty' Nothing True [] | name <- names ]
+          loc <- asks location
+          let decls = [ Decl (varIdentAt path name) ty' Nothing True [] loc | name <- names ]
           fmap (first (decls <>)) $
             localDeclsPrepared decls $
               go (i + 1) moreCommands
@@ -451,14 +455,17 @@ issueWarning message = do
   trace ("Warning: " <> message) $
     return ()
 
-issueTypeError :: TypeError var -> TypeCheck var a
-issueTypeError err = do
+fromTypeError :: TypeError var -> TypeCheck var (TypeErrorInScopedContext var)
+fromTypeError err = do
   context <- ask
-  throwError $ PlainTypeError $ TypeErrorInContext
+  return $ PlainTypeError $ TypeErrorInContext
     { typeErrorError = err
     , typeErrorContext = context
     }
 
+issueTypeError :: TypeError var -> TypeCheck var a
+issueTypeError err = fromTypeError err >>= throwError
+
 panicImpossible :: String -> a
 panicImpossible msg = error $ unlines
   [ "PANIC! Impossible happened (" <> msg <> ")!"
@@ -576,7 +583,7 @@ unsafeTraceAction' n = traceAction' n . unsafeCoerce
 data LocationInfo = LocationInfo
   { locationFilePath :: Maybe FilePath
   , locationLine     :: Maybe Int
-  }
+  } deriving (Eq)
 
 data Verbosity
   = Debug
@@ -623,6 +630,7 @@ data VarInfo var = VarInfo
   , varOrig                :: Maybe VarIdent
   , varIsAssumption        :: Bool -- FIXME: perhaps, introduce something like decl kind?
   , varDeclaredAssumptions :: [var]
+  , varLocation            :: Maybe LocationInfo
   } deriving (Functor, Foldable)
 
 data Context var = Context
@@ -700,26 +708,34 @@ withSection name sectionBody =
     (decls, errs) <- sectionBody
     localDeclsPrepared decls $
       performing (ActionCloseSection name) $ do
-        (\ decls' -> (decls', errs)) <$> endSection errs
+        result <- (Right <$> endSection errs) `catchError` (return . Left)
+        case result of
+          Left err              -> return ([], errs <> [err])
+          Right (decls', errs') -> return (decls', errs')
+        -- (\ decls' -> (decls', errs)) <$> endSection errs
 
 startSection :: Maybe Rzk.SectionName -> TypeCheck VarIdent a -> TypeCheck VarIdent a
 startSection name = local $ \Context{..} -> Context
   { localScopes = ScopeInfo { scopeName = name, scopeVars = [] } : localScopes
   , .. }
 
-endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent [Decl']
+endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])
 endSection errs = askCurrentScope >>= scopeToDecls errs
 
-scopeToDecls :: Eq var => [TypeErrorInScopedContext VarIdent] -> ScopeInfo var -> TypeCheck var [Decl var]
+scopeToDecls :: Eq var => [TypeErrorInScopedContext var] -> ScopeInfo var -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var])
 scopeToDecls errs ScopeInfo{..} = do
-  decls <- collectScopeDecls errs [] scopeVars
+  (decls, errs') <- collectScopeDecls errs [] scopeVars
   -- only issue unused variable errors if there were no errors prior in the section
-  when (null errs) $ do
-    forM_ decls $ \Decl{..} -> do
-      let unusedUsedVars = declUsedVars `intersect` map fst scopeVars
-      when (not (null unusedUsedVars)) $
-        issueTypeError $ TypeErrorUnusedUsedVariables unusedUsedVars declName
-  return decls
+  -- when (null errs) $ do
+  unusedErrors <- forM decls $ \Decl{..} -> do
+    let unusedUsedVars = declUsedVars `intersect` map fst scopeVars
+    if null errs && not (null unusedUsedVars)
+      then do
+        err <- local (\c -> c { location = declLocation }) $
+          fromTypeError (TypeErrorUnusedUsedVariables unusedUsedVars declName)
+        return [err]
+      else return []
+  return (decls, errs' <> concat unusedErrors)
 
 insertExplicitAssumptionFor
   :: Eq var => var -> (var, VarInfo var) -> TermT var -> TermT var
@@ -738,6 +754,7 @@ insertExplicitAssumptionFor' a decl VarInfo{..}
       , varIsAssumption = varIsAssumption
       , varOrig = varOrig
       , varDeclaredAssumptions = varDeclaredAssumptions
+      , varLocation = varLocation
       }
 
 makeAssumptionExplicit
@@ -776,29 +793,38 @@ makeAssumptionExplicit assumption@(a, aInfo) ((x, xInfo) : xs) = do
       , varIsAssumption = varIsAssumption xInfo
       , varOrig = varOrig xInfo
       , varDeclaredAssumptions = varDeclaredAssumptions xInfo \\ [a]
+      , varLocation = varLocation xInfo
       }
     xs' = map (fmap (insertExplicitAssumptionFor' a (x, xInfo))) xs
 
-collectScopeDecls :: Eq var => [TypeErrorInScopedContext VarIdent] -> [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var [Decl var]
+collectScopeDecls :: Eq var => [TypeErrorInScopedContext var] -> [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var])
 collectScopeDecls errs recentVars (decl@(var, VarInfo{..}) : vars)
   | varIsAssumption = do
       (used, recentVars') <- makeAssumptionExplicit decl recentVars
       -- only issue unused vars error if there were no other errors previously
-      when (null errs) $ do
-        when (not used) $ do
-          issueTypeError $ TypeErrorUnusedVariable var varType
-      collectScopeDecls errs recentVars' vars
+      -- when (null errs) $ do
+      unusedErr <-
+        if null errs && not used
+          then local (\c -> c { location = varLocation }) $
+            pure <$> fromTypeError (TypeErrorUnusedVariable var varType)
+          else return []
+      collectScopeDecls (errs <> unusedErr) recentVars' vars
   | otherwise = do
       collectScopeDecls errs (decl : recentVars) vars
-collectScopeDecls _ recentVars [] = return (toDecl <$> recentVars)
+collectScopeDecls errs recentVars [] = do
+  loc <- asks location
+  return (toDecl loc <$> recentVars, errs)
   where
-    toDecl (var, VarInfo{..}) = Decl
+    toDecl loc (var, VarInfo{..}) = Decl
       { declName = var
       , declType = varType
       , declValue = varValue
       , declIsAssumption = varIsAssumption
       , declUsedVars = varDeclaredAssumptions
+      , declLocation = updatePosition (varOrig >>= fmap fst . Rzk.hasPosition . fromVarIdent) <$> loc -- FIXME
       }
+    updatePosition Nothing l       = l
+    updatePosition (Just lineNo) l = l { locationLine = Just lineNo }
 
 abstractAssumption :: Eq var => (var, VarInfo var) -> Decl var -> Decl var
 abstractAssumption (var, VarInfo{..}) Decl{..} = Decl
@@ -807,6 +833,7 @@ abstractAssumption (var, VarInfo{..}) Decl{..} = Decl
   , declValue = (\body -> lambdaT newDeclType varOrig Nothing (abstract var body)) <$> declValue
   , declIsAssumption = declIsAssumption
   , declUsedVars = declUsedVars
+  , declLocation = declLocation
   }
   where
     newDeclType = typeFunT varOrig varType Nothing (abstract var declType)
@@ -923,13 +950,13 @@ localDeclsPrepared [] = id
 localDeclsPrepared (decl : decls) = localDeclPrepared decl . localDeclsPrepared decls
 
 localDecl :: Decl VarIdent -> TypeCheck VarIdent a -> TypeCheck VarIdent a
-localDecl (Decl x ty term isAssumption vars) tc = do
+localDecl (Decl x ty term isAssumption vars loc) tc = do
   ty' <- whnfT ty
   term' <- traverse whnfT term
-  localDeclPrepared (Decl x ty' term' isAssumption vars) tc
+  localDeclPrepared (Decl x ty' term' isAssumption vars loc) tc
 
 localDeclPrepared :: Decl VarIdent -> TypeCheck VarIdent a -> TypeCheck VarIdent a
-localDeclPrepared (Decl x ty term isAssumption vars) tc = do
+localDeclPrepared (Decl x ty term isAssumption vars loc) tc = do
   checkTopLevelDuplicate x
   local update tc
   where
@@ -939,6 +966,7 @@ localDeclPrepared (Decl x ty term isAssumption vars) tc = do
       , varOrig = Just x
       , varIsAssumption = isAssumption
       , varDeclaredAssumptions = vars
+      , varLocation = loc
       }
 
 type TypeCheck var = ReaderT (Context var) (Except (TypeErrorInScopedContext var))
@@ -1302,15 +1330,16 @@ switchVariance = local $ \Context{..} -> Context
       switch Contravariant = Covariant
 
 enterScopeContext :: Maybe VarIdent -> TermT var -> Context var -> Context (Inc var)
-enterScopeContext orig ty =
+enterScopeContext orig ty context =
   addVarInCurrentScope Z VarInfo
     { varType   = S <$> ty
     , varValue  = Nothing
     , varOrig   = orig
     , varIsAssumption = False
     , varDeclaredAssumptions = []
+    , varLocation = location context
     }
-  . fmap S
+    (S <$> context)
 
 enterScope :: Maybe VarIdent -> TermT var -> TypeCheck (Inc var) b -> TypeCheck var b
 enterScope orig ty action = do
@@ -1774,7 +1803,7 @@ nfT tt = performing (ActionNF tt) $ case tt of
               []   -> nfT type_
               rs'' -> TypeRestrictedT ty <$> nfT type_ <*> pure rs''
 
-checkDefinedVar :: Eq var => var -> TypeCheck var ()
+checkDefinedVar :: VarIdent -> TypeCheck VarIdent ()
 checkDefinedVar x = asks (lookup x . varInfos) >>= \case
   Nothing  -> issueTypeError $ TypeErrorUndefined x
   Just _ty -> return ()
diff --git a/stack.yaml b/stack.yaml
index b6882cb84..4d27df183 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,3 +1,3 @@
-resolver: nightly-2023-12-08
+resolver: nightly-2024-08-17
 packages:
   - rzk
diff --git a/stack.yaml.lock b/stack.yaml.lock
index b2aeb774b..cba22ab25 100644
--- a/stack.yaml.lock
+++ b/stack.yaml.lock
@@ -6,7 +6,7 @@
 packages: []
 snapshots:
 - completed:
-    sha256: 4bd22736896cecf9e1f3f6193e82b065d06c2bf5b5ec97d0079409d6d35f1f82
-    size: 710668
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2023/12/8.yaml
-  original: nightly-2023-12-08
+    sha256: c93fb97219f317bdba82c69b4388665268c1964d9636a6ecdc9a58f8771f0bc0
+    size: 658092
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2024/8/17.yaml
+  original: nightly-2024-08-17