From 96d8cccdff72a07b359a311d597bdff57b73d0ab Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Fri, 23 Feb 2024 01:41:10 +0000 Subject: [PATCH] Fix typo --- Cubical/Relation/Binary/Order/Poset/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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