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