✐‹creator "Kevin Kappelmann"› theory Galois imports Galois_Equivalences Galois_Relator begin paragraph ‹Summary› text ‹We define the concept of (partial) Galois connections, Galois equivalences, and the Galois relator. For details refer to \<^cite>‹"transport"›.› end