Show Universal Property

[darcs-mirror-agda-free-groups.git] / FreeGroups.agda

diff --git a/FreeGroups.agda b/FreeGroups.agda
index 6dce2b5..7aee5fe 100644 (file)
--- a/FreeGroups.agda
+++ b/FreeGroups.agda
@@ -175,4 +175,4 @@ group = record {
     inv (inv x) ++ inv x
       ≈⟨ linv (inv x) ⟩
     [] ∎
     inv (inv x) ++ inv x
       ≈⟨ linv (inv x) ⟩
     [] ∎

-    where open  Relation.Binary.EqReasoning (eqSetoid RedTo)
+    where open  Relation.Binary.EqReasoning (eqSetoid RedTo)
\ No newline at end of file