Fix typo

agda · Sep 7, 2024 · 96d8ccc · 96d8ccc
1 parent 4b2cafb
commit 96d8ccc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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