diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -6,6 +6,14 @@
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.7.6 — 2025-08-14
+
+Minor fixes:
+
+- Support BNFC 2.9.6 (see [#201](https://github.com/rzk-lang/rzk/pull/201))
+- Fix typo in the sHoTT link (see [#194](https://github.com/rzk-lang/rzk/pull/194))
+- Fix tuple pattern syntax (see [#193](https://github.com/rzk-lang/rzk/pull/193) and [#191](https://github.com/rzk-lang/rzk/pull/191))
+
 ## v0.7.5 — 2024-08-18
 
 Minor changes:
diff --git a/grammar/Syntax.cf b/grammar/Syntax.cf
--- a/grammar/Syntax.cf
+++ b/grammar/Syntax.cf
@@ -60,8 +60,10 @@
 PatternUnit.      Pattern ::= "unit" ;
 PatternVar.       Pattern ::= VarIdent ;
 PatternPair.      Pattern ::= "(" Pattern "," Pattern ")" ;
-PatternTuple.     Pattern ::= "(" Pattern "," Pattern "," [Pattern] ")" ;
+PatternTuple.     Pattern ::= "(" Pattern "," Pattern "," [Pattern1] ")" ;
 separator nonempty Pattern "" ;
+_. Pattern1 ::= Pattern ;
+separator nonempty Pattern1 "," ;
 
 -- Parameter introduction (for lambda abstractions)
 ParamPattern.      Param ::= Pattern ;
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.24
 
--- This file has been generated from package.yaml by hpack version 0.36.0.
+-- This file has been generated from package.yaml by hpack version 0.38.0.
 --
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.7.5
+version:        0.7.6
 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,14 +13,15 @@
 bug-reports:    https://github.com/rzk-lang/rzk/issues
 author:         Nikolai Kudasov
 maintainer:     nickolay.kudasov@gmail.com
-copyright:      2023-2024 Nikolai Kudasov
+copyright:      2023-2025 Nikolai Kudasov
 license:        BSD3
 license-file:   LICENSE
 build-type:     Custom
 extra-source-files:
+    grammar/Syntax.cf
+extra-doc-files:
     README.md
     ChangeLog.md
-    grammar/Syntax.cf
 
 source-repository head
   type: git
@@ -57,6 +58,8 @@
       Paths_rzk
   hs-source-dirs:
       src
+  default-extensions:
+      DeriveDataTypeable
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
   build-tools:
       alex >=3.2.4
@@ -101,6 +104,8 @@
       Paths_rzk
   hs-source-dirs:
       app
+  default-extensions:
+      DeriveDataTypeable
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N
   build-tools:
       alex >=3.2.4
@@ -132,6 +137,8 @@
   main-is: doctests.hs
   hs-source-dirs:
       test
+  default-extensions:
+      DeriveDataTypeable
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
   build-tools:
       alex >=3.2.4
@@ -139,16 +146,16 @@
   build-tool-depends:
       BNFC:bnfc >=2.9.4.1
   build-depends:
-      Glob
-    , QuickCheck
+      Glob >=0.9.3
+    , QuickCheck >=2.14
     , array >=0.5.3.0
-    , base
+    , base >=4.11.0.0 && <5.0
     , bifunctors >=5.5.3
     , bytestring >=0.10.8.2
     , directory >=1.2.7.0
-    , doctest
+    , doctest >=0.21.0
     , mtl >=2.2.2
-    , template-haskell
+    , template-haskell >=2.14.0.0
     , text >=1.2.3.1
     , yaml >=0.11.0.0
   default-language: Haskell2010
@@ -163,6 +170,8 @@
       Paths_rzk
   hs-source-dirs:
       test
+  default-extensions:
+      DeriveDataTypeable
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N
   build-tools:
       alex >=3.2.4
diff --git a/src/Language/Rzk/Free/Syntax.hs b/src/Language/Rzk/Free/Syntax.hs
--- a/src/Language/Rzk/Free/Syntax.hs
+++ b/src/Language/Rzk/Free/Syntax.hs
@@ -341,6 +341,7 @@
       Rzk.Unit loc                        -> Rzk.PatternUnit loc
       Rzk.Var loc x                       -> Rzk.PatternVar loc x
       Rzk.Pair loc l r                    -> Rzk.PatternPair loc (ttp l) (ttp r)
+      Rzk.Tuple loc t1 t2 ts              -> Rzk.PatternTuple loc (ttp t1) (ttp t2) (map ttp ts)
       term -> error ("ERROR: expected a pattern but got\n  " ++ Rzk.printTree term)
 
 fromTerm' :: Term' -> Rzk.Term
diff --git a/src/Language/Rzk/Syntax/Abs.hs b/src/Language/Rzk/Syntax/Abs.hs
--- a/src/Language/Rzk/Syntax/Abs.hs
+++ b/src/Language/Rzk/Syntax/Abs.hs
@@ -1,6 +1,5 @@
--- File generated by the BNF Converter (bnfc 2.9.5).
+-- File generated by the BNF Converter (bnfc 2.9.6).
 
-{-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -20,28 +19,28 @@
   )
 import qualified Data.String
 
-import qualified Data.Data    as C (Data, Typeable)
+import qualified Data.Data    as C (Data)
 import qualified GHC.Generics as C (Generic)
 
 type Module = Module' BNFC'Position
 data Module' a = Module a (LanguageDecl' a) [Command' a]
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type HoleIdent = HoleIdent' BNFC'Position
 data HoleIdent' a = HoleIdent a HoleIdentToken
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type VarIdent = VarIdent' BNFC'Position
 data VarIdent' a = VarIdent a VarIdentToken
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type LanguageDecl = LanguageDecl' BNFC'Position
 data LanguageDecl' a = LanguageDecl a (Language' a)
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type Language = Language' BNFC'Position
 data Language' a = Rzk1 a
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type Command = Command' BNFC'Position
 data Command' a
@@ -56,16 +55,16 @@
     | CommandSection a (SectionName' a)
     | CommandSectionEnd a (SectionName' a)
     | CommandDefine a (VarIdent' a) (DeclUsedVars' a) [Param' 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)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type DeclUsedVars = DeclUsedVars' BNFC'Position
 data DeclUsedVars' a = DeclUsedVars a [VarIdent' a]
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type SectionName = SectionName' BNFC'Position
 data SectionName' a
     = NoSectionName a | SomeSectionName a (VarIdent' a)
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type Pattern = Pattern' BNFC'Position
 data Pattern' a
@@ -73,7 +72,7 @@
     | 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)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type Param = Param' BNFC'Position
 data Param' a
@@ -81,7 +80,7 @@
     | ParamPatternType a [Pattern' a] (Term' a)
     | ParamPatternShape a [Pattern' a] (Term' a) (Term' a)
     | ParamPatternShapeDeprecated 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)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type ParamDecl = ParamDecl' BNFC'Position
 data ParamDecl' a
@@ -90,17 +89,17 @@
     | ParamTermShape a (Term' a) (Term' a) (Term' a)
     | ParamTermTypeDeprecated a (Pattern' a) (Term' 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)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, 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)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type Restriction = Restriction' BNFC'Position
 data Restriction' a
     = Restriction a (Term' a) (Term' a)
     | ASCII_Restriction 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)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 type Term = Term' BNFC'Position
 data Term' a
@@ -160,7 +159,7 @@
     | ASCII_TypeExtensionDeprecated a (ParamDecl' a) (Term' a)
     | ASCII_First a (Term' a)
     | ASCII_Second a (Term' a)
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
 
 commandPostulateNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Command' a
 commandPostulateNoParams = \ _a x vars ty -> CommandPostulate _a x vars [] ty
@@ -196,10 +195,10 @@
 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)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Generic, Data.String.IsString)
 
 newtype HoleIdentToken = HoleIdentToken String
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Generic, Data.String.IsString)
 
 -- | Start position (line, column) of something.
 
diff --git a/src/Language/Rzk/Syntax/Layout.hs b/src/Language/Rzk/Syntax/Layout.hs
--- a/src/Language/Rzk/Syntax/Layout.hs
+++ b/src/Language/Rzk/Syntax/Layout.hs
@@ -1,6 +1,6 @@
--- File generated by the BNF Converter (bnfc 2.9.5).
+-- File generated by the BNF Converter (bnfc 2.9.6).
 
-{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE PatternGuards #-}
diff --git a/src/Language/Rzk/Syntax/Lex.x b/src/Language/Rzk/Syntax/Lex.x
--- a/src/Language/Rzk/Syntax/Lex.x
+++ b/src/Language/Rzk/Syntax/Lex.x
@@ -1,8 +1,8 @@
--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6).
 
 -- Lexer definition for use with Alex 3
 {
-{-# OPTIONS -fno-warn-incomplete-patterns #-}
+{-# OPTIONS -Wno-incomplete-patterns #-}
 {-# OPTIONS_GHC -w #-}
 
 {-# LANGUAGE PatternSynonyms #-}
@@ -19,8 +19,8 @@
 
 -- Predefined character classes
 
-$c = [A-Z\192-\221] # [\215]  -- capital isolatin1 letter (215 = \times) FIXME
-$s = [a-z\222-\255] # [\247]  -- small   isolatin1 letter (247 = \div  ) FIXME
+$c = [A-Z\192-\222] # [\215]  -- capital isolatin1 letter (215 = \times)
+$s = [a-z\223-\255] # [\247]  -- small   isolatin1 letter (247 = \div  )
 $l = [$c $s]         -- letter
 $d = [0-9]           -- digit
 $i = [$l $d _ ']     -- identifier character
diff --git a/src/Language/Rzk/Syntax/Par.y b/src/Language/Rzk/Syntax/Par.y
--- a/src/Language/Rzk/Syntax/Par.y
+++ b/src/Language/Rzk/Syntax/Par.y
@@ -1,8 +1,8 @@
--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6).
 
 -- Parser definition for use with Happy
 {
-{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
 {-# LANGUAGE PatternSynonyms #-}
 
 module Language.Rzk.Syntax.Par
@@ -20,6 +20,8 @@
   , pSectionName
   , pPattern
   , pListPattern
+  , pPattern1
+  , pListPattern1
   , pParam
   , pListParam
   , pParamDecl
@@ -57,6 +59,8 @@
 %name pSectionName_internal SectionName
 %name pPattern_internal Pattern
 %name pListPattern_internal ListPattern
+%name pPattern1_internal Pattern1
+%name pListPattern1_internal ListPattern1
 %name pParam_internal Param
 %name pListParam_internal ListParam
 %name pParamDecl_internal ParamDecl
@@ -234,13 +238,21 @@
   : '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)) }
+  | '(' Pattern ',' Pattern ',' ListPattern1 ')' { (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
   : Pattern { (fst $1, (:[]) (snd $1)) }
   | Pattern ListPattern { (fst $1, (:) (snd $1) (snd $2)) }
 
+Pattern1 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Pattern) }
+Pattern1 : Pattern { (fst $1, (snd $1)) }
+
+ListPattern1 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Pattern]) }
+ListPattern1
+  : Pattern1 { (fst $1, (:[]) (snd $1)) }
+  | Pattern1 ',' ListPattern1 { (fst $1, (:) (snd $1) (snd $3)) }
+
 Param :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Param) }
 Param
   : Pattern { (fst $1, Language.Rzk.Syntax.Abs.ParamPattern (fst $1) (snd $1)) }
@@ -429,6 +441,12 @@
 
 pListPattern :: [Token] -> Err [Language.Rzk.Syntax.Abs.Pattern]
 pListPattern = fmap snd . pListPattern_internal
+
+pPattern1 :: [Token] -> Err Language.Rzk.Syntax.Abs.Pattern
+pPattern1 = fmap snd . pPattern1_internal
+
+pListPattern1 :: [Token] -> Err [Language.Rzk.Syntax.Abs.Pattern]
+pListPattern1 = fmap snd . pListPattern1_internal
 
 pParam :: [Token] -> Err Language.Rzk.Syntax.Abs.Param
 pParam = fmap snd . pParam_internal
diff --git a/src/Language/Rzk/Syntax/Print.hs b/src/Language/Rzk/Syntax/Print.hs
--- a/src/Language/Rzk/Syntax/Print.hs
+++ b/src/Language/Rzk/Syntax/Print.hs
@@ -1,11 +1,8 @@
--- File generated by the BNF Converter (bnfc 2.9.5).
+-- File generated by the BNF Converter (bnfc 2.9.6).
 
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
-#if __GLASGOW_HASKELL__ <= 708
-{-# LANGUAGE OverlappingInstances #-}
-#endif
 
 -- | Pretty-printer for Language.
 
@@ -198,10 +195,12 @@
     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 ")")])
+    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 1 patterns, doc (showString ")")])
 
 instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where
   prt _ [] = concatD []
+  prt 1 [x] = concatD [prt 1 x]
+  prt 1 (x:xs) = concatD [prt 1 x, doc (showString ","), prt 1 xs]
   prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]