Theory Transport_Functions_Order_Equivalence

✐‹creator "Kevin Kappelmann"›
subsection ‹Order Equivalence›
theory Transport_Functions_Order_Equivalence
  imports
    Transport_Functions_Monotone
    Transport_Functions_Galois_Equivalence
begin

paragraph ‹Dependent Function Relator›

context transport_Dep_Fun_Rel
begin

subparagraph ‹Inflationary›

lemma rel_unit_self_if_rel_selfI:
  assumes inflationary_unit1: "inflationary_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and refl_L1: "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and trans_L1: "transitive (≤⇘L1⇙)"
  and mono_l2: "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘L2 x x⇙) ⇒ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙)"
  and mono_r2: "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘R2 (l1 x) (l1 x)⇙) ⇒ (≤⇘L2 x (η⇩1 x)⇙)) (r2⇘x (l1 x)⇙)"
  and inflationary_unit2: "⋀x. x ≤⇘L1⇙ x ⟹
    inflationary_on (in_codom (≤⇘L2 x x⇙)) (≤⇘L2 x x⇙) (η⇘2 x (l1 x)⇙)"
  and L2_le1: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and L2_unit_le2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and ge_R2_l2_le2: "⋀x y. x ≤⇘L1⇙ x ⟹ in_codom (≤⇘L2 x (η⇩1 x)⇙) y ⟹
    (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y) ≤ (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y)"
  and trans_L2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "f ≤⇘L⇙ f"
  shows "f ≤⇘L⇙ η f"
proof (intro left_relI)
  fix x1 x2 assume [iff]: "x1 ≤⇘L1⇙ x2"
  moreover with inflationary_unit1 have "x2 ≤⇘L1⇙ η⇩1 x2" by blast
  ultimately have "x1 ≤⇘L1⇙ η⇩1 x2" using trans_L1 by blast
  with ‹f ≤⇘L⇙ f› have "f x1 ≤⇘L2 x1 (η⇩1 x2)⇙ f (η⇩1 x2)" by blast
  with L2_unit_le2 have "f x1 ≤⇘L2 x1 x2⇙ f (η⇩1 x2)" by blast
  moreover have "... ≤⇘L2 x1 x2⇙ η f x2"
  proof -
    from refl_L1 ‹x2 ≤⇘L1⇙ η⇩1 x2› have "η⇩1 x2 ≤⇘L1⇙ η⇩1 x2" by blast
    with ‹f ≤⇘L⇙ f› have "f (η⇩1 x2) ≤⇘L2 (η⇩1 x2) (η⇩1 x2)⇙ f (η⇩1 x2)" by blast
    with L2_le1 have "f (η⇩1 x2) ≤⇘L2 x2 (η⇩1 x2)⇙ f (η⇩1 x2)"
      using ‹x2 ≤⇘L1⇙ η⇩1 x2› by blast
    moreover from refl_L1 ‹x1 ≤⇘L1⇙ x2› have [iff]: "x2 ≤⇘L1⇙ x2" by blast
    ultimately have "f (η⇩1 x2) ≤⇘L2 x2 x2⇙ f (η⇩1 x2)" using L2_unit_le2 by blast
    with inflationary_unit2 have "f (η⇩1 x2) ≤⇘L2 x2 x2⇙ η⇘2 x2 (l1 x2)⇙ (f (η⇩1 x2))" by blast
    moreover have "... ≤⇘L2 x2 x2⇙ η f x2"
    proof -
      from ‹f (η⇩1 x2) ≤⇘L2 x2 x2⇙ f (η⇩1 x2)› mono_l2
        have "l2⇘(l1 x2) x2⇙ (f (η⇩1 x2)) ≤⇘R2 (l1 x2) (l1 x2)⇙ l2⇘(l1 x2) x2⇙ (f (η⇩1 x2))"
        by blast
      with ge_R2_l2_le2
        have "l2⇘(l1 x2) x2⇙ (f (η⇩1 x2)) ≤⇘R2 (l1 x2) (l1 x2)⇙ l2⇘(l1 x2) (η⇩1 x2)⇙ (f (η⇩1 x2))"
        using ‹f (η⇩1 x2) ≤⇘L2 x2 (η⇩1 x2)⇙ f (η⇩1 x2)› by blast
      with mono_r2 have "η⇘2 x2 (l1 x2)⇙ (f (η⇩1 x2)) ≤⇘L2 x2 (η⇩1 x2)⇙ η f x2"
        by auto
      with L2_unit_le2 show ?thesis by blast
    qed
    ultimately have "f (η⇩1 x2) ≤⇘L2 x2 x2⇙ η f x2" using trans_L2 by blast
    with L2_le1 show ?thesis by blast
  qed
  ultimately show "f x1 ≤⇘L2 x1 x2⇙ η f x2" using trans_L2 by blast
qed

subparagraph ‹Deflationary›

interpretation flip_inv :
  transport_Dep_Fun_Rel "(≥⇘R1⇙)" "(≥⇘L1⇙)" r1 l1 "flip2 R2" "flip2 L2" r2 l2
  rewrites "flip_inv.L ≡ (≥⇘R⇙)" and "flip_inv.R ≡ (≥⇘L⇙)"
  and "flip_inv.unit ≡ ε"
  and "flip_inv.t1.unit ≡ ε⇩1"
  and "⋀x y. flip_inv.t2_unit x y ≡ ε⇘2 y x⇙"
  and "⋀R x y. (flip2 R x y)¯ ≡ R y x"
  and "⋀R. in_codom R¯ ≡ in_dom R"
  and "⋀R x1 x2. in_codom (flip2 R x1 x2) ≡ in_dom (R x2 x1)"
  and "⋀x1 x2 x1' x2'. (flip2 R2 x1' x2' ⇒ flip2 L2 x1 x2) ≡ ((≤⇘R2 x2' x1'⇙) ⇒ (≤⇘L2 x2 x1⇙))"
  and "⋀x1 x2 x1' x2'. (flip2 L2 x1 x2 ⇒ flip2 R2 x1' x2') ≡ ((≤⇘L2 x2 x1⇙) ⇒ (≤⇘R2 x2' x1'⇙))"
  and "⋀(R :: 'z ⇒ 'z ⇒ bool) (P :: 'z ⇒ bool).
    (inflationary_on P R¯ :: ('z ⇒ 'z) ⇒ bool) ≡ deflationary_on P R"
  and "⋀(P :: 'b2 ⇒ bool) x.
    (inflationary_on P (flip2 R2 x x) :: ('b2 ⇒ 'b2) ⇒ bool) ≡ deflationary_on P (≤⇘R2 x x⇙)"
  and "⋀x1 x2 x3 x4. flip2 R2 x1 x2 ≤ flip2 R2 x3 x4 ≡ (≤⇘R2 x2 x1⇙) ≤ (≤⇘R2 x4 x3⇙)"
  and "⋀(R :: 'z ⇒ 'z ⇒ bool) (P :: 'z ⇒ bool). reflexive_on P R¯ ≡ reflexive_on P R"
  and "⋀(R :: 'z ⇒ 'z ⇒ bool). transitive R¯ ≡ transitive R"
  and "⋀x1' x2'. transitive (flip2 R2 x1' x2') ≡ transitive (≤⇘R2 x2' x1'⇙)"
  by (simp_all add: flip_inv_left_eq_ge_right flip_inv_right_eq_ge_left
    flip_unit_eq_counit t1.flip_unit_eq_counit t2.flip_unit_eq_counit
    galois_prop.rel_inv_half_galois_prop_right_eq_half_galois_prop_left_rel_inv
    mono_wrt_rel_eq_dep_mono_wrt_rel)

lemma counit_rel_self_if_rel_selfI:
  assumes "deflationary_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "transitive (≤⇘R1⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ ((≤⇘L2 (r1 x') (r1 x')⇙) ⇒ (≤⇘R2 (ε⇩1 x') x'⇙)) (l2⇘ x' (r1 x')⇙)"
  and "⋀x' x'. x' ≤⇘R1⇙ x' ⟹ ((≤⇘R2 x' x'⇙) ⇒ (≤⇘L2 (r1 x') (r1 x')⇙)) (r2⇘(r1 x') x'⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ deflationary_on (in_dom (≤⇘R2 x' x'⇙)) (≤⇘R2 x' x'⇙) (ε⇘2 (r1 x') x'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x' y'. x' ≤⇘R1⇙ x' ⟹ in_dom (≤⇘R2 (ε⇩1 x') x'⇙) y' ⟹
    (≤⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y') ≤ (≤⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y')"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  and "g ≤⇘R⇙ g"
  shows "ε g ≤⇘R⇙ g"
  using assms by (intro flip_inv.rel_unit_self_if_rel_selfI[simplified rel_inv_iff_rel])


subparagraph ‹Relational Equivalence›

lemma bi_related_unit_self_if_rel_self_aux:
  assumes rel_equiv_unit1: "rel_equivalence_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and mono_r2: "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘R2 (l1 x) (l1 x)⇙) ⇒ (≤⇘L2 x x⇙)) (r2⇘x (l1 x)⇙)"
  and rel_equiv_unit2: "⋀x. x ≤⇘L1⇙ x ⟹
    rel_equivalence_on (in_field (≤⇘L2 x x⇙)) (≤⇘L2 x x⇙) (η⇘2 x (l1 x)⇙)"
  and L2_le1: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and L2_le2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and [iff]: "x ≤⇘L1⇙ x"
  shows "((≤⇘R2 (l1 x) (l1 x)⇙) ⇒ (≤⇘L2 x (η⇩1 x)⇙)) (r2⇘x (l1 x)⇙)"
  and "((≤⇘R2 (l1 x) (l1 x)⇙) ⇒ (≤⇘L2 (η⇩1 x) x⇙)) (r2⇘x (l1 x)⇙)"
  and "deflationary_on (in_dom (≤⇘L2 x x⇙)) (≤⇘L2 x x⇙) η⇘2 x (l1 x)⇙"
  and "inflationary_on (in_codom (≤⇘L2 x x⇙)) (≤⇘L2 x x⇙) η⇘2 x (l1 x)⇙"
proof -
  from rel_equiv_unit1 have "x ≡⇘L1⇙ η⇩1 x" by blast
  with mono_r2 show "((≤⇘R2 (l1 x) (l1 x)⇙) ⇒ (≤⇘L2 x (η⇩1 x)⇙)) (r2⇘x (l1 x)⇙)"
    and "((≤⇘R2 (l1 x) (l1 x)⇙) ⇒ (≤⇘L2 (η⇩1 x) x⇙)) (r2⇘x (l1 x)⇙)"
    using L2_le1 L2_le2 by blast+
qed (insert rel_equiv_unit2, blast+)

interpretation flip : transport_Dep_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2
  rewrites "flip.counit ≡ η" and "flip.t1.counit ≡ η⇩1"
  and "⋀x y. flip.t2_counit x y ≡ η⇘2 y x⇙"
  by (simp_all add: order_functors.flip_counit_eq_unit)

lemma bi_related_unit_self_if_rel_selfI:
  assumes rel_equiv_unit1: "rel_equivalence_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and trans_L1: "transitive (≤⇘L1⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘L2 x x⇙) ⇒ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘R2 (l1 x) (l1 x)⇙) ⇒ (≤⇘L2 x x⇙)) (r2⇘x (l1 x)⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹
    rel_equivalence_on (in_field (≤⇘L2 x x⇙)) (≤⇘L2 x x⇙) (η⇘2 x (l1 x)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 (η⇩1 x1) x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_dom (≤⇘L2 (η⇩1 x) x⇙) y ⟹
    (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y) ≤ (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_codom (≤⇘L2 x (η⇩1 x)⇙) y ⟹
    (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y) ≤ (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "f ≤⇘L⇙ f"
  shows "f ≡⇘L⇙ η f"
proof -
  from rel_equiv_unit1 trans_L1 have "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
    by (intro reflexive_on_in_field_if_transitive_if_rel_equivalence_on)
  with assms show ?thesis
    by (intro bi_relatedI rel_unit_self_if_rel_selfI
      flip.counit_rel_self_if_rel_selfI
      bi_related_unit_self_if_rel_self_aux)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      deflationary_on_if_le_pred_if_deflationary_on
      reflexive_on_if_le_pred_if_reflexive_on
      in_field_if_in_dom in_field_if_in_codom)
qed


subparagraph ‹Lemmas for Monotone Function Relator›

lemma order_equivalence_if_order_equivalence_mono_assms_leftI:
  assumes order_equiv1: "((≤⇘L1⇙) ≡⇩o (≤⇘R1⇙)) l1 r1"
  and refl_R1: "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and R2_counit_le1: "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and mono_l2: "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and [iff]: "x1' ≤⇘R1⇙ x2'"
  shows "((in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙)) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x1' (r1 x1')⇙) (l2⇘x2' (r1 x1')⇙)"
  and "((in_codom (≤⇘L2 (r1 x1') (r1 x2')⇙)) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x2' (r1 x1')⇙) (l2⇘x2' (r1 x2')⇙)"
proof -
  from refl_R1 have "x1' ≤⇘R1⇙ x1'" "x2' ≤⇘R1⇙ x2'" by auto
  moreover with order_equiv1
    have "r1 x1' ≤⇘L1⇙ r1 x2'" "r1 x1' ≤⇘L1⇙ r1 x1'" "r1 x2' ≤⇘L1⇙ r1 x2'" by auto
  ultimately have "r1 x1' ⇘L1⇙⪅ x1'" "r1 x2' ⇘L1⇙⪅ x2'" by blast+
  note Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_l2 ‹x1' ≤⇘R1⇙ x2'›]
    ‹r1 x1' ≤⇘L1⇙ r1 x1'›]
  with ‹r1 x1' ⇘L1⇙⪅ x1'› R2_counit_le1
    show "((in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙)) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x1' (r1 x1')⇙) (l2⇘x2' (r1 x1')⇙)"
    by (intro Fun_Rel_predI) (auto dest!: in_field_if_in_dom)
  note Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_l2 ‹x2' ≤⇘R1⇙ x2'›]
    ‹r1 x1' ≤⇘L1⇙ r1 x2'›]
  with ‹r1 x2' ⇘L1⇙⪅ x2'› R2_counit_le1
    show "((in_codom (≤⇘L2 (r1 x1') (r1 x2')⇙)) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x2' (r1 x1')⇙) (l2⇘x2' (r1 x2')⇙)"
    by (intro Fun_Rel_predI) (auto dest!: in_field_if_in_codom)
qed

lemma order_equivalence_if_order_equivalence_mono_assms_rightI:
  assumes order_equiv1: "((≤⇘L1⇙) ≡⇩o (≤⇘R1⇙)) l1 r1"
  and refl_L1: "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and L2_unit_le2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and mono_r2: "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and [iff]: "x1 ≤⇘L1⇙ x2"
  shows "((in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x2)⇙) (r2⇘x2 (l1 x2)⇙)"
  and "((in_dom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x1)⇙) (r2⇘x1 (l1 x2)⇙)"
proof -
  from refl_L1 have "x1 ≤⇘L1⇙ x1" "x2 ≤⇘L1⇙ x2" by auto
  moreover with order_equiv1
    have "l1 x1 ≤⇘R1⇙ l1 x2" "l1 x1 ≤⇘R1⇙ l1 x1" "l1 x2 ≤⇘R1⇙ l1 x2" by auto
  ultimately have "x1 ⇘L1⇙⪅ l1 x1" "x2 ⇘L1⇙⪅ l1 x2" using order_equiv1
    by (auto intro!: t1.left_Galois_left_if_in_codom_if_inflationary_onI)
  note Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_r2 ‹x1 ≤⇘L1⇙ x2›]
    ‹l1 x2 ≤⇘R1⇙ l1 x2›]
  with ‹x2 ⇘L1⇙⪅ l1 x2› L2_unit_le2
    show "((in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x2)⇙) (r2⇘x2 (l1 x2)⇙)"
    by (intro Fun_Rel_predI) (auto dest!: in_field_if_in_codom)
  note Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_r2 ‹x1 ≤⇘L1⇙ x1›]
    ‹l1 x1 ≤⇘R1⇙ l1 x2›]
  with ‹x1 ⇘L1⇙⪅ l1 x1› L2_unit_le2
    show "((in_dom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x1)⇙) (r2⇘x1 (l1 x2)⇙)"
    by (intro Fun_Rel_predI) (auto dest!: in_field_if_in_dom)
qed

lemma l2_unit_bi_rel_selfI:
  assumes pre_equiv1: "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and mono_L2:
    "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and mono_R2:
    "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | (x2' ≤⇘R1⇙ x3' ∧ x4' ≤⇘R1⇙ ε⇩1 x3')) ⇛ (≥)) R2"
  and mono_l2: "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "x ≤⇘L1⇙ x"
  and "in_field (≤⇘L2 x x⇙) y"
  shows "l2⇘(l1 x) (η⇩1 x)⇙ y ≡⇘R2 (l1 x) (l1 x)⇙ l2⇘(l1 x) x⇙ y"
proof (rule bi_relatedI)
  note t1.preorder_equivalence_order_equivalenceE[elim!]
  from ‹x ≤⇘L1⇙ x› pre_equiv1 have "l1 x ≤⇘R1⇙ l1 x" "x ≤⇘L1⇙ η⇩1 x" "η⇩1 x ≤⇘L1⇙ x" by blast+
  with pre_equiv1 have "x ⇘L1⇙⪅ l1 x" "η⇩1 x ⇘L1⇙⪅ l1 x" by (auto 4 3)
  from pre_equiv1 ‹x ≤⇘L1⇙ η⇩1 x› have "x ≤⇘L1⇙ η⇩1 (η⇩1 x)" by fastforce
  moreover note ‹in_field (≤⇘L2 x x⇙) y›
    Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_L2 ‹η⇩1 x ≤⇘L1⇙ x›] ‹η⇩1 x ≤⇘L1⇙ x›]
    Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_L2 ‹x ≤⇘L1⇙ x›] ‹η⇩1 x ≤⇘L1⇙ x›]
  ultimately have "in_field (≤⇘L2 (η⇩1 x) (η⇩1 x)⇙) y" "in_field (≤⇘L2 x (η⇩1 x)⇙) y"
    using ‹x ≤⇘L1⇙ η⇩1 x› by blast+
  moreover note ‹x ⇘L1⇙⪅ l1 x›
    Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_l2 ‹l1 x ≤⇘R1⇙ l1 x›] ‹η⇩1 x ≤⇘L1⇙ x›]
  ultimately have "l2⇘(l1 x) (η⇩1 x)⇙ y ≤⇘R2 (ε⇩1 (l1 x)) (l1 x)⇙ l2⇘(l1 x) x⇙ y" by auto
  moreover from pre_equiv1 ‹l1 x ≤⇘R1⇙ l1 x›
    have "ε⇩1 (l1 x) ≤⇘R1⇙ l1 x" "l1 x ≤⇘R1⇙ ε⇩1 (l1 x)" by fastforce+
  moreover note Dep_Fun_Rel_relD[OF dep_mono_wrt_relD
    [OF mono_R2 ‹l1 x ≤⇘R1⇙ ε⇩1 (l1 x)›] ‹l1 x ≤⇘R1⇙ l1 x›]
  ultimately show "l2⇘(l1 x) (η⇩1 x)⇙ y ≤⇘R2 (l1 x) (l1 x)⇙ l2⇘(l1 x) x⇙ y" by blast
  note ‹η⇩1 x ⇘L1⇙⪅ l1 x› ‹in_field (≤⇘L2 x (η⇩1 x)⇙) y›
    Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_l2 ‹l1 x ≤⇘R1⇙ l1 x›] ‹x ≤⇘L1⇙ η⇩1 x›]
  then show "l2⇘(l1 x) x⇙ y ≤⇘R2 (l1 x) (l1 x)⇙ l2⇘(l1 x) (η⇩1 x)⇙ y" by auto
qed

lemma r2_counit_bi_rel_selfI:
  assumes pre_equiv1: "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and mono_L2:
    "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and mono_R2:
    "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | (x2' ≤⇘R1⇙ x3' ∧ x4' ≤⇘R1⇙ ε⇩1 x3')) ⇛ (≥)) R2"
  and mono_r2: "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "x' ≤⇘R1⇙ x'"
  and "in_field (≤⇘R2 x' x'⇙) y'"
  shows "r2⇘(r1 x') (ε⇩1 x')⇙ y' ≡⇘L2 (r1 x') (r1 x')⇙ r2⇘(r1 x') x'⇙ y'"
proof (rule bi_relatedI)
  note t1.preorder_equivalence_order_equivalenceE[elim!]
  from ‹x' ≤⇘R1⇙ x'› pre_equiv1 have "r1 x' ≤⇘L1⇙ r1 x'" "x' ≤⇘R1⇙ ε⇩1 x'" "ε⇩1 x' ≤⇘R1⇙ x'" by blast+
  with pre_equiv1 have "r1 x' ⇘L1⇙⪅ x'" "r1 x' ⇘L1⇙⪅ ε⇩1 x'" by fastforce+
  from pre_equiv1 ‹x' ≤⇘R1⇙ ε⇩1 x'› have "x' ≤⇘R1⇙ ε⇩1 (ε⇩1 x')" by fastforce
  moreover note ‹in_field (≤⇘R2 x' x'⇙) y'›
    Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_R2 ‹ε⇩1 x' ≤⇘R1⇙ x'›] ‹ε⇩1 x' ≤⇘R1⇙ x'›]
    Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_R2 ‹ε⇩1 x' ≤⇘R1⇙ x'›] ‹x' ≤⇘R1⇙ x'›]
  ultimately have "in_field (≤⇘R2 (ε⇩1 x') (ε⇩1 x')⇙) y'" "in_field (≤⇘R2 (ε⇩1 x') x'⇙) y'"
    using ‹x' ≤⇘R1⇙ ε⇩1 x'› ‹x' ≤⇘R1⇙ x'› by blast+
  moreover note ‹r1 x' ⇘L1⇙⪅ ε⇩1 x'›
    Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_r2 ‹r1 x' ≤⇘L1⇙ r1 x'›] ‹ε⇩1 x' ≤⇘R1⇙ x'›]
  ultimately show "r2⇘(r1 x') (ε⇩1 x')⇙ y' ≤⇘L2 (r1 x') (r1 x')⇙ r2⇘(r1 x') x'⇙ y'" by auto
  note ‹r1 x' ⇘L1⇙⪅ x'› ‹in_field (≤⇘R2 (ε⇩1 x') (ε⇩1 x')⇙) y'›
    Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_r2 ‹r1 x' ≤⇘L1⇙ r1 x'›] ‹x' ≤⇘R1⇙ ε⇩1 x'›]
  then have "r2⇘(r1 x') x'⇙ y' ≤⇘L2 (r1 x') (η⇩1 (r1 x'))⇙ r2⇘(r1 x') (ε⇩1 x')⇙ y'" by auto
  moreover from pre_equiv1 ‹r1 x' ≤⇘L1⇙ r1 x'›
    have "η⇩1 (r1 x') ≤⇘L1⇙ r1 x'" "r1 x' ≤⇘L1⇙ η⇩1 (r1 x')" by fastforce+
  moreover note Dep_Fun_Rel_relD[OF dep_mono_wrt_relD
    [OF mono_L2 ‹r1 x' ≤⇘L1⇙ r1 x'›] ‹r1 x' ≤⇘L1⇙ η⇩1 (r1 x')›]
  ultimately show "r2⇘(r1 x') x'⇙ y' ≤⇘L2 (r1 x') (r1 x')⇙ r2⇘(r1 x') (ε⇩1 x')⇙ y'"
    using pre_equiv1 by blast
qed

end


paragraph ‹Function Relator›

context transport_Fun_Rel
begin

corollary rel_unit_self_if_rel_selfI:
  assumes "inflationary_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "transitive (≤⇘L1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇒ (≤⇘L2⇙)) r2"
  and "inflationary_on (in_codom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "transitive (≤⇘L2⇙)"
  and "f ≤⇘L⇙ f"
  shows "f ≤⇘L⇙ η f"
  using assms by (intro tdfr.rel_unit_self_if_rel_selfI) simp_all

corollary counit_rel_self_if_rel_selfI:
  assumes "deflationary_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇒ (≤⇘L2⇙)) r2"
  and "deflationary_on (in_dom (≤⇘R2⇙)) (≤⇘R2⇙) ε⇩2"
  and "transitive (≤⇘R2⇙)"
  and "g ≤⇘R⇙ g"
  shows "ε g ≤⇘R⇙ g"
  using assms by (intro tdfr.counit_rel_self_if_rel_selfI) simp_all

lemma bi_related_unit_self_if_rel_selfI:
  assumes "rel_equivalence_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "transitive (≤⇘L1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇒ (≤⇘L2⇙)) r2"
  and "rel_equivalence_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "transitive (≤⇘L2⇙)"
  and "f ≤⇘L⇙ f"
  shows "f ≡⇘L⇙ η f"
  using assms by (intro tdfr.bi_related_unit_self_if_rel_selfI) simp_all

end


paragraph ‹Monotone Dependent Function Relator›

context transport_Mono_Dep_Fun_Rel
begin

subparagraph ‹Inflationary›

lemma inflationary_on_unitI:
  assumes "(tdfr.L ⇒ tdfr.R) l" and "(tdfr.R ⇒ tdfr.L) r"
  and "inflationary_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "transitive (≤⇘L1⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘L2 x x⇙) ⇒ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘R2 (l1 x) (l1 x)⇙) ⇒ (≤⇘L2 x (η⇩1 x)⇙)) (r2⇘x (l1 x)⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ inflationary_on (in_codom (≤⇘L2 x x⇙)) (≤⇘L2 x x⇙) (η⇘2 x (l1 x)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_codom (≤⇘L2 x (η⇩1 x)⇙) y ⟹
    (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y) ≤ (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  shows "inflationary_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
  unfolding left_rel_eq_tdfr_left_Refl_Rel using assms
  by (intro inflationary_onI Refl_RelI)
  (auto 6 2 intro: tdfr.rel_unit_self_if_rel_selfI[simplified unit_eq]
    elim!: Refl_RelE in_fieldE)


subparagraph ‹Deflationary›

lemma deflationary_on_counitI:
  assumes "(tdfr.L ⇒ tdfr.R) l" and "(tdfr.R ⇒ tdfr.L) r"
  and "deflationary_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "transitive (≤⇘R1⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ ((≤⇘L2 (r1 x') (r1 x')⇙) ⇒ (≤⇘R2 (ε⇩1 x') x'⇙)) (l2⇘ x' (r1 x')⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹
    ((≤⇘R2 x' x'⇙) ⇒ (≤⇘L2 (r1 x') (r1 x')⇙)) (r2⇘(r1 x') x'⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ deflationary_on (in_dom (≤⇘R2 x' x'⇙)) (≤⇘R2 x' x'⇙) (ε⇘2 (r1 x') x'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x' y'. x' ≤⇘R1⇙ x' ⟹ in_dom (≤⇘R2 (ε⇩1 x') x'⇙) y' ⟹
    (≤⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y') ≤ (≤⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y')"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "deflationary_on (in_field (≤⇘R⇙)) (≤⇘R⇙) ε"
  unfolding right_rel_eq_tdfr_right_Refl_Rel using assms
  by (intro deflationary_onI Refl_RelI)
  (auto 6 2 intro: tdfr.counit_rel_self_if_rel_selfI[simplified counit_eq]
    elim!: Refl_RelE in_fieldE)


subparagraph ‹Relational Equivalence›

context
begin

interpretation flip : transport_Mono_Dep_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2
  rewrites "flip.counit ≡ η" and "flip.t1.counit ≡ η⇩1"
  and "⋀x y. flip.t2_counit x y ≡ η⇘2 y x⇙"
  by (simp_all add: order_functors.flip_counit_eq_unit)

lemma rel_equivalence_on_unitI:
  assumes "(tdfr.L ⇒ tdfr.R) l" and "(tdfr.R ⇒ tdfr.L) r"
  and rel_equiv_unit1: "rel_equivalence_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and trans_L1: "transitive (≤⇘L1⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘L2 x x⇙) ⇒ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘R2 (l1 x) (l1 x)⇙) ⇒ (≤⇘L2 x x⇙)) (r2⇘x (l1 x)⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ rel_equivalence_on (in_field (≤⇘L2 x x⇙)) (≤⇘L2 x x⇙) (η⇘2 x (l1 x)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 (η⇩1 x1) x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_dom (≤⇘L2 (η⇩1 x) x⇙) y ⟹
    (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y) ≤ (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_codom (≤⇘L2 x (η⇩1 x)⇙) y ⟹
    (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y) ≤ (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  shows "rel_equivalence_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
proof -
  from rel_equiv_unit1 trans_L1 have "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
    by (intro reflexive_on_in_field_if_transitive_if_rel_equivalence_on)
  with assms show ?thesis
    by (intro rel_equivalence_onI inflationary_on_unitI
      flip.deflationary_on_counitI)
    (auto intro!: tdfr.bi_related_unit_self_if_rel_self_aux
      intro: inflationary_on_if_le_pred_if_inflationary_on
        deflationary_on_if_le_pred_if_deflationary_on
        reflexive_on_if_le_pred_if_reflexive_on
        in_field_if_in_dom in_field_if_in_codom
      elim!: rel_equivalence_onE
      simp only:)
qed

end

subparagraph ‹Order Equivalence›

interpretation flip : transport_Mono_Dep_Fun_Rel R1 L1 r1 l1 R2 L2 r2 l2
  rewrites "flip.unit ≡ ε" and "flip.t1.unit ≡ ε⇩1"
  and "flip.counit ≡ η" and "flip.t1.counit ≡ η⇩1"
  and "⋀x y. flip.t2_unit x y ≡ ε⇘2 y x⇙"
  by (simp_all add: order_functors.flip_counit_eq_unit)

lemma order_equivalenceI:
  assumes "(tdfr.L ⇒ tdfr.R) l" and "(tdfr.R ⇒ tdfr.L) r"
  and "rel_equivalence_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "rel_equivalence_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "transitive (≤⇘L1⇙)" and "transitive (≤⇘R1⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘L2 x x⇙) ⇒ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ ((≤⇘L2 (r1 x') (r1 x')⇙) ⇒ (≤⇘R2 x' x'⇙)) (l2⇘x' (r1 x')⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ ((≤⇘R2 x' x'⇙) ⇒ (≤⇘L2 (r1 x') (r1 x')⇙)) (r2⇘(r1 x') x'⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ ((≤⇘R2 (l1 x) (l1 x)⇙) ⇒ (≤⇘L2 x x⇙)) (r2⇘x (l1 x)⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ rel_equivalence_on (in_field (≤⇘L2 x x⇙)) (≤⇘L2 x x⇙) (η⇘2 x (l1 x)⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹
    rel_equivalence_on (in_field (≤⇘R2 x' x'⇙)) (≤⇘R2 x' x'⇙) (ε⇘2 (r1 x') x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 (η⇩1 x1) x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x2' x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' (ε⇩1 x2')⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_dom (≤⇘L2 (η⇩1 x) x⇙) y ⟹
    (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y) ≤ (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y)"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_codom (≤⇘L2 x (η⇩1 x)⇙) y ⟹
    (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y) ≤ (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y)"
  and "⋀x' y'. x' ≤⇘R1⇙ x' ⟹ in_dom (≤⇘R2 (ε⇩1 x') x'⇙) y' ⟹
    (≤⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y') ≤ (≤⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y')"
  and "⋀x' y'. x' ≤⇘R1⇙ x' ⟹ in_codom (≤⇘R2 x' (ε⇩1 x')⇙) y' ⟹
    (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y') ≤ (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y')"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘R1⇙ x2 ⟹ transitive (≤⇘R2 x1 x2⇙)"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms
  by (intro order_equivalenceI rel_equivalence_on_unitI flip.rel_equivalence_on_unitI
    mono_wrt_rel_leftI flip.mono_wrt_rel_leftI)
  auto

lemma order_equivalence_if_preorder_equivalenceI:
  assumes pre_equiv1: "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and order_equiv2: "⋀x x'. x ⇘L1⇙⪅ x' ⟹
    ((≤⇘L2 x (r1 x')⇙) ≡⇩o (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and L2_les: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
    "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 (η⇩1 x1) x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
    "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
    "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and R2_les: "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x2' x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
    "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
    "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
    "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' (ε⇩1 x2')⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙)) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x1' (r1 x1')⇙) (l2⇘x2' (r1 x1')⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((in_codom (≤⇘L2 (r1 x1') (r1 x2')⇙)) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x2' (r1 x1')⇙) (l2⇘x2' (r1 x2')⇙)"
  and l2_bi_rel: "⋀x y. x ≤⇘L1⇙ x ⟹ in_field (≤⇘L2 x x⇙) y ⟹
    l2⇘(l1 x) (η⇩1 x)⇙ y ≡⇘R2 (l1 x) (l1 x)⇙ l2⇘(l1 x) x⇙ y"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹
    ((in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x2)⇙) (r2⇘x2 (l1 x2)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹
    ((in_dom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x1)⇙) (r2⇘x1 (l1 x2)⇙)"
  and r2_bi_rel: "⋀x' y'. x' ≤⇘R1⇙ x' ⟹ in_field (≤⇘R2 x' x'⇙) y' ⟹
    r2⇘(r1 x') (ε⇩1 x')⇙ y' ≡⇘L2 (r1 x') (r1 x')⇙ r2⇘(r1 x') x'⇙ y'"
  and trans_L2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and trans_R2: "⋀x1 x2. x1 ≤⇘R1⇙ x2 ⟹ transitive (≤⇘R2 x1 x2⇙)"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
proof -
  from pre_equiv1 L2_les have L2_unit_eq1: "(≤⇘L2 (η⇩1 x) x⇙) = (≤⇘L2 x x⇙)"
    and L2_unit_eq2: "(≤⇘L2 x (η⇩1 x)⇙) = (≤⇘L2 x x⇙)"
    if "x ≤⇘L1⇙ x" for x using ‹x ≤⇘L1⇙ x›
    by (auto elim!: t1.preorder_equivalence_order_equivalenceE
      intro!: tdfr.left_rel2_unit_eqs_left_rel2I bi_related_if_rel_equivalence_on
      simp del: t1.unit_eq)
  from pre_equiv1 R2_les have R2_counit_eq1: "(≤⇘R2 (ε⇩1 x') x'⇙) = (≤⇘R2 x' x'⇙)"
    and R2_counit_eq2: "(≤⇘R2 x' (ε⇩1 x')⇙) = (≤⇘R2 x' x'⇙)" (is ?goal2)
    if "x' ≤⇘R1⇙ x'" for x' using ‹x' ≤⇘R1⇙ x'›
    by (auto elim!: t1.preorder_equivalence_order_equivalenceE
      intro!: flip.tdfr.left_rel2_unit_eqs_left_rel2I bi_related_if_rel_equivalence_on
      simp del: t1.counit_eq)
  from order_equiv2 have
    mono_l2: "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ⇒ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙)"
    and mono_r2: "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘R2 (l1 x) x'⇙) ⇒ (≤⇘L2 x (r1 x')⇙)) (r2⇘x x'⇙)"
    by auto
  moreover have "rel_equivalence_on (in_field (≤⇘L2 x x⇙)) (≤⇘L2 x x⇙) (η⇘2 x (l1 x)⇙)" (is ?goal1)
    and "((≤⇘L2 x x⇙) ⇒ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙)" (is ?goal2)
    if [iff]: "x ≤⇘L1⇙ x" for x
  proof -
    from pre_equiv1 have "x ⇘L1⇙⪅ l1 x" by (intro t1.left_GaloisI)
      (auto elim!: t1.preorder_equivalence_order_equivalenceE t1.order_equivalenceE bi_relatedE)
    with order_equiv2 have "((≤⇘L2 x x⇙) ≡⇩o (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (r2⇘x (l1 x)⇙)"
      by (auto simp flip: L2_unit_eq2)
    then show ?goal1 ?goal2 by (auto elim: order_functors.order_equivalenceE)
  qed
  moreover have
    "rel_equivalence_on (in_field (≤⇘R2 x' x'⇙)) (≤⇘R2 x' x'⇙) (ε⇘2 (r1 x') x'⇙)" (is ?goal1)
    and "((≤⇘R2 x' x'⇙) ⇒ (≤⇘L2 (r1 x') (r1 x')⇙)) (r2⇘(r1 x') x'⇙)" (is ?goal2)
    if [iff]: "x' ≤⇘R1⇙ x'" for x'
  proof -
    from pre_equiv1 have "r1 x' ⇘L1⇙⪅ x'" by blast
    with order_equiv2 have "((≤⇘L2 (r1 x') (r1 x')⇙) ≡⇩o (≤⇘R2 x' x'⇙)) (l2⇘x' (r1 x')⇙) (r2⇘(r1 x') x'⇙)"
      by (auto simp flip: R2_counit_eq1)
    then show ?goal1 ?goal2 by (auto elim: order_functors.order_equivalenceE)
  qed
  moreover from mono_l2 tdfr.mono_wrt_rel_left2_if_mono_wrt_rel_left2_if_left_GaloisI
    have "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇒ (≤⇘R2 x1' x2'⇙)) (l2⇘x2' (r1 x1')⇙)"
    using pre_equiv1 R2_les(2) by (blast elim!: le_relE)
  moreover from pre_equiv1 have "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
    by (intro t1.half_galois_prop_right_left_right_if_transitive_if_order_equivalence)
    (auto elim!: t1.preorder_equivalence_order_equivalenceE)
  moreover with mono_r2 tdfr.mono_wrt_rel_right2_if_mono_wrt_rel_right2_if_left_GaloisI
    have "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ ((≤⇘R2 (l1 x1) (l1 x2)⇙) ⇒ (≤⇘L2 x1 (η⇩1 x2)⇙)) (r2⇘x1 (l1 x2)⇙)"
    using pre_equiv1 by blast
  moreover with L2_les
    have "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ ((≤⇘R2 (l1 x1) (l1 x2)⇙) ⇒ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x2)⇙)"
    by blast
  moreover have "in_dom (≤⇘L2 (η⇩1 x) x⇙) y ⟹
      (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y) ≤ (≤⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y)"
      (is "_ ⟹ ?goal1")
    and "in_codom (≤⇘L2 x (η⇩1 x)⇙) y ⟹
      (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) x⇙ y) ≤ (≥⇘R2 (l1 x) (l1 x)⇙) (l2⇘(l1 x) (η⇩1 x)⇙ y)"
      (is "_ ⟹ ?goal2")
    if [iff]: "x ≤⇘L1⇙ x" for x y
  proof -
    presume "in_dom (≤⇘L2 (η⇩1 x) x⇙) y ∨ in_codom (≤⇘L2 x (η⇩1 x)⇙) y"
    then have "in_field (≤⇘L2 x x⇙) y" using L2_unit_eq1 L2_unit_eq2 by auto
    with l2_bi_rel have "l2⇘(l1 x) (η⇩1 x)⇙ y ≡⇘R2 (l1 x) (l1 x)⇙ l2⇘(l1 x) x⇙ y" by blast
    moreover from pre_equiv1 have ‹l1 x ≤⇘R1⇙ l1 x› by blast
    ultimately show ?goal1 ?goal2 using trans_R2 by blast+
  qed auto
  moreover have "in_dom (≤⇘R2 (ε⇩1 x') x'⇙) y' ⟹
      (≤⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y') ≤ (≤⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y')"
      (is "_ ⟹ ?goal1")
    and "in_codom (≤⇘R2 x' (ε⇩1 x')⇙) y' ⟹
      (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') x'⇙ y') ≤ (≥⇘L2 (r1 x') (r1 x')⇙) (r2⇘(r1 x') (ε⇩1 x')⇙ y')"
      (is "_ ⟹ ?goal2")
    if [iff]: "x' ≤⇘R1⇙ x'" for x' y'
  proof -
    presume "in_dom (≤⇘R2 (ε⇩1 x') x'⇙) y' ∨ in_codom (≤⇘R2 x' (ε⇩1 x')⇙) y'"
    then have "in_field (≤⇘R2 x' x'⇙) y'" using R2_counit_eq1 R2_counit_eq2 by auto
    with r2_bi_rel have "r2⇘(r1 x') (ε⇩1 x')⇙ y' ≡⇘L2 (r1 x') (r1 x')⇙ r2⇘(r1 x') x'⇙ y'"
      by blast
    moreover from pre_equiv1 have ‹r1 x' ≤⇘L1⇙ r1 x'› by blast
    ultimately show ?goal1 ?goal2 using trans_L2 by blast+
  qed auto
  ultimately show ?thesis using assms
    by (intro order_equivalenceI
      tdfr.mono_wrt_rel_left_if_transitiveI
      tdfr.mono_wrt_rel_left2_if_mono_wrt_rel_left2_if_left_GaloisI
      tdfr.mono_wrt_rel_right_if_transitiveI
      tdfr.mono_wrt_rel_right2_if_mono_wrt_rel_right2_if_left_GaloisI)
    (auto elim!: t1.preorder_equivalence_order_equivalenceE)
qed

lemma order_equivalence_if_preorder_equivalenceI':
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇩o (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 (η⇩1 x1) x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x2' x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' (ε⇩1 x2')⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "⋀x y. x ≤⇘L1⇙ x ⟹ in_field (≤⇘L2 x x⇙) y ⟹
    l2⇘(l1 x) (η⇩1 x)⇙ y ≡⇘R2 (l1 x) (l1 x)⇙ l2⇘(l1 x) x⇙ y"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x' y'. x' ≤⇘R1⇙ x' ⟹ in_field (≤⇘R2 x' x'⇙) y' ⟹
    r2⇘(r1 x') (ε⇩1 x')⇙ y' ≡⇘L2 (r1 x') (r1 x')⇙ r2⇘(r1 x') x'⇙ y'"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘R1⇙ x2 ⟹ transitive (≤⇘R2 x1 x2⇙)"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms by (intro order_equivalence_if_preorder_equivalenceI
    tdfr.order_equivalence_if_order_equivalence_mono_assms_leftI
    tdfr.order_equivalence_if_order_equivalence_mono_assms_rightI
    reflexive_on_in_field_if_transitive_if_rel_equivalence_on)
  (auto elim!: t1.preorder_equivalence_order_equivalenceE)

lemma order_equivalence_if_mono_if_preorder_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇩o (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≤⇘L1⇙) | η⇩1 x2 ≤⇘L1⇙ x1) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x2 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and "((x1' x2' ∷ (≤⇘R1⇙) | ε⇩1 x2' ≤⇘R1⇙ x1') ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x2' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | (x2' ≤⇘R1⇙ x3' ∧ x4' ≤⇘R1⇙ ε⇩1 x3')) ⇛ (≥)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘R1⇙ x2 ⟹ transitive (≤⇘R2 x1 x2⇙)"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms by (intro order_equivalence_if_preorder_equivalenceI'
    tdfr.l2_unit_bi_rel_selfI tdfr.r2_counit_bi_rel_selfI
    tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_leftI
    flip.tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_leftI
    tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_rightI
    flip.tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_rightI
    t1.galois_connection_left_right_if_transitive_if_order_equivalence
    flip.t1.galois_connection_left_right_if_transitive_if_order_equivalence
    reflexive_on_in_field_if_transitive_if_rel_equivalence_on)
  (auto elim!: t1.preorder_equivalence_order_equivalenceE)

theorem order_equivalence_if_mono_if_preorder_equivalenceI':
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘pre⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms by (intro order_equivalence_if_mono_if_preorder_equivalenceI
    tdfr.galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI
    flip.tdfr.galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI
    tdfr.transitive_left2_if_preorder_equivalenceI
    tdfr.transitive_right2_if_preorder_equivalenceI
    t1.preorder_on_in_field_left_if_transitive_if_order_equivalence
    flip.t1.preorder_on_in_field_left_if_transitive_if_order_equivalence
    t1.galois_equivalence_left_right_if_transitive_if_order_equivalence
    flip.t1.galois_equivalence_left_right_if_transitive_if_order_equivalence)
  (auto elim!: t1.preorder_equivalence_order_equivalenceE
    t2.preorder_equivalence_order_equivalenceE)

end


paragraph ‹Monotone Function Relator›

context transport_Mono_Fun_Rel
begin

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

lemma inflationary_on_unitI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "inflationary_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "transitive (≤⇘L1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇒ (≤⇘L2⇙)) r2"
  and "inflationary_on (in_codom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "transitive (≤⇘L2⇙)"
  shows "inflationary_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
  using assms by (intro tpdfr.inflationary_on_unitI
    tfr.mono_wrt_rel_leftI flip.tfr.mono_wrt_rel_leftI)
  simp_all

lemma deflationary_on_counitI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "deflationary_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇒ (≤⇘L2⇙)) r2"
  and "deflationary_on (in_dom (≤⇘R2⇙)) (≤⇘R2⇙) ε⇩2"
  and "transitive (≤⇘R2⇙)"
  shows "deflationary_on (in_field (≤⇘R⇙)) (≤⇘R⇙) ε"
  using assms by (intro tpdfr.deflationary_on_counitI
    tfr.mono_wrt_rel_leftI flip.tfr.mono_wrt_rel_leftI)
  simp_all

lemma rel_equivalence_on_unitI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "rel_equivalence_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "transitive (≤⇘L1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇒ (≤⇘L2⇙)) r2"
  and "rel_equivalence_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "transitive (≤⇘L2⇙)"
  shows "rel_equivalence_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
  using assms by (intro tpdfr.rel_equivalence_on_unitI
    tfr.mono_wrt_rel_leftI flip.tfr.mono_wrt_rel_leftI)
  simp_all

lemma order_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ≡⇘pre⇙ (≤⇘R2⇙)) l2 r2"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms by (intro tpdfr.order_equivalenceI
    tfr.mono_wrt_rel_leftI flip.tfr.mono_wrt_rel_leftI)
  (auto elim!: tdfrs.t1.preorder_equivalence_order_equivalenceE
    tdfrs.t2.preorder_equivalence_order_equivalenceE)

end


end