From d014e50cd7b538e9ab36c69cec5417bbdcc181b0 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 12:33:22 -0600
Subject: [PATCH] Add isomorphism_ap.

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

diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 59cd841..81cabe3 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -95,6 +95,13 @@ namespace eq
 
 end eq open eq
 
+namespace group
+
+  definition isomorphism_ap (A : Type) (F : A → Group) {a b : A} (p : a = b) : F a ≃g F b :=
+    isomorphism_of_eq (ap F p)
+
+end group
+
 namespace trunc
 
   -- TODO: redefine loopn_ptrunc_pequiv