diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 054a8c493e..93c23f6fe7 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -76,11 +76,11 @@ jobs:
           if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
              || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
-            echo "AGDA_COMMIT=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=18cc53941e924b144c0f1f3953280ef726009f7e" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
           else
             # Pick Agda version for master
-            echo "AGDA_COMMIT=tags/v2.6.4.3" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=tags/v2.7.0" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}"
           fi
 
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3eebef2bca..e45653321e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,7 +1,7 @@
 Version 2.2-dev
 ===============
 
-The library has been tested using Agda 2.6.4.3.
+The library has been tested using Agda 2.7.0.
 
 Highlights
 ----------
diff --git a/CHANGELOG/v2.1.1.md b/CHANGELOG/v2.1.1.md
new file mode 100644
index 0000000000..a6e081a55b
--- /dev/null
+++ b/CHANGELOG/v2.1.1.md
@@ -0,0 +1,8 @@
+Version 2.1.1
+=============
+
+The library has been tested using Agda 2.7.0.
+
+* Fixed `Reflection.AST.Definition` to take into account Agda now exposes a `Quantity` argument on the reflection `constructor` constructor.
+
+* In `Reflection.AST.Show` added new function `showQuantity`
diff --git a/CITATION.cff b/CITATION.cff
index 96507925e9..d24084c327 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -3,6 +3,6 @@ message: "If you use this software, please cite it as below."
 authors:
 - name: "The Agda Community"
 title: "Agda Standard Library"
-version: 2.1
-date-released: 2024-07-17
+version: 2.1.1
+date-released: 2024-09-07
 url: "https://github.com/agda/agda-stdlib"
\ No newline at end of file
diff --git a/doc/README.agda b/doc/README.agda
index 6a9a3e398c..844d531899 100644
--- a/doc/README.agda
+++ b/doc/README.agda
@@ -3,7 +3,7 @@
 module README where
 
 ------------------------------------------------------------------------
--- The Agda standard library, version 2.0
+-- The Agda standard library, version 2.1.1
 --
 -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
 -- with contributions from Andreas Abel, Stevan Andjelkovic,
@@ -19,7 +19,7 @@ module README where
 -- and other anonymous contributors.
 ------------------------------------------------------------------------
 
--- This version of the library has been tested using Agda 2.6.4.
+-- This version of the library has been tested using Agda 2.7.0
 
 -- The library comes with a .agda-lib file, for use with the library
 -- management system.
diff --git a/doc/installation-guide.md b/doc/installation-guide.md
index 893753932d..d06cec93e1 100644
--- a/doc/installation-guide.md
+++ b/doc/installation-guide.md
@@ -3,19 +3,19 @@ Installation instructions
 
 Note: the full story on installing Agda libraries can be found at [readthedocs](http://agda.readthedocs.io/en/latest/tools/package-system.html).
 
-Use version v2.1 of the standard library with Agda 2.6.4.X. You can find the correct version of the library to use for different Agda versions on the [Agda Wiki](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary).
+Use version v2.1.1 of the standard library with Agda 2.7.0. You can find the correct version of the library to use for different Agda versions on the [Agda Wiki](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary).
 
 1. Navigate to a suitable directory `$HERE` (replace appropriately) where
    you would like to install the library.
 
-2. Download the tarball of v2.1 of the standard library. This can either be
+2. Download the tarball of v2.1.1 of the standard library. This can either be
    done manually by visiting the Github repository for the library, or via the
    command line as follows:
    ```
-   wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v2.1.tar.gz
+   wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v2.1.1.tar.gz
    ```
    Note that you can replace `wget` with other popular tools such as `curl` and that
-   you can replace `2.1` with any other version of the library you desire.
+   you can replace `2.1.1` with any other version of the library you desire.
 
 3. Extract the standard library from the tarball. Again this can either be
    done manually or via the command line as follows:
@@ -26,7 +26,7 @@ Use version v2.1 of the standard library with Agda 2.6.4.X. You can find the cor
 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run
    the commands to install via cabal:
    ```
-   cd agda-stdlib-2.1
+   cd agda-stdlib-2.1.1
    cabal install
    ```
 
@@ -40,7 +40,7 @@ Use version v2.1 of the standard library with Agda 2.6.4.X. You can find the cor
 6. Register the standard library with Agda's package system by adding
    the following line to `$HOME/.agda/libraries`:
    ```
-   $HERE/agda-stdlib-2.1/standard-library.agda-lib
+   $HERE/agda-stdlib-2.1.1/standard-library.agda-lib
    ```
 
 Now, the standard library is ready to be used either:
diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 3f06fef070..45fc85a00f 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -15,12 +15,13 @@ open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_;
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 
-import Reflection.AST.Argument as Arg
-import Reflection.AST.Name     as Name
-import Reflection.AST.Term     as Term
+import Reflection.AST.Argument          as Arg
+import Reflection.AST.Argument.Quantity as Quantity
+import Reflection.AST.Name              as Name
+import Reflection.AST.Term              as Term
 
 ------------------------------------------------------------------------
--- Re-exporting type publically
+-- Re-exporting type publicly
 
 open import Agda.Builtin.Reflection public
   using    ( Definition
@@ -56,8 +57,14 @@ record′-injective₂ refl = refl
 record′-injective : ∀ {c c′ fs fs′} → record′ c fs ≡ record′ c′ fs′ → c ≡ c′ × fs ≡ fs′
 record′-injective = < record′-injective₁ , record′-injective₂ >
 
-constructor′-injective : ∀ {c c′} → constructor′ c ≡ constructor′ c′ → c ≡ c′
-constructor′-injective refl = refl
+constructor′-injective₁ : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → c ≡ c′
+constructor′-injective₁ refl = refl
+
+constructor′-injective₂ : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → q ≡ q′
+constructor′-injective₂ refl = refl
+
+constructor′-injective : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → c ≡ c′ × q ≡ q′
+constructor′-injective = < constructor′-injective₁ , constructor′-injective₂ >
 
 infix 4 _≟_
 
@@ -70,39 +77,40 @@ data-type pars cs ≟ data-type pars′ cs′ =
 record′ c fs      ≟ record′ c′ fs′      =
   map′ (uncurry (cong₂ record′)) record′-injective
            (c Name.≟ c′ ×-dec List.≡-dec (Arg.≡-dec Name._≟_) fs fs′)
-constructor′ d    ≟ constructor′ d′     =
-  map′ (cong constructor′) constructor′-injective (d Name.≟ d′)
+constructor′ d q  ≟ constructor′ d′ q′  =
+  map′ (uncurry (cong₂ constructor′)) constructor′-injective
+           (d Name.≟ d′ ×-dec q Quantity.≟ q′)
 axiom             ≟ axiom               = yes refl
 primitive′        ≟ primitive′          = yes refl
 
 -- antidiagonal
 function cs ≟ data-type pars cs₁ = no (λ ())
 function cs ≟ record′ c fs = no (λ ())
-function cs ≟ constructor′ d = no (λ ())
+function cs ≟ constructor′ d q = no (λ ())
 function cs ≟ axiom = no (λ ())
 function cs ≟ primitive′ = no (λ ())
 data-type pars cs ≟ function cs₁ = no (λ ())
 data-type pars cs ≟ record′ c fs = no (λ ())
-data-type pars cs ≟ constructor′ d = no (λ ())
+data-type pars cs ≟ constructor′ d q = no (λ ())
 data-type pars cs ≟ axiom = no (λ ())
 data-type pars cs ≟ primitive′ = no (λ ())
 record′ c fs ≟ function cs = no (λ ())
 record′ c fs ≟ data-type pars cs = no (λ ())
-record′ c fs ≟ constructor′ d = no (λ ())
+record′ c fs ≟ constructor′ d q = no (λ ())
 record′ c fs ≟ axiom = no (λ ())
 record′ c fs ≟ primitive′ = no (λ ())
-constructor′ d ≟ function cs = no (λ ())
-constructor′ d ≟ data-type pars cs = no (λ ())
-constructor′ d ≟ record′ c fs = no (λ ())
-constructor′ d ≟ axiom = no (λ ())
-constructor′ d ≟ primitive′ = no (λ ())
+constructor′ d q ≟ function cs = no (λ ())
+constructor′ d q ≟ data-type pars cs = no (λ ())
+constructor′ d q ≟ record′ c fs = no (λ ())
+constructor′ d q ≟ axiom = no (λ ())
+constructor′ d q ≟ primitive′ = no (λ ())
 axiom ≟ function cs = no (λ ())
 axiom ≟ data-type pars cs = no (λ ())
 axiom ≟ record′ c fs = no (λ ())
-axiom ≟ constructor′ d = no (λ ())
+axiom ≟ constructor′ d q = no (λ ())
 axiom ≟ primitive′ = no (λ ())
 primitive′ ≟ function cs = no (λ ())
 primitive′ ≟ data-type pars cs = no (λ ())
 primitive′ ≟ record′ c fs = no (λ ())
-primitive′ ≟ constructor′ d = no (λ ())
+primitive′ ≟ constructor′ d q = no (λ ())
 primitive′ ≟ axiom = no (λ ())
diff --git a/src/Reflection/AST/Instances.agda b/src/Reflection/AST/Instances.agda
index cb7cc014d5..27a766076d 100644
--- a/src/Reflection/AST/Instances.agda
+++ b/src/Reflection/AST/Instances.agda
@@ -17,6 +17,7 @@ import Reflection.AST.Abstraction as Abstraction
 import Reflection.AST.Argument as Argument
 import Reflection.AST.Argument.Visibility as Visibility
 import Reflection.AST.Argument.Relevance as Relevance
+import Reflection.AST.Argument.Quantity as Quantity
 import Reflection.AST.Argument.Information as Information
 import Reflection.AST.Pattern as Pattern
 import Reflection.AST.Term as Term
@@ -37,6 +38,7 @@ instance
   Meta-≡-isDecEquivalence = isDecEquivalence Meta._≟_
   Visibility-≡-isDecEquivalence = isDecEquivalence Visibility._≟_
   Relevance-≡-isDecEquivalence = isDecEquivalence Relevance._≟_
+  Quantity-≡-isDecEquivalence = isDecEquivalence Quantity._≟_
   ArgInfo-≡-isDecEquivalence = isDecEquivalence Information._≟_
   Pattern-≡-isDecEquivalence = isDecEquivalence Pattern._≟_
   Clause-≡-isDecEquivalence = isDecEquivalence Term._≟-Clause_
diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda
index a9de9a2993..8757e3aef1 100644
--- a/src/Reflection/AST/Show.agda
+++ b/src/Reflection/AST/Show.agda
@@ -24,6 +24,7 @@ open import Relation.Nullary.Decidable.Core using (yes; no)
 
 open import Reflection.AST.Abstraction hiding (map)
 open import Reflection.AST.Argument hiding (map)
+open import Reflection.AST.Argument.Quantity
 open import Reflection.AST.Argument.Relevance
 open import Reflection.AST.Argument.Visibility
 open import Reflection.AST.Argument.Modality
@@ -58,6 +59,10 @@ showVisibility visible   = "visible"
 showVisibility hidden    = "hidden"
 showVisibility instance′ = "instance"
 
+showQuantity : Quantity → String
+showQuantity quantity-0 = "quantity-0"
+showQuantity quantity-ω = "quantity-ω"
+
 showLiteral : Literal → String
 showLiteral (nat x)    = ℕ.show x
 showLiteral (word64 x) = ℕ.show (Word64.toℕ x)
@@ -144,6 +149,6 @@ showDefinition (data-type pars cs) =
  "datatype" <+> ℕ.show pars <+> braces (intersperse ", " (map showName cs))
 showDefinition (record′ c fs)      =
  "record" <+> showName c <+> braces (intersperse ", " (map (showName ∘′ unArg) fs))
-showDefinition (constructor′ d)    = "constructor" <+> showName d
+showDefinition (constructor′ d q)  = "constructor" <+> showName d <+> showQuantity q
 showDefinition axiom               = "axiom"
 showDefinition primitive′          = "primitive"