Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
-- This is a group with a set g, an operation *, and an identity e
record Group g ((*) : g -> g -> g) (e : g) where
constructor MkGroup
-- each of these fields provides a witness of one of the group laws
assoc : (a, b, c : g) -> (a * b) * c = a * (b * c)
ident : (a : g) -> (a * e = a, e * a = a)
inverse : (a : g) -> (b : g ** (a * b = e, b * a = e))
-- Given two groups g1 and g2, with identities e and e', e must be e'
uniquenessOfId : (g1 : Group g o e) -> (g2 : Group g o e') -> e = e'
uniquenessOfId {e} {e'} (MkGroup _ id _) (MkGroup _ id' _) =
-- these "rewrite" expressions pose that e * e' = e, and e * e' = e'
-- which lets us show that e = e'
rewrite sym (fst (id e')) in rewrite sym (snd (id' e)) in Refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.