use CongruenceQuotient to define coequalizer

[jdchristensen]

We should experiment with using CongruenceQuotient to define the coequalizer of two maps between groups. This should avoid having to deal with terms of the form -foo * bar. Given f, g : A $-> B, we probably want to define R b b' to be { a : A & f a = b * g a = b' }.

We should also delete the hypothesis in the Section defining ConguenceQuotient that asserts that the relation is an hprop, since it is never used. So we'll also avoid having strip truncations and apply tr.

Note that tensor products should simplify a bit as well.

If we do this, it's not clear whether to define the cokernel as the coequalizer against the zero map, or to keep the cokernel as the quotient by the image subgroup.

This is based on #2034 (comment)_

[jdchristensen]

I think it would also be helpful to allow a subgroup of a group to be defined with a predicate that isn't assume to take values in h-propositions. This would avoid us needing to strip_truncations and apply tr in various places, and would mean that we don't need a separate ab_cokernel_embedding.

[jdchristensen]

We should also delete the hypothesis in the Section defining ConguenceQuotient that asserts that the relation is an hprop, since it is never used

#2057 does this.

So we'll also avoid having strip truncations and apply tr.

#2057 alone doesn't simplify anything else, since those section variables were ignored. What would help would be to directly define coequalizers as the quotient by a non-truncated congruence relations, and to define the quotient of a group by a not-necessarily truncated subgroup.

[Alizter]

@jdchristensen I've tried formalising this, but I don't follow your idea for the relation R. You've written { a : A & f a = b * g a = b' } but I don't see how this relation is supposed to be reflexive.

[Alizter]

It seems to me, that we should really be using f a - g a = b - b'. This is a congruence, but this has the same issues that we were trying to avoid in the first place.

[jdchristensen]

@Alizter I think you're right. Would it help things if we wrote it as f a + b' = g a + b, so it's fairly symmetric and avoids negation?

[Alizter]

That appears to have worked, but I have yet to see if it offers any simplifications elsewhere.

[jdchristensen]

I guess we'll at least save having to strip truncations and apply tr, since the predicate is not truncated. But we could also achieve that by allowing (some) subgroups to be specified by an untruncated predicate. Maybe some other algebra is simplified as well?

[Alizter]

@jdchristensen I've created a PR if you would like to take a closer look. #2060

[jdchristensen]

The work in #2060 seems to have shown that this idea adds some complication without saving any work elsewhere, so I'm going to close this issue. @Alizter should probably close #2060 without merging.