From f56cd9ee5f735e98aa1c3e86238d178235a8ef32 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 18:38:19 +0000 Subject: [PATCH] fix: whitespace --- src/Data/Product/Function/Dependent/Setoid.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index f7f75e3c60..32c52e5944 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/src/Data/Product/Function/Dependent/Setoid.agda @@ -97,7 +97,7 @@ module _ where module _ (I↪J : I ↪ J) where private module ItoJ = RightInverse I↪J - + equivalence-↪ : (∀ {i} → Equivalence (A atₛ (ItoJ.from i)) (B atₛ i)) → Equivalence (I ×ₛ A) (J ×ₛ B) equivalence-↪ {A = A} {B = B} A⇔B = @@ -112,7 +112,7 @@ module _ where module _ (I↠J : I ↠ J) where private module ItoJ = Surjection I↠J - + equivalence-↠ : (∀ {x} → Equivalence (A atₛ x) (B atₛ (ItoJ.to x))) → Equivalence (I ×ₛ A) (J ×ₛ B) equivalence-↠ {A = A} {B = B} A⇔B = equivalence (↠⇒⇔ I↠J) B-to B-from