✐‹creator "Kevin Kappelmann"› theory Transport imports Transport_Bijections Transport_Compositions Transport_Functions Transport_Identity 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