Theory Transport_Compositions_Generic_Order_Equivalence

✐‹creator "Kevin Kappelmann"›
subsection ‹Order Equivalence›
theory Transport_Compositions_Generic_Order_Equivalence
  imports
    Transport_Compositions_Generic_Monotone
begin

context transport_comp
begin

context
begin

interpretation flip : transport_comp R2 L2 r2 l2 R1 L1 r1 l1  .

subsubsection ‹Unit›
paragraph ‹Inflationary›

lemma inflationary_on_in_dom_unitI:
  assumes "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and inflationary_unit1: "inflationary_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and inflationary_counit1: "inflationary_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and refl_R1: "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and inflationary_unit2: "inflationary_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and refl_L2: "reflexive_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and mono_in_dom_l1: "(in_dom (≤⇘L⇙) ⇛⇩m in_dom (≤⇘L2⇙)) l1"
  and in_codom_rel_comp_le: "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom ((≤⇘R1⇙))"
  shows "inflationary_on (in_dom (≤⇘L⇙)) (≤⇘L⇙) η"
proof (rule inflationary_onI)
  fix x assume "in_dom (≤⇘L⇙) x"
  show "x ≤⇘L⇙ η x"
  proof (rule left_relI)
    from ‹in_dom (≤⇘L⇙) x› ‹((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1› have "in_dom (≤⇘R1⇙) (l1 x)" by blast
    with refl_R1 have "l1 x ≤⇘R1⇙ l1 x" by blast
    moreover from ‹in_dom (≤⇘L⇙) x› have "in_dom (≤⇘L1⇙) x" by blast
    moreover note inflationary_unit1
    ultimately show "x ⇘L1⇙⪅ l1 x" by (intro t1.left_GaloisI) auto
    from ‹in_dom (≤⇘L⇙) x› mono_in_dom_l1 have "in_dom (≤⇘L2⇙) (l1 x)" by blast
    with inflationary_unit2 show "l1 x ≤⇘L2⇙ r2 (l x)" by auto
    show "r2 (l x) ⇘R1⇙⪅ η x"
    proof (rule flip.t2.left_GaloisI)
      from refl_L2 ‹in_dom (≤⇘L2⇙) (l1 x)› have "l1 x ≤⇘L2⇙ l1 x" by blast
      with in_codom_rel_comp_le ‹l1 x ≤⇘R1⇙ l1 x› ‹l1 x ≤⇘L2⇙ r2 (l x)›
        have "in_codom (≤⇘R1⇙) (r2 (l x))" by blast
      with ‹((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1› show "in_codom (≤⇘L1⇙) (η x)"
        by (auto intro: in_codom_if_rel_if_dep_mono_wrt_rel simp: mono_wrt_rel_eq_dep_mono_wrt_rel)
      from ‹in_codom (≤⇘R1⇙) (r2 (l x))› inflationary_counit1
        show "r2 (l x) ≤⇘R1⇙ l1 (η x)" by auto
    qed
  qed
qed

lemma inflationary_on_in_codom_unitI:
  assumes "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and inflationary_unit1: "inflationary_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and inflationary_counit1: "inflationary_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and refl_R1: "reflexive_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and inflationary_unit2: "inflationary_on (in_codom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and refl_L2: "reflexive_on (in_codom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and mono_in_codom_l1: "(in_codom (≤⇘L⇙) ⇛⇩m in_codom (≤⇘L2⇙)) l1"
  and in_codom_rel_comp_le: "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom ((≤⇘R1⇙))"
  shows "inflationary_on (in_codom (≤⇘L⇙)) (≤⇘L⇙) η"
proof (rule inflationary_onI)
  fix x assume "in_codom (≤⇘L⇙) x"
  show "x ≤⇘L⇙ η x"
  proof (rule left_relI)
    from ‹in_codom (≤⇘L⇙) x› have "in_codom (≤⇘L1⇙) x" "in_codom (≤⇘R1⇙) (l1 x)" by blast+
    with inflationary_unit1 show "x ⇘L1⇙⪅ l1 x" by (intro t1.left_GaloisI) auto
    from mono_in_codom_l1 ‹in_codom (≤⇘L⇙) x› have "in_codom (≤⇘L2⇙) (l1 x)" by blast
    with inflationary_unit2 show "l1 x ≤⇘L2⇙ r2 (l x)" by auto
    show "r2 (l x) ⇘R1⇙⪅ η x"
    proof (rule flip.t2.left_GaloisI)
      from refl_L2 ‹in_codom (≤⇘L2⇙) (l1 x)› have "l1 x ≤⇘L2⇙ l1 x" by blast
      moreover from refl_R1 ‹in_codom (≤⇘R1⇙) (l1 x)› have "l1 x ≤⇘R1⇙ l1 x" by blast
      moreover note in_codom_rel_comp_le ‹l1 x ≤⇘L2⇙ r2 (l x)›
      ultimately have "in_codom (≤⇘R1⇙) (r2 (l x))" by blast
      with ‹((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1› show "in_codom (≤⇘L1⇙) (η x)"
        by (auto intro: in_codom_if_rel_if_dep_mono_wrt_rel simp: mono_wrt_rel_eq_dep_mono_wrt_rel)
      from ‹in_codom (≤⇘R1⇙) (r2 (l x))› inflationary_counit1
        show "r2 (l x) ≤⇘R1⇙ l1 (η x)" by auto
    qed
  qed
qed

corollary inflationary_on_in_field_unitI:
  assumes "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "inflationary_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "inflationary_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "inflationary_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "reflexive_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "(in_dom (≤⇘L⇙) ⇛⇩m in_dom (≤⇘L2⇙)) l1"
  and "(in_codom (≤⇘L⇙) ⇛⇩m in_codom (≤⇘L2⇙)) l1"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom ((≤⇘R1⇙))"
  shows "inflationary_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
proof -
  from assms have "inflationary_on (in_dom (≤⇘L⇙)) (≤⇘L⇙) η"
    by (intro inflationary_on_in_dom_unitI)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)
  moreover from assms have "inflationary_on (in_codom (≤⇘L⇙)) (≤⇘L⇙) η"
    by (intro inflationary_on_in_codom_unitI)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)
  ultimately show ?thesis by (auto iff: in_field_iff_in_dom_or_in_codom)
qed


text ‹Deflationary›

lemma deflationary_on_in_dom_unitI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and refl_L1: "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and in_dom_R1_le_in_codom_R1: "in_dom (≤⇘R1⇙) ≤ in_codom (≤⇘R1⇙)"
  and deflationary_L2: "deflationary_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and refl_L2: "reflexive_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and mono_in_dom_l1: "(in_dom (≤⇘L⇙) ⇛⇩m in_dom (≤⇘L2⇙)) l1"
  and in_dom_rel_comp_le: "in_dom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_dom ((≤⇘R1⇙))"
  shows "deflationary_on (in_dom (≤⇘L⇙)) (≤⇘L⇙) η"
proof (rule deflationary_onI)
  fix x assume "in_dom (≤⇘L⇙) x"
  show "η x ≤⇘L⇙ x"
  proof (rule left_relI)
    from refl_L1 ‹in_dom (≤⇘L⇙) x› have "x ≤⇘L1⇙ x" by blast
    moreover with ‹((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1› have "l1 x ≤⇘R1⇙ l1 x" by blast
    ultimately show "l1 x ⇘R1⇙⪅ x" by auto
    from mono_in_dom_l1 ‹in_dom (≤⇘L⇙) x› have "in_dom (≤⇘L2⇙) (l1 x)" by blast
    with deflationary_L2 show "r2 (l x) ≤⇘L2⇙ l1 x" by auto
    show "η x ⇘L1⇙⪅ r2 (l x)"
    proof (rule t1.left_GaloisI)
      from refl_L2 ‹in_dom (≤⇘L2⇙) (l1 x)› have "l1 x ≤⇘L2⇙ l1 x" by blast
      with in_dom_rel_comp_le ‹r2 (l x) ≤⇘L2⇙ l1 x› ‹l1 x ≤⇘R1⇙ l1 x›
        have "in_dom (≤⇘R1⇙) (r2 (l x))" by blast
      with ‹((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1› have "in_dom (≤⇘L1⇙) (η x)"
        by (auto intro: in_dom_if_rel_if_dep_mono_wrt_rel simp: mono_wrt_rel_eq_dep_mono_wrt_rel)
      with refl_L1 show "η x ≤⇘L1⇙ r1 (r2 (l x))"
        by (auto intro: in_field_if_in_codom)
      from ‹in_dom (≤⇘R1⇙) (r2 (l x))› in_dom_R1_le_in_codom_R1
        show "in_codom (≤⇘R1⇙) (r2 (l x))" by blast
    qed
  qed
qed

lemma deflationary_on_in_codom_unitI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and refl_L1: "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and in_dom_R1_le_in_codom_R1: "in_dom (≤⇘R1⇙) ≤ in_codom (≤⇘R1⇙)"
  and deflationary_L2: "deflationary_on (in_codom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and refl_L2: "reflexive_on (in_codom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and mono_in_codom_l1: "(in_codom (≤⇘L⇙) ⇛⇩m in_codom (≤⇘L2⇙)) l1"
  and in_dom_rel_comp_le: "in_dom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_dom ((≤⇘R1⇙))"
  shows "deflationary_on (in_codom (≤⇘L⇙)) (≤⇘L⇙) η"
proof (rule deflationary_onI)
  fix x assume "in_codom (≤⇘L⇙) x"
  show "η x ≤⇘L⇙ x"
  proof (rule left_relI)
    from refl_L1 ‹in_codom (≤⇘L⇙) x› have "x ≤⇘L1⇙ x" by blast
    moreover with ‹((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1› have "l1 x ≤⇘R1⇙ l1 x" by blast
    ultimately show "l1 x ⇘R1⇙⪅ x" by auto
    from mono_in_codom_l1 ‹in_codom (≤⇘L⇙) x› have "in_codom (≤⇘L2⇙) (l1 x)" by blast
    with deflationary_L2 show "r2 (l x) ≤⇘L2⇙ l1 x" by auto
    show "η x ⇘L1⇙⪅ r2 (l x)"
    proof (rule t1.left_GaloisI)
      from refl_L2 ‹in_codom (≤⇘L2⇙) (l1 x)› have "l1 x ≤⇘L2⇙ l1 x" by blast
      with in_dom_rel_comp_le ‹r2 (l x) ≤⇘L2⇙ l1 x› ‹l1 x ≤⇘R1⇙ l1 x›
        have "in_dom (≤⇘R1⇙) (r2 (l x))" by blast
      with in_dom_R1_le_in_codom_R1 show "in_codom (≤⇘R1⇙) (r2 (l x))" by blast
      with ‹((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1› have "in_codom (≤⇘L1⇙) (η x)"
        by (auto intro: in_codom_if_rel_if_dep_mono_wrt_rel simp: mono_wrt_rel_eq_dep_mono_wrt_rel)
      with refl_L1 show "η x ≤⇘L1⇙ r1 (r2 (l x))" by auto
    qed
  qed
qed

corollary deflationary_on_in_field_unitI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "in_dom (≤⇘R1⇙) ≤ in_codom (≤⇘R1⇙)"
  and "deflationary_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "reflexive_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "(in_dom (≤⇘L⇙) ⇛⇩m in_dom (≤⇘L2⇙)) l1"
  and "(in_codom (≤⇘L⇙) ⇛⇩m in_codom (≤⇘L2⇙)) l1"
  and "in_dom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_dom ((≤⇘R1⇙))"
  shows "deflationary_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
proof -
  from assms have "deflationary_on (in_dom (≤⇘L⇙)) (≤⇘L⇙) η"
    by (intro deflationary_on_in_dom_unitI)
    (auto intro: deflationary_on_if_le_pred_if_deflationary_on
      reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)
  moreover from assms have "deflationary_on (in_codom (≤⇘L⇙)) (≤⇘L⇙) η"
    by (intro deflationary_on_in_codom_unitI)
    (auto intro: deflationary_on_if_le_pred_if_deflationary_on
      reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)
  ultimately show ?thesis by (auto iff: in_field_iff_in_dom_or_in_codom)
qed


text ‹Relational Equivalence›

corollary rel_equivalence_on_in_field_unitI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "inflationary_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "inflationary_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "rel_equivalence_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "reflexive_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "(in_dom (≤⇘L⇙) ⇛⇩m in_dom (≤⇘L2⇙)) l1"
  and "(in_codom (≤⇘L⇙) ⇛⇩m in_codom (≤⇘L2⇙)) l1"
  and "in_dom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_dom ((≤⇘R1⇙))"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom ((≤⇘R1⇙))"
  shows "rel_equivalence_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
  using assms by (intro rel_equivalence_onI
    inflationary_on_in_field_unitI deflationary_on_in_field_unitI)
  (auto simp only: in_codom_eq_in_dom_if_reflexive_on_in_field)


subsubsection ‹Counit›

text ‹Corresponding lemmas for the counit can be obtained by flipping the
interpretation of the locale, i.e.
‹
interpretation flip : transport_comp R2 L2 r2 l2 R1 L1 r1 l1
  rewrites "flip.t2.unit ≡ ε⇩1" and "flip.t2.counit ≡ η⇩1"
  and "flip.t1.unit ≡ ε⇩2" and "flip.t1.counit ≡ η⇩2"
  and "flip.unit ≡ ε" and "flip.counit ≡ η"
  unfolding transport_comp.transport_defs
  by (auto simp: order_functors.flip_counit_eq_unit)
›
›

end


subsubsection ‹Order Equivalence›

interpretation flip : transport_comp R2 L2 r2 l2 R1 L1 r1 l1
  rewrites "flip.t2.unit ≡ ε⇩1" and "flip.t2.counit ≡ η⇩1"
  and "flip.t1.unit ≡ ε⇩2" and "flip.t1.counit ≡ η⇩2"
  and "flip.counit ≡ η" and "flip.unit ≡ ε"
  by (simp_all only: order_functors.flip_counit_eq_unit)

lemma order_equivalenceI:
  assumes "((≤⇘L1⇙) ⇛⇩m (≤⇘R1⇙)) l1" "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "inflationary_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and rel_equiv_counit1: "rel_equivalence_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘R2⇙) ⇛⇩m (≤⇘L2⇙)) r2" "((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2"
  and rel_equiv_unit2: "rel_equivalence_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "inflationary_on (in_field (≤⇘R2⇙)) (≤⇘R2⇙) ε⇩2"
  and "reflexive_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "reflexive_on (in_field (≤⇘R2⇙)) (≤⇘R2⇙)"
  and middle_compatible: "middle_compatible_codom"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
proof (rule order_equivalenceI)
  show "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l" using rel_equiv_unit2 ‹((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1›
      ‹((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2› middle_compatible
    by (intro mono_wrt_rel_leftI) auto
  show "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r" using rel_equiv_counit1 ‹((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2›
      ‹((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1› middle_compatible
    by (intro flip.mono_wrt_rel_leftI)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      in_field_if_in_codom)
  from middle_compatible have in_dom_rel_comp_les:
    "in_dom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_dom (≤⇘L2⇙)"
    "in_dom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_dom ((≤⇘R1⇙))"
    by (auto intro: in_dom_right1_left2_right1_le_if_right1_left2_right1_le
      flip.in_dom_right1_left2_right1_le_if_right1_left2_right1_le)
  moreover then have "(in_dom (≤⇘L⇙) ⇛⇩m in_dom (≤⇘L2⇙)) l1"
    and "(in_codom (≤⇘L⇙) ⇛⇩m in_codom (≤⇘L2⇙)) l1"
    using ‹((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1› middle_compatible
    by (auto intro: mono_in_dom_left_rel_left1_if_in_dom_rel_comp_le
      mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le)
  ultimately show "rel_equivalence_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
    using assms by (intro rel_equivalence_on_in_field_unitI)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      intro!: in_field_if_in_codom)
  note in_dom_rel_comp_les
  moreover then have "(in_dom (≤⇘R⇙) ⇛⇩m in_dom (≤⇘R1⇙)) r2"
    and "(in_codom (≤⇘R⇙) ⇛⇩m in_codom (≤⇘R1⇙)) r2"
    using ‹((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2› middle_compatible
    by (auto intro!: flip.mono_in_dom_left_rel_left1_if_in_dom_rel_comp_le
      flip.mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le)
  ultimately show "rel_equivalence_on (in_field (≤⇘R⇙)) (≤⇘R⇙) ε"
    using assms by (intro flip.rel_equivalence_on_in_field_unitI)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      intro!: in_field_if_in_codom)
qed

corollary order_equivalence_if_order_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩o (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ≡⇩o (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘L2⇙)"
  and "reflexive_on (in_field (≤⇘R2⇙)) (≤⇘R2⇙)"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms by (intro order_equivalenceI) (auto
    elim!: t1.order_equivalenceE t2.order_equivalenceE rel_equivalence_onE
    intro!: reflexive_on_in_field_if_transitive_if_rel_equivalence_on
      t1.half_galois_prop_left_left_right_if_transitive_if_deflationary_on_if_mono_wrt_rel
      flip.t1.half_galois_prop_left_left_right_if_transitive_if_deflationary_on_if_mono_wrt_rel
    intro: deflationary_on_if_le_pred_if_deflationary_on in_field_if_in_codom)

corollary order_equivalence_if_galois_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ≡⇩G (≤⇘R2⇙)) l2 r2"
  and "reflexive_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "reflexive_on (in_field (≤⇘R2⇙)) (≤⇘R2⇙)"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms by (intro order_equivalenceI)
  (auto elim!: t1.galois_equivalenceE t2.galois_equivalenceE
    intro!: t1.inflationary_on_unit_if_reflexive_on_if_galois_equivalence
      flip.t1.inflationary_on_unit_if_reflexive_on_if_galois_equivalence
      t2.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence
      flip.t2.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence)

end


end