Theory Transport_Compositions_Agree
theory Transport_Compositions_Agree
imports
Transport_Compositions_Agree_Galois_Equivalence
Transport_Compositions_Agree_Galois_Relator
Transport_Compositions_Agree_Order_Equivalence
begin
paragraph ‹Summary›
text ‹The general - though probably not very useful - results for the
composition of transportable components under the condition of agreeing
middle relations can be found in @{locale "transport_comp_agree"}. The special
case of a coinciding middle relation can be found in
@{locale "transport_comp_same"}. The latter corresponds to the well-know result
in the literature, generalised to partial Galois connections and equivalences.›
end