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.
Data.Sum.Algebra
1 parent 1309c75 commit 018dd40Copy full SHA for 018dd40
src/Data/Sum/Algebra.agda
@@ -71,7 +71,7 @@ module _ (ℓ : Level) where
71
72
⊎-identity : Identity _↔_ ⊥ _⊎_
73
⊎-identity = ⊎-identityˡ , ⊎-identityʳ
74
-
+
75
------------------------------------------------------------------------
76
-- Algebraic structures
77
0 commit comments