diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex
index f510cda..9aa28fe 100644
--- a/src/ActorMonad.lagda.tex
+++ b/src/ActorMonad.lagda.tex
@@ -375,14 +375,13 @@
 Agda implements a sort of subtyping for sizes,
 so computations of different sizes can still be composed via bind.
 
-We don't give the constructors \AgdaRef[ActorMonad]{Return} and \AgdaRef[ActorMonad]{_∞>>=_}
+We don't give the constructors \AgdaRef[ActorMonad]{Return} and \AgdaInductiveConstructor{∞>>=}
 the names return and >>=,
 since we want those names to refer to the type \AgdaRef[ActorMonad]{∞ActorM}.
 Instead, the actual return and >>= are defined as a separate functions
-that wrap \AgdaRef[ActorMonad]{Return} and \AgdaRef[ActorMonad]{_∞>>=_}.
+that wrap \AgdaRef[ActorMonad]{Return} and \AgdaInductiveConstructor{∞>>=}.
 
 \AgdaTarget{Return}
-\AgdaTarget{_∞>>=_}
 \begin{code}
   Return : ∀ {A post} → (val : A) → ActorM i IS A (post val) post
   _∞>>=_ : ∀ {A B pre mid post} → (m : ∞ActorM i IS A pre mid) →
diff --git a/src/Examples/Types.lagda.tex b/src/Examples/Types.lagda.tex
index cae822e..3bf9a41 100644
--- a/src/Examples/Types.lagda.tex
+++ b/src/Examples/Types.lagda.tex
@@ -16,8 +16,10 @@
 data _≡_ {a} {A : Set a} (x : A) : A → Set a where
   refl : x ≡ x
 
-trivial = 4 ≡ 4
-definitional = (2 + 2) ≡ 4
+trivial : 4 ≡ 4
+trivial = refl
+definitional : (2 + 2) ≡ 4
+definitional = refl
 \end{code}
 %</PropositionalEquality>