Theory Transport_Functions_Order_Base

✐‹creator "Kevin Kappelmann"›
subsection ‹Basic Order Properties›
theory Transport_Functions_Order_Base
  imports
    Transport_Functions_Base
begin

paragraph ‹Dependent Function Relator›

context hom_Dep_Fun_Rel_orders
begin

lemma reflexive_on_in_domI:
  assumes refl_L: "reflexive_on (in_codom (≤⇘L⇙)) (≤⇘L⇙)"
  and R_le_R_if_L: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x2 x2⇙) ≤ (≤⇘R x1 x2⇙)"
  and pequiv_R: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ partial_equivalence_rel (≤⇘R x1 x2⇙)"
  shows "reflexive_on (in_dom DFR) DFR"
proof (intro reflexive_onI Dep_Fun_Rel_relI)
  fix f x1 x2
  assume "in_dom DFR f"
  then obtain g where "DFR f g" by auto
  moreover assume "x1 ≤⇘L⇙ x2"
  moreover with refl_L have "x2 ≤⇘L⇙ x2" by blast
  ultimately have "f x1 ≤⇘R x1 x2⇙ g x2" "f x2 ≤⇘R x1 x2⇙ g x2"
    using R_le_R_if_L by auto
  moreover with pequiv_R ‹x1 ≤⇘L⇙ x2›  have "g x2 ≤⇘R x1 x2⇙ f x2"
    by (blast dest: symmetricD)
  ultimately show "f x1 ≤⇘R x1 x2⇙ f x2" using pequiv_R ‹x1 ≤⇘L⇙ x2› by blast
qed

lemma reflexive_on_in_codomI:
  assumes refl_L: "reflexive_on (in_dom (≤⇘L⇙)) (≤⇘L⇙)"
  and R_le_R_if_L: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x1 x1⇙) ≤ (≤⇘R x1 x2⇙)"
  and pequiv_R: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ partial_equivalence_rel (≤⇘R x1 x2⇙)"
  shows "reflexive_on (in_codom DFR) DFR"
proof (intro reflexive_onI Dep_Fun_Rel_relI)
  fix f x1 x2
  assume "in_codom DFR f"
  then obtain g where "DFR g f" by auto
  moreover assume "x1 ≤⇘L⇙ x2"
  moreover with refl_L have "x1 ≤⇘L⇙ x1" by blast
  ultimately have "g x1 ≤⇘R x1 x2⇙ f x2" "g x1 ≤⇘R x1 x2⇙ f x1"
    using R_le_R_if_L by auto
  moreover with pequiv_R ‹x1 ≤⇘L⇙ x2›  have "f x1 ≤⇘R x1 x2⇙ g x1"
    by (blast dest: symmetricD)
  ultimately show "f x1 ≤⇘R x1 x2⇙ f x2" using pequiv_R ‹x1 ≤⇘L⇙ x2› by blast
qed

corollary reflexive_on_in_fieldI:
  assumes "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x2 x2⇙) ≤ (≤⇘R x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x1 x1⇙) ≤ (≤⇘R x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ partial_equivalence_rel (≤⇘R x1 x2⇙)"
  shows "reflexive_on (in_field DFR) DFR"
proof -
  from assms have "reflexive_on (in_dom DFR) DFR"
    by (intro reflexive_on_in_domI)
    (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)
  moreover from assms have "reflexive_on (in_codom DFR) DFR"
    by (intro reflexive_on_in_codomI)
    (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)
  ultimately show ?thesis by (auto iff: in_field_iff_in_dom_or_in_codom)
qed

lemma transitiveI:
  assumes refl_L: "reflexive_on (in_dom (≤⇘L⇙)) (≤⇘L⇙)"
  and R_le_R_if_L: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x1 x1⇙) ≤ (≤⇘R x1 x2⇙)"
  and trans: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ transitive (≤⇘R x1 x2⇙)"
  shows "transitive DFR"
proof (intro transitiveI Dep_Fun_Rel_relI)
  fix f1 f2 f3 x1 x2 assume "x1 ≤⇘L⇙ x2"
  with refl_L have "x1 ≤⇘L⇙ x1" by blast
  moreover assume "DFR f1 f2"
  ultimately have "f1 x1 ≤⇘R x1 x1⇙ f2 x1" by blast
  with R_le_R_if_L have "f1 x1 ≤⇘R x1 x2⇙ f2 x1" using ‹x1 ≤⇘L⇙ x2› by blast
  assume "DFR f2 f3"
  with ‹x1 ≤⇘L⇙ x2› have "f2 x1 ≤⇘R x1 x2⇙ f3 x2" by blast
  with ‹f1 x1 ≤⇘R x1 x2⇙ f2 x1› show "f1 x1 ≤⇘R x1 x2⇙  f3 x2"
    using trans ‹x1 ≤⇘L⇙ x2› by blast
qed

lemma transitiveI':
  assumes refl_L: "reflexive_on (in_codom (≤⇘L⇙)) (≤⇘L⇙)"
  and R_le_R_if_L: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x2 x2⇙) ≤ (≤⇘R x1 x2⇙)"
  and trans: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ transitive (≤⇘R x1 x2⇙)"
  shows "transitive DFR"
proof (intro Binary_Relations_Transitive.transitiveI Dep_Fun_Rel_relI)
  fix f1 f2 f3 x1 x2 assume "DFR f1 f2" "x1 ≤⇘L⇙ x2"
  then have "f1 x1 ≤⇘R x1 x2⇙ f2 x2" by blast
  from ‹x1 ≤⇘L⇙ x2› refl_L have "x2 ≤⇘L⇙ x2" by blast
  moreover assume "DFR f2 f3"
  ultimately have "f2 x2 ≤⇘R x2 x2⇙ f3 x2" by blast
  with R_le_R_if_L have "f2 x2 ≤⇘R x1 x2⇙ f3 x2" using ‹x1 ≤⇘L⇙ x2› by blast
  with ‹f1 x1 ≤⇘R x1 x2⇙ f2 x2› show "f1 x1 ≤⇘R x1 x2⇙ f3 x2"
    using trans ‹x1 ≤⇘L⇙ x2› by blast
qed

lemma preorder_on_in_fieldI:
  assumes "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x2 x2⇙) ≤ (≤⇘R x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x1 x1⇙) ≤ (≤⇘R x1 x2⇙)"
  and pequiv_R: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ partial_equivalence_rel (≤⇘R x1 x2⇙)"
  shows "preorder_on (in_field DFR) DFR"
  using assms by (intro preorder_onI reflexive_on_in_fieldI)
  (auto intro!: transitiveI dest: pequiv_R elim!: partial_equivalence_relE)

lemma symmetricI:
  assumes sym_L: "symmetric (≤⇘L⇙)"
  and R_le_R_if_L: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x1 x2⇙) ≤ (≤⇘R x2 x1⇙)"
  and sym_R: "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ symmetric (≤⇘R x1 x2⇙)"
  shows "symmetric DFR"
proof (intro symmetricI Dep_Fun_Rel_relI)
  fix f g x y assume "x ≤⇘L⇙ y"
  with sym_L have "y ≤⇘L⇙ x" by (rule symmetricD)
  moreover assume "DFR f g"
  ultimately have "f y ≤⇘R y x⇙ g x" by blast
  with sym_R ‹y ≤⇘L⇙ x› have "g x ≤⇘R y x⇙ f y" by (blast dest: symmetricD)
  with R_le_R_if_L ‹y ≤⇘L⇙ x› show "g x ≤⇘R x y⇙ f y" by blast
qed

corollary partial_equivalence_relI:
  assumes "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and sym_L: "symmetric (≤⇘L⇙)"
  and mono_R: "((x1 x2 ∷ (≤⇘L⇙)) ⇒ (x3 x4 ∷ (≤⇘L⇙) | x1 ≤⇘L⇙ x3) ⇛ (≤)) R"
  and "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ partial_equivalence_rel (≤⇘R x1 x2⇙)"
  shows "partial_equivalence_rel DFR"
proof -
  have "(≤⇘R x1 x2⇙) ≤ (≤⇘R x2 x1⇙)" if "x1 ≤⇘L⇙ x2" for x1 x2
  proof -
    from sym_L ‹x1 ≤⇘L⇙ x2› have "x2 ≤⇘L⇙ x1" by (rule symmetricD)
    with mono_R ‹x1 ≤⇘L⇙ x2› show ?thesis by blast
  qed
  with assms show ?thesis
    by (intro partial_equivalence_relI transitiveI symmetricI)
    (blast elim: partial_equivalence_relE[OF assms(4)])+
qed

end

context transport_Dep_Fun_Rel
begin

lemmas reflexive_on_in_field_leftI = dfro1.reflexive_on_in_fieldI
  [folded left_rel_eq_Dep_Fun_Rel]
lemmas transitive_leftI = dfro1.transitiveI[folded left_rel_eq_Dep_Fun_Rel]
lemmas transitive_leftI' = dfro1.transitiveI'[folded left_rel_eq_Dep_Fun_Rel]
lemmas preorder_on_in_field_leftI = dfro1.preorder_on_in_fieldI
  [folded left_rel_eq_Dep_Fun_Rel]
lemmas symmetric_leftI = dfro1.symmetricI[folded left_rel_eq_Dep_Fun_Rel]
lemmas partial_equivalence_rel_leftI = dfro1.partial_equivalence_relI
  [folded left_rel_eq_Dep_Fun_Rel]


subparagraph ‹Introduction Rules for Assumptions›

lemma transitive_left2_if_transitive_left2_if_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and L2_eq: "(≤⇘L2 x1 x2⇙) = (≤⇘L2 x1 (η⇩1 x2)⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ transitive (≤⇘L2 x (r1 x')⇙)"
  and "x1 ≤⇘L1⇙ x2"
  shows "transitive (≤⇘L2 x1 x2⇙)"
  by (subst L2_eq) (auto intro!: assms t1.left_Galois_left_if_left_relI)

lemma symmetric_left2_if_symmetric_left2_if_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and L2_eq: "(≤⇘L2 x1 x2⇙) = (≤⇘L2 x1 (η⇩1 x2)⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ symmetric (≤⇘L2 x (r1 x')⇙)"
  and "x1 ≤⇘L1⇙ x2"
  shows "symmetric (≤⇘L2 x1 x2⇙)"
  by (subst L2_eq) (auto intro!: assms t1.left_Galois_left_if_left_relI)

lemma partial_equivalence_rel_left2_if_partial_equivalence_rel_left2_if_left_GaloisI:
  assumes "((≤⇘L1⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and L2_eq: "(≤⇘L2 x1 x2⇙) = (≤⇘L2 x1 (η⇩1 x2)⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ partial_equivalence_rel (≤⇘L2 x (r1 x')⇙)"
  and "x1 ≤⇘L1⇙ x2"
  shows "partial_equivalence_rel (≤⇘L2 x1 x2⇙)"
  by (subst L2_eq) (auto intro!: assms t1.left_Galois_left_if_left_relI)

context
  assumes galois_prop: "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
begin

interpretation flip_inv :
  transport_Dep_Fun_Rel "(≥⇘R1⇙)" "(≥⇘L1⇙)" r1 l1 "flip2 R2" "flip2 L2" r2 l2
  rewrites "flip_inv.t1.unit ≡ ε⇩1"
  and "⋀R x y. (flip2 R x y) ≡ (R y x)¯"
  and "⋀R S. R¯ = S¯ ≡ R = S"
  and "⋀R S. (R¯ ⇒ S¯) ≡ (R ⇒ S)"
  and "⋀x x'. x' ⇘R1⇙⪆ x ≡ x ⇘L1⇙⪅ x'"
  and "((≥⇘R1⇙) ⊴⇩h (≥⇘L1⇙)) r1 l1 ≡ True"
  and "⋀(R :: 'z ⇒ 'z ⇒ bool). transitive R¯ ≡ transitive R"
  and "⋀(R :: 'z ⇒ 'z ⇒ bool). symmetric R¯ ≡ symmetric R"
  and "⋀(R :: 'z ⇒ 'z ⇒ bool). partial_equivalence_rel R¯ ≡ partial_equivalence_rel R"
  and "⋀P. (True ⟹ P) ≡ Trueprop P"
  and "⋀P Q. (True ⟹ PROP P ⟹ PROP Q) ≡ (PROP P ⟹ True ⟹ PROP Q)"
  using galois_prop
  by (auto intro!: Eq_TrueI simp: t1.flip_unit_eq_counit
    galois_prop.half_galois_prop_right_rel_inv_iff_half_galois_prop_left
    mono_wrt_rel_eq_dep_mono_wrt_rel
    simp del: rel_inv_iff_rel)

lemma transitive_right2_if_transitive_right2_if_left_GaloisI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "(≤⇘R2 x1 x2⇙) = (≤⇘R2 (ε⇩1 x1) x2⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ transitive (≤⇘R2 (l1 x) x'⇙)"
  and "x1 ≤⇘R1⇙ x2"
  shows "transitive (≤⇘R2 x1 x2⇙)"
  using galois_prop assms
  by (intro flip_inv.transitive_left2_if_transitive_left2_if_left_GaloisI
    [simplified rel_inv_iff_rel, of x1])
  auto

lemma symmetric_right2_if_symmetric_right2_if_left_GaloisI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "(≤⇘R2 x1 x2⇙) = (≤⇘R2 (ε⇩1 x1) x2⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ symmetric (≤⇘R2 (l1 x) x'⇙)"
  and "x1 ≤⇘R1⇙ x2"
  shows "symmetric (≤⇘R2 x1 x2⇙)"
  using galois_prop assms
  by (intro flip_inv.symmetric_left2_if_symmetric_left2_if_left_GaloisI
    [simplified rel_inv_iff_rel, of x1])
  auto

lemma partial_equivalence_rel_right2_if_partial_equivalence_rel_right2_if_left_GaloisI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "(≤⇘R2 x1 x2⇙) = (≤⇘R2 (ε⇩1 x1) x2⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ partial_equivalence_rel (≤⇘R2 (l1 x) x'⇙)"
  and "x1 ≤⇘R1⇙ x2"
  shows "partial_equivalence_rel (≤⇘R2 x1 x2⇙)"
  using galois_prop assms
  by (intro flip_inv.partial_equivalence_rel_left2_if_partial_equivalence_rel_left2_if_left_GaloisI
    [simplified rel_inv_iff_rel, of x1])
  auto

end

lemma transitive_left2_if_preorder_equivalenceI:
  assumes pre_equiv1: "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘pre⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "x1 ≤⇘L1⇙ x2"
  shows "transitive (≤⇘L2 x1 x2⇙)"
proof -
  from ‹x1 ≤⇘L1⇙ x2› pre_equiv1 have "x2 ≡⇘L1⇙ η⇩1 x2"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘L2 x1 x2⇙) = (≤⇘L2 x1 (η⇩1 x2)⇙)"
    by (intro left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro transitive_left2_if_transitive_left2_if_left_GaloisI[of x1]) blast+
qed

lemma symmetric_left2_if_partial_equivalence_rel_equivalenceI:
  assumes PER_equiv1: "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "x1 ≤⇘L1⇙ x2"
  shows "symmetric (≤⇘L2 x1 x2⇙)"
proof -
  from ‹x1 ≤⇘L1⇙ x2› PER_equiv1 have "x2 ≡⇘L1⇙ η⇩1 x2"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘L2 x1 x2⇙) = (≤⇘L2 x1 (η⇩1 x2)⇙)"
    by (intro left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro symmetric_left2_if_symmetric_left2_if_left_GaloisI[of x1]) blast+
qed

lemma partial_equivalence_rel_left2_if_partial_equivalence_rel_equivalenceI:
  assumes PER_equiv1: "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "x1 ≤⇘L1⇙ x2"
  shows "partial_equivalence_rel (≤⇘L2 x1 x2⇙)"
proof -
  from ‹x1 ≤⇘L1⇙ x2› PER_equiv1 have "x2 ≡⇘L1⇙ η⇩1 x2"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘L2 x1 x2⇙) = (≤⇘L2 x1 (η⇩1 x2)⇙)"
    by (intro left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro partial_equivalence_rel_left2_if_partial_equivalence_rel_left2_if_left_GaloisI[of x1])
    blast+
qed

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

lemma transitive_right2_if_preorder_equivalenceI:
  assumes pre_equiv1: "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘pre⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "x1' ≤⇘R1⇙ x2'"
  shows "transitive (≤⇘R2 x1' x2'⇙)"
proof -
  from ‹x1' ≤⇘R1⇙ x2'› pre_equiv1 have "x1' ≡⇘R1⇙ ε⇩1 x1'"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘R2 x1' x2'⇙) = (≤⇘R2 (ε⇩1 x1') x2'⇙)"
    by (intro flip.left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro transitive_right2_if_transitive_right2_if_left_GaloisI[of x1']) blast+
qed

lemma symmetric_right2_if_partial_equivalence_rel_equivalenceI:
  assumes PER_equiv1: "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "x1' ≤⇘R1⇙ x2'"
  shows "symmetric (≤⇘R2 x1' x2'⇙)"
proof -
  from ‹x1' ≤⇘R1⇙ x2'› PER_equiv1 have "x1' ≡⇘R1⇙ ε⇩1 x1'"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘R2 x1' x2'⇙) = (≤⇘R2 (ε⇩1 x1') x2'⇙)"
    by (intro flip.left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro symmetric_right2_if_symmetric_right2_if_left_GaloisI[of x1']) blast+
qed

lemma partial_equivalence_rel_right2_if_partial_equivalence_rel_equivalenceI:
  assumes PER_equiv1: "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘PER⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "x1' ≤⇘R1⇙ x2'"
  shows "partial_equivalence_rel (≤⇘R2 x1' x2'⇙)"
proof -
  from ‹x1' ≤⇘R1⇙ x2'› PER_equiv1 have "x1' ≡⇘R1⇙ ε⇩1 x1'"
    by (blast elim: t1.preorder_equivalence_order_equivalenceE
      intro: bi_related_if_rel_equivalence_on)
  with assms have "(≤⇘R2 x1' x2'⇙) = (≤⇘R2 (ε⇩1 x1') x2'⇙)"
    by (intro flip.left2_eq_if_bi_related_if_monoI) blast+
  with assms show ?thesis
    by (intro partial_equivalence_rel_right2_if_partial_equivalence_rel_right2_if_left_GaloisI[of x1'])
    blast+
qed

end

paragraph ‹Function Relator›

context transport_Fun_Rel
begin

lemma reflexive_on_in_field_leftI:
  assumes "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "partial_equivalence_rel (≤⇘L2⇙)"
  shows "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  using assms by (intro tdfr.reflexive_on_in_field_leftI) simp_all

lemma transitive_leftI:
  assumes "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "transitive (≤⇘L2⇙)"
  shows "transitive (≤⇘L⇙)"
  using assms by (intro tdfr.transitive_leftI) simp_all

lemma transitive_leftI':
  assumes "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "transitive (≤⇘L2⇙)"
  shows "transitive (≤⇘L⇙)"
  using assms by (intro tdfr.transitive_leftI') simp_all

lemma preorder_on_in_field_leftI:
  assumes "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "partial_equivalence_rel (≤⇘L2⇙)"
  shows "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  using assms by (intro tdfr.preorder_on_in_field_leftI) simp_all

lemma symmetric_leftI:
  assumes "symmetric (≤⇘L1⇙)"
  and "symmetric (≤⇘L2⇙)"
  shows "symmetric (≤⇘L⇙)"
  using assms by (intro tdfr.symmetric_leftI) simp_all

corollary partial_equivalence_rel_leftI:
  assumes "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "symmetric (≤⇘L1⇙)"
  and "partial_equivalence_rel (≤⇘L2⇙)"
  shows "partial_equivalence_rel (≤⇘L⇙)"
  using assms by (intro tdfr.partial_equivalence_rel_leftI) auto

end

paragraph ‹Monotone Dependent Function Relator›

context transport_Mono_Dep_Fun_Rel
begin

lemmas reflexive_on_in_field_leftI = Refl_Rel_reflexive_on_in_field[of tdfr.L,
  folded left_rel_eq_tdfr_left_Refl_Rel]
lemmas transitive_leftI = Refl_Rel_transitiveI
  [of tdfr.L, folded left_rel_eq_tdfr_left_Refl_Rel]
lemmas preorder_on_in_field_leftI = Refl_Rel_preorder_on_in_fieldI[of tdfr.L,
  folded left_rel_eq_tdfr_left_Refl_Rel]
lemmas symmetric_leftI = Refl_Rel_symmetricI[of tdfr.L,
  OF tdfr.symmetric_leftI, folded left_rel_eq_tdfr_left_Refl_Rel]
lemmas partial_equivalence_rel_leftI = Refl_Rel_partial_equivalence_relI[of tdfr.L,
  OF tdfr.partial_equivalence_rel_leftI, folded left_rel_eq_tdfr_left_Refl_Rel]

end


paragraph ‹Monotone Function Relator›

context transport_Mono_Fun_Rel
begin

lemma symmetric_leftI:
  assumes "symmetric (≤⇘L1⇙)"
  and "symmetric (≤⇘L2⇙)"
  shows "symmetric (≤⇘L⇙)"
  using assms by (intro tpdfr.symmetric_leftI) auto

lemma partial_equivalence_rel_leftI:
  assumes "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "symmetric (≤⇘L1⇙)"
  and "partial_equivalence_rel (≤⇘L2⇙)"
  shows "partial_equivalence_rel (≤⇘L⇙)"
  using assms by (intro tpdfr.partial_equivalence_rel_leftI) auto

end


end