We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent cf9c04e commit f56cd9eCopy full SHA for f56cd9e
src/Data/Product/Function/Dependent/Setoid.agda
@@ -97,7 +97,7 @@ module _ where
97
module _ (I↪J : I ↪ J) where
98
99
private module ItoJ = RightInverse I↪J
100
-
+
101
equivalence-↪ : (∀ {i} → Equivalence (A atₛ (ItoJ.from i)) (B atₛ i)) →
102
Equivalence (I ×ₛ A) (J ×ₛ B)
103
equivalence-↪ {A = A} {B = B} A⇔B =
@@ -112,7 +112,7 @@ module _ where
112
module _ (I↠J : I ↠ J) where
113
114
private module ItoJ = Surjection I↠J
115
116
equivalence-↠ : (∀ {x} → Equivalence (A atₛ x) (B atₛ (ItoJ.to x))) →
117
118
equivalence-↠ {A = A} {B = B} A⇔B = equivalence (↠⇒⇔ I↠J) B-to B-from
0 commit comments