Theory Transport_Identity

✐‹creator "Kevin Kappelmann"›
section ‹Transport using Identity›
theory Transport_Identity
  imports
    Transport_Bijections
begin

paragraph ‹Summary›
text ‹Setup for Transport using the identity transport function.›


locale transport_id = fixes L :: "'a ⇒ 'a ⇒ bool"
begin
sublocale tbij ?: transport_bijection L L id id
  by (intro transport_bijection.intro) auto

interpretation transport L L id id .

lemma left_Galois_eq_left [simp]: "(⇘L⇙⪅) = (≤⇘L⇙)"
  by (intro ext iffI) auto
end

locale transport_reflexive_on_in_field_id =
  fixes L :: "'a ⇒ 'a ⇒ bool"
  assumes reflexive_on_in_field: "reflexive_on (in_field L) L"
begin
sublocale tid ?: transport_id L .
sublocale trefl_bij ?: transport_reflexive_on_in_field_bijection L L id id
  using reflexive_on_in_field by unfold_locales auto
end

locale transport_preorder_on_in_field_id =
  fixes L :: "'a ⇒ 'a ⇒ bool"
  assumes preorder_on_in_field: "preorder_on (in_field L) L"
begin
sublocale tid ?: transport_id L .
sublocale tpre_bij ?: transport_preorder_on_in_field_bijection L L id id
  using preorder_on_in_field by unfold_locales auto
end

locale transport_partial_equivalence_rel_id =
  fixes L :: "'a ⇒ 'a ⇒ bool"
  assumes partial_equivalence_rel: "partial_equivalence_rel L"
begin
sublocale tid ?: transport_id L .
sublocale tper_bij ?: transport_partial_equivalence_rel_bijection L L id id
  using partial_equivalence_rel by unfold_locales auto
end

locale transport_eq_restrict_id = fixes P :: "'a ⇒ bool"
begin
sublocale tbij ?: transport_eq_restrict_bijection P P id id
  using bijection_on_self_id by (unfold_locales) fastforce+
sublocale tper_id ?: transport_partial_equivalence_rel_id "(=⇘P⇙)"
  by (intro transport_partial_equivalence_rel_id.intro partial_equivalence_rel_left)
end
interpretation transport_eq_restrict_id : transport_eq_restrict_id P for P .

locale transport_eq_id
begin
sublocale tbij ?: transport_eq_bijection id id
  using bijection_on_self_id by unfold_locales auto
sublocale tper_id ?: transport_partial_equivalence_rel_id "(=)"
  by (intro transport_partial_equivalence_rel_id.intro partial_equivalence_rel_left)
end
interpretation transport_eq_id : transport_eq_id .

end