From db6fccc971ed0a439904eabb021fc1b1739a0d7f Mon Sep 17 00:00:00 2001
From: spiceghello <stefano.piceghello@uib.no>
Date: Thu, 8 Jun 2017 14:50:25 -0600
Subject: [PATCH] pmap_eta

---
 pointed.hlean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/pointed.hlean b/pointed.hlean
index 8f1ea82..778f3bb 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -142,5 +142,14 @@ namespace pointed
   -- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q :=
   -- sorry
 
+/- Homotopy between a function and its eta expansion -/
+
+  definition pmap_eta {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (pmap.resp_pt f) :=
+  begin
+    fapply phomotopy.mk,
+    reflexivity,
+    esimp, exact !idp_con
+  end
+
 
 end pointed