Closed redxaxder closed 5 years ago
The universal property of free groups is that any function f from the underlying set a into some group b induces a (unique) group homomorphism phi from the free group to b which satisfies
f
a
b
phi
phi <<< free = f
This is a construction of the induced map.
This is worth including because there is currently no eliminator for FreeGroup other than pattern matching.
FreeGroup
I will release this shortly. I'm needing to install purescript on my machine.
Ok, all published :-)
The universal property of free groups is that any function
f
from the underlying seta
into some groupb
induces a (unique) group homomorphismphi
from the free group tob
which satisfiesphi <<< free = f
This is a construction of the induced map.