diff --git a/formalizations/guarded-cubical/Later.agda b/formalizations/guarded-cubical/Later.agda
index f41e863bea42805c8d0c63461c27a4ffb15415e4..dba75afd3a0586e47d0286776b69d62033db9a75 100644
--- a/formalizations/guarded-cubical/Later.agda
+++ b/formalizations/guarded-cubical/Later.agda
@@ -44,6 +44,7 @@ _⊛_ f x a = f a (x a)
 
 map▹ : (f : A → B) → ▹ k , A → ▹ k , B
 map▹ f x α = f (x α)
+_<$>_ = map▹
 
 -- The behaviour of fix is encoded with rewrite rules, following the
 -- definitional equalities of Clocked CTT.