michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott): add another constructor for pointed equivalences

Browse source
This commit is contained in:
Jakob von Raumer 2016-01-29 15:07:39 +00:00 committed by Leonardo de Moura
parent 23dec19aa7
commit cb3bc1a311
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
hott/types/pointed.hlean
View file

@ -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 _