I hereby claim:
- I am jmchapman on github.
- I am jmchapman (https://keybase.io/jmchapman) on keybase.
- I have a public key ASAwCpkx877cthVn_DjmKwouY8nqUlX00GiQPWwwcP7V1go
To claim this, I am signing this object:
I hereby claim:
To claim this, I am signing this object:
{-# OPTIONS --type-in-type #-} | |
module _ where | |
open import Relation.Binary.HeterogeneousEquality | |
open ≅-Reasoning renaming (begin_ to proof_) | |
open import Function | |
record Group : Set₁ where | |
field G : Set | |
e : G |