Theory InternalEquivalence
section "Internal Equivalences"
theory InternalEquivalence
imports Bicategory
begin
text ‹
An \emph{internal equivalence} in a bicategory consists of antiparallel 1-cells ‹f› and ‹g›
together with invertible 2-cells ‹«η : src f ⇒ g ⋆ f»› and ‹«ε : f ⋆ g ⇒ src g»›.
Objects in a bicategory are said to be \emph{equivalent} if they are connected by an
internal equivalence.
In this section we formalize the definition of internal equivalence and the related notions
``equivalence map'' and ``equivalent objects'', and we establish some basic facts about
these notions.
›
subsection "Definition of Equivalence"
text ‹
The following locale is defined to prove some basic facts about an equivalence
(or an adjunction) in a bicategory that are ``syntactic'' in the sense that they depend
only on the configuration (source, target, domain, codomain) of the arrows
involved and not on further properties such as the triangle identities (for adjunctions)
or assumptions about invertibility (for equivalences). Proofs about adjunctions and
equivalences become more automatic once we have introduction and simplification rules in
place about this syntax.
›
locale adjunction_data_in_bicategory =
bicategory +
fixes f :: 'a
and g :: 'a
and η :: 'a
and ε :: 'a
assumes ide_left [simp]: "ide f"
and ide_right [simp]: "ide g"
and unit_in_vhom: "«η : src f ⇒ g ⋆ f»"
and counit_in_vhom: "«ε : f ⋆ g ⇒ src g»"
begin
lemma antipar :
shows "trg g = src f" and "src g = trg f"
apply (metis counit_in_vhom hseqE ideD(1) ide_right src.preserves_reflects_arr
vconn_implies_hpar(3))
by (metis arrI not_arr_null seq_if_composable src.preserves_reflects_arr
unit_in_vhom vconn_implies_hpar(1) vconn_implies_hpar(3))
lemma counit_in_hom [intro]:
shows "«ε : trg f → trg f»" and "«ε : f ⋆ g ⇒ trg f»"
using counit_in_vhom vconn_implies_hpar antipar by auto
lemma unit_in_hom [intro]:
shows "«η : src f → src f»" and "«η : src f ⇒ g ⋆ f»"
using unit_in_vhom vconn_implies_hpar antipar by auto
lemma unit_simps [simp]:
shows "arr η" and "dom η = src f" and "cod η = g ⋆ f"
and "src η = src f" and "trg η = src f"
using unit_in_hom antipar by auto
lemma counit_simps [simp]:
shows "arr ε" and "dom ε = f ⋆ g" and "cod ε = trg f"
and "src ε = trg f" and "trg ε = trg f"
using counit_in_hom antipar by auto
text ‹
The expressions found in the triangle identities for an adjunction come up
relatively frequently, so it is useful to have established some basic facts
about them, even if the triangle identities themselves have not actually been
introduced as assumptions in the current context.
›
lemma triangle_in_hom:
shows "«(ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) : f ⋆ src f ⇒ trg f ⋆ f»"
and "«(g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) : trg g ⋆ g ⇒ g ⋆ src g»"
and "«𝗅[f] ⋅ (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋅ 𝗋⇧-⇧1[f] : f ⇒ f»"
and "«𝗋[g] ⋅ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ 𝗅⇧-⇧1[g] : g ⇒ g»"
using antipar by auto
lemma triangle_equiv_form:
shows "(ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) = 𝗅⇧-⇧1[f] ⋅ 𝗋[f] ⟷
𝗅[f] ⋅ (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋅ 𝗋⇧-⇧1[f] = f"
and "(g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) = 𝗋⇧-⇧1[g] ⋅ 𝗅[g] ⟷
𝗋[g] ⋅ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ 𝗅⇧-⇧1[g] = g"
proof -
show "(ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) = 𝗅⇧-⇧1[f] ⋅ 𝗋[f] ⟷
𝗅[f] ⋅ (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋅ 𝗋⇧-⇧1[f] = f"
proof
assume 1: "(ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) = 𝗅⇧-⇧1[f] ⋅ 𝗋[f]"
have "𝗅[f] ⋅ (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋅ 𝗋⇧-⇧1[f] =
𝗅[f] ⋅ ((ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η)) ⋅ 𝗋⇧-⇧1[f]"
using comp_assoc by simp
also have "... = 𝗅[f] ⋅ (𝗅⇧-⇧1[f] ⋅ 𝗋[f]) ⋅ 𝗋⇧-⇧1[f]"
using 1 by simp
also have "... = f"
using comp_assoc comp_arr_inv' comp_inv_arr' iso_lunit iso_runit
comp_arr_dom comp_cod_arr
by simp
finally show "𝗅[f] ⋅ (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋅ 𝗋⇧-⇧1[f] = f"
by simp
next
assume 2: "𝗅[f] ⋅ (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋅ 𝗋⇧-⇧1[f] = f"
have "𝗅⇧-⇧1[f] ⋅ 𝗋[f] = 𝗅⇧-⇧1[f] ⋅ f ⋅ 𝗋[f]"
using comp_cod_arr by simp
also have "... = (𝗅⇧-⇧1[f] ⋅ 𝗅[f]) ⋅ ((ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η)) ⋅ (𝗋⇧-⇧1[f] ⋅ 𝗋[f])"
using 2 comp_assoc by (metis (no_types, lifting))
also have "... = (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η)"
using comp_arr_inv' comp_inv_arr' iso_lunit iso_runit comp_arr_dom comp_cod_arr
hseqI' antipar
by (metis ide_left in_homE lunit_simps(4) runit_simps(4) triangle_in_hom(1))
finally show "(ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) = 𝗅⇧-⇧1[f] ⋅ 𝗋[f]"
by simp
qed
show "(g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) = 𝗋⇧-⇧1[g] ⋅ 𝗅[g] ⟷
𝗋[g] ⋅ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ 𝗅⇧-⇧1[g] = g"
proof
assume 1: "(g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) = 𝗋⇧-⇧1[g] ⋅ 𝗅[g]"
have "𝗋[g] ⋅ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ 𝗅⇧-⇧1[g] =
𝗋[g] ⋅ ((g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g)) ⋅ 𝗅⇧-⇧1[g]"
using comp_assoc by simp
also have "... = 𝗋[g] ⋅ (𝗋⇧-⇧1[g] ⋅ 𝗅[g]) ⋅ 𝗅⇧-⇧1[g]"
using 1 by simp
also have "... = g"
using comp_assoc comp_arr_inv' comp_inv_arr' iso_lunit iso_runit
comp_arr_dom comp_cod_arr
by simp
finally show "𝗋[g] ⋅ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ 𝗅⇧-⇧1[g] = g"
by simp
next
assume 2: "𝗋[g] ⋅ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ 𝗅⇧-⇧1[g] = g"
have "𝗋⇧-⇧1[g] ⋅ 𝗅[g] = 𝗋⇧-⇧1[g] ⋅ g ⋅ 𝗅[g]"
using comp_cod_arr by simp
also have "... = 𝗋⇧-⇧1[g] ⋅ (𝗋[g] ⋅ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ 𝗅⇧-⇧1[g]) ⋅ 𝗅[g]"
using 2 by simp
also have "... = (𝗋⇧-⇧1[g] ⋅ 𝗋[g]) ⋅ ((g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g)) ⋅ (𝗅⇧-⇧1[g] ⋅ 𝗅[g])"
using comp_assoc by simp
also have "... = (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g)"
using comp_arr_inv' comp_inv_arr' iso_lunit iso_runit comp_arr_dom comp_cod_arr
hseqI' antipar
by (metis ide_right in_homE lunit_simps(4) runit_simps(4) triangle_in_hom(2))
finally show "(g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) = 𝗋⇧-⇧1[g] ⋅ 𝗅[g]"
by simp
qed
qed
end
locale equivalence_in_bicategory =
adjunction_data_in_bicategory +
assumes unit_is_iso [simp]: "iso η"
and counit_is_iso [simp]: "iso ε"
begin
lemma dual_equivalence:
shows "equivalence_in_bicategory V H 𝖺 𝗂 src trg g f (inv ε) (inv η)"
using antipar by unfold_locales auto
end
abbreviation (in bicategory) internal_equivalence
where "internal_equivalence f g φ ψ ≡ equivalence_in_bicategory V H 𝖺 𝗂 src trg f g φ ψ"
subsection "Quasi-Inverses and Equivalence Maps"
text ‹
Antiparallel 1-cells ‹f› and ‹g› are \emph{quasi-inverses} if they can be extended to
an internal equivalence. We will use the term \emph{equivalence map} to refer to a 1-cell
that has a quasi-inverse.
›
context bicategory
begin
definition quasi_inverses
where "quasi_inverses f g ≡ ∃φ ψ. internal_equivalence f g φ ψ"
lemma quasi_inversesI:
assumes "ide f" and "ide g"
and "src f ≅ g ⋆ f" and "f ⋆ g ≅ trg f"
shows "quasi_inverses f g"
proof (unfold quasi_inverses_def)
have 1: "src g = trg f"
using assms ideD(1) isomorphic_implies_ide(2) by blast
obtain φ where φ: "«φ : src f ⇒ g ⋆ f» ∧ iso φ"
using assms isomorphic_def by auto
obtain ψ where ψ: "«ψ : f ⋆ g ⇒ trg f» ∧ iso ψ"
using assms isomorphic_def by auto
have "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g φ ψ"
using assms 1 φ ψ by unfold_locales auto
thus "∃φ ψ. internal_equivalence f g φ ψ" by auto
qed
lemma quasi_inversesE:
assumes "quasi_inverses f g"
and "⟦ide f; ide g; src f ≅ g ⋆ f; f ⋆ g ≅ trg f⟧ ⟹ T"
shows T
proof -
obtain φ ψ where φψ: "internal_equivalence f g φ ψ"
using assms quasi_inverses_def by auto
interpret φψ: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g φ ψ
using φψ by simp
have "ide f ∧ ide g"
by simp
moreover have "src f ≅ g ⋆ f"
using isomorphic_def φψ.unit_in_hom by auto
moreover have "f ⋆ g ≅ trg f"
using isomorphic_def φψ.counit_in_hom by auto
ultimately show T
using assms by blast
qed
lemma quasi_inverse_unique:
assumes "quasi_inverses f g" and "quasi_inverses f g'"
shows "isomorphic g g'"
proof -
obtain φ ψ where φψ: "internal_equivalence f g φ ψ"
using assms quasi_inverses_def by auto
interpret φψ: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g φ ψ
using φψ by simp
obtain φ' ψ' where φ'ψ': "internal_equivalence f g' φ' ψ'"
using assms quasi_inverses_def by auto
interpret φ'ψ': equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' φ' ψ'
using φ'ψ' by simp
have "«𝗋[g'] ⋅ (g' ⋆ ψ) ⋅ 𝖺[g', f, g] ⋅ (φ' ⋆ g) ⋅ 𝗅⇧-⇧1[g] : g ⇒ g'»"
using φψ.unit_in_hom φψ.unit_is_iso φψ.antipar φ'ψ'.antipar
by (intro comp_in_homI' hseqI') auto
moreover have "iso (𝗋[g'] ⋅ (g' ⋆ ψ) ⋅ 𝖺[g', f, g] ⋅ (φ' ⋆ g) ⋅ 𝗅⇧-⇧1[g])"
using φψ.unit_in_hom φψ.unit_is_iso φψ.antipar φ'ψ'.antipar
by (intro isos_compose) auto
ultimately show ?thesis
using isomorphic_def by auto
qed
lemma quasi_inverses_symmetric:
assumes "quasi_inverses f g"
shows "quasi_inverses g f"
using assms quasi_inverses_def equivalence_in_bicategory.dual_equivalence by metis
definition equivalence_map
where "equivalence_map f ≡ ∃g η ε. equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
lemma equivalence_mapI:
assumes "quasi_inverses f g"
shows "equivalence_map f"
using assms quasi_inverses_def equivalence_map_def by auto
lemma equivalence_mapE:
assumes "equivalence_map f"
obtains g where "quasi_inverses f g"
using assms equivalence_map_def quasi_inverses_def by auto
lemma equivalence_map_is_ide:
assumes "equivalence_map f"
shows "ide f"
using assms adjunction_data_in_bicategory.ide_left equivalence_in_bicategory_def
equivalence_map_def
by fastforce
lemma obj_is_equivalence_map:
assumes "obj a"
shows "equivalence_map a"
using assms
by (metis equivalence_mapI isomorphic_symmetric objE obj_self_composable(2) quasi_inversesI)
lemma equivalence_respects_iso:
assumes "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
and "«φ : f ⇒ f'»" and "iso φ" and "«ψ : g ⇒ g'»" and "iso ψ"
shows "internal_equivalence f' g' ((g' ⋆ φ) ⋅ (ψ ⋆ f) ⋅ η) (ε ⋅ (inv φ ⋆ g) ⋅ (f' ⋆ inv ψ))"
proof -
interpret E: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using assms by auto
show ?thesis
proof
show f': "ide f'" using assms by auto
show g': "ide g'" using assms by auto
show 1: "«(g' ⋆ φ) ⋅ (ψ ⋆ f) ⋅ η : src f' ⇒ g' ⋆ f'»"
using assms f' g' E.unit_in_hom E.antipar(2) vconn_implies_hpar(3)
apply (intro comp_in_homI)
apply auto
by (intro hcomp_in_vhom) auto
show "iso ((g' ⋆ φ) ⋅ (ψ ⋆ f) ⋅ η)"
using assms 1 g' vconn_implies_hpar(3) E.antipar(2) iso_hcomp
by (intro isos_compose) auto
show 1: "«ε ⋅ (inv φ ⋆ g) ⋅ (f' ⋆ inv ψ) : f' ⋆ g' ⇒ src g'»"
using assms f' ide_in_hom(2) vconn_implies_hpar(3-4) E.antipar(1-2)
by (intro comp_in_homI) auto
show "iso (ε ⋅ (inv φ ⋆ g) ⋅ (f' ⋆ inv ψ))"
using assms 1 isos_compose
by (metis E.counit_is_iso E.ide_right arrI f' hseqE ide_is_iso iso_hcomp
iso_inv_iso seqE)
qed
qed
lemma equivalence_map_preserved_by_iso:
assumes "equivalence_map f" and "f ≅ f'"
shows "equivalence_map f'"
proof -
obtain g η ε where E: "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
using assms equivalence_map_def by auto
interpret E: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using E by auto
obtain φ where φ: "«φ : f ⇒ f'» ∧ iso φ"
using assms isomorphic_def isomorphic_symmetric by blast
have "equivalence_in_bicategory V H 𝖺 𝗂 src trg f' g
((g ⋆ φ) ⋅ (g ⋆ f) ⋅ η) (ε ⋅ (inv φ ⋆ g) ⋅ (f' ⋆ inv g))"
using E φ equivalence_respects_iso [of f g η ε φ f' g g] by fastforce
thus ?thesis
using equivalence_map_def by auto
qed
lemma equivalence_preserved_by_iso_right:
assumes "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
and "«φ : g ⇒ g'»" and "iso φ"
shows "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' ((φ ⋆ f) ⋅ η) (ε ⋅ (f ⋆ inv φ))"
proof
interpret E: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using assms by auto
show "ide f" by simp
show "ide g'"
using assms(2) isomorphic_def by auto
show "«(φ ⋆ f) ⋅ η : src f ⇒ g' ⋆ f»"
using assms E.antipar(2) E.ide_left by blast
show "«ε ⋅ (f ⋆ inv φ) : f ⋆ g' ⇒ src g'»"
using assms vconn_implies_hpar(3-4) E.counit_in_vhom E.antipar(1) ide_in_hom(2)
by (intro comp_in_homI, auto)
show "iso ((φ ⋆ f) ⋅ η)"
using assms E.antipar isos_compose by auto
show "iso (ε ⋅ (f ⋆ inv φ))"
using assms E.antipar isos_compose by auto
qed
lemma equivalence_preserved_by_iso_left:
assumes "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
and "«φ : f ⇒ f'»" and "iso φ"
shows "equivalence_in_bicategory V H 𝖺 𝗂 src trg f' g ((g ⋆ φ) ⋅ η) (ε ⋅ (inv φ ⋆ g))"
proof
interpret E: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using assms by auto
show "ide f'"
using assms by auto
show "ide g"
by simp
show "«(g ⋆ φ) ⋅ η : src f' ⇒ g ⋆ f'»"
using assms E.unit_in_hom E.antipar by auto
show "«ε ⋅ (inv φ ⋆ g) : f' ⋆ g ⇒ src g»"
using assms E.counit_in_hom E.antipar ide_in_hom(2) vconn_implies_hpar(3) by auto
show "iso ((g ⋆ φ) ⋅ η)"
using assms E.antipar isos_compose by auto
show "iso (ε ⋅ (inv φ ⋆ g))"
using assms E.antipar isos_compose by auto
qed
definition some_quasi_inverse
where "some_quasi_inverse f = (SOME g. quasi_inverses f g)"
notation some_quasi_inverse ("_⇧~" [1000] 1000)
lemma quasi_inverses_some_quasi_inverse:
assumes "equivalence_map f"
shows "quasi_inverses f f⇧~"
and "quasi_inverses f⇧~ f"
using assms some_quasi_inverse_def quasi_inverses_def equivalence_map_def
someI_ex [of "λg. quasi_inverses f g"] quasi_inverses_symmetric
by auto
lemma quasi_inverse_antipar:
assumes "equivalence_map f"
shows "src f⇧~ = trg f" and "trg f⇧~ = src f"
proof -
obtain φ ψ where φψ: "equivalence_in_bicategory V H 𝖺 𝗂 src trg f f⇧~ φ ψ"
using assms equivalence_map_def quasi_inverses_some_quasi_inverse quasi_inverses_def
by blast
interpret φψ: equivalence_in_bicategory V H 𝖺 𝗂 src trg f ‹f⇧~› φ ψ
using φψ by simp
show "src f⇧~ = trg f"
using φψ.antipar by simp
show "trg f⇧~ = src f"
using φψ.antipar by simp
qed
lemma quasi_inverse_in_hom [intro]:
assumes "equivalence_map f"
shows "«f⇧~ : trg f → src f»"
and "«f⇧~ : f⇧~ ⇒ f⇧~»"
using assms equivalence_mapE
apply (intro in_homI in_hhomI)
apply (metis equivalence_map_is_ide ideD(1) not_arr_null quasi_inverse_antipar(2)
src.preserves_ide trg.is_extensional)
apply (simp_all add: quasi_inverse_antipar)
using assms quasi_inversesE quasi_inverses_some_quasi_inverse(2) by blast
lemma quasi_inverse_simps [simp]:
assumes "equivalence_map f"
shows "equivalence_map f⇧~" and "ide f⇧~"
and "src f⇧~ = trg f" and "trg f⇧~ = src f"
and "dom f⇧~ = f⇧~" and "cod f⇧~ = f⇧~"
using assms equivalence_mapE quasi_inverse_in_hom quasi_inverses_some_quasi_inverse
equivalence_map_is_ide
apply auto
by (meson equivalence_mapI)
lemma quasi_inverse_quasi_inverse:
assumes "equivalence_map f"
shows "(f⇧~)⇧~ ≅ f"
proof -
have "quasi_inverses f⇧~ (f⇧~)⇧~"
using assms quasi_inverses_some_quasi_inverse by simp
moreover have "quasi_inverses f⇧~ f"
using assms quasi_inverses_some_quasi_inverse quasi_inverses_symmetric by simp
ultimately show ?thesis
using quasi_inverse_unique by simp
qed
lemma comp_quasi_inverse:
assumes "equivalence_map f"
shows "f⇧~ ⋆ f ≅ src f" and "f ⋆ f⇧~ ≅ trg f"
proof -
obtain φ ψ where φψ: "equivalence_in_bicategory V H 𝖺 𝗂 src trg f f⇧~ φ ψ"
using assms equivalence_map_def quasi_inverses_some_quasi_inverse
quasi_inverses_def
by blast
interpret φψ: equivalence_in_bicategory V H 𝖺 𝗂 src trg f ‹f⇧~› φ ψ
using φψ by simp
show "f⇧~ ⋆ f ≅ src f"
using quasi_inverses_some_quasi_inverse quasi_inverses_def
φψ.unit_in_hom φψ.unit_is_iso isomorphic_def
by blast
show "f ⋆ f⇧~ ≅ trg f"
using quasi_inverses_some_quasi_inverse quasi_inverses_def
φψ.counit_in_hom φψ.counit_is_iso isomorphic_def
by blast
qed
lemma quasi_inverse_transpose:
assumes "ide f" and "ide g" and "ide h" and "f ⋆ g ≅ h"
shows "equivalence_map g ⟹ f ≅ h ⋆ g⇧~"
and "equivalence_map f ⟹ g ≅ f⇧~ ⋆ h"
proof -
have 1: "src f = trg g"
using assms equivalence_map_is_ide by fastforce
show "equivalence_map g ⟹ f ≅ h ⋆ g⇧~"
proof -
assume g: "equivalence_map g"
have 2: "ide g⇧~"
using g by simp
have "f ≅ f ⋆ src f"
using assms isomorphic_unit_right isomorphic_symmetric by blast
also have "... ≅ f ⋆ trg g"
using assms 1 isomorphic_reflexive by auto
also have "... ≅ f ⋆ g ⋆ g⇧~"
using assms g 1 comp_quasi_inverse(2) isomorphic_symmetric hcomp_ide_isomorphic
by simp
also have "... ≅ (f ⋆ g) ⋆ g⇧~"
using assms g 1 2 assoc'_in_hom [of f g "g⇧~"] iso_assoc' isomorphic_def by auto
also have "... ≅ h ⋆ g⇧~"
using assms g 1 2
by (simp add: hcomp_isomorphic_ide)
finally show ?thesis by blast
qed
show "equivalence_map f ⟹ g ≅ f⇧~ ⋆ h"
proof -
assume f: "equivalence_map f"
have 2: "ide f⇧~"
using f by simp
have "g ≅ src f ⋆ g"
using assms 1 isomorphic_unit_left isomorphic_symmetric by metis
also have "... ≅ (f⇧~ ⋆ f) ⋆ g"
using assms f 1 comp_quasi_inverse(1) [of f] isomorphic_symmetric
hcomp_isomorphic_ide
by simp
also have "... ≅ f⇧~ ⋆ f ⋆ g"
using assms f 1 assoc_in_hom [of "f⇧~" f g] iso_assoc isomorphic_def by auto
also have "... ≅ f⇧~ ⋆ h"
using assms f 1 equivalence_map_is_ide quasi_inverses_some_quasi_inverse
hcomp_ide_isomorphic
by simp
finally show ?thesis by blast
qed
qed
end
subsection "Composing Equivalences"
locale composite_equivalence_in_bicategory =
bicategory V H 𝖺 𝗂 src trg +
fg: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g ζ ξ +
hk: equivalence_in_bicategory V H 𝖺 𝗂 src trg h k σ τ
for V :: "'a ⇒ 'a ⇒ 'a" (infixr "⋅" 55)
and H :: "'a ⇒ 'a ⇒ 'a" (infixr "⋆" 53)
and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("𝖺[_, _, _]")
and 𝗂 :: "'a ⇒ 'a" ("𝗂[_]")
and src :: "'a ⇒ 'a"
and trg :: "'a ⇒ 'a"
and f :: "'a"
and g :: "'a"
and ζ :: "'a"
and ξ :: "'a"
and h :: "'a"
and k :: "'a"
and σ :: "'a"
and τ :: "'a" +
assumes composable: "src h = trg f"
begin
abbreviation η
where "η ≡ 𝖺⇧-⇧1[g, k, h ⋆ f] ⋅ (g ⋆ 𝖺[k, h, f]) ⋅ (g ⋆ σ ⋆ f) ⋅ (g ⋆ 𝗅⇧-⇧1[f]) ⋅ ζ"
abbreviation ε
where "ε ≡ τ ⋅ (h ⋆ 𝗅[k]) ⋅ (h ⋆ ξ ⋆ k) ⋅ (h ⋆ 𝖺⇧-⇧1[f, g, k]) ⋅ 𝖺[h, f, g ⋆ k]"
interpretation adjunction_data_in_bicategory V H 𝖺 𝗂 src trg ‹h ⋆ f› ‹g ⋆ k› η ε
proof
show "ide (h ⋆ f)"
using composable by simp
show "ide (g ⋆ k)"
using fg.antipar hk.antipar composable by simp
show "«η : src (h ⋆ f) ⇒ (g ⋆ k) ⋆ h ⋆ f»"
using fg.antipar hk.antipar composable by fastforce
show "«ε : (h ⋆ f) ⋆ g ⋆ k ⇒ src (g ⋆ k)»"
using fg.antipar hk.antipar composable by fastforce
qed
interpretation equivalence_in_bicategory V H 𝖺 𝗂 src trg ‹h ⋆ f› ‹g ⋆ k› η ε
proof
show "iso η"
using fg.antipar hk.antipar composable fg.unit_is_iso hk.unit_is_iso iso_hcomp
iso_lunit' hseq_char
by (intro isos_compose, auto)
show "iso ε"
using fg.antipar hk.antipar composable fg.counit_is_iso hk.counit_is_iso iso_hcomp
iso_lunit hseq_char
by (intro isos_compose, auto)
qed
lemma is_equivalence:
shows "equivalence_in_bicategory V H 𝖺 𝗂 src trg (h ⋆ f) (g ⋆ k) η ε"
..
sublocale equivalence_in_bicategory V H 𝖺 𝗂 src trg ‹h ⋆ f› ‹g ⋆ k› η ε
using is_equivalence by simp
end
context bicategory
begin
lemma equivalence_maps_compose:
assumes "equivalence_map f" and "equivalence_map f'" and "src f' = trg f"
shows "equivalence_map (f' ⋆ f)"
proof -
obtain g φ ψ where fg: "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g φ ψ"
using assms(1) equivalence_map_def by auto
interpret fg: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g φ ψ
using fg by auto
obtain g' φ' ψ' where f'g': "equivalence_in_bicategory V H 𝖺 𝗂 src trg f' g' φ' ψ'"
using assms(2) equivalence_map_def by auto
interpret f'g': equivalence_in_bicategory V H 𝖺 𝗂 src trg f' g' φ' ψ'
using f'g' by auto
interpret composite_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g φ ψ f' g' φ' ψ'
using assms(3) by (unfold_locales, auto)
show ?thesis
using equivalence_map_def equivalence_in_bicategory_axioms by auto
qed
lemma quasi_inverse_hcomp':
assumes "equivalence_map f" and "equivalence_map f'" and "equivalence_map (f ⋆ f')"
and "quasi_inverses f g" and "quasi_inverses f' g'"
shows "quasi_inverses (f ⋆ f') (g' ⋆ g)"
proof -
obtain φ ψ where g: "internal_equivalence f g φ ψ"
using assms quasi_inverses_def by auto
interpret g: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g φ ψ
using g by simp
obtain φ' ψ' where g': "internal_equivalence f' g' φ' ψ'"
using assms quasi_inverses_def by auto
interpret g': equivalence_in_bicategory V H 𝖺 𝗂 src trg f' g' φ' ψ'
using g' by simp
interpret gg': composite_equivalence_in_bicategory V H 𝖺 𝗂 src trg f' g' φ' ψ' f g φ ψ
using assms equivalence_map_is_ide [of "f ⋆ f'"]
apply unfold_locales
using ideD(1) by fastforce
show ?thesis
unfolding quasi_inverses_def
using gg'.equivalence_in_bicategory_axioms by auto
qed
lemma quasi_inverse_hcomp:
assumes "equivalence_map f" and "equivalence_map f'" and "equivalence_map (f ⋆ f')"
shows "(f ⋆ f')⇧~ ≅ f'⇧~ ⋆ f⇧~"
using assms quasi_inverses_some_quasi_inverse quasi_inverse_hcomp' quasi_inverse_unique
by metis
lemma quasi_inverse_respects_isomorphic:
assumes "equivalence_map f" and "equivalence_map f'" and "f ≅ f'"
shows "f⇧~ ≅ f'⇧~"
proof -
have hpar: "src f = src f' ∧ trg f = trg f'"
using assms isomorphic_implies_hpar by simp
have "f⇧~ ≅ f⇧~ ⋆ trg f"
using isomorphic_unit_right
by (metis assms(1) isomorphic_symmetric quasi_inverse_simps(2-3))
also have "... ≅ f⇧~ ⋆ f' ⋆ f'⇧~"
proof -
have "trg f ≅ f' ⋆ f'⇧~"
using assms quasi_inverse_hcomp
by (simp add: comp_quasi_inverse(2) hpar isomorphic_symmetric)
thus ?thesis
using assms hpar hcomp_ide_isomorphic isomorphic_implies_hpar(2) by auto
qed
also have "... ≅ (f⇧~ ⋆ f') ⋆ f'⇧~"
using assms hcomp_assoc_isomorphic hpar isomorphic_implies_ide(2) isomorphic_symmetric
by auto
also have "... ≅ (f⇧~ ⋆ f) ⋆ f'⇧~"
proof -
have "f⇧~ ⋆ f' ≅ f⇧~ ⋆ f"
using assms isomorphic_symmetric hcomp_ide_isomorphic isomorphic_implies_hpar(1)
by auto
thus ?thesis
using assms hcomp_isomorphic_ide isomorphic_implies_hpar(1) by auto
qed
also have "... ≅ src f ⋆ f'⇧~"
proof -
have "f⇧~ ⋆ f ≅ src f"
using assms comp_quasi_inverse by simp
thus ?thesis
using assms hcomp_isomorphic_ide isomorphic_implies_hpar by simp
qed
also have "... ≅ f'⇧~"
using assms isomorphic_unit_left
by (metis hpar quasi_inverse_simps(2,4))
finally show ?thesis by blast
qed
end
subsection "Equivalent Objects"
context bicategory
begin
definition equivalent_objects
where "equivalent_objects a b ≡ ∃f. «f : a → b» ∧ equivalence_map f"
lemma equivalent_objects_reflexive:
assumes "obj a"
shows "equivalent_objects a a"
using assms
by (metis equivalent_objects_def ide_in_hom(1) objE obj_is_equivalence_map)
lemma equivalent_objects_symmetric:
assumes "equivalent_objects a b"
shows "equivalent_objects b a"
using assms
by (metis equivalent_objects_def in_hhomE quasi_inverse_in_hom(1) quasi_inverse_simps(1))
lemma equivalent_objects_transitive [trans]:
assumes "equivalent_objects a b" and "equivalent_objects b c"
shows "equivalent_objects a c"
proof -
obtain f where f: "«f : a → b» ∧ equivalence_map f"
using assms equivalent_objects_def by auto
obtain g where g: "«g : b → c» ∧ equivalence_map g"
using assms equivalent_objects_def by auto
have "«g ⋆ f : a → c» ∧ equivalence_map (g ⋆ f)"
using f g equivalence_maps_compose by auto
thus ?thesis
using equivalent_objects_def by auto
qed
end
subsection "Transporting Arrows along Equivalences"
text ‹
We show in this section that transporting the arrows of one hom-category to another
along connecting equivalence maps yields an equivalence of categories.
This is useful, because it seems otherwise hard to establish that the transporting
functor is full.
›
locale two_equivalences_in_bicategory =
bicategory V H 𝖺 𝗂 src trg +
e⇩0: equivalence_in_bicategory V H 𝖺 𝗂 src trg e⇩0 d⇩0 η⇩0 ε⇩0 +
e⇩1: equivalence_in_bicategory V H 𝖺 𝗂 src trg e⇩1 d⇩1 η⇩1 ε⇩1
for V :: "'a ⇒ 'a ⇒ 'a" (infixr "⋅" 55)
and H :: "'a ⇒ 'a ⇒ 'a" (infixr "⋆" 53)
and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("𝖺[_, _, _]")
and 𝗂 :: "'a ⇒ 'a" ("𝗂[_]")
and src :: "'a ⇒ 'a"
and trg :: "'a ⇒ 'a"
and e⇩0 :: "'a"
and d⇩0 :: "'a"
and η⇩0 :: "'a"
and ε⇩0 :: "'a"
and e⇩1 :: "'a"
and d⇩1 :: "'a"
and η⇩1 :: "'a"
and ε⇩1 :: "'a"
begin
interpretation hom: subcategory V ‹λμ. «μ : src e⇩0 → src e⇩1»›
using hhom_is_subcategory by simp
no_notation in_hom ("«_ : _ → _»")
interpretation hom': subcategory V ‹λμ. «μ : trg e⇩0 → trg e⇩1»›
using hhom_is_subcategory by simp
no_notation in_hom ("«_ : _ → _»")
abbreviation (input) F
where "F ≡ λμ. e⇩1 ⋆ μ ⋆ d⇩0"
interpretation F: "functor" hom.comp hom'.comp F
proof
show 1: "⋀f. hom.arr f ⟹ hom'.arr (e⇩1 ⋆ f ⋆ d⇩0)"
using hom.arr_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C in_hhom_def e⇩0.antipar(1-2) by simp
show "⋀f. ¬ hom.arr f ⟹ e⇩1 ⋆ f ⋆ d⇩0 = hom'.null"
using 1 hom.arr_char⇩S⇩b⇩C hom'.null_char in_hhom_def
by (metis e⇩0.antipar(1) hseqE hseq_char' hcomp_simps(2))
show "⋀f. hom.arr f ⟹ hom'.dom (e⇩1 ⋆ f ⋆ d⇩0) = e⇩1 ⋆ hom.dom f ⋆ d⇩0"
using hom.arr_char⇩S⇩b⇩C hom.dom_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C hom'.dom_char⇩S⇩b⇩C
by (metis 1 hcomp_simps(3) e⇩0.ide_right e⇩1.ide_left hom'.inclusion hseq_char ide_char)
show "⋀f. hom.arr f ⟹ hom'.cod (e⇩1 ⋆ f ⋆ d⇩0) = e⇩1 ⋆ hom.cod f ⋆ d⇩0"
using hom.arr_char⇩S⇩b⇩C hom.cod_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C hom'.cod_char⇩S⇩b⇩C
by (metis 1 hcomp_simps(4) e⇩0.ide_right e⇩1.ide_left hom'.inclusion hseq_char ide_char)
show "⋀g f. hom.seq g f ⟹
e⇩1 ⋆ hom.comp g f ⋆ d⇩0 = hom'.comp (e⇩1 ⋆ g ⋆ d⇩0) (e⇩1 ⋆ f ⋆ d⇩0)"
using 1 hom.seq_char⇩S⇩b⇩C hom.arr_char⇩S⇩b⇩C hom.comp_char hom'.arr_char⇩S⇩b⇩C hom'.comp_char
whisker_left [of e⇩1] whisker_right [of d⇩0]
apply auto
apply (metis hseq_char seqE src_vcomp)
by (metis hseq_char hseq_char')
qed
abbreviation (input) G
where "G ≡ λμ'. d⇩1 ⋆ μ' ⋆ e⇩0"
interpretation G: "functor" hom'.comp hom.comp G
proof
show 1: "⋀f. hom'.arr f ⟹ hom.arr (d⇩1 ⋆ f ⋆ e⇩0)"
using hom.arr_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C in_hhom_def e⇩1.antipar(1) e⇩1.antipar(2)
by simp
show "⋀f. ¬ hom'.arr f ⟹ d⇩1 ⋆ f ⋆ e⇩0 = hom.null"
using 1 hom.arr_char⇩S⇩b⇩C hom'.null_char in_hhom_def
by (metis e⇩1.antipar(2) hom'.arrI⇩S⇩b⇩C hom.null_char hseqE hseq_char' hcomp_simps(2))
show "⋀f. hom'.arr f ⟹ hom.dom (d⇩1 ⋆ f ⋆ e⇩0) = d⇩1 ⋆ hom'.dom f ⋆ e⇩0"
using 1 hom.arr_char⇩S⇩b⇩C hom.dom_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C hom'.dom_char⇩S⇩b⇩C
by (metis hcomp_simps(3) e⇩0.ide_left e⇩1.ide_right hom.inclusion hseq_char ide_char)
show "⋀f. hom'.arr f ⟹ hom.cod (d⇩1 ⋆ f ⋆ e⇩0) = d⇩1 ⋆ hom'.cod f ⋆ e⇩0"
using 1 hom.arr_char⇩S⇩b⇩C hom.cod_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C hom'.cod_char⇩S⇩b⇩C
by (metis hcomp_simps(4) e⇩0.ide_left e⇩1.ide_right hom.inclusion hseq_char ide_char)
show "⋀g f. hom'.seq g f ⟹
d⇩1 ⋆ hom'.comp g f ⋆ e⇩0 = hom.comp (d⇩1 ⋆ g ⋆ e⇩0) (d⇩1 ⋆ f ⋆ e⇩0)"
using 1 hom'.seq_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C hom'.comp_char hom.arr_char⇩S⇩b⇩C hom.comp_char
whisker_left [of d⇩1] whisker_right [of e⇩0]
apply auto
apply (metis hseq_char seqE src_vcomp)
by (metis hseq_char hseq_char')
qed
interpretation GF: composite_functor hom.comp hom'.comp hom.comp F G ..
interpretation FG: composite_functor hom'.comp hom.comp hom'.comp G F ..
abbreviation (input) φ⇩0
where "φ⇩0 f ≡ (d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, f ⋆ d⇩0, e⇩0]) ⋅ 𝖺[d⇩1, e⇩1, (f ⋆ d⇩0) ⋆ e⇩0] ⋅
((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[f, d⇩0, e⇩0]) ⋅ (η⇩1 ⋆ f ⋆ η⇩0) ⋅ 𝗅⇧-⇧1[f ⋆ src e⇩0] ⋅ 𝗋⇧-⇧1[f]"
lemma φ⇩0_in_hom:
assumes "«f : src e⇩0 → src e⇩1»" and "ide f"
shows "«φ⇩0 f : src e⇩0 → src e⇩1»"
and "«φ⇩0 f : f ⇒ d⇩1 ⋆ (e⇩1 ⋆ f ⋆ d⇩0) ⋆ e⇩0»"
proof -
show "«φ⇩0 f : f ⇒ d⇩1 ⋆ (e⇩1 ⋆ f ⋆ d⇩0) ⋆ e⇩0»"
using assms e⇩0.antipar e⇩1.antipar by fastforce
thus "«φ⇩0 f : src e⇩0 → src e⇩1»"
using assms src_dom [of "φ⇩0 f"] trg_dom [of "φ⇩0 f"]
by (metis arrI dom_comp in_hhom_def runit'_simps(4) seqE)
qed
lemma iso_φ⇩0:
assumes "«f : src e⇩0 → src e⇩1»" and "ide f"
shows "iso (φ⇩0 f)"
using assms iso_lunit' iso_runit' e⇩0.antipar e⇩1.antipar
by (intro isos_compose) auto
interpretation φ: transformation_by_components hom.comp hom.comp hom.map ‹G o F› φ⇩0
proof
fix f
assume f: "hom.ide f"
show "hom.in_hom (φ⇩0 f) (hom.map f) (GF.map f)"
proof (unfold hom.in_hom_char⇩S⇩b⇩C, intro conjI)
show "hom.arr (hom.map f)"
using f by simp
show "hom.arr (GF.map f)"
using f by simp
show "hom.arr (φ⇩0 f)"
using f hom.ide_char⇩S⇩b⇩C hom.arr_char⇩S⇩b⇩C φ⇩0_in_hom by simp
show "«φ⇩0 f : hom.map f ⇒ GF.map f»"
using f hom.ide_char⇩S⇩b⇩C hom.arr_char⇩S⇩b⇩C hom'.ide_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C F.preserves_arr
φ⇩0_in_hom
by auto
qed
next
fix μ
assume μ: "hom.arr μ"
show "hom.comp (φ⇩0 (hom.cod μ)) (hom.map μ) =
hom.comp (GF.map μ) (φ⇩0 (hom.dom μ))"
proof -
have "hom.comp (φ⇩0 (hom.cod μ)) (hom.map μ) = φ⇩0 (cod μ) ⋅ μ"
proof -
have "hom.map μ = μ"
using μ by simp
moreover have "φ⇩0 (hom.cod μ) = φ⇩0 (cod μ)"
using μ hom.arr_char⇩S⇩b⇩C hom.cod_char⇩S⇩b⇩C by simp
moreover have "hom.arr (φ⇩0 (cod μ))"
using μ hom.arr_char⇩S⇩b⇩C φ⇩0_in_hom [of "cod μ"]
by (metis hom.arr_cod hom.cod_simp ide_cod in_hhom_def)
moreover have "seq (φ⇩0 (cod μ)) μ"
proof
show 1: "«μ : dom μ ⇒ cod μ»"
using μ hom.arr_char⇩S⇩b⇩C by auto
show "«φ⇩0 (cod μ) : cod μ ⇒ d⇩1 ⋆ (e⇩1 ⋆ cod μ ⋆ d⇩0) ⋆ e⇩0»"
using μ hom.arr_char⇩S⇩b⇩C φ⇩0_in_hom
by (metis 1 arrI hom.arr_cod hom.cod_simp ide_cod)
qed
ultimately show ?thesis
using μ hom.comp_char by simp
qed
also have "... = (d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0]) ⋅ 𝖺[d⇩1, e⇩1, (cod μ ⋆ d⇩0) ⋆ e⇩0] ⋅
((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[cod μ, d⇩0, e⇩0]) ⋅ (η⇩1 ⋆ cod μ ⋆ η⇩0) ⋅
𝗅⇧-⇧1[cod μ ⋆ src e⇩0] ⋅ 𝗋⇧-⇧1[cod μ] ⋅ μ"
using μ hom.arr_char⇩S⇩b⇩C comp_assoc by auto
also have "... = ((d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0]) ⋅ 𝖺[d⇩1, e⇩1, (cod μ ⋆ d⇩0) ⋆ e⇩0] ⋅
((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[cod μ, d⇩0, e⇩0]) ⋅ (η⇩1 ⋆ cod μ ⋆ η⇩0) ⋅
𝗅⇧-⇧1[cod μ ⋆ src e⇩0] ⋅ (μ ⋆ src e⇩0)) ⋅ 𝗋⇧-⇧1[dom μ]"
using μ hom.arr_char⇩S⇩b⇩C runit'_naturality [of μ] comp_assoc by auto
also have "... = ((d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0]) ⋅ 𝖺[d⇩1, e⇩1, (cod μ ⋆ d⇩0) ⋆ e⇩0] ⋅
((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[cod μ, d⇩0, e⇩0]) ⋅ (η⇩1 ⋆ cod μ ⋆ η⇩0) ⋅
(src e⇩1 ⋆ μ ⋆ src e⇩0) ⋅ 𝗅⇧-⇧1[dom μ ⋆ src e⇩0]) ⋅ 𝗋⇧-⇧1[dom μ]"
using μ hom.arr_char⇩S⇩b⇩C lunit'_naturality [of "μ ⋆ src e⇩0"] by force
also have "... = ((d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0]) ⋅ 𝖺[d⇩1, e⇩1, (cod μ ⋆ d⇩0) ⋆ e⇩0] ⋅
((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[cod μ, d⇩0, e⇩0]) ⋅ (η⇩1 ⋆ cod μ ⋆ η⇩0) ⋅
(src e⇩1 ⋆ μ ⋆ src e⇩0)) ⋅ 𝗅⇧-⇧1[dom μ ⋆ src e⇩0] ⋅ 𝗋⇧-⇧1[dom μ]"
using comp_assoc by simp
also have "... = ((d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0]) ⋅ 𝖺[d⇩1, e⇩1, (cod μ ⋆ d⇩0) ⋆ e⇩0] ⋅
((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[cod μ, d⇩0, e⇩0]) ⋅ ((d⇩1 ⋆ e⇩1) ⋆ μ ⋆ d⇩0 ⋆ e⇩0)) ⋅
(η⇩1 ⋆ dom μ ⋆ η⇩0) ⋅ 𝗅⇧-⇧1[dom μ ⋆ src e⇩0] ⋅ 𝗋⇧-⇧1[dom μ]"
proof -
have "(η⇩1 ⋆ cod μ ⋆ η⇩0) ⋅ (src e⇩1 ⋆ μ ⋆ src e⇩0) = η⇩1 ⋆ μ ⋆ η⇩0"
using μ hom.arr_char⇩S⇩b⇩C comp_arr_dom comp_cod_arr
interchange [of η⇩1 "src e⇩1" "cod μ ⋆ η⇩0" "μ ⋆ src e⇩0"]
interchange [of "cod μ" μ η⇩0 "src e⇩0"]
by (metis e⇩0.unit_in_hom(1) e⇩0.unit_simps(2) e⇩1.unit_simps(1) e⇩1.unit_simps(2)
hseqI' in_hhom_def)
also have "... = ((d⇩1 ⋆ e⇩1) ⋆ μ ⋆ d⇩0 ⋆ e⇩0) ⋅ (η⇩1 ⋆ dom μ ⋆ η⇩0)"
proof -
have "η⇩1 ⋆ μ ⋆ η⇩0 = (d⇩1 ⋆ e⇩1) ⋅ η⇩1 ⋆ μ ⋅ dom μ ⋆ (d⇩0 ⋆ e⇩0) ⋅ η⇩0"
using μ hom.arr_char⇩S⇩b⇩C comp_arr_dom comp_cod_arr by auto
also have "... = (d⇩1 ⋆ e⇩1) ⋅ η⇩1 ⋆ (μ ⋆ d⇩0 ⋆ e⇩0) ⋅ (dom μ ⋆ η⇩0)"
using μ hom.arr_char⇩S⇩b⇩C comp_cod_arr
interchange [of μ "dom μ" "d⇩0 ⋆ e⇩0" η⇩0]
by auto
also have "... = ((d⇩1 ⋆ e⇩1) ⋆ μ ⋆ d⇩0 ⋆ e⇩0) ⋅ (η⇩1 ⋆ dom μ ⋆ η⇩0)"
using μ hom.arr_char⇩S⇩b⇩C comp_arr_dom comp_cod_arr
interchange [of "d⇩1 ⋆ e⇩1" η⇩1 "μ ⋆ d⇩0 ⋆ e⇩0" "dom μ ⋆ η⇩0"]
interchange [of μ "dom μ" "d⇩0 ⋆ e⇩0" η⇩0]
by (metis e⇩0.unit_in_hom(1) e⇩0.unit_simps(1) e⇩0.unit_simps(3) e⇩1.unit_simps(1)
e⇩1.unit_simps(3) hom.inclusion hseqI)
finally show ?thesis by simp
qed
finally have "(η⇩1 ⋆ cod μ ⋆ η⇩0) ⋅ (src e⇩1 ⋆ μ ⋆ src e⇩0) =
((d⇩1 ⋆ e⇩1) ⋆ μ ⋆ d⇩0 ⋆ e⇩0) ⋅ (η⇩1 ⋆ dom μ ⋆ η⇩0)"
by simp
thus ?thesis
using comp_assoc by simp
qed
also have "... = ((d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0]) ⋅ 𝖺[d⇩1, e⇩1, (cod μ ⋆ d⇩0) ⋆ e⇩0] ⋅
((d⇩1 ⋆ e⇩1) ⋆ (μ ⋆ d⇩0) ⋆ e⇩0) ⋅ ((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[dom μ, d⇩0, e⇩0])) ⋅
(η⇩1 ⋆ dom μ ⋆ η⇩0) ⋅ 𝗅⇧-⇧1[dom μ ⋆ src e⇩0] ⋅ 𝗋⇧-⇧1[dom μ]"
using μ hom.arr_char⇩S⇩b⇩C e⇩0.antipar e⇩1.antipar assoc'_naturality [of μ d⇩0 e⇩0]
whisker_left [of "d⇩1 ⋆ e⇩1" "𝖺⇧-⇧1[cod μ, d⇩0, e⇩0]" "μ ⋆ d⇩0 ⋆ e⇩0"]
whisker_left [of "d⇩1 ⋆ e⇩1" "(μ ⋆ d⇩0) ⋆ e⇩0" "𝖺⇧-⇧1[dom μ, d⇩0, e⇩0]"]
by auto
also have "... = ((d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0]) ⋅ 𝖺[d⇩1, e⇩1, (cod μ ⋆ d⇩0) ⋆ e⇩0] ⋅
((d⇩1 ⋆ e⇩1) ⋆ (μ ⋆ d⇩0) ⋆ e⇩0)) ⋅ ((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[dom μ, d⇩0, e⇩0]) ⋅
(η⇩1 ⋆ dom μ ⋆ η⇩0) ⋅ 𝗅⇧-⇧1[dom μ ⋆ src e⇩0] ⋅ 𝗋⇧-⇧1[dom μ]"
using comp_assoc by simp
also have "... = ((d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0]) ⋅ (d⇩1 ⋆ e⇩1 ⋆ (μ ⋆ d⇩0) ⋆ e⇩0) ⋅
𝖺[d⇩1, e⇩1, (dom μ ⋆ d⇩0) ⋆ e⇩0]) ⋅ ((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[dom μ, d⇩0, e⇩0]) ⋅
(η⇩1 ⋆ dom μ ⋆ η⇩0) ⋅ 𝗅⇧-⇧1[dom μ ⋆ src e⇩0] ⋅ 𝗋⇧-⇧1[dom μ]"
using μ hom.arr_char⇩S⇩b⇩C e⇩0.antipar e⇩1.antipar
assoc_naturality [of d⇩1 e⇩1 "(μ ⋆ d⇩0) ⋆ e⇩0"] hseqI
by auto
also have "... = ((d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0]) ⋅ (d⇩1 ⋆ e⇩1 ⋆ (μ ⋆ d⇩0) ⋆ e⇩0)) ⋅
𝖺[d⇩1, e⇩1, (dom μ ⋆ d⇩0) ⋆ e⇩0] ⋅ ((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[dom μ, d⇩0, e⇩0]) ⋅
(η⇩1 ⋆ dom μ ⋆ η⇩0) ⋅ 𝗅⇧-⇧1[dom μ ⋆ src e⇩0] ⋅ 𝗋⇧-⇧1[dom μ]"
using comp_assoc by simp
also have "... = ((d⇩1 ⋆ (e⇩1 ⋆ μ ⋆ d⇩0) ⋆ e⇩0) ⋅ (d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, dom μ ⋆ d⇩0, e⇩0])) ⋅
𝖺[d⇩1, e⇩1, (dom μ ⋆ d⇩0) ⋆ e⇩0] ⋅ ((d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[dom μ, d⇩0, e⇩0]) ⋅
(η⇩1 ⋆ dom μ ⋆ η⇩0) ⋅ 𝗅⇧-⇧1[dom μ ⋆ src e⇩0] ⋅ 𝗋⇧-⇧1[dom μ]"
using μ hom.arr_char⇩S⇩b⇩C e⇩0.antipar e⇩1.antipar
assoc'_naturality [of e⇩1 "μ ⋆ d⇩0" e⇩0]
whisker_left [of d⇩1 "𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0]" "e⇩1 ⋆ (μ ⋆ d⇩0) ⋆ e⇩0"]
whisker_left [of d⇩1 "(e⇩1 ⋆ μ ⋆ d⇩0) ⋆ e⇩0" "𝖺⇧-⇧1[e⇩1, dom μ ⋆ d⇩0, e⇩0]"]
by auto
also have "... = hom.comp (GF.map μ) (φ⇩0 (hom.dom μ))"
proof -
have "hom.arr (GF.map μ)"
using μ by blast
moreover have "hom.arr (φ⇩0 (hom.dom μ))"
using μ hom.arr_char⇩S⇩b⇩C hom.in_hom_char⇩S⇩b⇩C φ⇩0_in_hom(1) hom.dom_closed hom.dom_simp
hom.inclusion ide_dom
by metis
moreover have "seq (GF.map μ) (φ⇩0 (hom.dom μ))"
proof
show "«φ⇩0 (hom.dom μ) : dom μ ⇒ d⇩1 ⋆ (e⇩1 ⋆ dom μ ⋆ d⇩0) ⋆ e⇩0»"
using μ hom.arr_char⇩S⇩b⇩C hom.dom_char⇩S⇩b⇩C hom.in_hom_char⇩S⇩b⇩C φ⇩0_in_hom hom.dom_closed
hom.dom_simp hom.inclusion ide_dom
by metis
show "«GF.map μ : d⇩1 ⋆ (e⇩1 ⋆ dom μ ⋆ d⇩0) ⋆ e⇩0 ⇒ d⇩1 ⋆ (e⇩1 ⋆ cod μ ⋆ d⇩0) ⋆ e⇩0»"
using μ hom.arr_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C F.preserves_arr
apply simp
apply (intro hcomp_in_vhom)
by (auto simp add: e⇩0.antipar e⇩1.antipar in_hhom_def)
qed
ultimately show ?thesis
using μ hom.comp_char comp_assoc hom.dom_simp by auto
qed
finally show ?thesis by blast
qed
qed
lemma transformation_by_components_φ⇩0:
shows "transformation_by_components hom.comp hom.comp hom.map (G o F) φ⇩0"
..
interpretation φ: natural_isomorphism hom.comp hom.comp hom.map ‹G o F› φ.map
proof
fix f
assume "hom.ide f"
hence f: "ide f ∧ «f : src e⇩0 → src e⇩1»"
using hom.ide_char⇩S⇩b⇩C hom.arr_char⇩S⇩b⇩C by simp
show "hom.iso (φ.map f)"
proof (unfold hom.iso_char⇩S⇩b⇩C hom.arr_char⇩S⇩b⇩C, intro conjI)
show "iso (φ.map f)"
using f iso_φ⇩0 φ.map_simp_ide hom.ide_char⇩S⇩b⇩C hom.arr_char⇩S⇩b⇩C by simp
moreover show "«φ.map f : src e⇩0 → src e⇩1»"
using f hom.ide_char hom.arr_char⇩S⇩b⇩C by blast
ultimately show "«inv (φ.map f) : src e⇩0 → src e⇩1»"
by auto
qed
qed
lemma natural_isomorphism_φ:
shows "natural_isomorphism hom.comp hom.comp hom.map (G o F) φ.map"
..
definition φ
where "φ ≡ φ.map"
lemma φ_ide_simp:
assumes "«f : src e⇩0 → src e⇩1»" and "ide f"
shows "φ f = φ⇩0 f"
unfolding φ_def
using assms hom.ide_char⇩S⇩b⇩C hom.arr_char⇩S⇩b⇩C by simp
lemma φ_components_are_iso:
assumes "«f : src e⇩0 → src e⇩1»" and "ide f"
shows "iso (φ f)"
using assms φ_def φ.components_are_iso hom.ide_char⇩S⇩b⇩C hom.arr_char⇩S⇩b⇩C hom.iso_char⇩S⇩b⇩C
by simp
lemma φ_eq:
shows "φ = (λμ. if «μ : src e⇩0 → src e⇩1» then φ⇩0 (cod μ) ⋅ μ else null)"
proof
fix μ
have "¬ «μ : src e⇩0 → src e⇩1» ⟹ φ.map μ = null"
using hom.comp_char hom.null_char hom.arr_char⇩S⇩b⇩C
by (simp add: φ.is_extensional)
moreover have "«μ : src e⇩0 → src e⇩1» ⟹ φ.map μ = φ⇩0 (cod μ) ⋅ μ"
unfolding φ.map_def
apply auto
using hom.comp_char hom.arr_char⇩S⇩b⇩C hom.dom_simp hom.cod_simp
apply simp
by (metis (no_types, lifting) φ⇩0_in_hom(1) hom.cod_closed hom.inclusion ide_cod local.ext)
ultimately show "φ μ = (if «μ : src e⇩0 → src e⇩1» then φ⇩0 (cod μ) ⋅ μ else null)"
unfolding φ_def by auto
qed
lemma φ_in_hom [intro]:
assumes "«μ : src e⇩0 → src e⇩1»"
shows "«φ μ : src e⇩0 → src e⇩1»"
and "«φ μ : dom μ ⇒ d⇩1 ⋆ (e⇩1 ⋆ cod μ ⋆ d⇩0) ⋆ e⇩0»"
proof -
show "«φ μ : src e⇩0 → src e⇩1»"
using assms φ_eq φ_def hom.arr_char⇩S⇩b⇩C φ.preserves_reflects_arr by presburger
show "«φ μ : dom μ ⇒ d⇩1 ⋆ (e⇩1 ⋆ cod μ ⋆ d⇩0) ⋆ e⇩0»"
unfolding φ_eq
using assms apply simp
apply (intro comp_in_homI)
apply auto
proof -
show "«𝗋⇧-⇧1[cod μ] : cod μ ⇒ cod μ ⋆ src e⇩0»"
using assms by auto
show "«𝗅⇧-⇧1[cod μ ⋆ src e⇩0] : cod μ ⋆ src e⇩0 ⇒ src e⇩1 ⋆ cod μ ⋆ src e⇩0»"
using assms by auto
show "«η⇩1 ⋆ cod μ ⋆ η⇩0 : src e⇩1 ⋆ cod μ ⋆ src e⇩0 ⇒ (d⇩1 ⋆ e⇩1) ⋆ cod μ ⋆ (d⇩0 ⋆ e⇩0)»"
using assms e⇩0.unit_in_hom(2) e⇩1.unit_in_hom(2)
apply (intro hcomp_in_vhom)
apply auto
by fastforce
show "«(d⇩1 ⋆ e⇩1) ⋆ 𝖺⇧-⇧1[cod μ, d⇩0, e⇩0] :
(d⇩1 ⋆ e⇩1) ⋆ cod μ ⋆ d⇩0 ⋆ e⇩0 ⇒ (d⇩1 ⋆ e⇩1) ⋆ (cod μ ⋆ d⇩0) ⋆ e⇩0»"
using assms assoc'_in_hom e⇩0.antipar(1-2) e⇩1.antipar(2)
apply (intro hcomp_in_vhom) by auto
show "«𝖺[d⇩1, e⇩1, (cod μ ⋆ d⇩0) ⋆ e⇩0] :
(d⇩1 ⋆ e⇩1) ⋆ (cod μ ⋆ d⇩0) ⋆ e⇩0 ⇒ d⇩1 ⋆ e⇩1 ⋆ (cod μ ⋆ d⇩0) ⋆ e⇩0»"
using assms assoc_in_hom e⇩0.antipar(1-2) e⇩1.antipar(2) by auto
show "«d⇩1 ⋆ 𝖺⇧-⇧1[e⇩1, cod μ ⋆ d⇩0, e⇩0] :
d⇩1 ⋆ e⇩1 ⋆ (cod μ ⋆ d⇩0) ⋆ e⇩0 ⇒ d⇩1 ⋆ (e⇩1 ⋆ cod μ ⋆ d⇩0) ⋆ e⇩0»"
using assms assoc'_in_hom [of "d⇩1" "e⇩1 ⋆ cod μ ⋆ d⇩0" "e⇩0"]
e⇩0.antipar(1-2) e⇩1.antipar(1-2)
apply (intro hcomp_in_vhom)
apply auto
by fastforce
qed
qed
lemma φ_simps [simp]:
assumes "«μ : src e⇩0 → src e⇩1»"
shows "arr (φ μ)"
and "src (φ μ) = src e⇩0" and "trg (φ μ) = src e⇩1"
and "dom (φ μ) = dom μ" and "cod (φ μ) = d⇩1 ⋆ (e⇩1 ⋆ cod μ ⋆ d⇩0) ⋆ e⇩0"
using assms φ_in_hom by auto
interpretation d⇩0: equivalence_in_bicategory V H 𝖺 𝗂 src trg d⇩0 e⇩0 ‹inv ε⇩0› ‹inv η⇩0›
using e⇩0.dual_equivalence by simp
interpretation d⇩1: equivalence_in_bicategory V H 𝖺 𝗂 src trg d⇩1 e⇩1 ‹inv ε⇩1› ‹inv η⇩1›
using e⇩1.dual_equivalence by simp
interpretation d⇩0e⇩0: two_equivalences_in_bicategory V H 𝖺 𝗂 src trg
d⇩0 e⇩0 ‹inv ε⇩0› ‹inv η⇩0› d⇩1 e⇩1 ‹inv ε⇩1› ‹inv η⇩1›
..
interpretation ψ: inverse_transformation hom'.comp hom'.comp hom'.map ‹F o G› d⇩0e⇩0.φ
proof -
interpret ψ': natural_isomorphism hom'.comp hom'.comp hom'.map ‹F o G› d⇩0e⇩0.φ
using d⇩0e⇩0.natural_isomorphism_φ e⇩0.antipar e⇩1.antipar d⇩0e⇩0.φ_eq d⇩0e⇩0.φ_def by metis
show "inverse_transformation hom'.comp hom'.comp hom'.map (F o G) d⇩0e⇩0.φ"
..
qed
definition ψ
where "ψ ≡ ψ.map"
lemma ψ_ide_simp:
assumes "«f': trg e⇩0 → trg e⇩1»" and "ide f'"
shows "ψ f' = 𝗋[f'] ⋅ 𝗅[f' ⋆ trg e⇩0] ⋅ (ε⇩1 ⋆ f' ⋆ ε⇩0) ⋅ ((e⇩1 ⋆ d⇩1) ⋆ 𝖺[f', e⇩0, d⇩0]) ⋅
𝖺⇧-⇧1[e⇩1, d⇩1, (f' ⋆ e⇩0) ⋆ d⇩0] ⋅ (e⇩1 ⋆ 𝖺[d⇩1, f' ⋆ e⇩0, d⇩0])"
proof -
have "hom'.ide f'"
using assms hom'.ide_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C by simp
hence "ψ.map f' = hom'.inv (d⇩0e⇩0.φ f')"
using assms by simp
also have "... = inv (d⇩0e⇩0.φ f')"
using hom'.inv_char⇩S⇩b⇩C ‹hom'.ide f'› by simp
also have "... = inv (d⇩0e⇩0.φ⇩0 f')"
using assms e⇩0.antipar e⇩1.antipar d⇩0e⇩0.φ_eq d⇩0e⇩0.φ_ide_simp [of f'] by simp
also have "... = ((((inv 𝗋⇧-⇧1[f'] ⋅ inv 𝗅⇧-⇧1[f' ⋆ trg e⇩0]) ⋅ inv (inv ε⇩1 ⋆ f' ⋆ inv ε⇩0)) ⋅
inv ((e⇩1 ⋆ d⇩1) ⋆ 𝖺⇧-⇧1[f', e⇩0, d⇩0])) ⋅ inv 𝖺[e⇩1, d⇩1, (f' ⋆ e⇩0) ⋆ d⇩0]) ⋅
inv (e⇩1 ⋆ 𝖺⇧-⇧1[d⇩1, f' ⋆ e⇩0, d⇩0])"
proof -
text ‹There has to be a better way to do this.›
have 1: "⋀A B C D E F.
⟦ iso A; iso B; iso C; iso D; iso E; iso F;
arr (((((A ⋅ B) ⋅ C) ⋅ D) ⋅ E) ⋅ F) ⟧ ⟹
inv (((((A ⋅ B) ⋅ C) ⋅ D) ⋅ E) ⋅ F) =
inv F ⋅ inv E ⋅ inv D ⋅ inv C ⋅ inv B ⋅ inv A"
using inv_comp isos_compose seqE by metis
have "arr (d⇩0e⇩0.φ⇩0 f')"
using assms e⇩0.antipar(2) e⇩1.antipar(2) d⇩0e⇩0.iso_φ⇩0 [of f'] iso_is_arr by simp
moreover have "iso 𝗋⇧-⇧1[f']"
using assms iso_runit' by simp
moreover have "iso 𝗅⇧-⇧1[f' ⋆ trg e⇩0]"
using assms iso_lunit' by auto
moreover have "iso (inv ε⇩1 ⋆ f' ⋆ inv ε⇩0)"
using assms e⇩0.antipar(2) e⇩1.antipar(2) in_hhom_def by simp
moreover have "iso ((e⇩1 ⋆ d⇩1) ⋆ 𝖺⇧-⇧1[f', e⇩0, d⇩0])"
using assms e⇩0.antipar e⇩1.antipar(1) e⇩1.antipar(2) in_hhom_def iso_hcomp
by (metis calculation(1) e⇩0.ide_left e⇩0.ide_right e⇩1.ide_left e⇩1.ide_right hseqE
ide_is_iso iso_assoc' seqE)
moreover have "iso 𝖺[e⇩1, d⇩1, (f' ⋆ e⇩0) ⋆ d⇩0]"
using assms e⇩0.antipar e⇩1.antipar by auto
moreover have "iso (e⇩1 ⋆ 𝖺⇧-⇧1[d⇩1, f' ⋆ e⇩0, d⇩0])"
using assms e⇩0.antipar e⇩1.antipar
by (metis calculation(1) e⇩0.ide_left e⇩0.ide_right e⇩1.ide_left e⇩1.ide_right
iso_hcomp ide_hcomp hseqE ideD(1) ide_is_iso in_hhomE iso_assoc'
seqE hcomp_simps(1-2))
ultimately show ?thesis
using 1 [of "e⇩1 ⋆ 𝖺⇧-⇧1[d⇩1, f' ⋆ e⇩0, d⇩0]" "𝖺[e⇩1, d⇩1, (f' ⋆ e⇩0) ⋆ d⇩0]"
"(e⇩1 ⋆ d⇩1) ⋆ 𝖺⇧-⇧1[f', e⇩0, d⇩0]" "inv ε⇩1 ⋆ f' ⋆ inv ε⇩0" "𝗅⇧-⇧1[f' ⋆ trg e⇩0]" "𝗋⇧-⇧1[f']"]
comp_assoc
by (metis e⇩0.antipar(2))
qed
also have "... = inv 𝗋⇧-⇧1[f'] ⋅ inv 𝗅⇧-⇧1[f' ⋆ trg e⇩0] ⋅ inv (inv ε⇩1 ⋆ f' ⋆ inv ε⇩0) ⋅
inv ((e⇩1 ⋆ d⇩1) ⋆ 𝖺⇧-⇧1[f', e⇩0, d⇩0]) ⋅ inv 𝖺[e⇩1, d⇩1, (f' ⋆ e⇩0) ⋆ d⇩0] ⋅
inv (e⇩1 ⋆ 𝖺⇧-⇧1[d⇩1, f' ⋆ e⇩0, d⇩0])"
using comp_assoc by simp
also have "... = 𝗋[f'] ⋅ 𝗅[f' ⋆ trg e⇩0] ⋅ (ε⇩1 ⋆ f' ⋆ ε⇩0) ⋅ ((e⇩1 ⋆ d⇩1) ⋆ 𝖺[f', e⇩0, d⇩0]) ⋅
𝖺⇧-⇧1[e⇩1, d⇩1, (f' ⋆ e⇩0) ⋆ d⇩0] ⋅ (e⇩1 ⋆ 𝖺[d⇩1, f' ⋆ e⇩0, d⇩0])"
proof -
have "inv 𝗋⇧-⇧1[f'] = 𝗋[f']"
using assms inv_inv iso_runit by blast
moreover have "inv 𝗅⇧-⇧1[f' ⋆ trg e⇩0] = 𝗅[f' ⋆ trg e⇩0]"
using assms iso_lunit by auto
moreover have "inv (inv ε⇩1 ⋆ f' ⋆ inv ε⇩0) = ε⇩1 ⋆ f' ⋆ ε⇩0"
proof -
have "src (inv ε⇩1) = trg f'"
using assms(1) e⇩1.antipar(2) by auto
moreover have "src f' = trg (inv ε⇩0)"
using assms(1) e⇩0.antipar(2) by auto
ultimately show ?thesis
using assms(2) e⇩0.counit_is_iso e⇩1.counit_is_iso by simp
qed
ultimately show ?thesis
using assms e⇩0.antipar e⇩1.antipar by auto
qed
finally show ?thesis
using ψ_def by simp
qed
lemma ψ_components_are_iso:
assumes "«f' : trg e⇩0 → trg e⇩1»" and "ide f'"
shows "iso (ψ f')"
using assms ψ_def ψ.components_are_iso hom'.ide_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C hom'.iso_char⇩S⇩b⇩C
by simp
lemma ψ_eq:
shows "ψ = (λμ'. if «μ': trg e⇩0 → trg e⇩1» then
μ' ⋅ 𝗋[dom μ'] ⋅ 𝗅[dom μ' ⋆ trg e⇩0] ⋅ (ε⇩1 ⋆ dom μ' ⋆ ε⇩0) ⋅
((e⇩1 ⋆ d⇩1) ⋆ 𝖺[dom μ', e⇩0, d⇩0]) ⋅ 𝖺⇧-⇧1[e⇩1, d⇩1, (dom μ' ⋆ e⇩0) ⋆ d⇩0] ⋅
(e⇩1 ⋆ 𝖺[d⇩1, dom μ' ⋆ e⇩0, d⇩0])
else null)"
proof
fix μ'
have "¬ «μ': trg e⇩0 → trg e⇩1» ⟹ ψ.map μ' = null"
using ψ.is_extensional hom'.arr_char⇩S⇩b⇩C hom'.null_char by simp
moreover have "«μ': trg e⇩0 → trg e⇩1» ⟹
ψ.map μ' = μ' ⋅ 𝗋[dom μ'] ⋅ 𝗅[dom μ' ⋆ trg e⇩0] ⋅ (ε⇩1 ⋆ dom μ' ⋆ ε⇩0) ⋅
((e⇩1 ⋆ d⇩1) ⋆ 𝖺[dom μ', e⇩0, d⇩0]) ⋅ 𝖺⇧-⇧1[e⇩1, d⇩1, (dom μ' ⋆ e⇩0) ⋆ d⇩0] ⋅
(e⇩1 ⋆ 𝖺[d⇩1, dom μ' ⋆ e⇩0, d⇩0])"
proof -
assume μ': "«μ': trg e⇩0 → trg e⇩1»"
have "«ψ.map (dom μ') : trg e⇩0 → trg e⇩1»"
using μ' hom'.arr_char⇩S⇩b⇩C hom'.dom_closed by auto
moreover have "seq μ' (ψ.map (dom μ'))"
proof -
have "hom'.seq μ' (ψ.map (dom μ'))"
using μ' ψ.preserves_cod hom'.arrI⇩S⇩b⇩C hom'.dom_simp hom'.cod_simp
apply (intro hom'.seqI) by auto
thus ?thesis
using hom'.seq_char⇩S⇩b⇩C by blast
qed
ultimately show ?thesis
using μ' ψ.is_natural_1 [of μ'] hom'.comp_char hom'.arr_char⇩S⇩b⇩C hom'.dom_closed
ψ_ide_simp [of "dom μ'"] hom'.dom_simp hom'.cod_simp
apply auto
by (metis ψ_def hom'.inclusion ide_dom)
qed
ultimately show "ψ μ' = (if «μ' : trg e⇩0 → trg e⇩1» then
μ' ⋅ 𝗋[dom μ'] ⋅ 𝗅[dom μ' ⋆ trg e⇩0] ⋅ (ε⇩1 ⋆ dom μ' ⋆ ε⇩0) ⋅
((e⇩1 ⋆ d⇩1) ⋆ 𝖺[dom μ', e⇩0, d⇩0]) ⋅
𝖺⇧-⇧1[e⇩1, d⇩1, (dom μ' ⋆ e⇩0) ⋆ d⇩0] ⋅
(e⇩1 ⋆ 𝖺[d⇩1, dom μ' ⋆ e⇩0, d⇩0])
else null)"
unfolding ψ_def by argo
qed
lemma ψ_in_hom [intro]:
assumes "«μ' : trg e⇩0 → trg e⇩1»"
shows "«ψ μ' : trg e⇩0 → trg e⇩1»"
and "«ψ μ' : e⇩1 ⋆ (d⇩1 ⋆ dom μ' ⋆ e⇩0) ⋆ d⇩0 ⇒ cod μ'»"
proof -
have 0: "ψ μ' = ψ.map μ'"
using ψ_def by auto
hence 1: "hom'.arr (ψ μ')"
using assms hom'.arr_char⇩S⇩b⇩C ψ.preserves_reflects_arr by auto
show "«ψ μ' : trg e⇩0 → trg e⇩1»"
using 1 hom'.arr_char⇩S⇩b⇩C by blast
show "«ψ μ' : e⇩1 ⋆ (d⇩1 ⋆ dom μ' ⋆ e⇩0) ⋆ d⇩0 ⇒ cod μ'»"
using assms 0 1 ψ.preserves_hom hom'.in_hom_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C
e⇩0.antipar e⇩1.antipar ψ.preserves_dom ψ.preserves_cod hom'.dom_char⇩S⇩b⇩C
apply (intro in_homI)
apply auto[1]
proof -
show "dom (ψ μ') = e⇩1 ⋆ (d⇩1 ⋆ dom μ' ⋆ e⇩0) ⋆ d⇩0"
proof -
have "hom'.dom (ψ μ') = FG.map (hom'.dom μ')"
using assms 0 ψ.preserves_dom hom'.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting))
thus ?thesis
using assms 0 1 hom.arr_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C hom'.dom_char⇩S⇩b⇩C G.preserves_arr
hom'.dom_closed
by auto
qed
show "cod (ψ μ') = cod μ'"
proof -
have "hom'.cod (ψ μ') = cod μ'"
using assms 0 ψ.preserves_cod hom'.arr_char⇩S⇩b⇩C hom'.cod_simp by auto
thus ?thesis
using assms 0 1 hom'.arr_char⇩S⇩b⇩C hom'.cod_char⇩S⇩b⇩C G.preserves_arr hom'.cod_closed by auto
qed
qed
qed
lemma ψ_simps [simp]:
assumes "«μ' : trg e⇩0 → trg e⇩1»"
shows "arr (ψ μ')"
and "src (ψ μ') = trg e⇩0" and "trg (ψ μ') = trg e⇩1"
and "dom (ψ μ') = e⇩1 ⋆ (d⇩1 ⋆ dom μ' ⋆ e⇩0) ⋆ d⇩0" and "cod (ψ μ') = cod μ'"
using assms ψ_in_hom by auto
interpretation equivalence_of_categories hom'.comp hom.comp F G φ ψ
proof -
interpret φ: natural_isomorphism hom.comp hom.comp hom.map ‹G o F› φ
using φ.natural_isomorphism_axioms φ_def by simp
interpret ψ: natural_isomorphism hom'.comp hom'.comp ‹F o G› hom'.map ψ
using ψ.natural_isomorphism_axioms ψ_def by simp
show "equivalence_of_categories hom'.comp hom.comp F G φ ψ"
..
qed
lemma induces_equivalence_of_hom_categories:
shows "equivalence_of_categories hom'.comp hom.comp F G φ ψ"
..
lemma equivalence_functor_F:
shows "equivalence_functor hom.comp hom'.comp F"
proof -
interpret φ': inverse_transformation hom.comp hom.comp hom.map ‹G o F› φ ..
interpret ψ': inverse_transformation hom'.comp hom'.comp ‹F o G› hom'.map ψ ..
interpret E: equivalence_of_categories hom.comp hom'.comp G F ψ'.map φ'.map ..
show ?thesis
using E.equivalence_functor_axioms by simp
qed
lemma equivalence_functor_G:
shows "equivalence_functor hom'.comp hom.comp G"
using equivalence_functor_axioms by simp
end
context bicategory
begin
text ‹
We now use the just-established equivalence of hom-categories to prove some cancellation
laws for equivalence maps. It is relatively straightforward to prove these results
directly, without using the just-established equivalence, but the proofs are somewhat
longer that way.
›
lemma equivalence_cancel_left:
assumes "equivalence_map e"
and "par μ μ'" and "src e = trg μ" and "e ⋆ μ = e ⋆ μ'"
shows "μ = μ'"
proof -
obtain d η ε where dηε: "equivalence_in_bicategory V H 𝖺 𝗂 src trg e d η ε"
using assms equivalence_map_def by auto
interpret e: equivalence_in_bicategory V H 𝖺 𝗂 src trg e d η ε
using dηε by simp
interpret i: equivalence_in_bicategory V H 𝖺 𝗂 src trg
‹src μ› ‹src μ› ‹inv 𝗂[src μ]› ‹𝗂[src μ]›
using assms iso_unit obj_src
by unfold_locales simp_all
interpret two_equivalences_in_bicategory V H 𝖺 𝗂 src trg
‹src μ› ‹src μ› ‹inv 𝗂[src μ]› ‹𝗂[src μ]› e d η ε
..
interpret hom: subcategory V ‹λμ'. in_hhom μ' (src (src μ)) (src e)›
using hhom_is_subcategory by blast
interpret hom': subcategory V ‹λμ'. in_hhom μ' (trg (src μ)) (trg e)›
using hhom_is_subcategory by blast
interpret F: equivalence_functor hom.comp hom'.comp ‹λμ'. e ⋆ μ' ⋆ src μ›
using equivalence_functor_F by simp
have "F μ = F μ'"
using assms hom.arr_char⇩S⇩b⇩C
apply simp
by (metis e.ide_left hcomp_reassoc(2) i.ide_right ideD(1) src_dom trg_dom trg_src)
moreover have "hom.par μ μ'"
using assms hom.arr_char⇩S⇩b⇩C hom.dom_char⇩S⇩b⇩C hom.cod_char⇩S⇩b⇩C
by (metis (no_types, lifting) in_hhomI src_dom src_src trg_dom)
ultimately show "μ = μ'"
using F.is_faithful by blast
qed
lemma equivalence_cancel_right:
assumes "equivalence_map e"
and "par μ μ'" and "src μ = trg e" and "μ ⋆ e = μ' ⋆ e"
shows "μ = μ'"
proof -
obtain d η ε where dηε: "equivalence_in_bicategory V H 𝖺 𝗂 src trg e d η ε"
using assms equivalence_map_def by auto
interpret e: equivalence_in_bicategory V H 𝖺 𝗂 src trg e d η ε
using dηε by simp
interpret i: equivalence_in_bicategory V H 𝖺 𝗂 src trg
‹trg μ› ‹trg μ› ‹inv 𝗂[trg μ]› ‹𝗂[trg μ]›
using assms iso_unit obj_src
by unfold_locales simp_all
interpret two_equivalences_in_bicategory V H 𝖺 𝗂 src trg
e d η ε ‹trg μ› ‹trg μ› ‹inv 𝗂[trg μ]› ‹𝗂[trg μ]›
..
interpret hom: subcategory V ‹λμ'. in_hhom μ' (trg e) (trg (trg μ))›
using hhom_is_subcategory by blast
interpret hom': subcategory V ‹λμ'. in_hhom μ' (src e) (src (trg μ))›
using hhom_is_subcategory by blast
interpret G: equivalence_functor hom.comp hom'.comp ‹λμ'. trg μ ⋆ μ' ⋆ e›
using equivalence_functor_G by simp
have "G μ = G μ'"
using assms hom.arr_char⇩S⇩b⇩C by simp
moreover have "hom.par μ μ'"
using assms hom.arr_char⇩S⇩b⇩C hom.dom_char⇩S⇩b⇩C hom.cod_char⇩S⇩b⇩C
by (metis (no_types, lifting) in_hhomI src_dom trg_dom trg_trg)
ultimately show "μ = μ'"
using G.is_faithful by blast
qed
lemma equivalence_isomorphic_cancel_left:
assumes "equivalence_map e" and "ide f" and "ide f'"
and "src f = src f'" and "src e = trg f" and "e ⋆ f ≅ e ⋆ f'"
shows "f ≅ f'"
proof -
have ef': "src e = trg f'"
using assms R.as_nat_iso.components_are_iso iso_is_arr isomorphic_implies_hpar(2)
by blast
obtain d η ε where e: "equivalence_in_bicategory V H 𝖺 𝗂 src trg e d η ε"
using assms equivalence_map_def by auto
interpret e: equivalence_in_bicategory V H 𝖺 𝗂 src trg e d η ε
using e by simp
interpret i: equivalence_in_bicategory V H 𝖺 𝗂 src trg
‹src f› ‹src f› ‹inv 𝗂[src f]› ‹𝗂[src f]›
using assms iso_unit obj_src
by unfold_locales auto
interpret two_equivalences_in_bicategory V H 𝖺 𝗂 src trg
‹src f› ‹src f› ‹inv 𝗂[src f]› ‹𝗂[src f]› e d η ε
..
interpret hom: subcategory V ‹λμ'. in_hhom μ' (src (src f)) (src e)›
using hhom_is_subcategory by blast
interpret hom': subcategory V ‹λμ'. in_hhom μ' (trg (src f)) (trg e)›
using hhom_is_subcategory by blast
interpret F: equivalence_functor hom.comp hom'.comp ‹λμ'. e ⋆ μ' ⋆ src f›
using equivalence_functor_F by simp
have 1: "F f ≅ F f'"
proof -
have "F f ≅ (e ⋆ f) ⋆ src f"
using assms hcomp_assoc_isomorphic equivalence_map_is_ide isomorphic_symmetric
by auto
also have "... ≅ (e ⋆ f') ⋆ src f'"
using assms ef' by (simp add: hcomp_isomorphic_ide)
also have "... ≅ F f'"
using assms ef' hcomp_assoc_isomorphic equivalence_map_is_ide by auto
finally show ?thesis by blast
qed
show "f ≅ f'"
proof -
obtain ψ where ψ: "«ψ : F f ⇒ F f'» ∧ iso ψ"
using 1 isomorphic_def by auto
have 2: "hom'.iso ψ"
using assms ψ hom'.iso_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C vconn_implies_hpar(1,2)
by auto
have 3: "hom'.in_hom ψ (F f) (F f')"
using assms 2 ψ ef' hom'.in_hom_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C
by (metis F.preserves_reflects_arr hom'.iso_is_arr hom.arr_char⇩S⇩b⇩C i.antipar(1)
ideD(1) ide_in_hom(1) trg_src)
obtain φ where φ: "hom.in_hom φ f f' ∧ F φ = ψ"
using assms 3 ψ F.is_full F.preserves_reflects_arr hom'.in_hom_char⇩S⇩b⇩C hom.ide_char⇩S⇩b⇩C
by fastforce
have "hom.iso φ"
using 2 φ F.reflects_iso by auto
thus ?thesis
using φ isomorphic_def hom.in_hom_char⇩S⇩b⇩C hom.arr_char⇩S⇩b⇩C hom.iso_char⇩S⇩b⇩C by auto
qed
qed
lemma equivalence_isomorphic_cancel_right:
assumes "equivalence_map e" and "ide f" and "ide f'"
and "trg f = trg f'" and "src f = trg e" and "f ⋆ e ≅ f' ⋆ e"
shows "f ≅ f'"
proof -
have f'e: "src f' = trg e"
using assms R.as_nat_iso.components_are_iso iso_is_arr isomorphic_implies_hpar(2)
by blast
obtain d η ε where dηε: "equivalence_in_bicategory V H 𝖺 𝗂 src trg e d η ε"
using assms equivalence_map_def by auto
interpret e: equivalence_in_bicategory V H 𝖺 𝗂 src trg e d η ε
using dηε by simp
interpret i: equivalence_in_bicategory V H 𝖺 𝗂 src trg
‹trg f› ‹trg f› ‹inv 𝗂[trg f]› ‹𝗂[trg f]›
using assms iso_unit obj_src
by unfold_locales auto
interpret two_equivalences_in_bicategory V H 𝖺 𝗂 src trg
e d η ε ‹trg f› ‹trg f› ‹inv 𝗂[trg f]› ‹𝗂[trg f]›
..
interpret hom: subcategory V ‹λμ'. in_hhom μ' (trg e) (trg (trg f))›
using hhom_is_subcategory by blast
interpret hom': subcategory V ‹λμ'. in_hhom μ' (src e) (src (trg f))›
using hhom_is_subcategory by blast
interpret G: equivalence_functor hom.comp hom'.comp ‹λμ'. trg f ⋆ μ' ⋆ e›
using equivalence_functor_G by simp
have 1: "G f ≅ G f'"
using assms hcomp_isomorphic_ide hcomp_ide_isomorphic by simp
show "f ≅ f'"
proof -
obtain ψ where ψ: "«ψ : G f ⇒ G f'» ∧ iso ψ"
using 1 isomorphic_def by auto
have 2: "hom'.iso ψ"
using assms ψ hom'.iso_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C vconn_implies_hpar(1-2) by auto
have 3: "hom'.in_hom ψ (G f) (G f')"
using assms 2 ψ f'e hom'.in_hom_char⇩S⇩b⇩C hom'.arr_char⇩S⇩b⇩C
by (metis G.preserves_arr hom'.iso_is_arr hom.ideI⇩S⇩b⇩C hom.ide_char ideD(1)
ide_in_hom(1) trg_trg)
obtain φ where φ: "hom.in_hom φ f f' ∧ G φ = ψ"
using assms 3 ψ G.is_full G.preserves_reflects_arr hom'.in_hom_char⇩S⇩b⇩C hom.ide_char⇩S⇩b⇩C
by fastforce
have "hom.iso φ"
using 2 φ G.reflects_iso by auto
thus ?thesis
using φ isomorphic_def hom.in_hom_char⇩S⇩b⇩C hom.arr_char⇩S⇩b⇩C hom.iso_char⇩S⇩b⇩C by auto
qed
qed
end
end