major reorganization separating setoid material

[williamdemeo]

• move Algebra.Products to Products.Basic
• move products of algebras over setoids from Algebra.Setoid to new module Products.Setoid
• move Algebra.Congruences to Congruences.Basic
• move congruences of algebras over setoids from Algebra.Setoid to new module Congruences.Setoid
• implement homomorphisms for algebras over setoids
• refactor to accommodate the above changes and
• make sure it all works by type checking the documentation modules:
  • UniversalAlgebra.lagda
  • agda-algebras-everything.lagda
• make some cosmetic improvements along the way (sorry)

[JacquesCarette]

What I mean is, that piece of code does not seem changed on what I can see in the PR on github. Did you forget to add/commit/push some of your work?

[williamdemeo]

I believe Homomorphisms/Setoid.lagda is changed so that HomFactorEpi no longer uses funext (though it still uses swelldef).