clean

agda · Sep 22, 2023 · bf2df18 · bf2df18
1 parent 75b2593
commit bf2df18
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Cubical/Foundations/HLevels/Filler.agda b/Cubical/Foundations/HLevels/Filler.agda
@@ -9,7 +9,7 @@ However, they offer some advantages:
 
 - They can exploit Agda's implicit argument inference,
   potentially sparing you from writing out all of the boundaries.
-  But don't have a high expectation, it is very likely to fail...
+  But don't have a high expectation, it's very likely to fail...
 
 -}
 {-# OPTIONS --safe #-}