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

Add isomorphism_ap.

Browse source
This commit is contained in:
favonia 2017-06-06 12:33:22 -06:00
parent 7125413a9a
commit d014e50cd7
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
move_to_lib.hlean
View file

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