From c701e6c51faf237dfbd097a81b7a08c92ea1f242 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Fri, 29 Jul 2016 11:47:51 -0700
Subject: Add HProp, Isomorphism

---
 src/Util/Isomorphism.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 src/Util/Isomorphism.v

(limited to 'src/Util/Isomorphism.v')

diff --git a/src/Util/Isomorphism.v b/src/Util/Isomorphism.v
new file mode 100644
index 000000000..a02afc3bf
--- /dev/null
+++ b/src/Util/Isomorphism.v
@@ -0,0 +1,4 @@
+Record IsIso {A B} (f : A -> B) :=
+  { iso_inv : B -> A;
+    is_right_inv : forall x, f (iso_inv x) = x;
+    is_left_inv : forall x, iso_inv (f x) = x }.
-- 
cgit v1.2.3