From 7940bf0cd601913a94daaccd6eaa77391c0800ab Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 16:57:17 -0600
Subject: [PATCH] Add pmap.eta.

---
 move_to_lib.hlean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 1b52a94..6944a29 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -102,6 +102,13 @@ namespace group
 
 end group
 
+namespace pmap
+
+  definition eta {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f :=
+  begin induction f, reflexivity end
+
+end pmap
+
 namespace trunc
 
   -- TODO: redefine loopn_ptrunc_pequiv