Theory Transport_Natural_Functors

✐‹creator "Kevin Kappelmann"›
theory Transport_Natural_Functors
  imports
    Transport_Natural_Functors_Galois
    Transport_Natural_Functors_Galois_Relator
    Transport_Natural_Functors_Order_Base
    Transport_Natural_Functors_Order_Equivalence
begin

paragraph ‹Summary›
text ‹Summary of results for a fixed natural functor with 3 parameters. All
apply-style proofs are written such that they also apply to functors with other
arities. An automatic derivation of these results for all natural functors needs
to be implemented in the BNF package. This is future work.›

context transport_natural_functor
begin

interpretation flip :
  transport_natural_functor R1 L1 r1 l1 R2 L2 r2 l2 R3 L3 r3 l3 .

theorem preorder_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ≡⇘pre⇙ (≤⇘R2⇙)) l2 r2"
  and "((≤⇘L3⇙) ≡⇘pre⇙ (≤⇘R3⇙)) l3 r3"
  shows "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  apply (insert assms)
  apply (elim transport.preorder_equivalence_galois_equivalenceE)
  apply (intro preorder_equivalence_if_galois_equivalenceI
    galois_equivalenceI
    preorder_on_in_field_leftI flip.preorder_on_in_field_leftI)
  apply assumption+
  done

theorem partial_equivalence_rel_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ≡⇘PER⇙ (≤⇘R2⇙)) l2 r2"
  and "((≤⇘L3⇙) ≡⇘PER⇙ (≤⇘R3⇙)) l3 r3"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  apply (insert assms)
  apply (elim transport.partial_equivalence_rel_equivalenceE
    transport.preorder_equivalence_galois_equivalenceE
    preorder_on_in_fieldE)
  apply (intro partial_equivalence_rel_equivalence_if_galois_equivalenceI
    galois_equivalenceI
    partial_equivalence_rel_leftI flip.partial_equivalence_rel_leftI
    partial_equivalence_relI)
  apply assumption+
  done

text ‹For the simplification of the Galois relator see
@{thm "left_Galois_eq_Frel_left_Galois"}.›

end


end