GroupUniqueId.idr

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