Theory Transport

✐‹creator "Kevin Kappelmann"›
theory Transport
  imports
    Transport_Black_Box
    Transport_White_Box
begin

paragraph ‹Summary›
text ‹We formalise the theory for the Transport framework.
The Transport framework allows us to transport terms along (partial) Galois
connections (@{term "galois.galois_connection"}) and equivalences
(@{term "galois.galois_equivalence"}).
For details, refer to \<^cite>‹"transport"›.›


end