diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 7cb403fb49..3d9674ce09 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -15,9 +15,10 @@ open import Relation.Nullary.Decidable            using (map′; _×-dec_; yes;
 open import Relation.Binary                       using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality 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
@@ -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₂ >
 
 _≟_ : DecidableEquality Definition
 function cs       ≟ function cs′        =
@@ -67,40 +74,41 @@ data-type pars cs ≟ data-type pars′ 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"