Prove that epi + mono <-> isequiv

I'm not sure if hit/iso.v is the right place for this.  I'm also not
sure that HSet.v is the right place to define mono, nor why we're
calling it [epi] rather than [IsEpi], [isepi], [is_epi],
[IsEpimorphism], [isepimorphism], or [is_epimorphism].