Quotient group of a finite group

[siddhartha-gadgil]

• The main subtlety is that we cannot in general (effectively) define quotient types.
• Instead, given a group G and a subgroup H, we show that there exists a transversal, i.e., a set T intersecting each coset in a singleton.
• We get a group operation on T if H is normal.
• The main step is to show that this is a quotient in the sense that we have a quotient homomorphism with kernel H and any homomorphism from G with kernel containing H factors through the quotient.