Skip to content

Commit

Permalink
fix: whitespace
Browse files Browse the repository at this point in the history
  • Loading branch information
jamesmckinna committed Jan 29, 2025
1 parent cf9c04e commit f56cd9e
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Data/Product/Function/Dependent/Setoid.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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
Expand Down

0 comments on commit f56cd9e

Please sign in to comment.