diff --git a/src/strict-positivity.md b/src/strict-positivity.md
index 9855532..fb4f141 100644
--- a/src/strict-positivity.md
+++ b/src/strict-positivity.md
@@ -10,7 +10,7 @@ Inductive bad := r (c : bad -> nat).
 ```agda
 -- rejected by Agda
 data Bad : Set where
-  r : (Bad → ℕ) → Curry
+  r : (Bad → ℕ) → Bad
 ```
 
 Here, the type `bad` is defined recursively as consisting of a
@@ -157,4 +157,4 @@ three are necessary:
 
 [^abel]: Section 7.1 of [A Semantic Analysis of Structural Recursion](http://www.cs.cmu.edu/~abel/publications.html), Andreas Abel (1999)
 
-[^blanqui]: [Inductive types in the Calculus of Algebraic Constructions](https://arxiv.org/abs/cs/0610070), Frédéric Blanqui (2006)
\ No newline at end of file
+[^blanqui]: [Inductive types in the Calculus of Algebraic Constructions](https://arxiv.org/abs/cs/0610070), Frédéric Blanqui (2006)