diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 7cb403fb49..887063d643 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -8,14 +8,15 @@
 
 module Reflection.AST.Definition where
 
-import Data.List.Properties as Listₚ              using (≡-dec)
-import Data.Nat.Properties as ℕₚ                 using (_≟_)
-open import Data.Product                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable            using (map′; _×-dec_; yes; no)
-open import Relation.Binary                       using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+import Data.List.Properties as List                    using (≡-dec)
+import Data.Nat.Properties as ℕ                        using (_≟_)
+open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
+open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_; yes; no)
+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.Argument.Quantity as Quantity
 import Reflection.AST.Name     as Name
 import Reflection.AST.Term     as Term
 
@@ -56,51 +57,59 @@ 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 _≟_
 
 _≟_ : DecidableEquality Definition
 function cs       ≟ function cs′        =
   map′ (cong function) function-injective (cs Term.≟-Clauses cs′)
 data-type pars cs ≟ data-type pars′ cs′ =
   map′ (uncurry (cong₂ data-type)) data-type-injective
-           (pars ℕₚ.≟ pars′ ×-dec Listₚ.≡-dec Name._≟_ cs cs′)
+           (pars ℕ.≟ pars′ ×-dec List.≡-dec Name._≟_ cs 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′)
+           (c Name.≟ c′ ×-dec List.≡-dec (Arg.≡-dec Name._≟_) fs fs′)
+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/Show.agda b/src/Reflection/AST/Show.agda
index ffe97352f4..7630416d5d 100644
--- a/src/Reflection/AST/Show.agda
+++ b/src/Reflection/AST/Show.agda
@@ -27,6 +27,7 @@ open import Reflection.AST.Argument hiding (map)
 open import Reflection.AST.Argument.Relevance
 open import Reflection.AST.Argument.Visibility
 open import Reflection.AST.Argument.Modality
+open import Reflection.AST.Argument.Quantity
 open import Reflection.AST.Argument.Information
 open import Reflection.AST.Definition
 open import Reflection.AST.Literal
@@ -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 (Word.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"