diff --git a/Cubical/Relation/Binary/Order/Poset/Properties.agda b/Cubical/Relation/Binary/Order/Poset/Properties.agda
index 14e6702e6..62799609a 100644
--- a/Cubical/Relation/Binary/Order/Poset/Properties.agda
+++ b/Cubical/Relation/Binary/Order/Poset/Properties.agda
@@ -623,7 +623,7 @@ module _
                                       MeetDistLJoin≃JoinDistLMeet ∙ₑ
                                       JoinDistLMeet≃JoinDistRMeet
 
-        -- Since all of those varieties of distributivity are equivalent, we say that MeetDistLJoin is are canonical version of distributivity
+        -- Since all of those varieties of distributivity are equivalent, we say that MeetDistLJoin is our canonical version of distributivity
         isDistributive : Type ℓ
         isDistributive = MeetDistLJoin