From 1625e708b18a2b3363929b48f34e8a0b07ea9cad Mon Sep 17 00:00:00 2001
From: Andrey Mokhov <andrey.mokhov@gmail.com>
Date: Sun, 24 Jun 2018 11:33:13 +0100
Subject: [PATCH] Add close

---
 src/API.agda | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/API.agda b/src/API.agda
index 659f9fe..1838152 100644
--- a/src/API.agda
+++ b/src/API.agda
@@ -60,3 +60,15 @@ biclique xs ys = connect (vertices xs) (vertices ys)
 star : ∀ {A} -> A -> List A -> Graph A
 star x ys = connect (vertex x) (vertices ys)
 
+-- Replace all overlays with connects, essentially producing something similar
+-- to a transitive closure, but not exactly it.
+-- This is a cruel function: I added it to demonstrate that from x ≡ y we cannot
+-- in general conclude that f x ≡ f y. Indeed:
+--                 x ≡ x + x
+--           close x ≡ x
+--     close (x + x) ≡ x * x
+close : ∀ {A} -> Graph A -> Graph A
+close ε       = ε
+close (v x)   = v x
+close (x + y) = x * y
+close (x * y) = x * y