From cb3bc1a311f4d5495f2b22e1192ab528a9a19fe2 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Fri, 29 Jan 2016 15:07:39 +0000 Subject: [PATCH] feat(hott): add another constructor for pointed equivalences --- hott/types/pointed.hlean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 94c8bc7456..2111309695 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -362,6 +362,10 @@ namespace pointed pequiv A B := pequiv.mk to_pmap is_equiv_to_pmap + definition pequiv_of_equiv [constructor] + (eqv : A ≃ B) (resp : equiv.to_fun eqv (point A) = point B) : A ≃* B := + pequiv.mk' (pmap.mk (equiv.to_fun eqv) resp) + definition equiv_of_pequiv [constructor] (f : A ≃* B) : A ≃ B := equiv.mk f _