From e7b64c5501e90110fb8ef5aa87346f16821f89e8 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Tue, 14 May 2019 16:46:29 +0200
Subject: [PATCH] feat(data/equiv/functor): map_equiv (#1026)

* feat(data/equiv/functor): map_equiv

* golf proofs
---
 src/data/equiv/functor.lean | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 src/data/equiv/functor.lean

diff --git a/src/data/equiv/functor.lean b/src/data/equiv/functor.lean
new file mode 100644
index 0000000000000..82c58aee97e97
--- /dev/null
+++ b/src/data/equiv/functor.lean
@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2019 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Simon Hudon
+-/
+
+import data.equiv.basic
+
+universes u v
+
+variables {α β : Type u} {f : Type u → Type v} [functor f] [is_lawful_functor f]
+open functor equiv function is_lawful_functor
+
+def functor.map_equiv (h : α ≃ β) : f α ≃ f β :=
+{ to_fun    := map h,
+  inv_fun   := map h.symm,
+  left_inv  := λ x,
+    by { rw map_map, convert is_lawful_functor.id_map x, ext a, apply symm_apply_apply },
+  right_inv := λ x,
+    by { rw map_map, convert is_lawful_functor.id_map x, ext a, apply apply_symm_apply } }