From 6fa2fa6ac598abe06cd0122a1ff2037d9d5efcdb Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Sun, 8 Sep 2024 22:52:53 +0000 Subject: [PATCH] Fix whitespace --- Cubical/Relation/Binary/Order/Poset/Subset.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Relation/Binary/Order/Poset/Subset.agda b/Cubical/Relation/Binary/Order/Poset/Subset.agda index 8a5387a6d..9153602a4 100644 --- a/Cubical/Relation/Binary/Order/Poset/Subset.agda +++ b/Cubical/Relation/Binary/Order/Poset/Subset.agda @@ -22,7 +22,7 @@ open import Cubical.Relation.Binary.Order.Poset.Properties private variable ℓ ℓ' ℓ'' ℓ''' ℓ₀ ℓ₁ : Level - + module _ (P : Poset ℓ ℓ') where