| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Bicategory/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 295 kB |
|
Quellcode-Bibliothek Strictness.thySprache: Isabelle |
|||||||||||||||
|
(* Title: Strictness Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2019 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) section "Strictness" theory Strictness imports Category3.ConcreteCategory Pseudofunctor CanonicalIsos begin text ‹ In this section we consider bicategories in which some or all of the canonical i are assumed to be identities. A \emph{normal} bicategory is one in which the un isomorphisms are identities, so that unit laws for horizontal composition are sa ``on the nose''. A \emph{strict} bicategory (also known as a \emph{2-category}) is a bicategory i the unit and associativity isomoprhisms are identities, so that horizontal compo strictly associative as well as strictly unital. From any given bicategory ‹B› we may construct a related strict bicategory ‹S›, its \emph{strictification}, together with a pseudofunctor that embeds ‹B› in ‹S› The Strictness Theorem states that this pseudofunctor is an equivalence pseudofu so that bicategory ‹B› is biequivalent to its strictification. The Strictness Theorem is often used informally to justify suppressing canonical isomorphisms; which amounts to proving a theorem about 2-categories and assertin it holds for all bicategories. Here we are working formally, so we can't just w our hands and mutter something about the Strictness Theorem when we want to avoi dealing with units and associativities. However, in cases where we can establis property we would like to prove is reflected by the embedding of a bicategory in strictification, then we can formally apply the Strictness Theorem to generalize bicategories a result proved for 2-categories. We will apply this approach here simplify the proof of some facts about internal equivalences in a bicategory. subsection "Normal and Strict Bicategories" text ‹ A \emph{normal} bicategory is one in which the unit isomorphisms are identities, so that unit laws for horizontal composition are satisfied ``on the nose''. › locale normal_bicategory = bicategory + assumes strict_lunit: "∧f. ide f ==> l[f] = f" and strict_runit: "∧f. ide f ==> r[f] = f" begin lemma strict_unit: assumes "obj a" shows "ide i[a]" using assms strict_runit unitor_coincidence(2) [of a] by auto lemma strict_lunit': assumes "ide f" shows "l-1[f] = f" using assms strict_lunit by simp lemma strict_runit': assumes "ide f" shows "r-1[f] = f" using assms strict_runit by simp lemma hcomp_obj_arr: assumes "obj b" and "arr f" and "b = trg f" shows "b ⋆ f = f" using assms strict_lunit by (metis comp_arr_dom comp_ide_arr ide_cod ide_dom lunit_naturality) lemma hcomp_arr_obj: assumes "arr f" and "obj a" and "src f = a" shows "f ⋆ a = f" using assms strict_runit by (metis comp_arr_dom comp_ide_arr ide_cod ide_dom runit_naturality) end text ‹ A \emph{strict} bicategory is a normal bicategory in which the associativities a identities, so that associativity of horizontal composition holds ``on the nose' locale strict_bicategory = normal_bicategory + assumes strict_assoc: "∧f g h. [ide f; ide g; ide h; src f = trg g; src g = trg h] ide a[f, g, h]" begin lemma strict_assoc': assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h" shows "ide a-1[f, g, h]" using assms strict_assoc by simp lemma hcomp_assoc: shows "(μ ⋆ ν) ⋆ τ = μ ⋆ ν ⋆ τ" proof (cases "hseq μ ν ∧ hseq ν τ") show "¬ (hseq μ ν ∧ hseq ν τ) ==> ?thesis" by (metis hseqE hseq_char' match_1 match_2) show "hseq μ ν ∧ hseq ν τ ==> ?thesis" proof - assume 1: "hseq μ ν ∧ hseq ν τ" have 2: "arr μ ∧ arr ν ∧ arr τ ∧ src μ = trg ν ∧ src ν = trg τ" using 1 by blast have "(μ ⋆ ν) ⋆ τ = a[cod μ, cod ν, cod τ] ⋅ ((μ ⋆ ν) ⋆ τ)" using 1 assoc_in_hom strict_assoc comp_cod_arr assoc_simps(4) hseq_char by simp also have "... = (μ ⋆ ν ⋆ τ) ⋅ a[dom μ, dom ν, dom τ]" using 1 assoc_naturality by auto also have "... = μ ⋆ ν ⋆ τ" using 2 assoc_in_hom [of "dom μ" "dom ν" "dom τ"] strict_assoc comp_arr_dom by auto finally show ?thesis by simp qed qed text ‹ In a strict bicategory, every canonical isomorphism is an identity. › interpretation bicategorical_language .. interpretation E: self_evaluation_map V H a i src trg .. notation E.eval (‹{_}›) lemma ide_eval_Can: assumes "Can t" shows "ide {t}" proof - have 1: "∧u1 u2. [ ide {u1}; ide {u2}; Arr u1; Arr u2; Dom u1 = Cod u2 ] ==> ide ({u1} ⋅ {u2})" by (metis (no_types, lifting) E.eval_simps'(4-5) comp_ide_self ide_char) have "∧u. Can u ==> ide {u}" proof - fix u show "Can u ==> ide {u}" (* TODO: Rename \<ll>_ide_simp \<rr>_ide_simp to \<ll>_ide_eq \<rr>_ide_eq *) using 1 α_def a'_def strict_lunit strict_runit strict_assoc strict_assoc' l_ide_simp r_ide_simp Can_implies_Arr comp_ide_arr E.eval_simps'(2-3) by (induct u) auto qed thus ?thesis using assms by simp qed lemma ide_can: assumes "Ide f" and "Ide g" and "\<lfloor>f\<rfloor> = \<lfloor>g\<rfloor>" shows "ide (can g f)" using assms Can_red Can_Inv red_in_Hom Inv_in_Hom can_def ide_eval_Can Can.simps(4) Dom_Inv red_simps(4) by presburger end context bicategory begin text ‹ The following result gives conditions for strictness of a bicategory that are ty somewhat easier to verify than those used for the definition. lemma is_strict_if: assumes "∧f. ide f ==> f ⋆ src f = f" and "∧f. ide f ==> trg f ⋆ f = f" and "∧a. obj a ==> ide i[a]" and "∧f g h. [ide f; ide g; ide h; src f = trg g; src g = trg h] ==> ide a[f, g, shows "strict_bicategory V H a i src trg" proof show "∧f g h. [ide f; ide g; ide h; src f = trg g; src g = trg h] ==> ide a[f, g, by fact fix f assume f: "ide f" show "l[f] = f" proof - have "f = l[f]" using assms f unit_simps(5) by (intro lunit_eqI) (auto simp add: comp_arr_ide) thus ?thesis by simp qed show "r[f] = f" proof - have "f = r[f]" proof (intro runit_eqI) show "ide f" by fact show "«f : f ⋆ src f ==> f¬" using f assms(1) by auto show "f ⋆ src f = (f ⋆ i[src f]) ⋅ a[f, src f, src f]" proof - have "(f ⋆ i[src f]) ⋅ a[f, src f, src f] = (f ⋆ src f) ⋅ a[f, src f, src f]" using f assms(2-3) unit_simps(5) by simp also have "... = (f ⋆ src f ⋆ src f) ⋅ a[f, src f, src f]" using f assms(1-2) ideD(1) trg_src src.preserves_ide by metis also have "... = f ⋆ src f" using f comp_arr_ide assms(1,4) assoc_in_hom [of f "src f" "src f"] by auto finally show ?thesis by simp qed qed thus ?thesis by simp qed qed end subsection "Strictification" (* * TODO: Perhaps change the typeface used for a symbol that stands for a bicategory; * for example, to avoid the clashes here between B used as the name of a bicategory * and B used to denote a syntactic identity term. *) text ‹ The Strictness Theorem asserts that every bicategory is biequivalent to a strict bicategory. More specifically, it shows how to construct, given an arbit bicategory, a strict bicategory (its \emph{strictification}) that is biequivalen Consequently, given a property ‹P› of bicategories that is ``bicategorical'' (\emph{i.e.}~respects biequivalence), if we want to show that ‹P› holds for a bi then it suffices to show that ‹P› holds for the strictification of ‹B›, and if w that ‹P› holds for all bicategories, it is sufficient to show that it holds for strict bicategories. This is very useful, because it becomes quite tedious, eve with the aid of a proof assistant, to do ``diagram chases'' with all the units a associativities fully spelled out. Given a bicategory ‹B›, the strictification ‹S› of ‹B› may be constructed as the whose arrows are triples ‹(A, B, μ)›, where ‹X› and ‹Y› are ``normal identity ter (essentially, nonempty horizontally composable lists of 1-cells of ‹B›) having t syntactic source and target, and ‹«μ : {X} ==> {Y}¬› in ‹B›. Vertical composition in ‹S› is given by composition of the underlying arrows in Horizontal composition in ‹S› is given by ‹(A, B, μ) ⋆ (A', B', μ') = (AA', BB', ν) where ‹AA'› and ‹BB'› denote concatenations of lists and where ‹ν› is defined as composition ‹can BB' (B \⋆ B') ⋅ (μ ⋆ μ') ⋅ can (A \⋆ A') AA'›, where ‹can (A \⋆ A ‹can BB' (B \⋆ B')› are canonical isomorphisms in ‹B›. The canonical isomorphis ‹can (A \⋆ A') AA'› corresponds to taking a pair of lists ‹A \⋆ A'› and ``shifting the parentheses to the right'' to obtain a single list ‹AA'›. The canonical isomorphism can ‹BB' (B \⋆ B')› corresponds to the inverse rearran The bicategory ‹B› embeds into its strictification ‹S› via the functor ‹UP› that each arrow ‹μ› of ‹B› to ‹(\⟨dom μ\⟩, \⟨cod μ\⟩, μ)›, where ‹\⟨dom μ\⟩› and ‹\⟨cod μ\⟩› denote one-element lists. This mapping extends to a pseudofunctor. There is also a pseudofunctor ‹DN›, which maps ‹(A, B, μ)› in ‹S› to ‹μ› in ‹B›; this is such that ‹DN o UP› is the identity on ‹B› and ‹UP o DN› is equivalent t identity on ‹S›, so we obtain a biequivalence between ‹B› and ‹S›. It seems difficult to find references that explicitly describe a strictification construction in elementary terms like this (in retrospect, it ought to have been easy to rediscover such a construction, but my thinking got off on the wrong tra One reference that I did find useful was cite‹"unapologetic-strictification"›, which discusses strictification for monoidal categories. locale strictified_bicategory = B: bicategory VB HB aB iB srcB trgB for VB :: "'a comp" (infixr ‹⋅B› 55) and HB :: "'a ==> 'a ==> 'a" (infixr ‹⋆B› 53) and aB :: "'a ==> 'a ==> 'a ==> 'a" (‹aB[_, _, _]›) and iB :: "'a ==> 'a" (‹iB[_]›) and srcB :: "'a ==> 'a" and trgB :: "'a ==> 'a" begin sublocale E: self_evaluation_map VB HB aB iB srcB trgB .. notation B.in_hhom (‹«_ : _ →B _¬›) notation B.in_hom (‹«_ : _ ==>B _¬›) notation E.eval (‹{_}›) notation E.Nmlize (‹\⌊_\⌋›) text ‹ The following gives the construction of a bicategory whose arrows are triples ‹( where ‹Nml A ∧ Ide A›, ‹Nml B ∧ Ide B›, ‹Src A = Src B›, ‹Trg A = Trg B›, and ‹μ We use @{locale concrete_category} to construct the vertical composition, so for arrows of the bicategory will be of the form ‹MkArr A B μ›. text ‹ The 1-cells of the bicategory correspond to normal, identity terms ‹A› in the bicategorical language associated with ‹B›. › abbreviation IDE where "IDE ≡ {A. E.Nml A ∧ E.Ide A}" text ‹ If terms ‹A› and ‹B› determine 1-cells of the strictification and have a common source and target, then the 2-cells between these 1-cells correspond to arrows ‹μ› of the underlying bicategory such that ‹«μ : {A} ==>B {B}¬›. › abbreviation HOM where "HOM A B ≡ {μ. E.Src A = E.Src B ∧ E.Trg A = E.Trg B ∧ «μ : {A} ==>B {B}¬}" text ‹ The map taking term ‹A ∈ OBJ› to its evaluation ‹{A} ∈ HOM A A› defines the embedding of 1-cells as identity 2-cells. › abbreviation EVAL where "EVAL ≡ E.eval" sublocale concrete_category IDE HOM EVAL ‹λ_ _ _ μ ν. μ ⋅B ν› using E.ide_eval_Ide B.comp_arr_dom B.comp_cod_arr B.comp_assoc by (unfold_locales, auto) lemma is_concrete_category: shows "concrete_category IDE HOM EVAL (λ_ _ _ μ ν. μ ⋅B ν)" .. abbreviation vcomp (infixr ‹⋅› 55) where "vcomp ≡ COMP" lemma arr_char: shows "arr F ⟷ E.Nml (Dom F) ∧ E.Ide (Dom F) ∧ E.Nml (Cod F) ∧ E.Ide (Cod F) ∧ E.Src (Dom F) = E.Src (Cod F) ∧ E.Trg (Dom F) = E.Trg (Cod F) ∧ «Map F : {Dom F} ==>B {Cod F}¬ ∧ F ≠ Null" using arr_char by auto lemma arrI (* [intro] *): assumes "E.Nml (Dom F)" and "E.Ide (Dom F)" and "E.Nml (Cod F)" and "E.Ide (Cod F)" and "E.Src (Dom F) = E.Src (Cod F)" and "E.Trg (Dom F) = E.Trg (Cod F)" and "«Map F : {Dom F} ==>B {Cod F}¬" and "F ≠ Null" shows "arr F" using assms arr_char by blast lemma arrE [elim]: assumes "arr F" shows "([ E.Nml (Dom F); E.Ide (Dom F); E.Nml (Cod F); E.Ide (Cod F); E.Src (Dom F) = E.Src (Cod F); E.Trg (Dom F) = E.Trg (Cod F); «Map F : {Dom F} ==>B {Cod F}¬; F ≠ Null ] ==> T) ==> T" using assms arr_char by simp lemma ide_char: shows "ide F ⟷ endo F ∧ B.ide (Map F)" proof show "ide F ==> endo F ∧ B.ide (Map F)" using ide_charCC by (simp add: E.ide_eval_Ide) show "endo F ∧ B.ide (Map F) ==> ide F" by (metis (no_types, lifting) B.ide_char B.in_homE arr_char ide_charCC mem_Collect_eq seq_char) qed lemma ideI [intro]: assumes "arr F" and "Dom F = Cod F" and "B.ide (Map F)" shows "ide F" using assms ide_char dom_char cod_char seq_char by presburger lemma ideE [elim]: assumes "ide F" shows "([ arr F; Dom F = Cod F; B.ide (Map F); Map F = {Dom F}; Map F = {Cod F} ] ==> T) ==> T" using assms by (metis (no_types, lifting) Map_ide(2) ide_char seq_char) text ‹ Source and target are defined by the corresponding syntactic operations on terms definition src where "src F ≡ if arr F then MkIde (E.Src (Dom F)) else null" definition trg where "trg F ≡ if arr F then MkIde (E.Trg (Dom F)) else null" lemma src_simps [simp]: assumes "arr F" shows "Dom (src F) = E.Src (Dom F)" and "Cod (src F) = E.Src (Dom F)" and "Map (src F) = {E.Src (Dom F)}" using assms src_def arr_char by auto lemma trg_simps [simp]: assumes "arr F" shows "Dom (trg F) = E.Trg (Dom F)" and "Cod (trg F) = E.Trg (Dom F)" and "Map (trg F) = {E.Trg (Dom F)}" using assms trg_def arr_char by auto interpretation src: endofunctor vcomp src using src_def comp_char E.Obj_implies_Ide apply (unfold_locales) apply auto[4] proof - show "∧g f. seq g f ==> src (g ⋅ f) = src g ⋅ src f" proof - fix g f assume gf: "seq g f" have "src (g ⋅ f) = MkIde (E.Src (Dom (g ⋅ f)))" using gf src_def comp_char by simp also have "... = MkIde (E.Src (Dom f))" using gf by (simp add: seq_char) also have "... = MkIde (E.Src (Dom g)) ⋅ MkIde (E.Src (Dom f))" using gf seq_char E.Obj_implies_Ide by auto also have "... = src g ⋅ src f" using gf src_def comp_char by auto finally show "src (g ⋅ f) = src g ⋅ src f" by blast qed qed interpretation trg: endofunctor vcomp trg using trg_def comp_char E.Obj_implies_Ide apply (unfold_locales) apply auto[4] proof - show "∧g f. seq g f ==> trg (g ⋅ f) = trg g ⋅ trg f" proof - fix g f assume gf: "seq g f" have "trg (g ⋅ f) = MkIde (E.Trg (Dom (g ⋅ f)))" using gf trg_def comp_char by simp also have "... = MkIde (E.Trg (Dom f))" using gf by (simp add: seq_char) also have "... = MkIde (E.Trg (Dom g)) ⋅ MkIde (E.Trg (Dom f))" using gf seq_char E.Obj_implies_Ide by auto also have "... = trg g ⋅ trg f" using gf trg_def comp_char by auto finally show "trg (g ⋅ f) = trg g ⋅ trg f" by blast qed qed interpretation horizontal_homs vcomp src trg using src_def trg_def Cod_in_Obj Map_in_Hom E.Obj_implies_Ide by unfold_locales auto notation in_hhom (‹«_ : _ → _¬›) definition hcomp (infixr ‹⋆› 53) where "μ ⋆ ν ≡ if arr μ ∧ arr ν ∧ src μ = trg ν then MkArr (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋅B (Map μ ⋆B Map ν) ⋅B B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν)) else null" lemma arr_hcomp: assumes "arr μ" and "arr ν" and "src μ = trg ν" shows "arr (μ ⋆ ν)" proof - have 1: "E.Ide (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) ∧ E.Nml (Dom μ \<lfloor>\<star>\<rfl E.Ide (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) ∧ E.Nml (Cod μ \<lfloor>\<star>\<rfloor> Co using assms arr_char src_def trg_def E.Ide_HcompNml E.Nml_HcompNml(1) by auto moreover have "«B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋅B (Map μ ⋆B Map B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) : {Dom μ \<lfloor>\<star>\<rfloor> Dom ν} ==>B {Cod μ \<lfloor>\<star>\<rfloor> Cod ν}¬" proof - have "«Map μ ⋆B Map ν : {Dom μ \<star> Dom ν} ==>B {Cod μ \<star> Cod ν}¬" using assms arr_char dom_char cod_char src_def trg_def E.eval_simps'(2-3) by auto moreover have "«B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) : {Dom μ \<lfloor>\<star>\<rfloor> Dom ν} ==>B {Dom μ \<star> Dom ν}¬ ∧ «B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) : {Cod μ \<star> Cod ν} ==>B {Cod μ \<lfloor>\<star>\<rfloor> Cod ν}¬" using assms 1 arr_char src_def trg_def apply (intro conjI B.in_homI) by auto ultimately show ?thesis by auto qed moreover have "E.Src (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) = E.Src (Cod μ \<lfloor>\<sta E.Trg (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) = E.Trg (Cod μ \<lfloor>\<star>\<rfloor> Co using assms arr_char src_def trg_def by (simp add: E.Src_HcompNml E.Trg_HcompNml) ultimately show ?thesis unfolding hcomp_def using assms by (intro arrI, auto) qed lemma src_hcomp [simp]: assumes "arr μ" and "arr ν" and "src μ = trg ν" shows "src (μ ⋆ ν) = src ν" using assms arr_char hcomp_def src_def trg_def arr_hcomp E.Src_HcompNml by simp lemma trg_hcomp [simp]: assumes "arr μ" and "arr ν" and "src μ = trg ν" shows "trg (hcomp μ ν) = trg μ" using assms arr_char hcomp_def src_def trg_def arr_hcomp E.Trg_HcompNml by simp lemma hseq_char: shows "arr (μ ⋆ ν) ⟷ arr μ ∧ arr ν ∧ src μ = trg ν" using arr_hcomp hcomp_def by simp lemma Dom_hcomp [simp]: assumes "arr μ" and "arr ν" and "src μ = trg ν" shows "Dom (μ ⋆ ν) = Dom μ \<lfloor>\<star>\<rfloor> Dom ν" using assms hcomp_def [of μ ν] by simp lemma Cod_hcomp [simp]: assumes "arr μ" and "arr ν" and "src μ = trg ν" shows "Cod (μ ⋆ ν) = Cod μ \<lfloor>\<star>\<rfloor> Cod ν" using assms hcomp_def [of μ ν] by simp lemma Map_hcomp [simp]: assumes "arr μ" and "arr ν" and "src μ = trg ν" shows "Map (μ ⋆ ν) = B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋅B (Map μ ⋆B Map ν) ⋅B B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν)" using assms hcomp_def [of μ ν] by simp interpretation "functor" VV.comp vcomp ‹λμν. hcomp (fst μν) (snd μν)› proof show "∧f. ¬ VV.arr f ==> fst f ⋆ snd f = null" using hcomp_def by auto show A: "∧f. VV.arr f ==> arr (fst f ⋆ snd f)" using VV.arrE hseq_char by blast show "∧f. VV.arr f ==> dom (fst f ⋆ snd f) = fst (VV.dom f) ⋆ snd (VV.dom f)" proof - fix f assume f: "VV.arr f" have "dom (fst f ⋆ snd f) = MkIde (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom (snd f) using f VV.arrE [of f] dom_char arr_hcomp hcomp_def by simp also have "... = fst (VV.dom f) ⋆ snd (VV.dom f)" proof - have "hcomp (fst (VV.dom f)) (snd (VV.dom f)) = MkArr (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom (snd f)) (Dom (fst f) \<lfloor>\<sta (B.can (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom (snd f)) (Dom (fst f) \<star> Dom ({Dom (fst f)} ⋆B {Dom (snd f)}) ⋅B B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( using f VV.arrE [of f] arr_hcomp hcomp_def VV.dom_simp by simp moreover have "B.can (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom (snd f)) (Dom (fst f) ({Dom (fst f)} ⋆B {Dom (snd f)}) ⋅B B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( {Dom (fst f) \<lfloor>\<star>\<rfloor> Dom (snd f)}" proof - have 1: "E.Ide (Dom (fst f) \<star> Dom (snd f))" using f VV.arr_charSbC arr_char dom_char apply simp by (metis (no_types, lifting) src_simps(1) trg_simps(1)) have 2: "E.Ide (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom (snd f))" using f VV.arr_charSbC arr_char dom_char apply simp by (metis (no_types, lifting) E.Ide_HcompNml src_simps(1) trg_simps(1)) have 3: "\<lfloor>Dom (fst f) \<star> Dom (snd f)\<rfloor> = \<lfloor>Dom (fst f) \<lfl using f VV.arr_charSbC arr_char dom_char apply simp by (metis (no_types, lifting) E.Nml_HcompNml(1) E.Nmlize_Nml src_simps(1) trg_simps(1)) have "({Dom (fst f)} ⋆B {Dom (snd f)}) ⋅B B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( using "1" "2" "3" B.comp_cod_arr by force thus ?thesis using 1 2 3 f VV.arr_charSbC B.can_Ide_self B.vcomp_can by simp qed ultimately show ?thesis by simp qed finally show "dom (fst f ⋆ snd f) = fst (VV.dom f) ⋆ snd (VV.dom f)" by simp qed show "∧f. VV.arr f ==> cod (fst f ⋆ snd f) = fst (VV.cod f) ⋆ snd (VV.cod f)" proof - fix f assume f: "VV.arr f" have "cod (fst f ⋆ snd f) = MkIde (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f) using f VV.arrE [of f] cod_char arr_hcomp hcomp_def by simp also have "... = fst (VV.cod f) ⋆ snd (VV.cod f)" proof - have "hcomp (fst (VV.cod f)) (snd (VV.cod f)) = MkArr (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) \<lfloor>\<sta (B.can (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) \<star> Cod ({Cod (fst f)} ⋆B {Cod (snd f)}) ⋅B B.can (Cod (fst f) \<star> Cod (snd f)) (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod ( using f VV.arrE [of f] arr_hcomp hcomp_def VV.cod_simp by simp moreover have "B.can (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) ({Cod (fst f)} ⋆B {Cod (snd f)}) ⋅B B.can (Cod (fst f) \<star> Cod (snd f)) (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod ( {Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)}" proof - have 1: "E.Ide (Cod (fst f) \<star> Cod (snd f))" using f VV.arr_charSbC arr_char dom_char apply simp by (metis (no_types, lifting) src_simps(1) trg_simps(1)) have 2: "E.Ide (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f))" using f VV.arr_charSbC arr_char dom_char apply simp by (metis (no_types, lifting) E.Ide_HcompNml src_simps(1) trg_simps(1)) have 3: "\<lfloor>Cod (fst f) \<star> Cod (snd f)\<rfloor> = \<lfloor>Cod (fst f) \<lfl using f VV.arr_charSbC arr_char dom_char apply simp by (metis (no_types, lifting) E.Nml_HcompNml(1) E.Nmlize_Nml src_simps(1) trg_simps(1)) have "({Cod (fst f)} ⋆B {Cod (snd f)}) ⋅B B.can (Cod (fst f) \<star> Cod (snd f)) (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod ( B.can (Cod (fst f) \<star> Cod (snd f)) (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod ( using "1" "2" "3" B.comp_cod_arr by force thus ?thesis using 1 2 3 f VV.arr_charSbC B.can_Ide_self B.vcomp_can by simp qed ultimately show ?thesis by simp qed finally show "cod (fst f ⋆ snd f) = fst (VV.cod f) ⋆ snd (VV.cod f)" by simp qed show "∧g f. VV.seq g f ==> fst (VV.comp g f) ⋆ snd (VV.comp g f) = (fst g ⋆ snd g) ⋅ (fst f ⋆ snd f)" proof - fix f g assume fg: "VV.seq g f" have f: "arr (fst f) ∧ arr (snd f) ∧ src (fst f) = trg (snd f)" using fg VV.seq_charSbC VV.arr_charSbC by simp have g: "arr (fst g) ∧ arr (snd g) ∧ src (fst g) = trg (snd g)" using fg VV.seq_charSbC VV.arr_charSbC by simp have 1: "arr (fst (VV.comp g f)) ∧ arr (snd (VV.comp g f)) ∧ src (fst (VV.comp g f)) = trg (snd (VV.comp g f))" using fg VV.arrE by blast have 0: "VV.comp g f = (fst g ⋅ fst f, snd g ⋅ snd f)" using fg 1 VV.comp_char VxV.comp_char by (metis (no_types, lifting) VV.seq_charSbC VxV.seqEPC) let ?X = "MkArr (Dom (fst (VV.comp g f)) \<lfloor>\<star>\<rfloor> Dom (snd (VV.comp g (Cod (fst (VV.comp g f)) \<lfloor>\<star>\<rfloor> Cod (snd (VV.comp g f))) (B.can (Cod (fst (VV.comp g f)) \<lfloor>\<star>\<rfloor> Cod (snd (VV.comp g f))) (Cod (fst (VV.comp g f)) \<star> Cod (snd (VV.comp g f))) ⋅B (Map (fst (VV.comp g f)) ⋆B Map (snd (VV.comp g f))) ⋅B B.can (Dom (fst (VV.comp g f)) \<star> Dom (snd (VV.comp g f))) (Dom (fst (VV.comp g f)) \<lfloor>\<star>\<rfloor> Dom (snd (VV.comp g f))))" have 2: "fst (VV.comp g f) ⋆ snd (VV.comp g f) = ?X" unfolding hcomp_def using 1 by simp also have "... = (fst g ⋆ snd g) ⋅ (fst f ⋆ snd f)" proof - let ?GG = "MkArr (Dom (fst g) \<lfloor>\<star>\<rfloor> Dom (snd g)) (Cod (fst g) \<lfl (B.can (Cod (fst g) \<lfloor>\<star>\<rfloor> Cod (snd g)) (Cod (fst g) \<star> Cod (Map (fst g) ⋆B Map (snd g)) ⋅B B.can (Dom (fst g) \<star> Dom (snd g)) (Dom (fst g) \<lfloor>\<star>\<rfloor> Dom ( let ?FF = "MkArr (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom (snd f)) (Cod (fst f) \<lfl (B.can (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) \<star> Cod (Map (fst f) ⋆B Map (snd f)) ⋅B B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( have 4: "arr ?FF ∧ arr ?GG ∧ Dom ?GG = Cod ?FF" proof - have "arr ?FF ∧ arr ?GG" using f g fg VV.arr_charSbC VV.seqE hcomp_def A by presburger thus ?thesis using 0 1 by (simp add: fg seq_char) qed have "(fst g ⋆ snd g) ⋅ (fst f ⋆ snd f) = ?GG ⋅ ?FF" unfolding hcomp_def using 1 f g fg VV.arr_charSbC VV.seqE by simp also have "... = ?X" proof (intro arr_eqI) show "seq ?GG ?FF" using fg 4 seq_char by blast show "arr ?X" using fg 1 arr_hcomp hcomp_def by simp show "Dom (?GG ⋅ ?FF) = Dom ?X" using fg 0 1 4 seq_char by simp show "Cod (?GG ⋅ ?FF) = Cod ?X" using fg 0 1 4 seq_char by simp show "Map (?GG ⋅ ?FF) = Map ?X" proof - have "Map (?GG ⋅ ?FF) = Map ?GG ⋅B Map ?FF" using 4 by auto also have "... = (B.can (Cod (fst g) \<lfloor>\<star>\<rfloor> Cod (snd g)) (Cod (fst g) \<sta (Map (fst g) ⋆B Map (snd g)) ⋅B B.can (Dom (fst g) \<star> Dom (snd g)) (Dom (fst g) \<lfloor>\<star>\<rfloor> Dom ( (B.can (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) \<star> Cod (Map (fst f) ⋆B Map (snd f)) ⋅B B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( using fg by simp also have "... = B.can (Cod (fst g) \<lfloor>\<star>\<rfloor> Cod (snd g)) (Cod (fst g) \<star ((Map (fst g) ⋆B Map (snd g)) ⋅B (Map (fst f) ⋆B Map (snd f))) ⋅B B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( proof - have "(B.can (Cod (fst g) \<lfloor>\<star>\<rfloor> Cod (snd g)) (Cod (fst g) \<star> (Map (fst g) ⋆B Map (snd g)) ⋅B B.can (Dom (fst g) \<star> Dom (snd g)) (Dom (fst g) \<lfloor>\<star>\<rfloor> Dom ( (B.can (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) \<star> Cod (Map (fst f) ⋆B Map (snd f)) ⋅B B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( B.can (Cod (fst g) \<lfloor>\<star>\<rfloor> Cod (snd g)) (Cod (fst g) \<star> Cod ( ((Map (fst g) ⋆B Map (snd g)) ⋅B (B.can (Dom (fst g) \<star> Dom (snd g)) (Dom (fst g) \<lfloor>\<star>\<rfloor> Dom B.can (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) \<star> Cod ( (Map (fst f) ⋆B Map (snd f))) ⋅B B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( using B.comp_assoc by simp also have "... = B.can (Cod (fst g) \<lfloor>\<star>\<rfloor> Cod (snd g)) (Cod (fst ((Map (fst g) ⋆B Map (snd g)) ⋅B (Map (fst f) ⋆B Map (snd f))) ⋅B B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( proof - have "(B.can (Dom (fst g) \<star> Dom (snd g)) (Dom (fst g) \<lfloor>\<star>\<rfloor> (B.can (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) \<star> Cod {Cod (fst f) \<star> Cod (snd f)}" proof - have "(B.can (Dom (fst g) \<star> Dom (snd g)) (Dom (fst g) \<lfloor>\<star>\<rfloor> (B.can (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) \<star> Cod B.can (Dom (fst g) \<star> Dom (snd g)) (Cod (fst f) \<star> Cod (snd f))" proof - have "E.Ide (Dom (fst g) \<star> Dom (snd g))" using g arr_char by (metis (no_types, lifting) E.Ide.simps(3) src_simps(2) trg_simps(2)) moreover have "E.Ide (Dom (fst g) \<lfloor>\<star>\<rfloor> Dom (snd g))" using 4 by auto moreover have "E.Ide (Cod (fst f) \<star> Cod (snd f))" using f arr_char by (metis (no_types, lifting) E.Ide.simps(3) src_simps(2) trg_simps(2)) moreover have "\<lfloor>Dom (fst g) \<star> Dom (snd g)\<rfloor> = \<lfloor>Dom (fst g) \<lfloor>\<s using g E.Nml_HcompNml(1) calculation(1) by fastforce moreover have "\<lfloor>Dom (fst g) \<lfloor>\<star>\<rfloor> Dom (snd g)\<rfloor> = \<lfloor>Cod (f using g fg seq_char by (metis (no_types, lifting) VV.seq_charSbC VxV.seqEPC calculation(4)) moreover have "Dom (fst g) \<lfloor>\<star>\<rfloor> Dom (snd g) = Cod (fst f) \<lfloor>\<star>\<rfl using 0 1 by (simp add: seq_char) ultimately show ?thesis using B.vcomp_can by simp qed also have "... = {Cod (fst f) \<star> Cod (snd f)}" proof - have "Dom (fst g) \<star> Dom (snd g) = Cod (fst f) \<star> Cod (snd f)" using 0 f g fg seq_char VV.seq_charSbC VV.arr_charSbC by simp thus ?thesis using f B.can_Ide_self [of "Dom (fst f) \<star> Dom (snd f)"] by (metis (no_types, lifting) B.can_Ide_self E.Ide.simps(3) arrE src_simps(2) trg_simps(2)) qed finally show ?thesis by simp qed hence "(B.can (Dom (fst g) \<star> Dom (snd g)) (Dom (fst g) \<lfloor>\<star>\<rfloor B.can (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) \<star> Cod ( (Map (fst f) ⋆B Map (snd f)) = {Cod (fst f) \<star> Cod (snd f)} ⋅B (Map (fst f) ⋆B Map (snd f))" by simp also have "... = Map (fst f) ⋆B Map (snd f)" proof - have 1: "∀p. arr p ⟶ map (cod p) ⋅ map p = map p" by blast have 3: "{Cod (fst f)} ⋅B Map (fst f) = Map (map (cod (fst f)) ⋅ map (fst f))" by (simp add: f) have 4: "map (cod (fst f)) ⋅ map (fst f) = fst f" using 1 f map_simp by simp show ?thesis proof - have 2: "{Cod (snd f)} ⋅B Map (snd f) = Map (snd f)" using 1 f map_simp by (metis (no_types, lifting) Dom_cod Map_cod Map_comp arr_cod) have "B.seq {Cod (snd f)} (Map (snd f))" using f 2 by auto moreover have "B.seq {Cod (fst f)} (Map (fst f))" using 4 f 3 by auto moreover have "{Cod (fst f)} ⋅B Map (fst f) ⋆B {Cod (snd f)} ⋅B Map (snd f) = Map (fst f) ⋆B Map (snd f)" using 2 3 4 by presburger ultimately show ?thesis by (simp add: B.interchange) qed qed finally have "(B.can (Dom (fst g) \<star> Dom (snd g)) (Dom (fst g) \<lfloor>\<star>\<rfloor> Dom B.can (Cod (fst f) \<lfloor>\<star>\<rfloor> Cod (snd f)) (Cod (fst f) \<star> Cod ( (Map (fst f) ⋆B Map (snd f)) = Map (fst f) ⋆B Map (snd f)" by simp thus ?thesis using fg B.comp_cod_arr by simp qed finally show ?thesis by simp qed also have "... = B.can (Cod (fst g) \<lfloor>\<star>\<rfloor> Cod (snd g)) (Cod (fst (Map (fst g ⋅ fst f) ⋆B Map (snd g ⋅ snd f)) ⋅B B.can (Dom (fst f) \<star> Dom (snd f)) (Dom (fst f) \<lfloor>\<star>\<rfloor> Dom ( proof - have 2: "Dom (fst g) = Cod (fst f)" using 0 f g fg VV.seq_charSbC [of g f] VV.arr_charSbC arr_char seq_char by (metis (no_types, lifting) fst_conv) hence "Map (fst g ⋅ fst f) = Map (fst g) ⋅B Map (fst f)" using f g Map_comp [of "fst f" "fst g"] by simp moreover have "B.seq (Map (fst g)) (Map (fst f)) ∧ B.seq (Map (snd g)) (Map (snd f))" using f g 0 1 2 arr_char by (metis (no_types, lifting) B.seqI' prod.sel(2) seq_char) ultimately show ?thesis using 0 1 seq_char Map_comp B.interchange by auto qed also have "... = Map ?X" using fg 0 1 by (simp add: seq_char) finally show ?thesis by simp qed qed finally show ?thesis by simp qed finally show "fst (VV.comp g f) ⋆ snd (VV.comp g f) = (fst g ⋆ snd g) ⋅ (fst f ⋆ s by simp qed qed interpretation horizontal_composition vcomp hcomp src trg using hseq_char by (unfold_locales, auto) lemma hcomp_assoc: assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ" shows "(μ ⋆ ν) ⋆ τ = μ ⋆ ν ⋆ τ" proof (intro arr_eqI) have μν: "«Map μ ⋆B Map ν : {Dom μ \<star> Dom ν} ==>B {Cod μ \<star> Cod ν}¬" using assms src_def trg_def arr_char by (auto simp add: E.eval_simps'(2-3) Pair_inject) have ντ: "«Map ν ⋆B Map τ : {Dom ν \<star> Dom τ} ==>B {Cod ν \<star> Cod τ}¬" using assms src_def trg_def arr_char by (auto simp add: E.eval_simps'(2-3) Pair_inject) show "hseq (μ ⋆ ν) τ" using assms μν ντ by auto show "hseq μ (ν ⋆ τ)" using assms μν ντ by auto show "Dom ((μ ⋆ ν) ⋆ τ) = Dom (μ ⋆ ν ⋆ τ)" proof - have "E.Nml (Dom μ) ∧ E.Nml (Dom ν) ∧ E.Nml (Dom τ)" using assms by blast moreover have "E.Src (Dom μ) = E.Trg (Dom ν) ∧ E.Src (Dom ν) = E.Trg (Dom τ)" using assms μν ντ by (metis (no_types, lifting) src_simps(2) trg_simps(2)) ultimately show ?thesis using assms μν ντ E.HcompNml_assoc by simp qed show "Cod ((μ ⋆ ν) ⋆ τ) = Cod (μ ⋆ ν ⋆ τ)" proof - have "E.Nml (Cod μ) ∧ E.Nml (Cod ν) ∧ E.Nml (Cod τ)" using assms by blast moreover have "E.Src (Cod μ) = E.Trg (Cod ν) ∧ E.Src (Cod ν) = E.Trg (Cod τ)" using assms μν ντ by (metis (no_types, lifting) arrE src_simps(2) trg_simps(2)) ultimately show ?thesis using assms μν ντ E.HcompNml_assoc by simp qed show "Map ((μ ⋆ ν) ⋆ τ) = Map (μ ⋆ ν ⋆ τ)" proof - have "Map ((μ ⋆ ν) ⋆ τ) = B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod μ \<star (Map μ ⋆B Map ν ⋆B Map τ) ⋅B B.can (Dom μ \<star> Dom ν \<star> Dom τ) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν \<lfloor>\< proof - have 1: "Map ((μ ⋆ ν) ⋆ τ) = B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Cod τ) ((Cod μ \<lfl (B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋅B (Map μ ⋆B Map ν) ⋅B B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) ⋆B Map τ) ⋅B B.can ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> Dom τ) (Dom μ \<lfloor>\<star>\<rflo using assms μν ντ hcomp_def E.HcompNml_assoc src_def trg_def arr_char E.Nml_HcompNml E.Ide_HcompNml by auto (* 5 sec *) also have "... = B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Cod τ) ((Co (B.can ((Cod μ \<lfloor>\<star>\<rfloor> Cod ν) \<star> Cod τ) (Cod μ \<star> Cod ν \<star> (Map μ ⋆B Map ν ⋆B Map τ) ⋅B B.can (Dom μ \<star> Dom ν \<star> Dom τ) ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> B.can ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> Dom τ) (Dom μ \<lfloor>\<star>\<rflo proof - have "B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋅B (Map μ ⋆B Map ν) ⋅B B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) ⋆B B.can ((Cod μ \<lfloor>\<star>\<rfloor> Cod ν) \<star> Cod τ) (Cod μ \<star> Cod ν \<star> (Map μ ⋆B Map ν ⋆B Map τ) ⋅B B.can (Dom μ \<star> Dom ν \<star> Dom τ) ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> proof - have "B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋅B (Map μ ⋆B Map ν) ⋅B B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) ⋆B Map τ = (B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋆B B.can (Cod τ) (Co ((Map μ ⋆B Map ν) ⋅B B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) ⋆B Map τ)" proof - have "B.seq (B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν)) ((Map μ ⋆B Map ν) ⋅B B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν))" by (metis (no_types, lifting) B.arrI Map_hcomp arrE arr_hcomp assms(1) assms(2) assms(4)) moreover have "B.seq (B.can (Cod τ) (Cod τ)) (Map τ)" using B.can_in_hom assms(3) by blast moreover have "B.ide (B.can (Cod τ) (Cod τ))" using B.can_Ide_self E.ide_eval_Ide arr_char assms(3) by presburger ultimately show ?thesis by (metis (no_types) B.comp_ide_arr B.interchange) qed also have "... = (B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋆B B.can (Co ((Map μ ⋆B Map ν) ⋆B Map τ) ⋅B (B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) ⋆B B.can (Dom τ) (Dom τ))" proof - have "B.seq (Map μ ⋆B Map ν) (B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> by (metis (no_types, lifting) B.arrI B.null_is_zero(2) B.ext Map_hcomp arrE arr_hcomp assms(1) assms(2) assms(4)) moreover have "B.seq (Map τ) (B.can (Dom τ) (Dom τ))" using assms(3) by fastforce ultimately show ?thesis using B.interchange by (metis (no_types, lifting) B.can_Ide_self B.comp_arr_ide E.ide_eval_Ide arrE assms(3)) qed also have "... = (B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋆B B.can (Co (B.can ((Cod μ \<star> Cod ν) \<star> Cod τ) (Cod μ \<star> Cod ν \<star> Cod τ) ⋅B (Map μ ⋆B Map ν ⋆B Map τ) ⋅B B.can (Dom μ \<star> Dom ν \<star> Dom τ) ((Dom μ \<star> Dom ν) \<star> Dom τ)) ⋅B (B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) ⋆B B.can (Dom τ) (Dom τ))" proof - have "(Map μ ⋆B Map ν) ⋆B Map τ = B.a' {Cod μ} {Cod ν} {Cod τ} ⋅B (Map μ ⋆B Map ν ⋆B Map τ) ⋅B aB {Dom μ} {Dom ν} {Dom τ}" using B.hcomp_reassoc(1) by (metis (no_types, lifting) B.hcomp_in_vhomE B.in_homE μν ντ arrE assms(1) assms(2) assms(3)) also have "... = B.can ((Cod μ \<star> Cod ν) \<star> Cod τ) (Cod μ \<star> Cod ν \<star> C (Map μ ⋆B Map ν ⋆B Map τ) ⋅B B.can (Dom μ \<star> Dom ν \<star> Dom τ) ((Dom μ \<star> Dom ν) \<star> Dom τ)" using assms arr_char src_def trg_def arr_char B.canE_associator by simp finally show ?thesis by simp qed also have "... = ((B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋆B B.can (C (B.can ((Cod μ \<star> Cod ν) \<star> Cod τ) (Cod μ \<star> Cod ν \<star> Cod τ))) ⋅B (Map μ ⋆B Map ν ⋆B Map τ) ⋅B (B.can (Dom μ \<star> Dom ν \<star> Dom τ) ((Dom μ \<star> Dom ν) \<star> Dom τ) ⋅B (B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) ⋆B B.can (Dom τ) (Dom τ)))" using B.comp_assoc by simp also have "... = B.can ((Cod μ \<lfloor>\<star>\<rfloor> Cod ν) \<star> Cod τ) (Cod μ \<star> Cod ν (Map μ ⋆B Map ν ⋆B Map τ) ⋅B B.can (Dom μ \<star> Dom ν \<star> Dom τ) ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> proof - have "(B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) (Cod μ \<star> Cod ν) ⋆B B.can (Cod τ (B.can ((Cod μ \<star> Cod ν) \<star> Cod τ) (Cod μ \<star> Cod ν \<star> Cod τ)) = B.can ((Cod μ \<lfloor>\<star>\<rfloor> Cod ν) \<star> Cod τ) (Cod μ \<star> Cod ν \<star> proof - have "E.Ide (Cod μ \<star> Cod ν)" by (metis (no_types, lifting) E.Ide.simps(3) arrE assms(1-2,4) src_simps(1) trg_simps(1)) moreover have "E.Ide (Cod μ \<lfloor>\<star>\<rfloor> Cod ν)" using E.Ide_HcompNml assms(1) assms(2) calculation by auto moreover have "\<lfloor>Cod μ \<star> Cod ν\<rfloor> = \<lfloor>Cod μ \<lfloor>\<star>\<rflo using E.Nml_HcompNml(1) assms(1) assms(2) calculation(1) by fastforce moreover have "E.Src (Cod μ \<star> Cod ν) = E.Trg (Cod τ)" by (metis (no_types, lifting) E.Src.simps(3) arrE assms(2-3,5) src_simps(2) trg_simps(2)) moreover have "E.Src (Cod μ \<lfloor>\<star>\<rfloor> Cod ν) = E.Trg (Cod τ)" using E.Src_HcompNml assms(1) assms(2) calculation(1) calculation(4) by fastforce moreover have "\<lfloor>Cod μ \<star> Cod ν \<star> Cod τ\<rfloor> = \<lfloor>(Cod μ \<star> by (metis (no_types, lifting) E.Arr.simps(3) E.Nmlize_Hcomp_Hcomp E.Nmlize_Hcomp_Hcomp' E.Ide_implies_Arr E.Src.simps(3) arrE assms(3) calculation(1) calculation(4)) ultimately show ?thesis using assms(3) B.hcomp_can B.vcomp_can by auto qed moreover have "B.can (Dom μ \<star> Dom ν \<star> Dom τ) ((Dom μ \<star> Dom ν) \<star> Dom τ) ⋅B (B.can (Dom μ \<star> Dom ν) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) ⋆B B.can (Dom τ) (Do B.can (Dom μ \<star> Dom ν \<star> Dom τ) ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> proof - have "E.Ide (Dom μ \<lfloor>\<star>\<rfloor> Dom ν)" by (metis (no_types, lifting) E.Ide_HcompNml arrE assms(1-2,4) src_simps(2) trg_simps(2)) moreover have "E.Ide (Dom μ \<star> Dom ν)" by (metis (no_types, lifting) E.Ide.simps(3) arrE assms(1-2,4) src_simps(1) trg_simps(1)) moreover have "\<lfloor>Dom μ \<lfloor>\<star>\<rfloor> Dom ν\<rfloor> = \<lfloor>Dom μ \<st using E.Nml_HcompNml(1) assms(1-2) calculation(2) by fastforce moreover have "E.Src (Dom μ \<lfloor>\<star>\<rfloor> Dom ν) = E.Trg (Dom τ)" by (metis (no_types, lifting) E.Ide.simps(3) E.Src_HcompNml arrE assms(1-3,5) calculation(2) src_simps(2) trg_simps(2)) moreover have "E.Src (Dom μ \<star> Dom ν) = E.Trg (Dom τ)" using E.Src_HcompNml assms(1-2) calculation(2) calculation(4) by fastforce moreover have "E.Ide ((Dom μ \<star> Dom ν) \<star> Dom τ)" using E.Ide.simps(3) assms(3) calculation(2) calculation(5) by blast moreover have "\<lfloor>(Dom μ \<star> Dom ν) \<star> Dom τ\<rfloor> = \<lfloor>Dom μ \<star using E.Nmlize_Hcomp_Hcomp calculation(6) by auto ultimately show ?thesis using assms(3) B.hcomp_can B.vcomp_can by auto qed ultimately show ?thesis by simp qed finally show ?thesis by simp qed thus ?thesis by simp qed also have "... = (B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Cod τ) ((C B.can ((Cod μ \<lfloor>\<star>\<rfloor> Cod ν) \<star> Cod τ) (Cod μ \<star> Cod ν \<star> (Map μ ⋆B Map ν ⋆B Map τ) ⋅B B.can (Dom μ \<star> Dom ν \<star> Dom τ) ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> B.can ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> Dom τ) (Dom μ \<lfloor>\<star>\<rflo using B.comp_assoc by simp also have "... = B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Co (Map μ ⋆B Map ν ⋆B Map τ) ⋅B B.can (Dom μ \<star> Dom ν \<star> Dom τ) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν \<lfloor>\< proof - have "B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Cod τ) ((Cod μ B.can ((Cod μ \<lfloor>\<star>\<rfloor> Cod ν) \<star> Cod τ) (Cod μ \<star> Cod ν \<star> B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod μ \<star proof - have "E.Ide (Cod μ \<star> Cod ν \<star> Cod τ)" using assms src_def trg_def by fastforce moreover have "E.Ide ((Cod μ \<lfloor>\<star>\<rfloor> Cod ν) \<star> Cod τ)" using assms arr_char src_def trg_def E.Ide_HcompNml E.Src_HcompNml by auto moreover have "E.Ide (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Cod τ using assms arr_char src_def trg_def by (simp add: E.Nml_HcompNml(1) E.Ide_HcompNml E.Trg_HcompNml) moreover have "\<lfloor>Cod μ \<star> Cod ν \<star> Cod τ\<rfloor> = \<lfloor>(Cod μ \<lfloo using assms arr_char src_def trg_def E.Nml_HcompNml E.HcompNml_assoc by simp moreover have "\<lfloor>(Cod μ \<lfloor>\<star>\<rfloor> Cod ν) \<star> Cod τ\<rfloor> = \<l using assms arr_char src_def trg_def E.Nml_HcompNml E.HcompNml_assoc by simp ultimately show ?thesis by simp qed moreover have "B.can (Dom μ \<star> Dom ν \<star> Dom τ) ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> B.can ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> Dom τ) (Dom μ \<lfloor>\<star>\<rflo B.can (Dom μ \<star> Dom ν \<star> Dom τ) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν \<lfloor>\< proof - have "E.Ide (Dom μ \<star> Dom ν \<star> Dom τ)" using assms src_def trg_def by fastforce moreover have "E.Ide ((Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> Dom τ)" using assms arr_char src_def trg_def E.Ide_HcompNml E.Src_HcompNml by auto moreover have "E.Ide (Dom μ \<lfloor>\<star>\<rfloor> Dom ν \<lfloor>\<star>\<rfloor> Dom τ using assms arr_char src_def trg_def by (simp add: E.Nml_HcompNml(1) E.Ide_HcompNml E.Trg_HcompNml) moreover have "\<lfloor>Dom μ \<star> Dom ν \<star> Dom τ\<rfloor> = \<lfloor>(Dom μ \<lfloo using assms arr_char src_def trg_def E.Nml_HcompNml E.HcompNml_assoc by simp moreover have "\<lfloor>(Dom μ \<lfloor>\<star>\<rfloor> Dom ν) \<star> Dom τ\<rfloor> = \<lfloor>Dom μ \< using assms arr_char src_def trg_def E.Nml_HcompNml E.HcompNml_assoc by simp ultimately show ?thesis by simp qed ultimately show ?thesis by simp qed finally show ?thesis by simp qed also have "... = Map (μ ⋆ ν ⋆ τ)" proof - have 1: "Map (μ ⋆ ν ⋆ τ) = B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod μ \<star (Map μ ⋆B B.can (Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod ν \<star> Cod τ) ⋅B (Map ν ⋆B Map τ) ⋅B B.can (Dom ν \<star> Dom τ) (Dom ν \<lfloor>\<star>\<rfloor> Dom τ)) ⋅B B.can (Dom μ \<star> Dom ν \<lfloor>\<star>\<rfloor> Dom τ) (Dom μ \<lfloor>\<star>\<rfloor using assms Map_hcomp [of μ "ν ⋆ τ"] Map_hcomp [of ν τ] by simp also have "... = B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod ((B.can (Cod μ) (Cod μ) ⋆B B.can (Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod ν \<star> C (Map μ ⋆B Map ν ⋆B Map τ) ⋅B (B.can (Dom μ) (Dom μ) ⋆B B.can (Dom ν \<star> Dom τ) (Dom ν \<lfloor>\<star>\<rfloor> Dom τ))) ⋅B B.can (Dom μ \<star> Dom ν \<lfloor>\<star>\<rfloor> Dom τ) (Dom μ \<lfloor>\<star>\<rfloor proof - have "Map μ ⋆B B.can (Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod ν \<star> Cod τ) ⋅B (Map ν ⋆B Map τ) ⋅B B.can (Dom ν \<star> Dom τ) (Dom ν \<lfloor>\<star>\<rfloor> Dom τ) = (B.can (Cod μ) (Cod μ) ⋆B B.can (Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod ν \<star> Co (Map μ ⋆B (Map ν ⋆B Map τ) ⋅B B.can (Dom ν \<star> Dom τ) (Dom ν \<lfloor>\<star>\<rfloor> Dom τ))" using assms B.interchange B.comp_cod_arr by (metis (no_types, lifting) B.can_Ide_self B.in_homE Map_hcomp arrE hseq_char) also have "... = (B.can (Cod μ) (Cod μ) ⋆B B.can (Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod ν \<star> Cod τ)) ⋅B (Map μ ⋆B Map ν ⋆B Map τ) ⋅B (B.can (Dom μ) (Dom μ) ⋆B B.can (Dom ν \<star> Dom τ) (Dom ν \<lfloor>\<star>\<rfloor> Dom τ))" using assms B.interchange B.comp_arr_dom [of "Map μ" "B.can (Dom μ) (Dom μ)"] by (metis (no_types, lifting) B.can_Ide_self B.null_is_zero(2) B.ext B.in_homE Map_hcomp arrE hseq_char) finally have "Map μ ⋆B B.can (Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod ν \<star> Cod τ) ⋅B (Map ν ⋆B Map τ) ⋅B B.can (Dom ν \<star> Dom τ) (Dom ν \<lfloor>\<star>\<rfloor> Dom τ) = (B.can (Cod μ) (Cod μ) ⋆B B.can (Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod ν \<star> Co (Map μ ⋆B Map ν ⋆B Map τ) ⋅B (B.can (Dom μ) (Dom μ) ⋆B B.can (Dom ν \<star> Dom τ) (Dom ν \<lfloor>\<star>\<rfloor> Do by simp thus ?thesis by simp qed also have "... = (B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Co (B.can (Cod μ) (Cod μ) ⋆B B.can (Cod ν \<lfloor>\<star>\<rfloor> Cod τ) (Cod ν \<star> Co (Map μ ⋆B Map ν ⋆B Map τ) ⋅B ((B.can (Dom μ) (Dom μ) ⋆B B.can (Dom ν \<star> Dom τ) (Dom ν \<lfloor>\<star>\<rfloor> Dom τ)) ⋅B B.can (Dom μ \<star> Dom ν \<lfloor>\<star>\<rfloor> Dom τ) (Dom μ \<lfloor>\<star>\<rfloor using B.comp_assoc by simp also have "... = B.can (Cod μ \<lfloor>\<star>\<rfloor> Cod ν \<lfloor>\<star>\<rfloor> Co (Map μ ⋆B Map ν ⋆B Map τ) ⋅B B.can (Dom μ \<star> Dom ν \<star> Dom τ) (Dom μ \<lfloor>\<star>\<rfloor> Dom ν \<lfloor>\< using assms μν ντ E.HcompNml_assoc src_def trg_def arr_char E.Src_HcompNml E.Trg_HcompNml E.Nml_HcompNml E.Ide_HcompNml by simp finally show ?thesis by simp qed ultimately show ?thesis by metis qed qed lemma obj_char: shows "obj a ⟷ endo a ∧ E.Obj (Dom a) ∧ Map a = {Dom a}" proof assume a: "obj a" show "endo a ∧ E.Obj (Dom a) ∧ Map a = {Dom a}" proof (intro conjI) show "endo a" using a ide_char by blast show "E.Obj (Dom a)" using a ide_char src_def by (metis (no_types, lifting) E.Ide_implies_Arr E.Obj_Trg arrE obj_def trg_simps(1) trg_src) show "Map a = {Dom a}" using a ide_char src_def by blast qed next assume a: "endo a ∧ E.Obj (Dom a) ∧ Map a = {Dom a}" show "obj a" proof - have "arr a" using a by auto moreover have "src a = a" using a E.Obj_in_Hom(1) seq_char by (intro arr_eqI, auto) ultimately show ?thesis using obj_def by simp qed qed lemma hcomp_obj_self: assumes "obj a" shows "a ⋆ a = a" proof (intro arr_eqI) show "hseq a a" using assms by auto show "arr a" using assms by auto show 1: "Dom (a ⋆ a) = Dom a" unfolding hcomp_def using assms arr_char E.HcompNml_Trg_Nml apply simp by (metis (no_types, lifting) objE obj_def trg_simps(1)) show 2: "Cod (a ⋆ a) = Cod a" unfolding hcomp_def using assms 1 arr_char E.HcompNml_Trg_Nml apply simp by (metis (no_types, lifting) Dom_hcomp ideE objE) show "Map (a ⋆ a) = Map a" using "1" Map_ide(1) assms by fastforce qed lemma hcomp_ide_src: assumes "ide f" shows "f ⋆ src f = f" proof (intro arr_eqI) show "hseq f (src f)" using assms by simp show "arr f" using assms by simp show 1: "Dom (f ⋆ src f) = Dom f" unfolding hcomp_def using assms apply simp using assms ide_char arr_char E.HcompNml_Nml_Src by (metis (no_types, lifting) ideD(1)) show "Cod (f ⋆ src f) = Cod f" unfolding hcomp_def using assms apply simp using assms ide_char arr_char E.HcompNml_Nml_Src by (metis (no_types, lifting) ideD(1)) show "Map (f ⋆ src f) = Map f" by (simp add: "1" Map_ide(1) assms) qed lemma hcomp_trg_ide: assumes "ide f" shows "trg f ⋆ f = f" proof (intro arr_eqI) show "hseq (trg f) f" using assms by auto show "arr f" using assms by auto show 1: "Dom (trg f ⋆ f) = Dom f" unfolding hcomp_def using assms apply simp using assms ide_char arr_char E.HcompNml_Trg_Nml by (metis (no_types, lifting) ideD(1)) show "Cod (trg f ⋆ f) = Cod f" unfolding hcomp_def using assms apply simp using assms ide_char arr_char E.HcompNml_Trg_Nml by (metis (no_types, lifting) ideD(1)) show "Map (trg f ⋆ f) = Map f" by (simp add: "1" Map_ide(1) assms) qed interpretation L: full_functor vcomp vcomp L proof fix a a' g assume a: "ide a" and a': "ide a'" assume g: "in_hom g (L a') (L a)" have a_eq: "a = MkIde (Dom a)" using a dom_char [of a] by simp have a'_eq: "a' = MkIde (Dom a')" using a' dom_char [of a'] by simp have 1: "Cod g = Dom a" proof - have "Dom (L a) = Dom a" by (simp add: a hcomp_trg_ide) thus ?thesis using g cod_char [of g] by (metis (no_types, lifting) Dom_cod in_homE) qed have 2: "Dom g = Dom a'" using a' g hcomp_trg_ide in_hom_char by auto let ?f = "MkArr (Dom a') (Cod a) (Map g)" have f: "in_hom ?f a' a" by (metis (no_types, lifting) "1" "2" MkArr_Map a a' g ideE in_hom_char) moreover have "L ?f = g" proof - have "L ?f = trg (MkArr (Dom a') (Cod a) (Map g)) ⋆ MkArr (Dom a') (Cod a) (Map g)" using f by auto also have "... = MkIde (E.Trg (Cod a)) ⋆ MkArr (Dom a') (Cod a) (Map g)" using a a' f trg_def [of a] vconn_implies_hpar by auto also have "... = MkArr (E.Trg (Cod a) \<lfloor>\<star>\<rfloor> Dom a') (E.Trg (Cod a (B.can (E.Trg (Cod a) \<lfloor>\<star>\<rfloor> Cod a) (E.Trg (Cod a) \<star> Cod a) ({E.Trg (Cod a)} ⋆B Map g) ⋅B B.can (E.Trg (Cod a) \<star> Dom a') (E.Trg (Cod a) \<lfloor>\<star>\<rfloor> Dom a' using hcomp_def apply simp by (metis (no_types, lifting) Cod.simps(1) arrE f in_homE src_trg trg.preserves_arr trg_def) also have "... = MkArr (Dom a') (Cod a) (B.can (Cod a) (E.Trg (Cod a) \<star> Cod a) ⋅B (trgB {Cod a} ⋆B Map g) ⋅B B.can (E.Trg (Cod a) \<star> Dom a') (Dom a'))" proof - have "E.Trg (Cod a) \<lfloor>\<star>\<rfloor> Dom a' = Dom a'" using a a' arr_char E.HcompNml_Trg_Nml by (metis (no_types, lifting) f ideE trg_simps(1) vconn_implies_hpar(4)) moreover have "E.Trg (Cod a) \<lfloor>\<star>\<rfloor> Cod a = Cod a" using a a' arr_char E.HcompNml_Trg_Nml by blast moreover have "{E.Trg (Cod a)} = trgB {Cod a}" using a a' arr_char E.eval_simps'(3) by fastforce ultimately show ?thesis by simp qed also have "... = MkArr (Dom a') (Cod a) (B.lunit {Cod a} ⋅B (trgB {Cod a} ⋆B Map g) ⋅B B.lunit' {Dom a'})" proof - have "E.Trg (Cod a) = E.Trg (Dom a')" using a a' a_eq g ide_char arr_char src_def trg_def trg_hcomp ‹Cod g = Dom a› ‹Dom g = Dom a'› by (metis (no_types, lifting) Cod.simps(1) in_homE) moreover have "B.can (Cod a) (E.Trg (Cod a) \<star> Cod a) = B.lunit {Cod a}" using a ide_char arr_char B.canE_unitor(2) by blast moreover have "B.can (E.Trg (Dom a') \<star> Dom a') (Dom a') = B.lunit' {Dom a'}" using a' ide_char arr_char B.canE_unitor(4) by blast ultimately show ?thesis by simp qed also have "... = MkArr (Dom g) (Cod g) (Map g)" proof - have "srcB {Cod a} = srcB (Map g)" using a f g ide_char arr_char src_def B.comp_cod_arr by (metis (no_types, lifting) B.vconn_implies_hpar(1) B.vconn_implies_hpar(3) Cod.simps(1) Map.simps(1) in_homE) moreover have "B.lunit {Cod g} ⋅B (trgB (Map g) ⋆B Map g) ⋅B B.lunit' {Dom g} = Map g" proof - have "B.lunit {Cod g} ⋅B (trgB (Map g) ⋆B Map g) ⋅B B.lunit' {Dom g} = B.lunit {Cod g} ⋅B B.lunit' {Cod g} ⋅B Map g" using g ide_char arr_char B.lunit'_naturality by (metis (no_types, lifting) partial_composition_axioms B.in_homE partial_composition.arrI) also have "... = (B.lunit {Cod g} ⋅B B.lunit' {Cod g}) ⋅B Map g" using B.comp_assoc by simp also have "... = {Cod g} ⋅B Map g" using g E.ide_eval_Ide B.comp_arr_inv' by fastforce also have "... = Map g" using g E.ide_eval_Ide B.comp_cod_arr by fastforce finally show ?thesis by simp qed ultimately have "B.lunit {Cod a} ⋅B (trgB {Cod a} ⋆B Map g) ⋅B B.lunit' {Dom a'} = Map g" using a a' 1 2 f g hcomp_def dom_char cod_char by (metis (no_types, lifting) B.null_is_zero(2) B.ext B.lunit_simps(2) B.lunit_simps(3) B.src.preserves_reflects_arr B.trg_vcomp B.vseq_implies_hpar(1) ideE) thus ?thesis using a 1 2 by auto qed also have "... = g" using g MkArr_Map by blast finally show ?thesis by simp qed ultimately show "∃f. in_hom f a' a ∧ L f = g" by blast qed interpretation R: full_functor vcomp vcomp R proof fix a a' g assume a: "ide a" and a': "ide a'" assume g: "in_hom g (R a') (R a)" have a_eq: "a = MkIde (Dom a)" using a dom_char [of a] by simp have a'_eq: "a' = MkIde (Dom a')" using a' dom_char [of a'] by simp have 1: "Cod g = Dom a" using a g hcomp_ide_src in_hom_char by force have 2: "Dom g = Dom a'" using a' g hcomp_ide_src by auto let ?f = "MkArr (Dom a') (Cod a) (Map g)" have f: "in_hom ?f a' a" proof (intro in_homI) show 3: "arr (MkArr (Dom a') (Cod a) (Map g))" by (metis (no_types, lifting) "1" "2" Cod.simps(1) MkArr_Map a_eq g in_homE) show "dom (MkArr (Dom a') (Cod a) (Map g)) = a'" using a a' 3 dom_char by auto show "cod (MkArr (Dom a') (Cod a) (Map g)) = a" using a a' 3 cod_char by auto qed moreover have "R ?f = g" proof - have "R ?f = MkArr (Dom a') (Cod a) (Map g) ⋆ src (MkArr (Dom a') (Cod a) (Map g))" using f by auto also have "... = MkArr (Dom a') (Cod a) (Map g) ⋆ MkIde (E.Src (Cod a))" using a a' f src_def [of a] vconn_implies_hpar by auto also have "... = MkArr (Dom a' \<lfloor>\<star>\<rfloor> E.Src (Cod a)) (Cod a \<lfloo (B.can (Cod a \<lfloor>\<star>\<rfloor> E.Src (Cod a)) (Cod a \<star> E.Src (Cod a)) (Map g ⋆B {E.Src (Cod a)}) ⋅B B.can (Dom a' \<star> E.Src (Cod a)) (Dom a' \<lfloor>\<star>\<rfloor> E.Src (Cod a) using hcomp_def apply simp by (metis (no_types, lifting) Cod_cod arrE f in_homE trg_src src.preserves_arr src_def) also have "... = MkArr (Dom a') (Cod a) (B.can (Cod a) (Cod a \<star> E.Src (Cod a)) ⋅B (Map g ⋆B srcB {Cod a}) ⋅B B.can (Dom a' \<star> E.Src (Cod a)) (Dom a'))" proof - have "Dom a' \<lfloor>\<star>\<rfloor> E.Src (Cod a) = Dom a'" using a a' arr_char E.HcompNml_Nml_Src by (metis (no_types, lifting) f ideE src_simps(1) vconn_implies_hpar(3)) moreover have "Cod a \<lfloor>\<star>\<rfloor> E.Src (Cod a) = Cod a" using a a' arr_char E.HcompNml_Nml_Src by blast moreover have "{E.Src (Cod a)} = srcB {Cod a}" using a a' arr_char E.eval_simps'(2) by fastforce ultimately show ?thesis by simp qed also have "... = MkArr (Dom a') (Cod a) (B.runit {Cod a} ⋅B (Map g ⋆B srcB {Cod a}) ⋅B B.runit' {Dom a'})" by (metis (no_types, lifting) B.canE_unitor(1) B.canE_unitor(3) a a' arrE f ideE src_simps(1) vconn_implies_hpar(3)) also have "... = MkArr (Dom g) (Cod g) (Map g)" proof - have "srcB {Cod a} = srcB (Map g)" using a f g ide_char arr_char src_def B.comp_cod_arr by (metis (no_types, lifting) B.vconn_implies_hpar(1) B.vconn_implies_hpar(3) Cod.simps(1) Map.simps(1) in_homE) moreover have "B.runit {Cod g} ⋅B (Map g ⋆B srcB (Map g)) ⋅B B.runit' {Dom g} = Map g" proof - have "B.runit {Cod g} ⋅B (Map g ⋆B srcB (Map g)) ⋅B B.runit' {Dom g} = B.runit {Cod g} ⋅B B.runit'{Cod g} ⋅B Map g" using g ide_char arr_char B.runit'_naturality [of "Map g"] by (metis (no_types, lifting) partial_composition_axioms B.in_homE partial_composition.arrI) also have "... = (B.runit {Cod g} ⋅B B.runit' {Cod g}) ⋅B Map g" using B.comp_assoc by simp also have "... = {Cod g} ⋅B Map g" using g E.ide_eval_Ide B.comp_arr_inv' by fastforce also have "... = Map g" using g E.ide_eval_Ide B.comp_cod_arr by fastforce finally show ?thesis by simp qed ultimately have "B.runit {Cod a} ⋅B (Map g ⋆B srcB {Cod a}) ⋅B B.runit' {Dom a'} = Map g" using a a' 1 2 f g hcomp_def dom_char cod_char by (metis (no_types, lifting) ideE) thus ?thesis using a 1 2 by auto qed also have "... = g" using g MkArr_Map by blast finally show ?thesis by simp qed ultimately show "∃f. in_hom f a' a ∧ R f = g" by blast qed interpretation L: faithful_functor vcomp vcomp L proof fix f f' assume par: "par f f'" and eq: "L f = L f'" show "f = f'" proof (intro arr_eqI) have 1: "Dom f = Dom f' ∧ Cod f = Cod f'" using par dom_char cod_char by auto show "arr f" using par by simp show "arr f'" using par by simp show 2: "Dom f = Dom f'" and 3: "Cod f = Cod f'" using 1 by auto show "Map f = Map f'" proof - have "B.L (Map f) = trgB (Map f) ⋆B Map f" using par by auto also have "... = trgB (Map f') ⋆B Map f'" proof - have "{E.Trg (Dom f)} ⋆B Map f = {E.Trg (Dom f')} ⋆B Map f'" proof - have A: "«B.can (E.Trg (Dom f) \<star> Dom f) (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> {E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Dom f} ==>B {E.Trg (Dom f)} ⋆B {Dom f}¬" using par arr_char B.can_in_hom E.Ide_HcompNml E.Ide_Nmlize_Ide E.Nml_Trg E.Nmlize_Nml E.HcompNml_Trg_Nml src_def trg_def by (metis (no_types, lifting) E.eval_simps(3) E.ide_eval_Ide E.Ide_implies_Arr B.canE_unitor(4) B.lunit'_in_vhom) have B: "«B.can (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Cod f) (E.Trg (Dom f) \<star> {E.Trg (Dom f)} ⋆B {Cod f} ==>B {E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Cod f}¬" using par arr_char B.can_in_hom E.Ide_HcompNml E.Ide_Nmlize_Ide E.Nml_Trg E.Nmlize_Nml E.HcompNml_Trg_Nml src_def trg_def by (metis (no_types, lifting) E.Nmlize.simps(3) E.eval.simps(3) E.Ide.simps(3) E.Ide_implies_Arr E.Src_Trg trg.preserves_arr trg_simps(2)) have C: "«{E.Trg (Dom f)} ⋆B Map f : {E.Trg (Dom f)} ⋆B {Dom f} ==>B {E.Trg (Dom f)} ⋆B {Cod f}¬" using par arr_char by (metis (no_types, lifting) E.eval_simps'(1) E.eval_simps(3) E.ide_eval_Ide E.Ide_implies_Arr E.Obj_Trg E.Obj_implies_Ide B.hcomp_in_vhom B.ide_in_hom(2) B.src_trg) have 3: "({E.Trg (Dom f)} ⋆B Map f) ⋅B B.can (E.Trg (Dom f) \<star> Dom f) (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Dom f) ({E.Trg (Dom f')} ⋆B Map f') ⋅B B.can (E.Trg (Dom f') \<star> Dom f') (E.Trg (Dom f') \<lfloor>\<star>\<rfloor> Dom proof - have 2: "B.can (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Cod f) (E.Trg (Dom f) \<star> ({E.Trg (Dom f)} ⋆B Map f) ⋅B B.can (E.Trg (Dom f) \<star> Dom f) (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Dom f) B.can (E.Trg (Dom f') \<lfloor>\<star>\<rfloor> Cod f') (E.Trg (Dom f') \<star> Cod ({E.Trg (Dom f')} ⋆B Map f') ⋅B B.can (E.Trg (Dom f') \<star> Dom f') (E.Trg (Dom f') \<lfloor>\<star>\<rfloor> Dom using par eq hcomp_def trg_def src_trg trg.preserves_arr Map_hcomp trg_simps(1) trg_simps(2) trg_simps(3) by auto have "B.mono (B.can (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Cod f) (E.Trg (Dom f) \< using par arr_char B.inverse_arrows_can B.iso_is_section B.section_is_mono src_def trg_def E.Nmlize_Nml E.HcompNml_Trg_Nml E.Ide_implies_Arr trg.preserves_arr trg_simps(1) by auto moreover have "B.seq (B.can (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Cod f) (E.Trg (Dom f) \<star> (({E.Trg (Dom f)} ⋆B Map f) ⋅B B.can (E.Trg (Dom f) \<star> Dom f) (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Dom f)) using A B C by auto moreover have "B.seq (B.can (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Cod f) (E.Trg (Dom f) \<star> (({E.Trg (Dom f')} ⋆B Map f') ⋅B B.can (E.Trg (Dom f') \<star> Dom f') (E.Trg (Dom f') \<lfloor>\<star>\<rfloor> Dom using par 1 2 arr_char calculation(2) by auto moreover have "B.can (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Cod f) (E.Trg (Dom f) \< B.can (E.Trg (Dom f') \<lfloor>\<star>\<rfloor> Cod f') (E.Trg (Dom f') \<star> Cod using par 1 arr_char by simp ultimately show ?thesis using 2 B.mono_cancel cod_char by auto qed show ?thesis proof - have "B.epi (B.can (E.Trg (Dom f) \<star> Dom f) (E.Trg (Dom f) \<lfloor>\<star>\<rfl using par arr_char B.inverse_arrows_can B.iso_is_retraction B.retraction_is_epi E.Nmlize_Nml E.HcompNml_Trg_Nml src_def trg_def E.Ide_implies_Arr by (metis (no_types, lifting) E.Nmlize.simps(3) E.Ide.simps(3) E.Src_Trg trg.preserves_arr trg_simps(1)) moreover have "B.seq ({E.Trg (Dom f)} ⋆B Map f) (B.can (E.Trg (Dom f) \<star> Dom f) (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Dom f) using A C by auto moreover have "B.seq ({E.Trg (Dom f')} ⋆B Map f') (B.can (E.Trg (Dom f) \<star> Dom f) (E.Trg (Dom f) \<lfloor>\<star>\<rfloor> Dom f) using 1 3 calculation(2) by auto ultimately show ?thesis using par 1 3 arr_char B.epi_cancel by simp qed qed moreover have "trgB (Map f) = {E.Trg (Dom f)} ∧ trgB (Map f') = {E.Trg (Dom f')}" using par arr_char trg_def E.Ide_implies_Arr B.comp_arr_dom B.vseq_implies_hpar(2) E.eval_simps(3) by (metis (no_types, lifting) B.vconn_implies_hpar(2)) ultimately show ?thesis by simp qed also have "... = B.L (Map f')" using par B.hseqE B.hseq_char' by auto finally have "B.L (Map f) = B.L (Map f')" by simp thus ?thesis using 2 3 par arr_char B.L.is_faithful by (metis (no_types, lifting) B.in_homE) qed qed qed interpretation R: faithful_functor vcomp vcomp R proof fix f f' assume par: "par f f'" and eq: "R f = R f'" show "f = f'" proof (intro arr_eqI) have 1: "Dom f = Dom f' ∧ Cod f = Cod f'" using par dom_char cod_char by auto show "arr f" using par by simp show "arr f'" using par by simp show 2: "Dom f = Dom f'" and 3: "Cod f = Cod f'" using 1 by auto show "Map f = Map f'" proof - have "B.R (Map f) = Map f ⋆B srcB (Map f)" using par apply simp by (metis B.hseqE B.hseq_char') also have "... = Map f' ⋆B srcB (Map f')" proof - have "Map f ⋆B {E.Src (Dom f)} = Map f' ⋆B {E.Src (Dom f')}" proof - have 2: "E.Ide (Cod f \<star> E.Src (Dom f))" using par arr_char src.preserves_arr by auto hence 3: "E.Ide (Cod f \<lfloor>\<star>\<rfloor> E.Src (Dom f))" using par arr_char E.Nml_Src E.Ide_HcompNml calculation by auto have 4: "\<lfloor>Cod f \<star> E.Src (Dom f)\<rfloor> = \<lfloor>Cod f \<lfloor>\<star> using par arr_char by (simp add: E.Nml_HcompNml(1)) have A: "«B.can (Dom f \<star> E.Src (Dom f)) (Dom f \<lfloor>\<star>\<rfloor> E.Src (D {Dom f \<lfloor>\<star>\<rfloor> E.Src (Dom f)} ==>B {Dom f} ⋆B {E.Src (Dom f)}¬" using par arr_char B.can_in_hom E.Ide_HcompNml E.Ide_Nmlize_Ide E.Nml_Src E.Nmlize_Nml E.HcompNml_Nml_Src src_def trg_def by (metis (no_types, lifting) E.eval_simps(2) E.ide_eval_Ide E.Ide_implies_Arr B.canE_unitor(3) B.runit'_in_vhom) have B: "«B.can (Cod f \<lfloor>\<star>\<rfloor> E.Src (Dom f)) (Cod f \<star> E.Src (D {Cod f} ⋆B {E.Src (Dom f)} ==>B {Cod f \<lfloor>\<star>\<rfloor> E.Src (Dom f)}¬" using 2 3 4 B.can_in_hom [of "Cod f \<star> E.Src (Dom f)" "Cod f \<lfloor>\<star>\<rfloor> by simp have C: "«Map f ⋆B {E.Src (Dom f)} : {Dom f} ⋆B {E.Src (Dom f)} ==>B {Cod f} ⋆B {E.Src (Dom f)}¬" using par arr_char E.Ide_Nmlize_Ide E.Nml_Trg E.Nmlize_Nml E.HcompNml_Trg_Nml src_def trg_def E.ide_eval_Ide E.Ide_implies_Arr E.Obj_implies_Ide apply (intro B.hcomp_in_vhom) apply (simp add: B.ide_in_hom(2)) apply simp by (metis (no_types, lifting) A B.ideD(1) B.not_arr_null B.seq_if_composable B.src.preserves_reflects_arr B.vconn_implies_hpar(3) E.HcompNml_Nml_Src) have 5: "(Map f ⋆B {E.Src (Dom f)}) ⋅B B.can (Dom f \<star> E.Src (Dom f)) (Dom f \<lfloor>\<star>\<rfloor> E.Src (Dom f)) (Map f' ⋆B {E.Src (Dom f')}) ⋅B B.can (Dom f' \<star> E.Src (Dom f')) (Dom f' \<lfloor>\<star>\<rfloor> E.Src (Dom f proof - have 6: "B.can (Cod f \<lfloor>\<star>\<rfloor> E.Src (Dom f)) (Cod f \<star> E.Src (D (Map f ⋆B {E.Src (Dom f)}) ⋅B B.can (Dom f \<star> E.Src (Dom f)) (Dom f \<lfloor>\<star>\<rfloor> E.Src (Dom f)) B.can (Cod f' \<lfloor>\<star>\<rfloor> E.Src (Dom f')) (Cod f' \<star> E.Src (Dom f (Map f' ⋆B {E.Src (Dom f')}) ⋅B B.can (Dom f' \<star> E.Src (Dom f')) (Dom f' \<lfloor>\<star>\<rfloor> E.Src (Dom f using par eq hcomp_def src_def trg_src src.preserves_arr Map_hcomp src_simps(1) src_simps(2) src_simps(3) by auto have "B.mono (B.can (Cod f \<lfloor>\<star>\<rfloor> E.Src (Dom f)) (Cod f \<star> E. using 2 3 4 B.inverse_arrows_can(1) B.iso_is_section B.section_is_mono by simp moreover have "B.seq (B.can (Cod f \<lfloor>\<star>\<rfloor> E.Src (Dom f)) (Cod f \<star> E.Src ( ((Map f ⋆B {E.Src (Dom f)}) ⋅B B.can (Dom f \<star> E.Src (Dom f)) (Dom f \<lfloor>\<star>\<rfloor> E.Src (Dom f))) using A B C by auto moreover have "B.seq (B.can (Cod f \<lfloor>\<star>\<rfloor> E.Src (Dom f)) (Cod f \<star> E.Src ( ((Map f' ⋆B {E.Src (Dom f')}) ⋅B B.can (Dom f' \<star> E.Src (Dom f')) (Dom f' \<lfloor>\<star>\<rfloor> E.Src (Dom f using par 1 6 arr_char calculation(2) by auto moreover have "B.can (Cod f \<lfloor>\<star>\<rfloor> E.Src (Dom f)) (Cod f \<star> E. B.can (Cod f' \<lfloor>\<star>\<rfloor> E.Src (Dom f')) (Cod f' \<star> E.Src (Dom f using par 1 arr_char by simp ultimately show ?thesis using 6 B.mono_cancel cod_char by auto qed show ?thesis proof - have "B.epi (B.can (Dom f \<star> E.Src (Dom f)) (Dom f \<lfloor>\<star>\<rfloor> E.S using 2 3 4 B.inverse_arrows_can(1) B.iso_is_retraction B.retraction_is_epi by (metis (no_types, lifting) E.Nml_Src E.Nmlize.simps(3) E.Nmlize_Nml E.HcompNml_Nml_Src E.Ide.simps(3) par arrE) moreover have "B.seq (Map f ⋆B {E.Src (Dom f)}) (B.can (Dom f \<star> E.Src (Dom f)) (Dom f \<lfloor>\<star>\<rfloor> E.Src (Dom f)) using A C by auto moreover have "B.seq (Map f' ⋆B {E.Src (Dom f')}) (B.can (Dom f \<star> E.Src (Dom f)) (Dom f \<lfloor>\<star>\<rfloor> E.Src (Dom f)) using 1 5 calculation(2) by auto ultimately show ?thesis using par 1 5 arr_char B.epi_cancel by simp qed qed moreover have "srcB (Map f) = {E.Src (Dom f)} ∧ srcB (Map f') = {E.Src (Dom f')}" using par arr_char src_def by (metis (no_types, lifting) B.vconn_implies_hpar(1) E.Nml_implies_Arr E.eval_simps(2)) ultimately show ?thesis by simp qed also have "... = B.R (Map f')" using par B.hseqE B.hseq_char' by auto finally have "B.R (Map f) = B.R (Map f')" by simp thus ?thesis using 2 3 par arr_char B.R.is_faithful by (metis (no_types, lifting) B.in_homE) qed qed qed definition a where "a τ μ ν ≡ if VVV.arr (τ, μ, ν) then hcomp τ (hcomp μ ν) else null" interpretation natural_isomorphism VVV.comp vcomp HoHV HoVH ‹λτμν. a (fst τμν) (fst (snd τμν)) (snd (snd τμν))› proof show "∧τμν. ¬ VVV.arr τμν ==> a (fst τμν) (fst (snd τμν)) (snd (snd τμν)) = null" using a_def by simp show 1: "∧τμν. VVV.arr τμν ==> arr (a (fst τμν) (fst (snd τμν)) (snd (snd τμν)))" using VVV.arr_charSbC VV.arr_charSbC a_def hcomp_assoc HoHV_def VVV.dom_simp VV.dom_sim by force show "∧τμν. VVV.arr τμν ==> HoVH τμν ⋅ a (fst (VVV.dom τμν)) (fst (snd (VVV.dom τμν))) (snd (snd (VVV.dom τμν))) = a (fst τμν) (fst (snd τμν)) (snd (snd τμν))" using a_def HoVH.as_nat_trans.naturality1 HoVH_def by auto show "∧τμν. VVV.arr τμν ==> a (fst (VVV.cod τμν)) (fst (snd (VVV.cod τμν))) (snd (snd (VVV.cod τμν))) ⋅ HoHV τμν = a (fst τμν) (fst (snd τμν)) (snd (snd τμν))" proof - fix τμν assume τμν: "VVV.arr τμν" have "HoHV τμν = a (fst τμν) (fst (snd τμν)) (snd (snd τμν))" unfolding a_def HoHV_def using τμν HoHV.preserves_cod hcomp_assoc VVV.arr_charSbC VV.arr_charSbC by simp thus "a (fst (VVV.cod τμν)) (fst (snd (VVV.cod τμν))) (snd (snd (VVV.cod τμν))) ⋅ HoHV τμν = a (fst τμν) (fst (snd τμν)) (snd (snd τμν))" using 1 τμν comp_cod_arr a_def HoVH.as_nat_trans.naturality2 by (metis (no_types, lifting) HoVH_def prod.collapse) qed show "∧fgh. VVV.ide fgh ==> iso (a (fst fgh) (fst (snd fgh)) (snd (snd fgh)))" using a_def HoVH.preserves_ide HoVH_def by auto qed definition i where "i ≡ λa. a" sublocale bicategory vcomp hcomp a i src trg using hcomp_obj_self a_def hcomp_assoc VVV.arr_charSbC VV.arr_charSbC apply unfold_locales by (auto simp add: i_def ide_in_hom(2)) lemma is_bicategory: shows "bicategory vcomp hcomp a i src trg" .. sublocale strict_bicategory vcomp hcomp a i src trg proof show "∧fgh. ide fgh ==> lunit fgh = fgh" proof - fix fgh assume fgh: "ide fgh" have "fgh = lunit fgh" proof (intro lunit_eqI) show "ide fgh" using fgh by simp show "«fgh : trg fgh ⋆ fgh ==> fgh¬" using fgh hcomp_def hcomp_trg_ide by auto show "trg fgh ⋆ fgh = (i (trg fgh) ⋆ fgh) ⋅ a' (trg fgh) (trg fgh) fgh" proof - have "(i (trg fgh) ⋆ fgh) ⋅ a' (trg fgh) (trg fgh) fgh = (trg fgh ⋆ fgh) ⋅ a' (trg fgh) (trg fgh) fgh" using fgh i_def by metis also have "... = (trg fgh ⋆ fgh) ⋅ (trg fgh ⋆ trg fgh ⋆ fgh)" using fgh a_def by fastforce also have "... = trg fgh ⋆ fgh" using fgh hcomp_obj_self hcomp_assoc by (simp add: hcomp_trg_ide) finally show ?thesis by simp qed qed thus "lunit fgh = fgh" by simp qed show "∧fgh. ide fgh ==> runit fgh = fgh" proof - fix fgh assume fgh: "ide fgh" have "fgh = runit fgh" proof (intro runit_eqI) show "ide fgh" using fgh by simp show "«fgh : fgh ⋆ src fgh ==> fgh¬" using fgh hcomp_def hcomp_ide_src by auto show "fgh ⋆ src fgh = (fgh ⋆ i (src fgh)) ⋅ a fgh (src fgh) (src fgh)" proof - have "(fgh ⋆ i (src fgh)) ⋅ a fgh (src fgh) (src fgh) = (fgh ⋆ src fgh) ⋅ a fgh (src fgh) (src fgh)" using fgh i_def by metis also have "... = (fgh ⋆ src fgh) ⋅ (fgh ⋆ src fgh ⋆ src fgh)" using fgh a_def by fastforce also have "... = fgh ⋆ src fgh" using fgh comp_arr_dom hcomp_obj_self by simp finally show ?thesis by simp qed qed thus "runit fgh = fgh" by simp qed show "∧f g h. [ ide f; ide g; ide h; src f = trg g; src g = trg h ] ==> ide (a f using a_def VV.arr_charSbC VVV.arr_charSbC by auto qed theorem is_strict_bicategory: shows "strict_bicategory vcomp hcomp a i src trg" .. lemma iso_char: shows "iso μ ⟷ arr μ ∧ B.iso (Map μ)" and "iso μ ==> inv μ = MkArr (Cod μ) (Dom μ) (B.inv (Map μ))" proof - have 1: "iso μ ==> arr μ ∧ B.iso (Map μ)" proof - assume μ: "iso μ" obtain ν where ν: "inverse_arrows μ ν" using μ by auto have "B.inverse_arrows (Map μ) (Map ν)" proof show "B.ide (Map μ ⋅B Map ν)" proof - have "Map μ ⋅B Map ν = Map (μ ⋅ ν)" using μ ν inverse_arrows_def Map_comp arr_char seq_char by (metis (no_types, lifting) ide_compE) moreover have "B.ide ..." using ν ide_char by blast ultimately show ?thesis by simp qed show "B.ide (Map ν ⋅B Map μ)" proof - have "Map ν ⋅B Map μ = Map (ν ⋅ μ)" using μ ν inverse_arrows_def comp_char [of ν μ] by simp moreover have "B.ide ..." using ν ide_char by blast ultimately show ?thesis by simp qed qed thus "arr μ ∧ B.iso (Map μ)" using μ by auto qed let ?ν = "MkArr (Cod μ) (Dom μ) (B.inv (Map μ))" have 2: "arr μ ∧ B.iso (Map μ) ==> iso μ ∧ inv μ = ?ν" proof assume μ: "arr μ ∧ B.iso (Map μ)" have ν: "«?ν : cod μ ==> dom μ¬" using μ arr_char dom_char cod_char by auto have 4: "inverse_arrows μ ?ν" proof show "ide (?ν ⋅ μ)" proof - have "?ν ⋅ μ = dom μ" using μ ν MkArr_Map comp_char seq_char B.comp_inv_arr' dom_char by auto thus ?thesis using μ by simp qed show "ide (μ ⋅ ?ν)" proof - have "μ ⋅ ?ν = cod μ" using μ ν MkArr_Map comp_char seq_char B.comp_arr_inv' cod_char by auto thus ?thesis using μ by simp qed qed thus "iso μ" by auto show "inv μ = ?ν" using 4 inverse_unique by simp qed have 3: "arr μ ∧ B.iso (Map μ) ==> iso μ" using 2 by simp show "iso μ ⟷ arr μ ∧ B.iso (Map μ)" using 1 3 by blast show "iso μ ==> inv μ = ?ν" using 1 2 by blast qed subsection "The Strictness Theorem" text ‹ The Strictness Theorem asserts: ``Every bicategory is biequivalent to a strict b This amounts to an equivalent (and perhaps more desirable) formulation of the Coherence Theorem. In this section we prove the Strictness Theorem by constructing an equivalence p from a bicategory to its strictification. text ‹ We define a map ‹UP› from the given bicategory ‹B› to its strictification, and show that it is an equivalence pseudofunctor. The following auxiliary definition is not logically necessary, but it provides s terms that can be the targets of simplification rules and thereby enables some p to be done by simplification that otherwise could not be. Trying to eliminate i breaks some short proofs below, so I have kept it. definition UP0 where "UP0 a ≡ if B.obj a then MkIde \<langle>a\<rangle>0 else null" lemma obj_UP0 [simp]: assumes "B.obj a" shows "obj (UP0 a)" unfolding obj_def using assms UP0_def ide_MkIde [of "\<langle>a\<rangle>0"] src_def by simp lemma UP0_in_hom [intro]: assumes "B.obj a" shows "«UP0 a : UP0 a → UP0 a¬" and "«UP0 a : UP0 a ==> UP0 a¬" using assms obj_UP0 by blast+ lemma UP0_simps [simp]: assumes "B.obj a" shows "ide (UP0 a)" "arr (UP0 a)" and "src (UP0 a) = UP0 a" and "trg (UP0 a) = UP0 a" and "dom (UP0 a) = UP0 a" and "cod (UP0 a) = UP0 a" using assms obj_UP0 apply blast using assms obj_UP0 obj_simps by simp_all definition UP where "UP μ ≡ if B.arr μ then MkArr \<langle>B.dom μ\<rangle> \<langle>B.cod μ\<rangle> μ lemma Dom_UP [simp]: assumes "B.arr μ" shows "Dom (UP μ) = \<langle>B.dom μ\<rangle>" using assms UP_def by fastforce lemma Cod_UP [simp]: assumes "B.arr μ" shows "Cod (UP μ) = \<langle>B.cod μ\<rangle>" using assms UP_def by fastforce lemma Map_UP [simp]: assumes "B.arr μ" shows "Map (UP μ) = μ" using assms UP_def by fastforce lemma arr_UP: assumes "B.arr μ" shows "arr (UP μ)" using assms UP_def by (intro arrI, fastforce+) lemma UP_in_hom [intro]: assumes "B.arr μ" shows "«UP μ : UP0 (srcB μ) → UP0 (trgB μ)¬" and "«UP μ : UP (B.dom μ) ==> UP (B.cod μ)¬" using assms arr_UP UP_def UP0_def dom_char cod_char src_def trg_def by auto lemma UP_simps [simp]: assumes "B.arr μ" shows "arr (UP μ)" and "src (UP μ) = UP0 (srcB μ)" and "trg (UP μ) = UP0 (trgB μ)" and "dom (UP μ) = UP (B.dom μ)" and "cod (UP μ) = UP (B.cod μ)" using assms arr_UP UP_in_hom by auto interpretation UP: "functor" VB vcomp UP using UP_def arr_UP UP_simps(4-5) arr_UP UP_def comp_char seq_char by unfold_locales auto interpretation UP: weak_arrow_of_homs VB srcB trgB vcomp src trg UP proof fix μ assume μ: "B.arr μ" show "UP (srcB μ) ≅ src (UP μ)" proof - let ?φ = "MkArr \<langle>srcB μ\<rangle> \<langle>srcB μ\<rangle>0 (srcB μ)" have φ: "«?φ : UP (srcB μ) ==> src (UP μ)¬" using μ UP_def src_def arr_UP by (intro MkArr_in_hom) auto have "iso ?φ" using μ φ iso_char src_def by auto thus ?thesis using φ isomorphic_def by auto qed show "UP (trgB μ) ≅ trg (UP μ)" proof - let ?φ = "MkArr \<langle>trgB μ\<rangle> \<langle>trgB μ\<rangle>0 (trgB μ)" have φ: "«?φ : UP (trgB μ) ==> trg (UP μ)¬" using μ UP_def trg_def arr_UP by (intro MkArr_in_hom) auto have "iso ?φ" using μ φ iso_char trg_def by auto thus ?thesis using φ isomorphic_def by auto qed qed interpretation HoUP_UP: composite_functor B.VV.comp VV.comp vcomp UP.FF ‹λμν. hcomp (fst μν) (snd μν)› .. interpretation UPoH: composite_functor B.VV.comp VB vcomp ‹λμν. fst μν ⋆B snd μν› UP .. abbreviation Φo where "Φo fg ≡ MkArr (\<langle>fst fg\<rangle> \<star> \<langle>snd fg\<rangle>) \<langl interpretation Φ: transformation_by_components B.VV.comp vcomp HoUP_UP.map UPoH.map Φo proof fix fg assume fg: "B.VV.ide fg" show "«Φo fg : HoUP_UP.map fg ==> UPoH.map fg¬" proof (intro in_homI) show 1: "arr (Φo fg)" using fg arr_char B.VV.ide_charSbC B.VV.arr_charSbC by auto show "dom (Φo fg) = HoUP_UP.map fg" using 1 fg UP.FF_def B.VV.arr_charSbC B.VV.ide_charSbC dom_char hcomp_def B.can_Ide_self by simp show "cod (Φo fg) = UPoH.map fg" using fg arr_char cod_char B.VV.ide_charSbC B.VV.arr_charSbC UP_def by auto qed next fix μν assume μν: "B.VV.arr μν" show "Φo (B.VV.cod μν) ⋅ HoUP_UP.map μν = UPoH.map μν ⋅ Φo (B.VV.dom μν)" proof - have "Φo (B.VV.cod μν) ⋅ HoUP_UP.map μν = MkArr (\<langle>B.dom (fst μν)\<rangle> \<star> \<langle>B.dom (snd μν)\<rangle>) (\<langle>B.cod (fst μν) ⋆B B.cod (snd μν)\<rangle>) (fst μν ⋆B snd μν)" proof - have "Φo (B.VV.cod μν) ⋅ HoUP_UP.map μν = MkArr (\<langle>B.cod (fst μν)\<rangle> \<star> \<langle>B.cod (snd μν)\<rangle>) (\<langl (B.cod (fst μν) ⋆B B.cod (snd μν)) ⋅ MkArr (\<langle>B.dom (fst μν)\<rangle> \<star> \<langle>B.dom (snd μν)\<rangle>) (\<langle>B.cod (fst μν)\<rangle> \<star> \<langle>B.cod (snd μν)\<rangle>) (fst μν ⋆B snd μν)" using μν B.VV.arr_charSbC arr_char UP.FF_def hcomp_def UP_def B.VV.cod_simp src_def trg_def B.can_in_hom B.can_Ide_self B.comp_arr_dom B.comp_cod_arr by auto also have "... = MkArr (\<langle>B.dom (fst μν)\<rangle> \<star> \<langle>B.dom (snd μν)\<r (\<langle>B.cod (fst μν) ⋆B B.cod (snd μν)\<rangle>) ((B.cod (fst μν) ⋆B B.cod (snd μν)) ⋅B (fst μν ⋆B snd μν))" using μν B.VV.arr_charSbC by (intro comp_MkArr arr_MkArr, auto) also have "... = MkArr (\<langle>B.dom (fst μν)\<rangle> \<star> \<langle>B.dom (snd μν)\<r (\<langle>B.cod (fst μν) ⋆B B.cod (snd μν)\<rangle>) (fst μν ⋆B snd μν)" using μν B.VV.arr_charSbC B.comp_cod_arr by auto finally show ?thesis by simp qed also have "... = UPoH.map μν ⋅ Φo (B.VV.dom μν)" proof - have "UPoH.map μν ⋅ Φo (B.VV.dom μν) = MkArr (\<langle>B.dom (fst μν) ⋆B B.dom (snd μν)\<rangle>) (\<langle>B.cod (fst μν) ⋆B B.cod (snd μν)\<rangle>) (fst μν ⋆B snd μν) ⋅ MkArr (\<langle>B.dom (fst μν)\<rangle> \<star> \<langle>B.dom (snd μν)\<rangle>) (\<langle>B.dom (fst μν) ⋆B B.dom (snd μν)\<rangle>) (B.dom (fst μν) ⋆B B.dom (snd μν))" using μν B.VV.arr_charSbC arr_char UP.FF_def hcomp_def UP_def B.VV.dom_simp src_def trg_def B.can_in_hom B.can_Ide_self B.comp_arr_dom B.comp_cod_arr by auto also have "... = MkArr (\<langle>B.dom (fst μν)\<rangle> \<star> \<langle>B.dom (snd μν)\<r (\<langle>B.cod (fst μν) ⋆B B.cod (snd μν)\<rangle>) ((fst μν ⋆B snd μν) ⋅B (B.dom (fst μν) ⋆B B.dom (snd μν)))" using μν B.VV.arr_charSbC arr_MkArr apply (intro comp_MkArr arr_MkArr) by auto also have "... = MkArr (\<langle>B.dom (fst μν)\<rangle> \<star> \<langle>B.dom (snd μν)\<r (\<langle>B.cod (fst μν) ⋆B B.cod (snd μν)\<rangle>) (fst μν ⋆B snd μν)" using μν B.VV.arr_charSbC B.comp_arr_dom by auto finally show ?thesis by simp qed finally show ?thesis by simp qed qed abbreviation cmpUP where "cmpUP ≡ Φ.map" lemma cmpUP_in_hom [intro]: assumes "B.arr (fst μν)" and "B.arr (snd μν)" and "srcB (fst μν) = trgB (snd μν)" shows "«cmpUP μν : UP0 (srcB (snd μν)) → UP0 (trgB (fst μν))¬" and "«cmpUP μν : UP (B.dom (fst μν)) ⋆ UP (B.dom (snd μν)) ==> UP (B.cod (fst μν) ⋆B B.cod (snd μν))¬" proof - let ?μ = "fst μν" and ?ν = "snd μν" show 1: "«cmpUP μν : UP (B.dom ?μ) ⋆ UP (B.dom ?ν) ==> UP (B.cod ?μ ⋆B B.cod ?ν)¬" proof show "arr (cmpUP μν)" using assms by auto show "dom (cmpUP μν) = UP (B.dom ?μ) ⋆ UP (B.dom ?ν)" proof - have "B.VV.in_hom (?μ, ?ν) (B.dom ?μ, B.dom ?ν) (B.cod ?μ, B.cod ?ν)" using assms B.VV.in_hom_charSbC B.VV.arr_charSbC by auto hence "dom (cmpUP μν) = HoUP_UP.map (B.dom ?μ, B.dom ?ν)" by auto also have "... = UP (B.dom ?μ) ⋆ UP (B.dom ?ν)" using assms UP.FF_def by fastforce finally show ?thesis by simp qed show "cod (cmpUP μν) = UP (B.cod ?μ ⋆B B.cod ?ν)" using assms B.VV.in_hom_charSbC B.VV.arr_charSbC B.VV.cod_simp by auto qed show "«cmpUP μν : UP0 (srcB ?ν) → UP0 (trgB ?μ)¬" using assms 1 src_dom [of "cmpUP μν"] trg_dom [of "cmpUP μν"] by fastforce qed lemma cmpUP_simps [simp]: assumes "B.arr (fst μν)" and "B.arr (snd μν)" and "srcB (fst μν) = trgB (snd μν)" shows "arr (cmpUP μν)" and "src (cmpUP μν) = UP0 (srcB (snd μν))" and "trg (cmpUP μν) = UP0 (trgB (fst μν))" and "dom (cmpUP μν) = UP (B.dom (fst μν)) ⋆ UP (B.dom (snd μν))" and "cod (cmpUP μν) = UP (B.cod (fst μν) ⋆B B.cod (snd μν))" using assms cmpUP_in_hom [of μν] by auto lemma cmpUP_ide_simps [simp]: assumes "B.ide (fst fg)" and "B.ide (snd fg)" and "srcB (fst fg) = trgB (snd fg)" shows "Dom (cmpUP fg) = \<langle>fst fg\<rangle> \<star> \<langle>snd fg\<rangle>" and "Cod (cmpUP fg) = \<langle>fst fg ⋆B snd fg\<rangle>" and "Map (cmpUP fg) = fst fg ⋆B snd fg" using assms B.VV.ide_charSbC B.VV.arr_charSbC by auto interpretation Φ: natural_isomorphism B.VV.comp vcomp HoUP_UP.map UPoH.map cmpUP proof fix fg assume fg: "B.VV.ide fg" have "arr (cmpUP fg)" using fg Φ.preserves_reflects_arr [of fg] by simp thus "iso (cmpUP fg)" using fg iso_char by simp qed lemma cmpUP_ide_simp: assumes "B.ide f" and "B.ide g" and "srcB f = trgB g" shows "cmpUP (f, g) = MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<langle> using assms B.VV.ide_charSbC B.VV.arr_charSbC by simp lemma cmpUP'_ide_simp: assumes "B.ide f" and "B.ide g" and "srcB f = trgB g" shows "inv (cmpUP (f, g)) = MkArr \<langle>f ⋆B g\<rangle> (\<langle>f\<rangle> \<star using assms cmpUP_ide_simp iso_char Φ.components_are_iso [of "(f, g)"] B.VV.ide_charSbC B.VV.arr_charSbC by simp interpretation UP: pseudofunctor VB HB aB iB srcB trgB vcomp hcomp a i src trg UP cmpUP proof fix f g h assume f: "B.ide f" and g: "B.ide g" and h: "B.ide h" and fg: "srcB f = trgB g" and gh: "srcB g = trgB h" show "UP aB[f, g, h] ⋅ cmpUP (f ⋆B g, h) ⋅ (cmpUP (f, g) ⋆ UP h) = cmpUP (f, g ⋆B h) ⋅ (UP f ⋆ cmpUP (g, h)) ⋅ a (UP f) (UP g) (UP h)" proof - have "UP aB[f, g, h] ⋅ cmpUP (f ⋆B g, h) ⋅ (cmpUP (f, g) ⋆ UP h) = MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<rangle>) \<lan proof - have 1: "UP.hseqD (MkIde \<langle>f\<rangle>) (MkIde \<langle>g\<rangle>)" using f g fg hseq_char src_def trg_def arr_char by auto have 2: "UP.hseqD (MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<langle>f ⋆B (MkIde \<langle>h\<rangle>)" proof - have "MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<langle>f ⋆B g\<rangle> ( MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<langle>f ⋆B g\<rangle> (f ⋆B proof - have "MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<langle>f ⋆B g\<rangle> ( MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<langle>f ⋆B g\<rangle> (f ⋆B using f g fg by simp also have "... = MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<langle>f ⋆B g using f g fg by (intro comp_MkArr arr_MkArr, auto) also have "... = MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<langle>f ⋆B g using f g fg by simp finally show ?thesis by blast qed thus ?thesis using f g h fg gh arr_char src_def trg_def by auto qed have "UP aB[f, g, h] = MkArr \<langle>(f ⋆B g) ⋆B h\<rangle> \<langle>f ⋆B g ⋆B h\<ra using f g h fg gh UP_def B.HoHV_def B.HoVH_def B.VVV.arr_charSbC B.VV.arr_charSbC B.VVV.dom_charSbC B.VVV.cod_charSbC by simp moreover have "cmpUP (f ⋆B g, h) = MkArr (\<langle>f ⋆B g\<rangle> \<star> \<langle>h\<rangle>) \<la MkArr (\<langle>f ⋆B g\<rangle> \<star> \<langle>h\<rangle>) (\<langle>f ⋆B g\<rangle> using f g h fg gh Φ.map_simp_ide Φ.map_def B.VV.arr_charSbC UP.FF_def B.VV.cod_simp hcomp_def B.can_Ide_self by simp moreover have "cmpUP (f, g) ⋆ UP h = MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<rangle>) (\<la proof - have "MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) (\<langle>f\<rangle> \<star (B.can (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) (\<langle>f\<rangle> \<star> \<l MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) (\<langle>f\<rangle> \<star> \<la using f g fg B.can_Ide_self B.comp_arr_dom B.comp_cod_arr by simp moreover have "MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<langle>f ⋆B g\<r MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) (\<langle>f\<rangle> \<star> \<la MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<langle>f ⋆B g\<rangle> (f ⋆B by (metis (no_types, lifting) 2 B.ideD(1) E.eval.simps(2-3) cod_MkArr comp_arr_ide f g ide_char' seq_char) moreover have "B.can ((\<langle>f\<rangle> \<star> \<langle>g\<rangle>) \<star> \<langle> using f g h fg gh B.canI_associator_0 B.inverse_arrows_can by simp ultimately show ?thesis using 1 2 f g h fg gh Φ.map_def UP_def hcomp_def UP.FF_def B.VV.arr_charSbC B.can_Ide_self B.comp_cod_arr B.VV.cod_simp by simp qed ultimately have "UP aB[f, g, h] ⋅ cmpUP (f ⋆B g, h) ⋅ (cmpUP (f, g) ⋆ UP h) = MkArr \<langle>(f ⋆B g) ⋆B h\<rangle> \<langle>f ⋆B g ⋆B h\<rangle> aB[f, g, h] ⋅ MkArr (\<langle>f ⋆B g\<rangle> \<star> \<langle>h\<rangle>) \<langle>(f ⋆B g) ⋆B h\<ra MkArr (\<langle>f ⋆B g\<rangle> \<star> \<langle>h\<rangle>) (\<langle>f ⋆B g\<rangle> MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<rangle>) (\<la using comp_assoc by presburger also have "... = MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle> (aB[f, g, h] ⋅B ((f ⋆B g) ⋆B h) ⋅B ((f ⋆B g) ⋆B h) ⋅B B.inv aB[f, g, h])" proof - have "Arr (MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<ran Arr (MkArr (\<langle>f ⋆B g\<rangle> \<star> \<langle>h\<rangle>) (\<langle>f ⋆B g\<ran Arr (MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<rangle>) (((f ⋆B g) ⋆B h) ⋅B B.inv aB[f, g, h])) ∧ Arr (MkArr (\<langle>f ⋆B g\<rangle> \<star> \<langle>h\<rangle>) \<langle>(f ⋆B g) ⋆B Arr (MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<rangle>) (((f ⋆B g) ⋆B h) ⋅B ((f ⋆B g) ⋆B h) ⋅B B.inv aB[f, g, h])) ∧ Arr (MkArr \<langle>(f ⋆B g) ⋆B h\<rangle> \<langle>f ⋆B g ⋆B h\<rangle> aB[f, g, h] using f g h fg gh B.α.preserves_hom B.HoHV_def B.HoVH_def by auto thus ?thesis using f g h fg gh comp_def B.comp_arr_dom B.comp_cod_arr by simp qed also have "... = MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle> using B.comp_cod_arr B.comp_arr_inv' by (auto simp add: f fg g gh h) finally show ?thesis by simp qed also have "... = cmpUP (f, g ⋆B h) ⋅ (UP f ⋆ cmpUP (g, h)) ⋅ a (UP f) (UP g) (UP h proof - have "cmpUP (f, g ⋆B h) ⋅ (UP f ⋆ cmpUP (g, h)) ⋅ a (UP f) (UP g) (UP h) = cmpUP (f, g ⋆B h) ⋅ (MkIde \<langle>f\<rangle> ⋆ cmpUP (g, h)) ⋅ (MkIde \<langle>f\<rangle> ⋆ MkIde \<langle>g\<rangle> ⋆ MkIde \<langle>h\<rangle>)" using f g h fg gh VVV.arr_charSbC VV.arr_charSbC arr_char src_def trg_def UP_def a_def by auto also have "... = MkArr (\<langle>f\<rangle> \<star> \<langle>g ⋆B h\<rangle>) \<langle>f MkArr (\<langle>f\<rangle> \<star> \<langle>g ⋆B h\<rangle>) (\<langle>f\<rangle> \<star MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<rangle>) (\<la MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<rangle>) (\<la proof - have "cmpUP (f, g ⋆B h) = MkArr (\<langle>f\<rangle> \<star> \<langle>g ⋆B h\<rangle>) MkArr (\<langle>f\<rangle> \<star> \<langle>g ⋆B h\<rangle>) (\<langle>f\<rangle> \<star using f g h fg gh Φ.map_simp_ide Φ.map_def UP.FF_def UP_def hcomp_def B.VV.arr_charSbC B.can_Ide_self B.comp_arr_dom B.comp_cod_arr src_def trg_def arr_char B.VV.cod_simp by auto moreover have "cmpUP (g, h) = MkArr (\<langle>g\<rangle> \<star> \<langle>h\<rangle>) \<langle>g using g h gh cmpUP_ide_simp by blast moreover have "MkIde \<langle>f\<rangle> ⋆ MkArr (\<langle>g\<rangle> \<star> \<langle>h MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<rangle>) (\<la using f g h fg gh hcomp_def arr_char src_def trg_def B.can_Ide_self B.comp_arr_dom B.comp_cod_arr by auto moreover have "MkIde \<langle>f\<rangle> ⋆ MkIde \<langle>g\<rangle> ⋆ MkIde \<langle>h\<rangle> MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<rangle>) (\<la proof - have "«f : f ==>B f¬ ∧ «g : g ==>B g¬ ∧ «h : h ==>B h¬" using f g h by auto thus ?thesis using f g h fg gh hcomp_def arr_char src_def trg_def B.can_Ide_self B.comp_arr_dom B.comp_cod_arr by auto qed ultimately show ?thesis using comp_assoc by auto qed also have "... = MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle> proof - have "Arr (MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<ran Arr (MkArr (\<langle>f\<rangle> \<star> \<langle>g\<rangle> \<star> \<langle>h\<rangle>) Arr (MkArr (\<langle>f\<rangle> \<star> \<langle>g ⋆B h\<rangle>) (\<langle>f\<rangle> Arr (MkArr (\<langle>f\<rangle> \<star> \<langle>g ⋆B h\<rangle>) \<langle>f ⋆B g ⋆B h using f g h fg gh by auto thus ?thesis using f g h fg gh comp_def by auto qed finally show ?thesis by simp qed finally show ?thesis by blast qed qed lemma UP_is_pseudofunctor: shows "pseudofunctor VB HB aB iB srcB trgB vcomp hcomp a i src trg UP cmpUP" .. lemma UP_map0_obj [simp]: assumes "B.obj a" shows "UP.map0 a = UP0 a" using assms UP.map0_def by auto interpretation UP: full_functor VB vcomp UP proof fix μ f g assume f: "B.ide f" and g: "B.ide g" assume μ: "«μ : UP f ==> UP g¬" show "∃ν. «ν : f ==>B g¬ ∧ UP ν = μ" proof - have 1: "«Map μ : f ==>B g¬" using f g μ UP_def arr_char in_hom_char by auto moreover have "UP (Map μ) = μ" proof - have "μ = MkArr (Dom μ) (Cod μ) (Map μ)" using μ MkArr_Map by auto also have "... = UP (Map μ)" using "1" B.arrI UP.as_nat_trans.preserves_hom UP_def μ in_hom_char by force finally show ?thesis by auto qed ultimately show ?thesis by blast qed qed interpretation UP: faithful_functor VB vcomp UP using arr_char UP_def by (unfold_locales, simp_all) interpretation UP: fully_faithful_functor VB vcomp UP .. lemma UP_is_fully_faithful_functor: shows "fully_faithful_functor VB vcomp UP" .. no_notation B.in_hom (‹«_ : _ →B _¬›) (* Inherited from functor, I think. *) lemma Map_reflects_hhom: assumes "B.obj a" and "B.obj b" and "ide g" and "«g : UP.map0 a → UP.map0 b¬" shows "«Map g : a →B b¬" proof have 1: "B.ide (Map g)" using assms ide_char by blast show "B.arr (Map g)" using 1 by simp show "srcB (Map g) = a" proof - have "srcB (Map g) = Map (src g)" using assms src_def apply simp by (metis (no_types, lifting) E.eval_simps(2) E.Ide_implies_Arr arr_char ideE) also have "... = Map (UP.map0 a)" using assms by (metis (no_types, lifting) in_hhomE) also have "... = a" using assms UP.map0_def UP_def [of a] src_def by auto finally show ?thesis by simp qed show "trgB (Map g) = b" proof - have "trgB (Map g) = Map (trg g)" using assms trg_def apply simp by (metis (no_types, lifting) E.eval_simps(3) E.Ide_implies_Arr arr_char ideE) also have "... = Map (UP.map0 b)" using assms by (metis (no_types, lifting) in_hhomE) also have "... = b" using assms UP.map0_def UP_def [of b] src_def by auto finally show ?thesis by simp qed qed lemma eval_Dom_ide [simp]: assumes "ide g" shows "{Dom g} = Map g" using assms dom_char ideD by auto lemma Cod_ide: assumes "ide f" shows "Cod f = Dom f" using assms dom_char by auto lemma Map_preserves_objects: assumes "obj a" shows "B.obj (Map a)" proof - have "srcB (Map a) = Map (src a)" using assms src_def apply simp using E.eval_simps(2) E.Ide_implies_Arr arr_char ideE by (metis (no_types, lifting) objE) also have 1: "... = {E.Src (Dom a)}" using assms src_def by auto also have "... = {\<langle>Map a\<rangle>0}" using assms B.src.extensionality 1 obj_simps(2) by force also have "... = Map a" using assms by auto finally have "srcB (Map a) = Map a" by simp moreover have "B.arr (Map a)" using assms B.ideD arr_char by auto ultimately show ?thesis using B.obj_def by simp qed interpretation UP: equivalence_pseudofunctor VB HB aB iB srcB trgB vcomp hcomp a i src trg UP cmpUP proof (* UP is full, hence locally full. *) show "∧f f' ν. [ B.ide f; B.ide f'; srcB f = srcB f'; trgB f = trgB f'; «ν : UP f ==> UP f'¬ ] ==> ∃μ. «μ : f ==>B f'¬ ∧ UP μ = ν" using UP.is_full by simp (* UP is biessentially surjective on objects. *) show "∧b. obj b ==> ∃a. B.obj a ∧ equivalent_objects (UP.map0 a) b" proof - fix b assume b: "obj b" have 1: "B.obj (Map b)" using b Map_preserves_objects by simp have 3: "UP.map0 (Map b) = MkArr \<langle>Map b\<rangle>0 \<langle>Map b\<rangle>0 (Ma using b 1 UP.map0_def [of "Map b"] UP_def src_def arr_char by auto have 4: "b = MkArr (Dom b) (Dom b) (Map b)" using b objE eval_Dom_ide by (metis (no_types, lifting) dom_char ideD(2) obj_def) let ?φ = "MkArr \<langle>Map b\<rangle>0 (Dom b) (Map b)" have φ: "arr ?φ" proof - have 2: "E.Obj (Dom b)" using b obj_char by blast have "E.Nml \<langle>Map b\<rangle>0 ∧ E.Ide \<langle>Map b\<rangle>0" using 1 by auto moreover have "E.Nml (Dom b) ∧ E.Ide (Dom b)" using b arr_char [of b] by auto moreover have "E.Src \<langle>Map b\<rangle>0 = E.Src (Dom b)" using b 1 2 apply (cases "Dom b") apply simp_all by fastforce moreover have "E.Trg \<langle>Map b\<rangle>0 = E.Trg (Dom b)" using b 1 2 apply (cases "Dom b") apply simp_all by fastforce moreover have "«Map b : {\<langle>Map b\<rangle>0} ==>B {Dom b}¬" using b 1 by (elim objE, auto) ultimately show ?thesis using arr_char ‹E.Nml \⟨Map b\⟩0 ∧ E.Ide \⟨Map b\⟩0› by auto qed hence "iso ?φ" using 1 iso_char by auto moreover have "dom ?φ = UP.map0 (Map b)" using φ dom_char b 1 3 B.objE UP.map0_def UP_def src_def by auto moreover have "cod ?φ = b" using φ cod_char b 4 1 by auto ultimately have "isomorphic (UP.map0 (Map b)) b" using φ 3 4 isomorphic_def by blast moreover have 5: "obj (UP.map0 (Map b))" using 1 UP.map0_simps(2) by simp ultimately have 6: "UP.map0 (Map b) = b" using b isomorphic_objects_are_equal by simp have "equivalent_objects (UP.map0 (Map b)) b" using b 6 equivalent_objects_reflexive [of b] by simp thus "∃a. B.obj a ∧ equivalent_objects (UP.map0 a) b" using 1 6 by auto qed (* UP is locally essentially surjective. *) show "∧a b g. [ B.obj a; B.obj b; «g : UP.map0 a → UP.map0 b¬; ide g ] ==> ∃f. «f : a →B b¬ ∧ B.ide f ∧ isomorphic (UP f) g" proof - fix a b g assume a: "B.obj a" and b: "B.obj b" assume g_in_hhom: "«g : UP.map0 a → UP.map0 b¬" assume ide_g: "ide g" have 1: "B.ide (Map g)" using ide_g ide_char by blast have "arr (UP a)" using a by auto have "arr (UP b)" using b by auto have Map_g_eq: "Map g = {Dom g}" using ide_g by simp have Map_g_in_hhom: "«Map g : a →B b¬" using a b ide_g g_in_hhom Map_reflects_hhom by simp let ?φ = "MkArr \<langle>Map g\<rangle> (Dom g) (Map g)" have φ: "arr ?φ" proof - have "«Map ?φ : {Dom ?φ} ==>B {Cod ?φ}¬" using 1 Map_g_eq by auto moreover have "E.Ide \<langle>Map g\<rangle> ∧ E.Nml \<langle>Map g\<rangle>" using 1 by simp moreover have "E.Ide (Dom g) ∧ E.Nml (Dom g)" using ide_g arr_char ide_char by blast moreover have "E.Src \<langle>Map g\<rangle> = E.Src (Dom g)" using ide_g g_in_hhom src_def Map_g_in_hhom by (metis (no_types, lifting) B.ideD(2) B.in_hhom_def B.objE B.obj_def' Dom.simps(1) E.Src.simps(2) UP.map0_def ‹arr (UP a)› a in_hhomE UP_def) moreover have "E.Trg \<langle>Map g\<rangle> = E.Trg (Dom g)" proof - have "E.Trg \<langle>Map g\<rangle> = \<langle>b\<rangle>0" using Map_g_in_hhom by auto also have "... = E.Trg (Dom g)" proof - have "E.Trg (Dom g) = Dom (trg g)" using ide_g trg_def by simp also have "... = Dom (UP.map0 b)" using g_in_hhom by auto also have "... = \<langle>b\<rangle>0" using b ‹arr (UP b)› UP.map0_def src_def UP_def B.objE by auto finally show ?thesis by simp qed finally show ?thesis by simp qed ultimately show ?thesis using arr_char by simp qed have "«?φ : UP (Map g) ==> g¬" by (simp add: "1" φ ide_g in_hom_char) moreover have "iso ?φ" using φ 1 iso_char by simp ultimately have "isomorphic (UP (Map g)) g" using isomorphic_def by auto thus "∃f. «f : a →B b¬ ∧ B.ide f ∧ isomorphic (UP f) g" using 1 Map_g_in_hhom by auto qed qed theorem UP_is_equivalence_pseudofunctor: shows "equivalence_pseudofunctor VB HB aB iB srcB trgB vcomp hcomp a i src trg UP cmpUP" .. text ‹ Next, we work out the details of the equivalence pseudofunctor ‹DN› in the converse direction. › definition DN where "DN μ ≡ if arr μ then Map μ else B.null" lemma DN_in_hom [intro]: assumes "arr μ" shows "«DN μ : DN (src μ) →B DN (trg μ)¬" and "«DN μ : DN (dom μ) ==>B DN (cod μ)¬" using assms DN_def arr_char [of μ] B.vconn_implies_hpar(1-2) E.eval_in_hom(1) B.in_hhom_def by auto lemma DN_simps [simp]: assumes "arr μ" shows "B.arr (DN μ)" and "srcB (DN μ) = DN (src μ)" and "trgB (DN μ) = DN (trg μ)" and "B.dom (DN μ) = DN (dom μ)" and "B.cod (DN μ) = DN (cod μ)" using assms DN_in_hom by auto interpretation "functor" vcomp VB DN using DN_def seqE Map_comp seq_char by unfold_locales auto interpretation DN: weak_arrow_of_homs vcomp src trg VB srcB trgB DN proof fix μ assume μ: "arr μ" show "B.isomorphic (DN (src μ)) (srcB (DN μ))" proof - have "DN (src μ) = srcB (DN μ)" using B.src.extensionality DN_def DN_simps(2) by auto moreover have "B.ide (DN (src μ))" using μ by simp ultimately show ?thesis using μ B.isomorphic_reflexive by auto qed show "B.isomorphic (DN (trg μ)) (trgB (DN μ))" proof - have "DN (trg μ) = trgB (DN μ)" using ‹B.isomorphic (DN (src μ)) (srcB (DN μ))› by fastforce moreover have "B.ide (DN (trg μ))" using μ by simp ultimately show ?thesis using B.isomorphic_reflexive by auto qed qed interpretation "functor" VV.comp B.VV.comp DN.FF using DN.functor_FF by auto interpretation HoDN_DN: composite_functor VV.comp B.VV.comp VB DN.FF ‹λμν. HB (fst μν) (snd μν)› .. interpretation DNoH: composite_functor VV.comp vcomp VB ‹λμν. fst μν ⋆ snd μν› DN .. abbreviation Ψo where "Ψo fg ≡ B.can (Dom (fst fg) \<lfloor>\<star>\<rfloor> Dom (snd fg)) (Dom (fst abbreviation Ψo' where "Ψo' fg ≡ B.can (Dom (fst fg) \<star> Dom (snd fg)) (Dom (fst fg) \<lfloor>\<st lemma Ψo_in_hom: assumes "VV.ide fg" shows "«Ψo fg : Map (fst fg) ⋆B Map (snd fg) ==>B {Dom (fst fg) \<lfloor>\<star>\<rflo and "«Ψo' fg : {Dom (fst fg) \<lfloor>\<star>\<rfloor> Dom (snd fg)} ==>B Map (fst fg) and "B.inverse_arrows (Ψo fg) (Ψo' fg)" proof - have 1: "E.Ide (Dom (fst fg) \<star> Dom (snd fg))" unfolding E.Ide.simps(3) apply (intro conjI) using assms VV.ide_char VV.arr_charSbC arr_char apply simp using VV.arr_charSbC VV.ideD(1) assms apply blast by (metis (no_types, lifting) VV.arrE VV.ideD(1) assms src_simps(1) trg_simps(1)) have 2: "E.Ide (Dom (fst fg) \<lfloor>\<star>\<rfloor> Dom (snd fg))" using 1 by (meson E.Ide.simps(3) E.Ide_HcompNml VV.arr_charSbC VV.ideD(1) arr_char assms) have 3: "\<lfloor>Dom (fst fg) \<star> Dom (snd fg)\<rfloor> = \<lfloor>Dom (fst fg) \< by (metis (no_types, lifting) E.Ide.simps(3) E.Nml_HcompNml(1) E.Nmlize.simps(3) E.Nmlize_Nml VV.arr_charSbC VV.ideD(1) arr_char assms 1) have 4: "{Dom (fst fg) \<star> Dom (snd fg)} = Map (fst fg) ⋆B Map (snd fg)" using assms VV.ide_charSbC VV.arr_charSbC arr_char by simp show "«Ψo fg : Map (fst fg) ⋆B Map (snd fg) ==>B {Dom (fst fg) \<lfloor>\<star>\<rfloo using 1 2 3 4 by auto show "«Ψo' fg : {Dom (fst fg) \<lfloor>\<star>\<rfloor> Dom (snd fg)} ==>B Map (fst fg using 1 2 3 4 by auto show "B.inverse_arrows (Ψo fg) (Ψo' fg)" using 1 2 3 B.inverse_arrows_can by blast qed interpretation Ψ: transformation_by_components VV.comp VB HoDN_DN.map DNoH.map Ψo proof fix fg assume fg: "VV.ide fg" have 1: "{Dom (fst fg) \<star> Dom (snd fg)} = Map (fst fg) ⋆B Map (snd fg)" using fg VV.ide_charSbC VV.arr_charSbC arr_char by simp show "«Ψo fg : HoDN_DN.map fg ==>B DNoH.map fg¬" proof show "B.arr (Ψo fg)" using fg Ψo_in_hom by blast show "B.dom (Ψo fg) = HoDN_DN.map fg" proof - have "B.dom (Ψo fg) = Map (fst fg) ⋆B Map (snd fg)" using fg Ψo_in_hom by blast also have "... = HoDN_DN.map fg" using fg DN.FF_def DN_def VV.arr_charSbC src_def trg_def VV.ide_charSbC by auto finally show ?thesis by simp qed show "B.cod (Ψo fg) = DNoH.map fg" proof - have "B.cod (Ψo fg) = {Dom (fst fg) \<lfloor>\<star>\<rfloor> Dom (snd fg)}" using fg Ψo_in_hom by blast also have "... = DNoH.map fg" proof - have "DNoH.map fg = B.can (Cod (fst fg) \<lfloor>\<star>\<rfloor> Cod (snd fg)) (Cod (fst fg) \<star> Co (Map (fst fg) ⋆B Map (snd fg)) ⋅B B.can (Dom (fst fg) \<star> Dom (snd fg)) (Dom (fst fg) \<lfloor>\<star>\<rfloor> Do using fg DN_def Map_hcomp VV.arr_charSbC apply simp using VV.ideD(1) by blast also have "... = B.can (Cod (fst fg) \<lfloor>\<star>\<rfloor> Cod (snd fg)) (Cod (fst fg) \<star> Co B.can (Dom (fst fg) \<star> Dom (snd fg)) (Dom (fst fg) \<lfloor>\<star>\<rfloor> Do proof - have "(Map (fst fg) ⋆B Map (snd fg)) ⋅B B.can (Dom (fst fg) \<star> Dom (snd fg)) (Dom (fst fg) \<lfloor>\<star>\<rfloor> Do B.can (Dom (fst fg) \<star> Dom (snd fg)) (Dom (fst fg) \<lfloor>\<star>\<rfloor> Do using fg 1 Ψo_in_hom B.comp_cod_arr by blast thus ?thesis by simp qed also have "... = {Dom (fst fg) \<lfloor>\<star>\<rfloor> Dom (snd fg)}" proof - have "B.can (Cod (fst fg) \<lfloor>\<star>\<rfloor> Cod (snd fg)) (Cod (fst fg) \<sta using fg VV.ide_charSbC Cod_ide by simp thus ?thesis using fg 1 Ψo_in_hom [of fg] B.comp_arr_inv' by fastforce qed finally show ?thesis by simp qed finally show ?thesis by blast qed qed next show "∧f. VV.arr f ==> Ψo (VV.cod f) ⋅B HoDN_DN.map f = DNoH.map f ⋅B Ψo (VV.dom f)" proof - fix μν assume μν: "VV.arr μν" show "Ψo (VV.cod μν) ⋅B HoDN_DN.map μν = DNoH.map μν ⋅B Ψo (VV.dom μν)" proof - have 1: "E.Ide (Dom (fst μν) \<star> Dom (snd μν))" unfolding E.Ide.simps(3) by (metis (no_types, lifting) VV.arrE μν arrE src_simps(2) trg_simps(2)) have 2: "E.Ide (Dom (fst μν) \<lfloor>\<star>\<rfloor> Dom (snd μν))" using 1 by (meson E.Ide.simps(3) E.Ide_HcompNml VV.arr_charSbC VV.ideD(1) arr_char μν) have 3: "\<lfloor>Dom (fst μν) \<star> Dom (snd μν)\<rfloor> = \<lfloor>Dom (fst μν) \<lfloor by (metis (no_types, lifting) E.Ide.simps(3) E.Nml_HcompNml(1) E.Nmlize.simps(3) E.Nmlize_Nml VV.arr_charSbC arr_char μν 1) have 4: "E.Ide (Cod (fst μν) \<star> Cod (snd μν))" unfolding E.Ide.simps(3) by (metis (no_types, lifting) "1" E.Ide.simps(3) VV.arrE μν arr_char) have 5: "E.Ide (Cod (fst μν) \<lfloor>\<star>\<rfloor> Cod (snd μν))" using 4 by (meson E.Ide.simps(3) E.Ide_HcompNml VV.arr_charSbC VV.ideD(1) arr_char μν) have 6: "\<lfloor>Cod (fst μν) \<star> Cod (snd μν)\<rfloor> = \<lfloor>Cod (fst μν) \<lfloor by (metis (no_types, lifting) E.Ide.simps(3) E.Nml_HcompNml(1) E.Nmlize.simps(3) E.Nmlize_Nml VV.arr_charSbC arr_char μν 1) have A: "«Ψo' μν : {Dom (fst μν) \<lfloor>\<star>\<rfloor> Dom (snd μν)} ==>B {Dom (fst μν) \<star> Dom (snd μν)}¬" using 1 2 3 by auto have B: "«Map (fst μν) ⋆B Map (snd μν) : {Dom (fst μν) \<star> Dom (snd μν)} ==>B {Cod (fst μν) \<star> Cod (snd μν)}¬" using μν VV.arr_charSbC arr_char src_def trg_def E.Nml_implies_Arr E.eval_simps'(2-3) by auto have C: "«B.can (Cod (fst μν) \<lfloor>\<star>\<rfloor> Cod (snd μν)) (Cod (fst μν) \<star> C {Cod (fst μν) \<star> Cod (snd μν)} ==>B {Cod (fst μν) \<lfloor>\<star>\<rfloor> Cod (snd μν using 4 5 6 by auto have "Ψo (VV.cod μν) ⋅B HoDN_DN.map μν = B.can (Cod (fst μν) \<lfloor>\<star>\<rfloor> Cod (snd μν)) (Cod (fst μν) \<star> Cod (snd (Map (fst μν) ⋆B Map (snd μν))" using μν VV.arr_charSbC VV.cod_charSbC arr_char src_def trg_def cod_char DN.FF_def DN_def by auto also have "... = B.can (Cod (fst μν) \<lfloor>\<star>\<rfloor> Cod (snd μν)) (Cod (fst μν) \<star> Cod (snd μν)) ⋅B (Map (fst μν) ⋆B Map (snd μν)) ⋅B Ψo' μν ⋅B Ψo μν" using B μν VV.arr_charSbC arr_char src_def trg_def E.Ide_HcompNml E.Nml_HcompNml(1) B.can_Ide_self B.comp_arr_dom by auto also have "... = DNoH.map μν ⋅B Ψo (VV.dom μν)" proof - have "DNoH.map μν ⋅B Ψo (VV.dom μν) = B.can (Cod (fst μν) \<lfloor>\<star>\<rfloor> Cod (snd μν)) (Cod (fst μν) \<star> Cod (snd (Map (fst μν) ⋆B Map (snd μν)) ⋅B Ψo' μν ⋅B Ψo (VV.dom μν)" using μν DN_def VV.arr_charSbC B.comp_assoc by simp moreover have "Ψo (VV.dom μν) = Ψo μν" using μν VV.dom_charSbC VV.arr_charSbC by auto ultimately show ?thesis using B.comp_assoc by simp qed finally show ?thesis by blast qed qed qed abbreviation cmpDN where "cmpDN ≡ Ψ.map" interpretation Ψ: natural_isomorphism VV.comp VB HoDN_DN.map DNoH.map cmpDN using Ψo_in_hom B.iso_def Ψ.map_simp_ide apply unfold_locales apply auto by blast no_notation B.in_hom (‹«_ : _ →B _¬›) lemma cmpDN_in_hom [intro]: assumes "arr (fst μν)" and "arr (snd μν)" and "src (fst μν) = trg (snd μν)" shows "«cmpDN μν : DN (src (snd μν)) →B DN (trg (fst μν))¬" and "«cmpDN μν : DN (dom (fst μν)) ⋆B DN (dom (snd μν)) ==>B DN (cod (fst μν) ⋆ cod (snd μν))¬" proof - have 1: "VV.arr μν" using assms VV.arr_charSbC by simp show 2: "«cmpDN μν : DN (dom (fst μν)) ⋆B DN (dom (snd μν)) ==>B DN (cod (fst μν) ⋆ cod (snd μν))¬" proof - have "HoDN_DN.map (VV.dom μν) = DN (dom (fst μν)) ⋆B DN (dom (snd μν))" using assms 1 DN.FF_def VV.dom_simp by auto moreover have "DNoH.map (VV.cod μν) = DN (cod (fst μν) ⋆ cod (snd μν))" using assms 1 VV.cod_simp by simp ultimately show ?thesis using assms 1 Ψ.preserves_hom by auto qed show "«cmpDN μν : DN (src (snd μν)) →B DN (trg (fst μν))¬" using assms 2 B.src_dom [of "cmpDN μν"] B.trg_dom [of "cmpDN μν"] by (elim B.in_homE, intro B.in_hhomI) auto qed lemma cmpDN_simps [simp]: assumes "arr (fst μν)" and "arr (snd μν)" and "src (fst μν) = trg (snd μν)" shows "B.arr (cmpDN μν)" and "srcB (cmpDN μν) = DN (src (snd μν))" and "trgB (cmpDN μν) = DN (trg (fst μν))" and "B.dom (cmpDN μν) = DN (dom (fst μν)) ⋆B DN (dom (snd μν))" and "B.cod (cmpDN μν) = DN (cod (fst μν) ⋆ cod (snd μν))" proof show "VV.arr μν" using assms by blast have 1: "«cmpDN μν : DN (src (snd μν)) →B DN (trg (fst μν))¬" using assms by blast show "srcB (cmpDN μν) = DN (src (snd μν))" using 1 by fast show "trgB (cmpDN μν) = DN (trg (fst μν))" using 1 by fast have 2: "«cmpDN μν : DN (dom (fst μν)) ⋆B DN (dom (snd μν)) ==>B DN (cod (fst μν) ⋆ cod (snd μν))¬" using assms by blast show "B.dom (cmpDN μν) = DN (dom (fst μν)) ⋆B DN (dom (snd μν))" using 2 by fast show "B.cod (cmpDN μν) = DN (cod (fst μν) ⋆ cod (snd μν))" using 2 by fast qed interpretation DN: pseudofunctor vcomp hcomp a i src trg VB HB aB iB srcB trgB DN cmpDN proof show "∧f g h. [ ide f; ide g; ide h; src f = trg g; src g = trg h ] ==> DN (a f g h) ⋅B cmpDN (f ⋆ g, h) ⋅B (cmpDN (f, g) ⋆B DN h) = cmpDN (f, g ⋆ h) ⋅B (DN f ⋆B cmpDN (g, h)) ⋅B aB[DN f, DN g, DN h]" proof - fix f g h assume f: "ide f" and g: "ide g" and h: "ide h" and fg: "src f = trg g" and gh: "src g = trg h" show "DN (a f g h) ⋅B cmpDN (f ⋆ g, h) ⋅B (cmpDN (f, g) ⋆B DN h) = cmpDN (f, g ⋆ h) ⋅B (DN f ⋆B cmpDN (g, h)) ⋅B aB[DN f, DN g, DN h]" proof - have 1: "E.Trg (Dom g) = E.Trg (Dom g \<lfloor>\<star>\<rfloor> Dom h) ∧ {E.Trg (Dom g)} = {E.Trg (Dom g \<lfloor>\<star>\<rfloor> Dom h)}" using f g h fg gh arr_char src_def trg_def E.Trg_HcompNml by (metis (no_types, lifting) ideD(1) src_simps(2) trg_simps(2)) have 2: "arr (MkArr (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom (B.can (Cod f \<lfloor>\<star>\<rfloor> Cod g \<lfloor>\<star>\<rfloor> Cod h) (Cod f (Map f ⋆B B.can (Cod g \<lfloor>\<star>\<rfloor> Cod h) (Cod g \<star> Cod h) ⋅B (Map g ⋆B Map h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom B.can (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \<lfloor>\<star>\<rf proof - have "«B.can (Cod f \<lfloor>\<star>\<rfloor> Cod g \<lfloor>\<star>\<rfloor> Cod h) (Co (Map f ⋆B B.can (Cod g \<lfloor>\<star>\<rfloor> Cod h) (Cod g \<star> Cod h) ⋅B (Map g ⋆B Map h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom B.can (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \<lfloor>\<star>\<rf EVAL (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ==>B EVAL (Cod f \<lfloor>\<star>\<rfloor> Cod g \<lfloor>\<star>\<rfloor> Cod h)¬" proof (intro B.comp_in_homI) show 2: "«B.can (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \<lfloor>\<s EVAL (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ==>B EVAL (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h)¬" using f g h fg gh 1 apply (intro B.can_in_hom) apply (metis (no_types, lifting) E.Ide_HcompNml E.Nml_HcompNml(1) arr_char ideD(1) src_simps(1) trg_simps(1)) apply (metis (no_types, lifting) E.Ide.simps(3) E.Ide_HcompNml ideD(1) arr_char src_simps(1) trg_simps(1)) by (metis (no_types, lifting) E.Nml_HcompNml(1) E.Nmlize.simps(3) E.Nmlize_Nml ideD(1) arr_char src_simps(1) trg_simps(1)) show "«B.can (Cod f \<lfloor>\<star>\<rfloor> Cod g \<lfloor>\<star>\<rfloor> Cod h) (Co EVAL (Cod f \<star> Cod g \<lfloor>\<star>\<rfloor> Cod h) ==>B EVAL (Cod f \<lfloor>\<star>\<rfloor> Cod g \<lfloor>\<star>\<rfloor> Cod h)¬" proof - have "E.Ide (Cod f \<star> Cod g \<lfloor>\<star>\<rfloor> Cod h)" using f g h fg gh 1 Cod_ide E.Ide_HcompNml arr_char apply simp by (metis (no_types, lifting) ideD(1) src_simps(1) trg_simps(1)) moreover have "E.Ide (Cod f \<lfloor>\<star>\<rfloor> Cod g \<lfloor>\<star>\<rfloor> Co using f g h fg gh by (metis (no_types, lifting) E.Ide.simps(3) E.Ide_HcompNml E.Nml_HcompNml(1) arr_char calculation ideD(1) src_simps(1) trg_simps(1)) moreover have "E.Nmlize (Cod f \<star> Cod g \<lfloor>\<star>\<rfloor> Cod h) = E.Nmlize (Cod f \<lfloor>\<star>\<rfloor> Cod g \<lfloor>\<star>\<rfloor> Cod h)" using f g h fg gh by (metis (no_types, lifting) E.Ide.simps(3) E.Nml_HcompNml(1) E.Nmlize.simps(3) E.Nmlize_Nml arr_char calculation(1) ideD(1) src_simps(1) trg_simps(1)) ultimately show ?thesis using B.can_in_hom [of "Cod f \<star> Cod g \<lfloor>\<star>\<rfloor> Cod h" "Cod f \<lfl by blast qed show "«Map f ⋆B B.can (Cod g \<lfloor>\<star>\<rfloor> Cod h) (Cod g \<star> Cod h) ⋅B (Map g ⋆B Map h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom EVAL (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) ==>B EVAL (Cod f \<star> C using f g h fg gh B.can_in_hom apply simp proof (intro B.hcomp_in_vhom B.comp_in_homI) show 1: "«B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom h) : EVAL (Dom g \<lfloor>\<star>\<rfloor> Dom h) ==>B EVAL (Dom g \<star> Dom h)¬" using g h gh B.can_in_hom by (metis (no_types, lifting) E.Ide.simps(3) E.Ide_HcompNml E.Nml_HcompNml(1) E.Nmlize.simps(3) E.Nmlize_Nml arr_char ideD(1) src_simps(1) trg_simps(1)) show "«B.can (Cod g \<lfloor>\<star>\<rfloor> Cod h) (Cod g \<star> Cod h) : EVAL (Cod g \<star> Cod h) ==>B EVAL (Cod g \<lfloor>\<star>\<rfloor> Cod h)¬" using g h gh B.can_in_hom by (metis (no_types, lifting) Cod_ide E.Ide.simps(3) E.Ide_HcompNml E.Nml_HcompNml(1) E.Nmlize.simps(3) E.Nmlize_Nml arr_char ideD(1) src_simps(2) trg_simps(2)) show "«Map g ⋆B Map h : EVAL (Dom g \<star> Dom h) ==>B EVAL (Cod g \<star> Cod h)¬" proof show 2: "B.hseq (Map g) (Map h)" using g h gh by (metis (no_types, lifting) B.null_is_zero(1-2) B.hseq_char' B.ideD(1) Map_hcomp ideE ide_hcomp) show "B.dom (Map g ⋆B Map h) = EVAL (Dom g \<star> Dom h)" using g h gh 2 by fastforce show "B.cod (Map g ⋆B Map h) = EVAL (Cod g \<star> Cod h)" using g h gh 2 by fastforce qed show "«Map f : Map f ==>B EVAL (Cod f)¬" using f arr_char Cod_ide by auto show "srcB (Map f) = trgB {Dom g \<lfloor>\<star>\<rfloor> Dom h}" using f g h fg gh 1 2 src_def trg_def B.arrI B.hseqE B.not_arr_null B.trg.extensionality B.trg.preserves_hom B.vconn_implies_hpar(2) B.vconn_implies_hpar(4) E.eval.simps(3) by (metis (no_types, lifting) Map_ide(1)) qed qed thus ?thesis using f g h fg gh arr_char src_def trg_def E.Nml_HcompNml E.Ide_HcompNml ideD(1) apply (intro arr_MkArr) by auto qed have 3: "E.Ide (Dom g \<lfloor>\<star>\<rfloor> Dom h)" using g h gh ide_char arr_char src_def trg_def E.Ide_HcompNml Cod_ide by (metis (no_types, lifting) ideD(1) src_simps(2) trg_simps(2)) have 4: "E.Ide (Dom g \<star> Dom h)" by (metis (no_types, lifting) E.Ide.simps(3) arrE g gh h ideE src_simps(1) trg_simps(1)) have 5: "E.Nmlize (Dom g \<lfloor>\<star>\<rfloor> Dom h) = E.Nmlize (Dom g \<star> Do using g h gh ide_char arr_char src_def trg_def E.Nml_HcompNml by (metis (no_types, lifting) 4 E.Ide.simps(3) E.Nmlize.simps(3) E.Nmlize_Nml ideD(1)) have 6: "E.Ide (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h)" using f g h fg gh arr_char src_def trg_def by (metis (no_types, lifting) 1 E.Nml_HcompNml(1) E.Ide_HcompNml ideD(1) src_simps(2) trg_simps(2)) have 7: "E.Ide (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h)" using f g h fg gh arr_char src_def trg_def by (metis (no_types, lifting) 1 3 E.Ide.simps(3) ideD(1) src_simps(2) trg_simps(2)) have 8: "E.Nmlize (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h E.Nmlize (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h)" using f g h fg gh arr_char src_def trg_def 7 E.Nml_HcompNml(1) ideD(1) by auto have "DN (a f g h) ⋅B cmpDN (f ⋆ g, h) ⋅B (cmpDN (f, g) ⋆B DN h) = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ((Dom f proof - have 9: "VVV.arr (f, g, h)" using f g h fg gh VVV.arr_charSbC VV.arr_charSbC arr_char ideD by simp have 10: "VV.ide (f, g)" using f g fg VV.ide_charSbC by auto have 11: "VV.ide (hcomp f g, h)" using f g h fg gh VV.ide_charSbC VV.arr_charSbC by simp have 12: "arr (MkArr (Dom g \<lfloor>\<star>\<rfloor> Dom h) (Cod g \<lfloor>\<star>\<rf (B.can (Cod g \<lfloor>\<star>\<rfloor> Cod h) (Cod g \<star> Cod h) ⋅B (Map g ⋆B Map h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom h)))" proof (intro arr_MkArr) show "Dom g \<lfloor>\<star>\<rfloor> Dom h ∈ IDE" using g h gh by (metis (no_types, lifting) 3 E.Nml_HcompNml(1) arr_char ideD(1) mem_Collect_eq src_simps(2) trg_simps(2)) show "Cod g \<lfloor>\<star>\<rfloor> Cod h ∈ IDE" using g h gh Cod_ide ‹Dom g \⌊\⋆\⌋ Dom h ∈ IDE› by auto show "B.can (Cod g \<lfloor>\<star>\<rfloor> Cod h) (Cod g \<star> Cod h) ⋅B (Map g ⋆B Map h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom h) ∈ HOM (Dom g \<lfloor>\<star>\<rfloor> Dom h) (Cod g \<lfloor>\<star>\<rfloor> Cod h)" proof show "E.Src (Dom g \<lfloor>\<star>\<rfloor> Dom h) = E.Src (Cod g \<lfloor>\<star>\<rf E.Trg (Dom g \<lfloor>\<star>\<rfloor> Dom h) = E.Trg (Cod g \<lfloor>\<star>\<rfloor> «B.can (Cod g \<lfloor>\<star>\<rfloor> Cod h) (Cod g \<star> Cod h) ⋅B (Map g ⋆B Map h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom {Dom g \<lfloor>\<star>\<rfloor> Dom h} ==>B {Cod g \<lfloor>\<star>\<rfloor> Cod h}¬" proof (intro conjI) show "E.Src (Dom g \<lfloor>\<star>\<rfloor> Dom h) = E.Src (Cod g \<lfloor>\<star>\<rf using g h gh Cod_ide by simp show "E.Trg (Dom g \<lfloor>\<star>\<rfloor> Dom h) = E.Trg (Cod g \<lfloor>\<star>\<rf using g h gh Cod_ide by simp show "«B.can (Cod g \<lfloor>\<star>\<rfloor> Cod h) (Cod g \<star> Cod h) ⋅B (Map g ⋆B Map h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom {Dom g \<lfloor>\<star>\<rfloor> Dom h} ==>B {Cod g \<lfloor>\<star>\<rfloor> Cod h}¬" proof (intro B.comp_in_homI) show "«B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom h) : {Dom g \<lfloor>\<star>\<rfloor> Dom h} ==>B {Dom g \<star> Dom h}¬" using 3 4 5 by blast show "«Map g ⋆B Map h : {Dom g \<star> Dom h} ==>B {Cod g \<star> Cod h}¬" using g h gh by (metis (no_types, lifting) 4 B.ide_in_hom(2) Cod_ide E.eval.simps(3) E.ide_eval_Ide Map_ide(2)) show "«B.can (Cod g \<lfloor>\<star>\<rfloor> Cod h) (Cod g \<star> Cod h) : {Cod g \<star> Cod h} ==>B {Cod g \<lfloor>\<star>\<rfloor> Cod h}¬" using 3 4 5 Cod_ide g h by auto qed qed qed qed have "DN (a f g h) = {Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> D proof - have "DN (a f g h) = (B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f ((Map f ⋆B B.can (Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom g \<star> Dom h) ⋅B (Map g ⋆B Map h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom B.can (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \<lfloor>\<star>\<rf using f g h fg gh 1 2 9 12 DN_def a_def Cod_ide by simp also have "... = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ( (Map f ⋆B {Dom g \<lfloor>\<star>\<rfloor> Dom h}) ⋅B B.can (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \<lfloor>\<star>\<rf proof - have "«B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom h) : {Dom g \<lfloor>\<star>\<rfloor> Dom h} ==>B Map g ⋆B Map h¬" using g h 3 4 5 B.can_in_hom [of "Dom g \<lfloor>\<star>\<rfloor> Dom h" "Dom g \<star> Dom h by simp hence "Map f ⋆B B.can (Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom g \<star> Dom h) ⋅ (Map g ⋆B Map h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom Map f ⋆B B.can (Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom g \<star> Dom h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom h)" using B.comp_cod_arr by auto also have "... = Map f ⋆B {Dom g \<lfloor>\<star>\<rfloor> Dom h}" using f g h fg gh 3 4 5 B.can_Ide_self by auto finally have "Map f ⋆B B.can (Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom g \<star> Do (Map g ⋆B Map h) ⋅B B.can (Dom g \<star> Dom h) (Dom g \<lfloor>\<star>\<rfloor> Dom Map f ⋆B {Dom g \<lfloor>\<star>\<rfloor> Dom h}" by simp thus ?thesis by simp qed also have "... = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ( B.can (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \<lfloor>\<star>\<rf proof - have "«B.can (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \<lfloor>\<sta {Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h} ==>B Map f ⋆B using f g h 6 7 8 B.can_in_hom [of "Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h" by simp hence "(Map f ⋆B {Dom g \<lfloor>\<star>\<rfloor> Dom h}) ⋅B B.can (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \<lfloor>\<star>\<rf B.can (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \<lfloor>\<star>\<rf using B.comp_cod_arr by auto thus ?thesis by simp qed also have "... = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ( using f g h fg gh 6 7 8 by auto also have "... = {Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h} using f g h fg gh 6 B.can_Ide_self by blast finally show ?thesis by simp qed have "DN (a f g h) ⋅B cmpDN (f ⋆ g, h) ⋅B (cmpDN (f, g) ⋆B DN h) = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ((Dom f B.can ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<lfloor>\<star>\<rfloor> Dom h) ((Dom (B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g) (Dom f \<star> Dom g) ⋆B Map h)" proof - have "DN (a f g h) = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ((Dom f using f g h fg gh DN_def 1 4 6 7 B.can_Ide_self E.HcompNml_assoc E.Ide.simps(3) ‹DN (a f g h) = {Dom f \⌊\⋆\⌋ Dom g \⌊\⋆\⌋ Dom h}› ide_char by (metis (no_types, lifting) arr_char ideD(1)) thus ?thesis using f g h fg gh 10 11 DN_def Ψ.map_simp_ide by simp qed also have "... = (B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) B.can ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<lfloor>\<star>\<rfloor> Dom h) ((Dom (B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g) (Dom f \<star> Dom g) ⋆B Map h)" using B.comp_assoc by simp also have "... = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ( B.can ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<star> Dom h) ((Dom f \<star> Dom g) proof - have "B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g) (Dom f \<star> Dom g) ⋆B Map h = B.can ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<star> Dom h) ((Dom f \<star> Dom g) proof - have "B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g) (Dom f \<star> Dom g) ⋆B Map h = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g) (Dom f \<star> Dom g) ⋆B B.can (Dom h) using h B.can_Ide_self by fastforce also have "... = B.can ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<star> Dom h) ((Dom f using f g h 1 4 7 arr_char E.Nml_HcompNml(1) E.Src_HcompNml B.hcomp_can [of "Dom f \<star> Dom g" "Dom f \<lfloor>\<star>\<rfloor> Dom g" "Dom h" "Do by (metis (no_types, lifting) E.Nmlize.simps(3) E.Nmlize_Nml E.Ide.simps(3) E.Ide_HcompNml E.Src.simps(3) arrE ideD(1)) finally show ?thesis by simp qed moreover have "B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ((Dom f B.can ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<lfloor>\<star>\<rfloor> Dom h) ((Dom B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ((Dom f proof - have "E.Ide ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<star> Dom h)" using f g h 1 4 7 by (metis (no_types, lifting) E.Ide.simps(3) E.Ide_HcompNml E.Src_HcompNml arrE ideD(1)) moreover have "E.Ide ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<lfloor>\<star>\<rfloor> using f g h 1 7 E.Ide_HcompNml E.Nml_HcompNml(1) arr_char calculation ideD(1) by auto moreover have "E.Ide (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Do using f g h 1 4 6 by blast moreover have "E.Nmlize ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<star> Dom h) = E.Nmlize ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<lfloor>\<star>\<rfloor> Dom h)" using f g h 1 4 7 by (metis (no_types, lifting) E.Nml_HcompNml(1) E.Nmlize.simps(3) E.Nmlize_Nml E.Ide.simps(3) arrE calculation(1) ideD(1)) moreover have "E.Nmlize ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<lfloor>\<star>\<rfloo E.Nmlize (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h)" using f g h 1 4 7 E.HcompNml_assoc by fastforce ultimately show ?thesis using B.vcomp_can by simp qed ultimately show ?thesis by simp qed also have "... = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> proof - have "E.Ide ((Dom f \<star> Dom g) \<star> Dom h)" using 1 4 7 by simp moreover have "E.Ide ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<star> Dom h)" using f g 1 4 7 by (metis (no_types, lifting) E.Ide.simps(3) E.Ide_HcompNml E.Src_HcompNml arrE ideD(1)) moreover have "E.Ide (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Do using f g h 6 by blast moreover have "E.Nmlize ((Dom f \<star> Dom g) \<star> Dom h) = E.Nmlize ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<star> Dom h)" using f g h 1 7 E.Nml_HcompNml(1) by fastforce moreover have "E.Nmlize ((Dom f \<lfloor>\<star>\<rfloor> Dom g) \<star> Dom h) = E.Nmlize (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h)" using f g h 1 4 7 by (metis (no_types, lifting) E.Nml_HcompNml(1) E.Nmlize.simps(3) E.Nmlize_Nml E.HcompNml_assoc E.Ide.simps(3) arrE ideD(1)) ultimately show ?thesis using B.vcomp_can by simp qed finally show ?thesis by simp qed also have "... = cmpDN (f, g ⋆ h) ⋅B (DN f ⋆B cmpDN (g, h)) ⋅B aB[DN f, DN g, DN h]" proof - have "cmpDN (f, g ⋆ h) ⋅B (DN f ⋆B cmpDN (g, h)) ⋅B aB[DN f, DN g, DN h] = (cmpDN (f, g ⋆ h) ⋅B (DN f ⋆B cmpDN (g, h))) ⋅B aB[DN f, DN g, DN h]" using B.comp_assoc by simp also have "... = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ( B.can (Dom f \<star> Dom g \<star> Dom h) ((Dom f \<star> Dom g) \<star> Dom h)" proof - have "cmpDN (f, g ⋆ h) ⋅B (DN f ⋆B cmpDN (g, h)) = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \< proof - have "cmpDN (f, g ⋆ h) ⋅B (DN f ⋆B cmpDN (g, h)) = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \< (Map f ⋆B B.can (Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom g \<star> Dom h))" using f g h fg gh VV.ide_charSbC VV.arr_charSbC DN_def by simp also have "... = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ( (B.can (Dom f) (Dom f) ⋆B B.can (Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom g \<sta proof - have "Map f = B.can (Dom f) (Dom f)" using f arr_char B.can_Ide_self [of "Dom f"] Map_ide by (metis (no_types, lifting) ide_char') thus ?thesis by simp qed also have "... = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor> Dom h) ( B.can (Dom f \<star> Dom g \<lfloor>\<star>\<rfloor> Dom h) (Dom f \<star> Dom g \<sta using 1 4 5 7 B.hcomp_can by auto also have "... = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloor using 1 4 5 6 7 8 B.vcomp_can by auto finally show ?thesis by simp qed moreover have "aB[DN f, DN g, DN h] = B.can (Dom f \<star> Dom g \<star> Dom h) ((Dom f \<star> Dom g) \<star> Dom h)" using f g h 1 4 7 DN_def B.canE_associator(1) by auto ultimately show ?thesis by simp qed also have "... = B.can (Dom f \<lfloor>\<star>\<rfloor> Dom g \<lfloor>\<star>\<rfloo using 1 4 5 6 7 8 E.Nmlize_Hcomp_Hcomp B.vcomp_can by simp finally show ?thesis by simp qed finally show ?thesis by blast qed qed qed lemma DN_is_pseudofunctor: shows "pseudofunctor vcomp hcomp a i src trg VB HB aB iB srcB trgB DN cmpDN" .. interpretation faithful_functor vcomp VB DN using arr_char dom_char cod_char DN_def apply unfold_locales by (metis (no_types, lifting) Cod_dom Dom_cod MkArr_Map) no_notation B.in_hom (‹«_ : _ →B _¬›) lemma DN_UP: assumes "B.arr μ" shows "DN (UP μ) = μ" using assms UP_def DN_def arr_UP by auto interpretation DN: equivalence_pseudofunctor vcomp hcomp a i src trg VB HB aB iB srcB trgB DN cmpDN proof (* DN is locally (but not globally) full. *) show "∧f f' ν. [ ide f; ide f'; src f = src f'; trg f = trg f'; «ν : DN f ==>B DN f ==> ∃μ. «μ : f ==> f'¬ ∧ DN μ = ν" proof - fix f f' ν assume f: "ide f" and f': "ide f'" and eq_src: "src f = src f'" and eq_trg: "trg f = trg f'" and ν: "«ν : DN f ==>B DN f'¬" show "∃μ. «μ : f ==> f'¬ ∧ DN μ = ν" proof - let ?μ = "MkArr (Dom f) (Dom f') ν" have μ: "«?μ : f ==> f'¬" proof - have "E.Src (Dom f) = E.Src (Dom f')" using f f' by (metis (no_types, lifting) eq_src ideD(1) src_simps(2)) moreover have "E.Trg (Dom f) = E.Trg (Dom f')" using f f' by (metis (no_types, lifting) eq_trg ideD(1) trg_simps(2)) ultimately show ?thesis using f f' ν DN_def MkArr_Map [of f] MkArr_Map [of f'] by (intro MkArr_in_hom) auto qed moreover have "DN ?μ = ν" using μ DN_def by auto ultimately show ?thesis by blast qed qed (* DN is biessentially surjective on objects. *) show "∧a'. B.obj a' ==> ∃a. obj a ∧ B.equivalent_objects (DN.map0 a) a'" proof - fix a' assume a': "B.obj a'" have "obj (UP.map0 a')" using a' UP.map0_simps(1) by simp moreover have "B.equivalent_objects (DN.map0 (UP.map0 a')) a'" proof - have "arr (MkArr \<langle>a'\<rangle> \<langle>a'\<rangle> a')" using a' UP_def [of a'] UP.preserves_reflects_arr [of a'] by auto moreover have "arr (MkArr \<langle>a'\<rangle>0 \<langle>a'\<rangle>0 a')" using a' arr_char obj_simps by auto ultimately have "DN.map0 (UP.map0 a') = a'" using a' UP.map0_def DN.map0_def DN_def src_def by auto thus ?thesis using a' B.equivalent_objects_reflexive by simp qed ultimately show "∃a. obj a ∧ B.equivalent_objects (DN.map0 a) a'" by blast qed (* DN is locally essentially surjective. *) show "∧a b g. [ obj a; obj b; «g : DN.map0 a →B DN.map0 b¬; B.ide g ] ==> ∃f. «f : a → b¬ ∧ ide f ∧ B.isomorphic (DN f) g" proof - fix a b g assume a: "obj a" and b: "obj b" and g: "«g : DN.map0 a →B DN.map0 b¬" and ide_g: "B.ide g" have "ide (UP g)" using ide_g UP.preserves_ide by simp moreover have "B.isomorphic (DN (UP g)) g" using ide_g DN_UP B.isomorphic_reflexive by simp moreover have "«UP g : a → b¬" proof show "arr (UP g)" using g UP.preserves_reflects_arr by auto show "src (UP g) = a" proof - have "src (UP g) = MkArr \<langle>srcB g\<rangle>0 \<langle>srcB g\<rangle>0 (srcB g using ide_g src_def UP_def UP.preserves_reflects_arr [of g] B.ideD(1) by simp also have "... = a" proof - have "srcB g = srcB (DN.map0 a)" using a g B.in_hhom_def by simp also have "... = Map a" using a Map_preserves_objects DN.map0_def DN_def B.src_src B.obj_simps by auto finally have "srcB g = Map a" by simp hence "MkArr \<langle>srcB g\<rangle>0 \<langle>srcB g\<rangle>0 (srcB g) = MkArr \<l by simp also have "... = a" using a obj_char [of a] MkIde_Dom [of a] apply (cases "Dom a") apply force by simp_all finally show ?thesis by simp qed finally show ?thesis by simp qed show "trg (UP g) = b" proof - have "trg (UP g) = MkArr \<langle>trgB g\<rangle>0 \<langle>trgB g\<rangle>0 (trgB g using ide_g trg_def UP_def UP.preserves_reflects_arr [of g] B.ideD(1) by simp also have "... = b" proof - have "trgB g = trgB (DN.map0 b)" using b g B.in_hhom_def by simp also have "... = Map b" using b Map_preserves_objects DN.map0_def DN_def B.src_src B.obj_simps by auto finally have "trgB g = Map b" by simp hence "MkArr \<langle>trgB g\<rangle>0 \<langle>trgB g\<rangle>0 (trgB g) = MkArr \<l by simp also have "... = b" using b obj_char [of b] MkIde_Dom [of b] apply (cases "Dom b") apply force by simp_all finally show ?thesis by simp qed finally show ?thesis by simp qed qed ultimately show "∃f. «f : a → b¬ ∧ ide f ∧ B.isomorphic (DN f) g" by blast qed qed theorem DN_is_equivalence_pseudofunctor: shows "equivalence_pseudofunctor vcomp hcomp a i src trg VB HB aB iB srcB trgB DN cmpDN" .. text ‹ The following gives an explicit formula for a component of the unit isomorphism the pseudofunctor ‹UP› from a bicategory to its strictification. It is not currently being used -- I originally proved it in order to establish s that I later proved in a more abstract setting -- but it might be useful at some › interpretation UP: equivalence_pseudofunctor VB HB aB iB srcB trgB vcomp hcomp a i src trg UP cmpUP using UP_is_equivalence_pseudofunctor by auto lemma UP_unit_char: assumes "B.obj a" shows "UP.unit a = MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a" proof - have " MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a = UP.unit a" proof (intro UP.unit_eqI) show "B.obj a" using assms by simp have 0: "«a : a ==>B a¬" using assms by auto have 1: "arr (MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a)" apply (unfold arr_char, intro conjI) using assms by auto have 2: "arr (MkArr \<langle>a\<rangle> \<langle>a\<rangle> a)" apply (unfold arr_char, intro conjI) using assms by auto have 3: "arr (MkArr \<langle>a\<rangle>0 \<langle>a\<rangle>0 a)" apply (unfold arr_char, intro conjI) using assms by auto show "«MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a : UP.map0 a ==> UP a¬" using assms 1 2 UP_def UP.map0_def src_def by (intro MkArr_in_hom) auto show "iso (MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a)" using assms 1 iso_char by auto show "MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a ⋅ i (UP.map0 a) = (UP iB[a] ⋅ cmpUP (a, a)) ⋅ (MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a ⋆ MkArr \<langle>a\<rangle> proof - have "MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a ⋅ i (UP.map0 a) = MkArr \<langle>a\<rangle>0 \<la unfolding i_def UP.map0_def UP_def using assms 0 1 2 src_def by auto also have "... = (UP iB[a] ⋅ cmpUP (a, a)) ⋅ (MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a ⋆ MkArr proof - have "(UP iB[a] ⋅ cmpUP (a, a)) ⋅ (MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a ⋆ MkArr \<langle>a\< (MkArr \<langle>a ⋆B a\<rangle> \<langle>a\<rangle> iB[a] ⋅ MkArr (\<langle>a\<rangle> \<star> \<langle>a\< ⋅ (MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a ⋆ MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a)" using assms UP_def cmpUP_ide_simp by auto also have "... = (MkArr \<langle>a ⋆B a\<rangle> \<langle>a\<rangle> iB[a] ⋅ MkArr (\<langle>a\<rangl ⋅ MkArr \<langle>a\<rangle>0 (\<langle>a\<rangle> \<star> \<langle>a\<rangle>) (B.runit' a)" using assms 0 1 2 3 hcomp_def B.comp_cod_arr src_def trg_def B.can_Ide_self B.canE_unitor [of "\<langle>a\<rangle>0"] B.comp_cod_arr by auto also have "... = MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> ((iB[a] ⋅B (a ⋆B a)) ⋅B B.runit' a)" proof - have "MkArr \<langle>a ⋆B a\<rangle> \<langle>a\<rangle> iB[a] ⋅ MkArr (\<langle>a\<rangle> \<star> \<lan MkArr (\<langle>a\<rangle> \<star> \<langle>a\<rangle>) \<langle>a\<rangle> (iB[a] ⋅B (a ⋆B a))" using assms by (intro comp_MkArr arr_MkArr) auto moreover have "MkArr (\<langle>a\<rangle> \<star> \<langle>a\<rangle>) \<langle>a\<rangle> (iB[a] ⋅B ⋅ MkArr \<langle>a\<rangle>0 (\<langle>a\<rangle> \<star> \<langle>a\<rangle>) (B.runit' a) = MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> ((iB[a] ⋅B (a ⋆B a)) ⋅B B.runit' a)" using assms 0 B.comp_arr_dom by (intro comp_MkArr arr_MkArr, auto) ultimately show ?thesis by argo qed also have "... = MkArr \<langle>a\<rangle>0 \<langle>a\<rangle> a" using assms B.comp_arr_dom B.comp_arr_inv' B.iso_unit B.unitor_coincidence(2) by simp finally show ?thesis by argo qed finally show ?thesis by simp qed qed thus ?thesis by simp qed end subsection "Pseudofunctors into a Strict Bicategory" text ‹ In the special case of a pseudofunctor into a strict bicategory, we can obtain explicit formulas for the images of the units and associativities under the pseu which only involve the structure maps of the pseudofunctor, since the units and in the target bicategory are all identities. This is useful in applying stricti › locale pseudofunctor_into_strict_bicategory = pseudofunctor + D: strict_bicategory VD HD aD iD srcD trgD begin lemma image_of_unitor: assumes "C.ide g" shows "F lC[g] = (D.inv (unit (trgC g)) ⋆D F g) ⋅D D.inv (Φ (trgC g, g))" and "F rC[g] = (F g ⋆D D.inv (unit (srcC g))) ⋅D D.inv (Φ (g, srcC g))" and "F (C.lunit' g) = Φ (trgC g, g) ⋅D (unit (trgC g) ⋆D F g)" and "F (C.runit' g) = Φ (g, srcC g) ⋅D (F g ⋆D unit (srcC g))" proof - show A: "F lC[g] = (D.inv (unit (trgC g)) ⋆D F g) ⋅D D.inv (Φ (trgC g, g))" proof - have 1: "«(D.inv (unit (trgC g)) ⋆D F g) ⋅D D.inv (Φ (trgC g, g)) : F (trgC g ⋆C g) ==>D F g¬" proof show "«D.inv (unit (trgC g)) ⋆D F g : F (trgC g) ⋆D F g ==>D F g¬" using assms unit_char by (auto simp add: D.hcomp_obj_arr) show "«D.inv (Φ (trgC g, g)) : F (trgC g ⋆C g) ==>D F (trgC g) ⋆D F g¬" using assms cmp_in_hom(2) D.inv_is_inverse by simp qed have "(D.inv (unit (trgC g)) ⋆D F g) ⋅D D.inv (Φ (trgC g, g)) = F g ⋅D (D.inv (unit (trgC g)) ⋆D F g) ⋅D D.inv (Φ (trgC g, g))" using 1 D.comp_cod_arr by auto also have "... = (F lC[g] ⋅D Φ (trgC g, g) ⋅D (unit (trgC g) ⋆D F g)) ⋅D (D.inv (unit (trgC g)) ⋆D F g) ⋅D D.inv (Φ (trgC g, g))" using assms lunit_coherence [of g] D.strict_lunit by simp also have "... = F lC[g] ⋅D Φ (trgC g, g) ⋅D ((unit (trgC g) ⋆D F g) ⋅D (D.inv (unit (trgC g)) ⋆D F g)) ⋅D D.inv (Φ (trgC g, g))" using D.comp_assoc by simp also have "... = F lC[g]" proof - have "(unit (trgC g) ⋆D F g) ⋅D (D.inv (unit (trgC g)) ⋆D F g) = F (trgC g) ⋆D F g" using assms unit_char D.whisker_right by (metis C.ideD(1) C.obj_trg C.trg.preserves_reflects_arr D.comp_arr_inv' unit_simps(5) preserves_arr preserves_ide) moreover have "Φ (trgC g, g) ⋅D D.inv (Φ (trgC g, g)) = F (trgC g ⋆C g)" using assms D.comp_arr_inv D.inv_is_inverse by simp ultimately show ?thesis using assms D.comp_arr_dom D.comp_cod_arr unit_char by auto qed finally show ?thesis by simp qed show B: "F rC[g] = (F g ⋆D D.inv (unit (srcC g))) ⋅D D.inv (Φ (g, srcC g))" proof - have 1: "«(F g ⋆D D.inv (unit (srcC g))) ⋅D D.inv (Φ (g, srcC g)) : F (g ⋆C srcC g) ==>D F g¬" proof show "«F g ⋆D D.inv (unit (srcC g)) : F g ⋆D F (srcC g) ==>D F g¬" using assms unit_char by (auto simp add: D.hcomp_arr_obj) show "«D.inv (Φ (g, srcC g)) : F (g ⋆C srcC g) ==>D F g ⋆D F (srcC g)¬" using assms cmp_in_hom(2) by simp qed have "(F g ⋆D D.inv (unit (srcC g))) ⋅D D.inv (Φ (g, srcC g)) = F g ⋅D (F g ⋆D D.inv (unit (srcC g))) ⋅D D.inv (Φ (g, srcC g))" using 1 D.comp_cod_arr by auto also have "... = (F rC[g] ⋅D Φ (g, srcC g) ⋅D (F g ⋆D unit (srcC g))) ⋅D (F g ⋆D D.inv (unit (srcC g))) ⋅D D.inv (Φ (g, srcC g))" using assms runit_coherence [of g] D.strict_runit by simp also have "... = F rC[g] ⋅D (Φ (g, srcC g) ⋅D ((F g ⋆D unit (srcC g)) ⋅D (F g ⋆D D.inv (unit (srcC g))))) ⋅D D.inv (Φ (g, srcC g))" using D.comp_assoc by simp also have "... = F rC[g]" proof - have "(F g ⋆D unit (srcC g)) ⋅D (F g ⋆D D.inv (unit (srcC g))) = F g ⋆D F (srcC g)" using assms D.whisker_left unit_char by (metis C.ideD(1) C.obj_src C.src.preserves_ide D.comp_arr_inv' D.ideD(1) unit_simps(5) preserves_ide) moreover have "Φ (g, srcC g) ⋅D D.inv (Φ (g, srcC g)) = F (g ⋆C srcC g)" using assms D.comp_arr_inv D.inv_is_inverse by simp ultimately show ?thesis using assms D.comp_arr_dom D.comp_cod_arr unit_char cmp_in_hom(2) [of g "srcC g"] by auto qed finally show ?thesis by simp qed show "F (C.lunit' g) = Φ (trgC g, g) ⋅D (unit (trgC g) ⋆D F g)" proof - have "F (C.lunit' g) = D.inv (F lC[g])" using assms C.iso_lunit preserves_inv by simp also have "... = D.inv ((D.inv (unit (trgC g)) ⋆D F g) ⋅D D.inv (Φ (trgC g, g)))" using A by simp also have "... = Φ (trgC g, g) ⋅D (unit (trgC g) ⋆D F g)" proof - have "D.iso (D.inv (Φ (trgC g, g))) ∧ D.inv (D.inv (Φ (trgC g, g))) = Φ (trgC g, g)" using assms by simp moreover have "D.iso (D.inv (unit (trgC g)) ⋆D F g) ∧ D.inv (D.inv (unit (trgC g)) ⋆D F g) = unit (trgC g) ⋆D F g" using assms unit_char by simp moreover have "D.seq (D.inv (unit (trgC g)) ⋆D F g) (D.inv (Φ (trgC g, g)))" using assms unit_char by (metis A C.lunit_simps(1) preserves_arr) ultimately show ?thesis using D.inv_comp by simp qed finally show ?thesis by simp qed show "F (C.runit' g) = Φ (g, srcC g) ⋅D (F g ⋆D unit (srcC g))" proof - have "F (C.runit' g) = D.inv (F rC[g])" using assms C.iso_runit preserves_inv by simp also have "... = D.inv ((F g ⋆D D.inv (unit (srcC g))) ⋅D D.inv (Φ (g, srcC g)))" using B by simp also have "... = Φ (g, srcC g) ⋅D (F g ⋆D unit (srcC g))" proof - have "D.iso (D.inv (Φ (g, srcC g))) ∧ D.inv (D.inv (Φ (g, srcC g))) = Φ (g, srcC g)" using assms by simp moreover have "D.iso (F g ⋆D D.inv (unit (srcC g))) ∧ D.inv (F g ⋆D D.inv (unit (srcC g))) = F g ⋆D unit (srcC g)" using assms unit_char by simp moreover have "D.seq (F g ⋆D D.inv (unit (srcC g))) (D.inv (Φ (g, srcC g)))" using assms unit_char by (metis B C.runit_simps(1) preserves_arr) ultimately show ?thesis using D.inv_comp by simp qed finally show ?thesis by simp qed qed lemma image_of_associator: assumes "C.ide f" and "C.ide g" and "C.ide h" and "srcC f = trgC g" and "srcC g = trgC h" shows "F aC[f, g, h] = Φ (f, g ⋆C h) ⋅D (F f ⋆D Φ (g, h)) ⋅D (D.inv (Φ (f, g)) ⋆D F h) ⋅D D.inv (Φ (f ⋆C g, h))" and "F (C.a' f g h) = Φ (f ⋆C g, h) ⋅D (Φ (f, g) ⋆D F h) ⋅D (F f ⋆D D.inv (Φ (g, h))) ⋅D D.inv (Φ (f, g ⋆C h))" proof - show 1: "F aC[f, g, h] = Φ (f, g ⋆C h) ⋅D (F f ⋆D Φ (g, h)) ⋅D (D.inv (Φ (f, g)) ⋆D F h) ⋅D D.inv (Φ (f ⋆C g, h))" proof - have 2: "D.seq (Φ (f, g ⋆C h)) ((F f ⋆D Φ (g, h)) ⋅D aD[F f, F g, F h])" using assms D.assoc_in_hom(2) [of "F f" "F g" "F h"] cmp_simps(1,4) C.VV.cod_simp by (intro D.seqI) auto moreover have 3: "F aC[f, g, h] ⋅D Φ (f ⋆C g, h) ⋅D (Φ (f, g) ⋆D F h) = Φ (f, g ⋆C h) ⋅D (F f ⋆D Φ (g, h)) ⋅D aD[F f, F g, F h]" using assms assoc_coherence [of f g h] by blast moreover have "D.iso (Φ (f ⋆C g, h) ⋅D (Φ (f, g) ⋆D F h))" using assms 2 3 C.VV.arr_charSbC C.VV.dom_charSbC C.VV.cod_charSbC FF_def D.isos by auto ultimately have "F aC[f, g, h] = (Φ (f, g ⋆C h) ⋅D ((F f ⋆D Φ (g, h)) ⋅D aD[F f, F g, F h])) ⋅D D.inv (Φ (f ⋆C g, h) ⋅D (Φ (f, g) ⋆D F h))" using D.invert_side_of_triangle(2) [of "Φ (f, g ⋆C h) ⋅D (F f ⋆D Φ (g, h)) ⋅D aD[F f, F g, F h]" "F aC[f, g, h]" "Φ (f ⋆C g, h) ⋅D (Φ (f, g) ⋆D F h)"] by presburger also have "... = Φ (f, g ⋆C h) ⋅D (F f ⋆D Φ (g, h)) ⋅D (D.inv (Φ (f, g)) ⋆D F h) ⋅D D.inv (Φ (f ⋆C g, h))" proof - have "D.inv (Φ (f ⋆C g, h) ⋅D (Φ (f, g) ⋆D F h)) = (D.inv (Φ (f, g)) ⋆D F h) ⋅D D.inv (Φ (f ⋆C g, h))" proof - have "D.seq (Φ (f ⋆C g, h)) (Φ (f, g) ⋆D F h)" using assms by fastforce thus ?thesis using assms D.inv_comp by simp qed moreover have "(F f ⋆D Φ (g, h)) ⋅D aD[F f, F g, F h] = (F f ⋆D Φ (g, h))" using assms D.comp_arr_dom D.assoc_in_hom [of "F f" "F g" "F h"] cmp_in_hom by (metis "2" "3" D.comp_arr_ide D.hseq_char D.seqE D.strict_assoc cmp_simps(2) cmp_simps(3) preserves_ide) ultimately show ?thesis using D.comp_assoc by simp qed finally show ?thesis by simp qed show "F (C.a' f g h) = Φ (f ⋆C g, h) ⋅D (Φ (f, g) ⋆D F h) ⋅D (F f ⋆D D.inv (Φ (g, h))) ⋅D D.inv (Φ (f, g ⋆C h))" proof - have "F (C.a' f g h) = D.inv (F aC[f, g, h])" using assms preserves_inv by simp also have "... = D.inv (Φ (f, g ⋆C h) ⋅D (F f ⋆D Φ (g, h)) ⋅D (D.inv (Φ (f, g)) ⋆D F h) ⋅D D.inv (Φ (f ⋆C g, h)))" using 1 by simp also have "... = Φ (f ⋆C g, h) ⋅D (Φ (f, g) ⋆D F h) ⋅D (F f ⋆D D.inv (Φ (g, h))) ⋅D D.inv (Φ (f, g ⋆C h))" using assms C.VV.arr_charSbC FF_def D.hcomp_assoc D.comp_assoc C.VV.dom_simp C.VV.cod_simp (* OK, this is pretty cool, but not as cool as if I didn't have to direct it. *) by (simp add: D.inv_comp D.isos_compose) finally show ?thesis by simp qed qed end subsection "Internal Equivalences in a Strict Bicategory" text ‹ In this section we prove a useful fact about internal equivalences in a strict b namely, that if the ``right'' triangle identity holds for such an equivalence th ``left'' does, as well. Later we will dualize this property, and use strictific extend it to arbitrary bicategories. › locale equivalence_in_strict_bicategory = strict_bicategory + equivalence_in_bicategory begin lemma triangle_right_implies_left: shows "(g ⋆ ε) ⋅ (η ⋆ g) = g ==> (ε ⋆ f) ⋅ (f ⋆ η) = f" proof - text ‹ The formal proof here was constructed following the string diagram sketch below, which appears in cite‹"nlab-zigzag-diagram"› (see it also in context in cite‹"nlab-adjoint-equivalence"›). The diagram is reproduced here by permission of its author, Mike Shulman, who says (private communication): ``Just don't give the impression that the proof itself is due to me, because it' I don't know who first gave that proof; it's probably folklore.'' \begin{figure}[h] \includegraphics[width=6.5in]{triangle_right_implies_left.png} \end{figure} › assume 1: "(g ⋆ ε) ⋅ (η ⋆ g) = g" have 2: "(inv η ⋆ g) ⋅ (g ⋆ inv ε) = g" proof - have "(inv η ⋆ g) ⋅ (g ⋆ inv ε) = inv ((g ⋆ ε) ⋅ (η ⋆ g))" using antipar inv_comp hcomp_assoc by simp also have "... = g" using 1 by simp finally show ?thesis by blast qed have "(ε ⋆ f) ⋅ (f ⋆ η) = (ε ⋆ f) ⋅ (f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε) ⋆ f) ⋅ (f ⋆ η)" proof - have "(f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε) ⋆ f) ⋅ (f ⋆ η) = f ⋆ η" using 2 ide_left ide_right antipar whisker_left by (metis comp_cod_arr unit_simps(1) unit_simps(3)) thus ?thesis by simp qed also have "... = (ε ⋆ f) ⋅ (f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε) ⋆ f) ⋅ (f ⋆ η) ⋆ (inv η ⋅ η)" proof - have "inv η ⋅ η = src f" by (simp add: comp_inv_arr') thus ?thesis by (metis antipar(1) antipar(2) arrI calculation comp_ide_arr hcomp_arr_obj ideD(1) ide_left ide_right obj_src seqE strict_assoc' triangle_in_hom(1) vconn_implies_hpar(1)) qed also have "... = (ε ⋅ (f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε)) ⋆ ((f ⋆ inv η) ⋅ (f ⋆ η))) ⋅ (f ⋆ η)" using ide_left ide_right antipar unit_is_iso by (metis "2" arr_inv calculation comp_arr_dom comp_inv_arr' counit_simps(1) counit_simps(2) dom_inv hcomp_arr_obj ideD(1) unit_simps(1) unit_simps(2) unit_simps(5) obj_trg seqI whisker_left) also have "... = (ε ⋅ (f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε)) ⋆ ((f ⋆ inv η) ⋅ ((inv ε ⋆ f) ⋅ (ε ⋆ f)) ⋅ (f ⋆ η))) ⋅ (f ⋆ η)" proof - have "(inv ε ⋆ f) ⋅ (ε ⋆ f) = (f ⋆ g) ⋆ f" using whisker_right [of f "inv ε" ε] counit_in_hom by (simp add: antipar(1) comp_inv_arr') thus ?thesis using hcomp_assoc comp_arr_dom by (metis comp_cod_arr ide_left local.unit_simps(1) local.unit_simps(3) whisker_left) qed also have "... = (((ε ⋅ (f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε))) ⋅ (f ⋆ g)) ⋆ (((f ⋆ inv η) ⋅ (inv ε ⋆ f)) ⋅ (ε ⋆ f) ⋅ (f ⋆ η))) ⋅ (f ⋆ η)" using ide_left ide_right antipar comp_assoc whisker_right comp_cod_arr by (metis "2" comp_arr_dom counit_simps(1-2)) also have "... = (((ε ⋅ (f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε))) ⋆ ((f ⋆ inv η) ⋅ (inv ε ⋆ f))) ⋅ ((f ⋆ g) ⋆ (ε ⋆ f) ⋅ (f ⋆ η))) ⋅ (f ⋆ η)" proof - have 3: "seq (ε ⋅ (f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε))) (f ⋆ g)" using 2 antipar by auto moreover have 4: "seq ((f ⋆ inv η) ⋅ (inv ε ⋆ f)) ((ε ⋆ f) ⋅ (f ⋆ η))" using antipar hcomp_assoc by auto ultimately show ?thesis using interchange by simp qed also have "... = ((ε ⋅ (f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε))) ⋆ ((f ⋆ inv η) ⋅ (inv ε ⋆ f))) ⋅ ((f ⋆ g) ⋆ (ε ⋆ f) ⋅ (f ⋆ η)) ⋅ (f ⋆ η)" using comp_assoc by presburger also have "... = ((ε ⋆ (f ⋆ inv η) ⋅ (inv ε ⋆ f)) ⋅ ((f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε)) ⋆ f)) ⋅ (f ⋆ (g ⋆ ε) ⋅ (η ⋆ g) ⋆ f) ⋅ (f ⋆ η)" proof - have "(ε ⋅ (f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε))) ⋆ ((f ⋆ inv η) ⋅ (inv ε ⋆ f)) = (ε ⋆ (f ⋆ inv η) ⋅ (inv ε ⋆ f)) ⋅ ((f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε)) ⋆ f)" proof - have "seq ε (f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε))" using 2 antipar by simp moreover have "seq ((f ⋆ inv η) ⋅ (inv ε ⋆ f)) f" using antipar hcomp_assoc hcomp_obj_arr by auto ultimately show ?thesis using comp_assoc comp_arr_dom hcomp_obj_arr interchange [of ε "f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε)" "(f ⋆ inv η) ⋅ (inv ε ⋆ f)" f] by simp qed moreover have "((f ⋆ g) ⋆ (ε ⋆ f) ⋅ (f ⋆ η)) ⋅ (f ⋆ η) = (f ⋆ (g ⋆ ε) ⋅ (η ⋆ g) ⋆ f) ⋅ (f ⋆ η)" proof - have "((f ⋆ g) ⋆ (ε ⋆ f) ⋅ (f ⋆ η)) ⋅ (f ⋆ η) = (f ⋆ g ⋆ ε ⋆ f) ⋅ (f ⋆ (g ⋆ f) ⋆ η) ⋅ (f ⋆ η ⋆ src f)" using antipar comp_assoc hcomp_assoc whisker_left hcomp_arr_obj by simp also have "... = (f ⋆ g ⋆ ε ⋆ f) ⋅ (f ⋆ ((g ⋆ f) ⋆ η) ⋅ (η ⋅ src f))" using antipar comp_arr_dom whisker_left hcomp_arr_obj by simp also have "... = (f ⋆ g ⋆ ε ⋆ f) ⋅ (f ⋆ η ⋆ η)" using antipar comp_arr_dom comp_cod_arr hcomp_arr_obj interchange [of "g ⋆ f" η η "src f"] by simp also have "... = (f ⋆ g ⋆ ε ⋆ f) ⋅ (f ⋆ η ⋆ g ⋆ f) ⋅ (f ⋆ src f ⋆ η)" using antipar comp_arr_dom comp_cod_arr whisker_left interchange [of η "src f" "g ⋆ f" η] by simp also have "... = ((f ⋆ g ⋆ ε ⋆ f) ⋅ (f ⋆ η ⋆ g ⋆ f)) ⋅ (f ⋆ η)" using antipar comp_assoc by (simp add: hcomp_obj_arr) also have "... = (f ⋆ (g ⋆ ε) ⋅ (η ⋆ g) ⋆ f) ⋅ (f ⋆ η)" using antipar comp_assoc whisker_left whisker_right hcomp_assoc by simp finally show ?thesis by blast qed ultimately show ?thesis by simp qed also have "... = (ε ⋆ (f ⋆ inv η) ⋅ (inv ε ⋆ f)) ⋅ ((f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε) ⋆ f) ⋅ (f ⋆ (g ⋆ ε) ⋅ (η ⋆ g) ⋆ f)) ⋅ (f ⋆ η)" using comp_assoc hcomp_assoc antipar(1) antipar(2) by auto also have "... = (ε ⋆ (f ⋆ inv η) ⋅ (inv ε ⋆ f)) ⋅ ((f ⋆ (inv η ⋆ g) ⋅ (g ⋆ inv ε) ⋅ (g ⋆ ε) ⋅ (η ⋆ g) ⋆ f)) ⋅ (f ⋆ η)" using ide_left ide_right antipar comp_cod_arr comp_assoc whisker_left by (metis "1" "2" comp_ide_self unit_simps(1) unit_simps(3)) also have "... = (ε ⋆ (f ⋆ inv η) ⋅ (inv ε ⋆ f)) ⋅ (f ⋆ η)" proof - have "(inv η ⋆ g) ⋅ (g ⋆ inv ε) ⋅ (g ⋆ ε) ⋅ (η ⋆ g) = g" using ide_left ide_right antipar comp_arr_dom comp_assoc by (metis "1" "2" comp_ide_self) thus ?thesis using antipar comp_cod_arr by simp qed also have "... = (f ⋆ inv η) ⋅ ((inv ε ⋆ f) ⋅ (ε ⋆ f)) ⋅ (f ⋆ η)" proof - have "(ε ⋆ (f ⋆ inv η) ⋅ (inv ε ⋆ f)) ⋅ (f ⋆ η) = (trg f ⋅ ε ⋆ (f ⋆ inv η) ⋅ (inv ε ⋆ f)) ⋅ (f ⋆ η)" using hcomp_obj_arr comp_cod_arr by simp also have "... = ((trg f ⋆ f ⋆ inv η) ⋅ (ε ⋆ inv ε ⋆ f)) ⋅ (f ⋆ η)" using antipar hcomp_arr_obj hcomp_assoc interchange by auto also have "... = (f ⋆ inv η) ⋅ ((inv ε ⋆ f) ⋅ (ε ⋆ f)) ⋅ (f ⋆ η)" proof - have "(inv ε ⋆ f) ⋅ (ε ⋆ f) = (trg f ⋆ inv ε ⋆ f) ⋅ (ε ⋆ trg f ⋆ f)" using hseqI' by (simp add: hcomp_obj_arr) also have "... = ε ⋆ inv ε ⋆ f" using antipar comp_arr_dom comp_cod_arr interchange [of "trg f" ε "inv ε ⋆ f" "trg f ⋆ f"] by force finally have "(inv ε ⋆ f) ⋅ (ε ⋆ f) = ε ⋆ inv ε ⋆ f" by simp moreover have "trg f ⋆ f ⋆ inv η = f ⋆ inv η" using hcomp_obj_arr [of "trg f" "f ⋆ inv η"] by fastforce ultimately have "((trg f ⋆ f ⋆ inv η) ⋅ (ε ⋆ inv ε ⋆ f)) ⋅ (f ⋆ η) = ((f ⋆ inv η) ⋅ ((inv ε ⋆ f) ⋅ (ε ⋆ f))) ⋅ (f ⋆ η)" by simp thus ?thesis using comp_assoc by simp qed finally show ?thesis by simp qed also have "... = f ⋆ inv η ⋅ η" proof - have "(inv ε ⋆ f) ⋅ (ε ⋆ f) = f ⋆ g ⋆ f" using ide_left ide_right antipar counit_is_iso whisker_right hcomp_assoc by (metis comp_arr_dom comp_inv_arr' counit_simps(1) counit_simps(2) seqE) thus ?thesis using ide_left ide_right antipar unit_is_iso comp_cod_arr by (metis arr_inv dom_inv unit_simps(1) unit_simps(3) seqI whisker_left) qed also have "... = f ⋆ src f" using antipar by (simp add: comp_inv_arr') also have "... = f" using hcomp_arr_obj by simp finally show ?thesis by simp qed end text ‹ Now we use strictification to generalize the preceding result to arbitrary bicat I originally attempted to generalize this proof directly from the strict case, b in the necessary canonical isomorphisms, but it turned out to be too daunting. The proof using strictification is still fairly tedious, but it is manageable. › context equivalence_in_bicategory begin interpretation S: strictified_bicategory V H a i src trg .. notation S.vcomp (infixr ‹⋅S› 55) notation S.hcomp (infixr ‹⋆S› 53) notation S.in_hom (‹«_ : _ ==>S _¬›) notation S.in_hhom (‹«_ : _ →S _¬›) interpretation UP: equivalence_pseudofunctor V H a i src trg S.vcomp S.hcomp S.a S.i S.src S.trg S.UP S.cmpUP using S.UP_is_equivalence_pseudofunctor by auto interpretation UP: pseudofunctor_into_strict_bicategory V H a i src trg S.vcomp S.hcomp S.a S.i S.src S.trg S.UP S.cmpUP .. interpretation E: equivalence_in_bicategory S.vcomp S.hcomp S.a S.i S.src S.trg ‹S.UP f› ‹S.UP g› ‹S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋅S UP.unit (src f)› ‹S.inv (UP.unit (trg f)) ⋅S S.UP ε ⋅S S.cmpUP (f, g)› using equivalence_in_bicategory_axioms UP.preserves_equivalence [of f g η ε] by au interpretation E: equivalence_in_strict_bicategory S.vcomp S.hcomp S.a S.i S.src ‹S.UP f› ‹S.UP g› ‹S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋅S UP.unit (src f)› ‹S.inv (UP.unit (trg f)) ⋅S S.UP ε ⋅S S.cmpUP (f, g)› .. lemma UP_triangle: shows "S.UP ((g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g)) = S.cmpUP (g, src g) ⋅S (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g) ⋅S S.inv (S.cmpUP (trg g, g))" and "S.UP (r-1[g] ⋅ l[g]) = (S.cmpUP (g, src g) ⋅S (S.UP g ⋆S UP.unit (src g))) ⋅S (S.inv (UP.unit (trg g)) ⋆S S.UP g) ⋅S S.inv (S.cmpUP (trg g, g))" and "S.UP ((ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η)) = S.cmpUP (trg f, f) ⋅S (S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η) ⋅S S.inv (S.cmpUP (f, src f))" and "S.UP (l-1[f] ⋅ r[f]) = (S.cmpUP (trg f, f) ⋅S (UP.unit (trg f) ⋆S S.UP f)) ⋅S (S.UP f ⋆S S.inv (UP.unit (src f))) ⋅S S.inv (S.cmpUP (f, src f))" and "(g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g) = r-1[g] ⋅ l[g] ==> S.cmpUP (trg f, f) ⋅S (S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η) ⋅S S.inv (S.cmpUP (f, src f)) = (S.cmpUP (trg f, f) ⋅S (UP.unit (trg f) ⋆S S.UP f)) ⋅S (S.UP f ⋆S S.inv (UP.unit (src f))) ⋅S S.inv (S.cmpUP (f, src f))" proof - show T1: "S.UP ((g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g)) = S.cmpUP (g, src g) ⋅S (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g) ⋅S S.inv (S.cmpUP (trg g, g))" proof - have "S.UP ((g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g)) = S.UP (g ⋆ ε) ⋅S S.UP a[g, f, g] ⋅S S.UP (η ⋆ g)" using antipar by simp also have "... = (S.cmpUP (g, src g) ⋅S (S.UP g ⋆S S.UP ε) ⋅S ((S.inv (S.cmpUP (g, f ⋆ g)) ⋅S S.cmpUP (g, f ⋆ g)) ⋅S (S.UP g ⋆S S.cmpUP (f, g))) ⋅S (((S.inv (S.cmpUP (g, f)) ⋆S S.UP g) ⋅S (S.inv (S.cmpUP (g ⋆ f, g)))) ⋅S S.cmpUP (g ⋆ f, g)) ⋅S (S.UP η ⋆S S.UP g)) ⋅S S.inv (S.cmpUP (trg g, g))" proof - have "S.UP a[g, f, g] = S.cmpUP (g, f ⋆ g) ⋅S (S.UP g ⋆S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋆S S.UP g) ⋅S S.inv (S.cmpUP (g ⋆ f, g))" using ide_left ide_right antipar UP.image_of_associator [of g f g] by simp moreover have "S.UP (g ⋆ ε) = S.cmpUP (g, src g) ⋅S (S.UP g ⋆S S.UP ε) ⋅S S.inv (S.cmpUP (g, f ⋆ g))" proof - have "S.seq (S.cmpUP (g, src g)) (S.UP g ⋆S S.UP ε)" using antipar UP.FF_def UP.cmp_in_hom [of g "src g"] apply (intro S.seqI) by auto moreover have "S.UP (g ⋆ ε) ⋅S S.cmpUP (g, f ⋆ g) = S.cmpUP (g, src g) ⋅S (S.UP g ⋆S S.UP ε)" using antipar UP.Φ.naturality [of "(g, ε)"] UP.FF_def VV.arr_charSbC VV.dom_simp VV.cod_simp by simp moreover have "S.iso (S.cmpUP (g, f ⋆ g))" using antipar by simp ultimately show ?thesis using S.invert_side_of_triangle(2) [of "S.cmpUP (g, src g) ⋅S (S.UP g ⋆S S.UP ε)" "S.UP (g ⋆ ε)" "S.cmpUP (g, f ⋆ g)"] S.comp_assoc by presburger qed moreover have "S.UP (η ⋆ g) = (S.cmpUP (g ⋆ f, g) ⋅S (S.UP η ⋆S S.UP g)) ⋅S S.inv (S.cmpUP (trg g, g))" proof - have "S.UP (η ⋆ g) ⋅S S.cmpUP (trg g, g) = S.cmpUP (g ⋆ f, g) ⋅S (S.UP η ⋆S S.UP g)" using antipar UP.Φ.naturality [of "(η, g)"] UP.FF_def VV.arr_charSbC VV.dom_simp VV.cod_simp by simp moreover have "S.seq (S.cmpUP (g ⋆ f, g)) (S.UP η ⋆S S.UP g)" using antipar UP.cmp_in_hom(2) by (intro S.seqI, auto) ultimately show ?thesis using antipar S.invert_side_of_triangle(2) by simp qed ultimately show ?thesis using S.comp_assoc by simp qed also have "... = S.cmpUP (g, src g) ⋅S ((S.UP g ⋆S S.UP ε) ⋅S (S.UP g ⋆S S.cmpUP (f, g))) ⋅S ((S.inv (S.cmpUP (g, f)) ⋆S S.UP g) ⋅S (S.UP η ⋆S S.UP g)) ⋅S S.inv (S.cmpUP (trg g, g))" proof - have "(S.inv (S.cmpUP (g ⋆ f, g)) ⋅S S.cmpUP (g ⋆ f, g)) ⋅S (S.UP η ⋆S S.UP g) = (S.UP η ⋆S S.UP g)" using antipar S.comp_inv_arr' S.comp_cod_arr by auto moreover have "(S.inv (S.cmpUP (g, f ⋆ g)) ⋅S S.cmpUP (g, f ⋆ g)) ⋅S (S.UP g ⋆S S.cmpUP (f, g)) = (S.UP g ⋆S S.cmpUP (f, g))" proof - have "S.inv (S.cmpUP (g, f ⋆ g)) ⋅S S.cmpUP (g, f ⋆ g) = S.UP g ⋆S S.UP (f ⋆ g)" using antipar S.comp_inv_arr' UP.cmp_in_hom by auto thus ?thesis using antipar VV.arr_charSbC S.comp_cod_arr by simp qed ultimately show ?thesis using S.comp_assoc by simp qed also have "... = S.cmpUP (g, src g) ⋅S (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g) ⋅S S.inv (S.cmpUP (trg g, g))" using antipar VV.arr_charSbC S.whisker_left S.whisker_right by auto finally show ?thesis by simp qed show T2: "S.UP (r-1[g] ⋅ l[g]) = (S.cmpUP (g, src g) ⋅S (S.UP g ⋆S UP.unit (src g))) ⋅S (S.inv (UP.unit (trg g)) ⋆S S.UP g) ⋅S S.inv (S.cmpUP (trg g, g))" using UP.image_of_unitor by simp show "S.UP ((ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η)) = S.cmpUP (trg f, f) ⋅S (S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η) ⋅S S.inv (S.cmpUP (f, src f))" proof - have "S.UP ((ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η)) = S.UP (ε ⋆ f) ⋅S S.UP a-1[f, g, f] ⋅S S.UP (f ⋆ η)" using antipar by simp also have "... = S.cmpUP (trg f, f) ⋅S (S.UP ε ⋆S S.UP f) ⋅S (S.inv (S.cmpUP (f ⋆ g, f)) ⋅S S.cmpUP (f ⋆ g, f) ⋅S (S.cmpUP (f, g) ⋆S S.UP f)) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f))) ⋅S (S.inv (S.cmpUP (f, g ⋆ f)) ⋅S S.cmpUP (f, g ⋆ f) ⋅S (S.UP f ⋆S S.UP η)) ⋅S S.inv (S.cmpUP (f, src f))" proof - have "S.UP a-1[f, g, f] = S.cmpUP (f ⋆ g, f) ⋅S (S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f))) ⋅S S.inv (S.cmpUP (f, g ⋆ f))" using ide_left ide_right antipar UP.image_of_associator by simp moreover have "S.UP (ε ⋆ f) = S.cmpUP (trg f, f) ⋅S (S.UP ε ⋆S S.UP f) ⋅S S.inv (S.cmpUP (f ⋆ g, f))" proof - have "S.seq (S.cmpUP (trg f, f)) (S.UP ε ⋆S S.UP f)" using antipar UP.FF_def VV.ide_charSbC VV.arr_charSbC UP.cmp_in_hom [of "trg f" f apply (intro S.seqI) by auto moreover have "S.cmpUP (trg f, f) ⋅S (S.UP ε ⋆S S.UP f) = S.UP (ε ⋆ f) ⋅S S.cmpUP (f ⋆ g, f)" using antipar UP.Φ.naturality [of "(ε, f)"] UP.FF_def VV.arr_charSbC VV.dom_simp VV.cod_simp by simp moreover have "S.iso (S.cmpUP (f ⋆ g, f))" using antipar by simp ultimately show ?thesis using antipar S.comp_assoc S.invert_side_of_triangle(2) [of "S.cmpUP (trg f, f) ⋅S (S.UP ε ⋆S S.UP f)" "S.UP (ε ⋆ f)" "S.cmpUP (f ⋆ g, f)"] by metis qed moreover have "S.UP (f ⋆ η) = (S.cmpUP (f, g ⋆ f) ⋅S (S.UP f ⋆S S.UP η)) ⋅S S.inv (S.cmpUP (f, src f))" proof - have "S.cmpUP (f, g ⋆ f) ⋅S (S.UP f ⋆S S.UP η) = S.UP (f ⋆ η) ⋅S S.cmpUP (f, src f)" using antipar UP.Φ.naturality [of "(f, η)"] UP.FF_def VV.arr_charSbC VV.dom_simp VV.cod_simp by simp moreover have "S.seq (S.cmpUP (f, g ⋆ f)) (S.UP f ⋆S S.UP η)" using antipar by (intro S.seqI, auto) ultimately show ?thesis using antipar S.invert_side_of_triangle(2) by auto qed ultimately show ?thesis using S.comp_assoc by simp qed also have "... = S.cmpUP (trg f, f) ⋅S ((S.UP ε ⋆S S.UP f) ⋅S (S.cmpUP (f, g) ⋆S S.UP f)) ⋅S ((S.UP f ⋆S S.inv (S.cmpUP (g, f))) ⋅S (S.UP f ⋆S S.UP η)) ⋅S S.inv (S.cmpUP (f, src f))" proof - have "(S.inv (S.cmpUP (f ⋆ g, f)) ⋅S S.cmpUP (f ⋆ g, f)) ⋅S (S.cmpUP (f, g) ⋆S S.UP f) = (S.cmpUP (f, g) ⋆S S.UP f)" using antipar S.comp_cod_arr VV.arr_charSbC S.comp_inv_arr' by auto moreover have "(S.inv (S.cmpUP (f, g ⋆ f)) ⋅S S.cmpUP (f, g ⋆ f)) ⋅S (S.UP f ⋆S S.UP η) = (S.UP f ⋆S S.UP η)" using antipar S.comp_inv_arr' S.comp_cod_arr by auto ultimately show ?thesis using S.comp_assoc by simp qed also have "... = S.cmpUP (trg f, f) ⋅S (S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η) ⋅S S.inv (S.cmpUP (f, src f))" using antipar VV.arr_charSbC S.whisker_left S.whisker_right by auto finally show ?thesis by simp qed show "S.UP (l-1[f] ⋅ r[f]) = (S.cmpUP (trg f, f) ⋅S (UP.unit (trg f) ⋆S S.UP f)) ⋅S (S.UP f ⋆S S.inv (UP.unit (src f))) ⋅S S.inv (S.cmpUP (f, src f))" using UP.image_of_unitor by simp show "(g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g) = r-1[g] ⋅ l[g] ==> S.cmpUP (trg f, f) ⋅S (S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η) ⋅S S.inv (S.cmpUP (f, src f)) = (S.cmpUP (trg f, f) ⋅S (UP.unit (trg f) ⋆S S.UP f)) ⋅S (S.UP f ⋆S S.inv (UP.unit (src f))) ⋅S S.inv (S.cmpUP (f, src f))" proof - assume A: "(g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g) = r-1[g] ⋅ l[g]" have B: "(S.UP g ⋆S S.inv (UP.unit (src g)) ⋅S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋅S UP.unit (trg g) ⋆S S.UP g) = S.UP g" proof - show "(S.UP g ⋆S S.inv (UP.unit (src g)) ⋅S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋅S UP.unit (trg g) ⋆S S.UP g) = S.UP g" proof - have 2: "S.cmpUP (g, src g) ⋅S (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g) ⋅S S.inv (S.cmpUP (trg g, g)) = (S.cmpUP (g, src g) ⋅S (S.UP g ⋆S UP.unit (src g))) ⋅S (S.inv (UP.unit (trg g)) ⋆S S.UP g) ⋅S S.inv (S.cmpUP (trg g, g))" using A T1 T2 by simp show ?thesis proof - have 8: "S.seq (S.cmpUP (g, src g)) ((S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g) ⋅S S.inv (S.cmpUP (trg g, g)))" using antipar VV.arr_charSbC S.hcomp_assoc by (metis (no_types, lifting) S.arr_UP T1 arrI triangle_in_hom(2)) have 7: "S.seq (S.cmpUP (g, src g)) ((S.UP g ⋆S UP.unit (src g)) ⋅S (S.inv (UP.unit (trg g)) ⋆S S.UP g) ⋅S S.inv (S.cmpUP (trg g, g)))" using antipar 2 8 S.comp_assoc by auto have 5: "(S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g) = (S.UP g ⋆S UP.unit (src g)) ⋅S (S.inv (UP.unit (trg g)) ⋆S S.UP g)" proof - have "((S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g)) ⋅S S.inv (S.cmpUP (trg g, g)) = ((S.UP g ⋆S UP.unit (src g)) ⋅S (S.inv (UP.unit (trg g)) ⋆S S.UP g)) ⋅S S.inv (S.cmpUP (trg g, g))" proof - have "S.mono (S.cmpUP (g, src g))" using antipar S.iso_is_section S.section_is_mono by simp thus ?thesis using 2 8 7 S.mono_cancel S.comp_assoc by presburger qed moreover have "S.epi (S.inv (S.cmpUP (trg g, g)))" using antipar S.iso_is_retraction S.retraction_is_epi by simp moreover have "S.seq ((S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g)) (S.inv (S.cmpUP (trg g, g)))" using S.comp_assoc S.seq_char 8 by presburger moreover have "S.seq ((S.UP g ⋆S UP.unit (src g)) ⋅S (S.inv (UP.unit (trg g)) ⋆S S.UP g)) (S.inv (S.cmpUP (trg g, g)))" using antipar calculation(1,3) by presburger ultimately show ?thesis using 2 S.epi_cancel by blast qed have 6: "S.seq (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g)" using antipar VV.arr_charSbC S.hcomp_assoc by auto have 3: "(S.UP g ⋆S S.inv (UP.unit (src g))) ⋅S (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g) = (S.inv (UP.unit (trg g)) ⋆S S.UP g)" proof - have "S.seq (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g)" using 6 by simp moreover have "(S.UP g ⋆S UP.unit (src g)) ⋅S (S.inv (UP.unit (trg g)) ⋆S S.UP g) = (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g)" using 5 by argo moreover have "S.iso (S.UP g ⋆S UP.unit (src g))" using antipar UP.unit_char S.UP_map0_obj by simp moreover have "S.inv (S.UP g ⋆S UP.unit (src g)) = S.UP g ⋆S S.inv (UP.unit (src g))" using antipar UP.unit_char S.UP_map0_obj by simp ultimately show ?thesis using S.invert_side_of_triangle(1) [of "(S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g)) ⋅S (S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g)" "S.UP g ⋆S UP.unit (src g)" "S.inv (UP.unit (trg g)) ⋆S S.UP g"] by presburger qed have 4: "((S.UP g ⋆S S.inv (UP.unit (src g))) ⋅S (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g))) ⋅S ((S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g)) ⋅S (UP.unit (trg g) ⋆S S.UP g) = S.UP g" proof - have "(((S.UP g ⋆S S.inv (UP.unit (src g))) ⋅S (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g))) ⋅S ((S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g)) ⋅S (UP.unit (trg g) ⋆S S.UP g)) = (((S.UP g ⋆S S.inv (UP.unit (src g))) ⋅S (S.UP g ⋆S S.UP ε ⋅S S.cmpUP (f, g))) ⋅S ((S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋆S S.UP g))) ⋅S (UP.unit (trg g) ⋆S S.UP g)" using S.comp_assoc by simp also have "... = (S.inv (UP.unit (trg g)) ⋆S S.UP g) ⋅S (UP.unit (trg g) ⋆S S.UP g)" using 3 S.comp_assoc by auto also have "... = S.inv (UP.unit (trg g)) ⋅S UP.unit (trg g) ⋆S S.UP g" using UP.unit_char(2) S.whisker_right by auto also have "... = UP.map0 (trg g) ⋆S S.UP g" using UP.unit_char [of "trg g"] S.comp_inv_arr S.inv_is_inverse by simp also have "... = S.UP g" using S.UP_map0_obj by (simp add: S.hcomp_obj_arr) finally show ?thesis by blast qed thus ?thesis using antipar S.whisker_left S.whisker_right UP.unit_char S.comp_assoc by simp qed qed qed show "S.cmpUP (trg f, f) ⋅S (S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η) ⋅S S.inv (S.cmpUP (f, src f)) = (S.cmpUP (trg f, f) ⋅S (UP.unit (trg f) ⋆S S.UP f)) ⋅S (S.UP f ⋆S S.inv (UP.unit (src f))) ⋅S S.inv (S.cmpUP (f, src f))" proof - have "(S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η) = (UP.unit (trg f) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (UP.unit (src f)))" proof - have 2: "(S.inv (UP.unit (trg f)) ⋆S S.UP f) ⋅S ((S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η)) ⋅S (S.UP f ⋆S UP.unit (src f)) = S.UP f" proof - have "S.UP f = (S.inv (UP.unit (trg f)) ⋅S S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋅S UP.unit (src f))" using B antipar E.triangle_right_implies_left by argo also have "... = (S.inv (UP.unit (trg f)) ⋆S S.UP f) ⋅S ((S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η)) ⋅S (S.UP f ⋆S UP.unit (src f))" proof - have "S.inv (UP.unit (trg f)) ⋅S S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f = (S.inv (UP.unit (trg f)) ⋆S S.UP f) ⋅S (S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f)" using UP.unit_char S.whisker_right by simp moreover have "S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η ⋅S UP.unit (src f) = (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η) ⋅S (S.UP f ⋆S UP.unit (src f))" using antipar UP.unit_char S.whisker_left S.comp_assoc by simp ultimately show ?thesis using S.comp_assoc by presburger qed finally show ?thesis by argo qed show ?thesis proof - have "((S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η)) ⋅S (S.UP f ⋆S UP.unit (src f)) = (UP.unit (trg f) ⋆S S.UP f)" proof - have "S.inv (S.inv (UP.unit (trg f)) ⋆S S.UP f) ⋅S S.UP f = UP.unit (trg f) ⋆S S.UP f" using UP.unit_char S.comp_arr_dom S.UP_map0_obj by (simp add: S.hcomp_obj_arr) moreover have "S.arr (S.UP f)" by simp moreover have "S.iso (S.inv (UP.unit (trg f)) ⋆S S.UP f)" using S.UP_map0_obj by (simp add: UP.unit_char(2)) ultimately show ?thesis using 2 S.invert_side_of_triangle(1) [of "S.UP f" "S.inv (UP.unit (trg f)) ⋆S S.UP f" "((S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η)) ⋅S (S.UP f ⋆S UP.unit (src f))"] by presburger qed moreover have "S.hseq (UP.unit (trg f)) (S.UP f) ∧ S.iso (S.UP f ⋆S UP.unit (src f)) ∧ S.inv (S.UP f ⋆S UP.unit (src f)) = S.UP f ⋆S S.inv (UP.unit (src f))" using UP.unit_char S.UP_map0_obj by simp ultimately show ?thesis using S.invert_side_of_triangle(2) [of "UP.unit (trg f) ⋆S S.UP f" "(S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η)" "S.UP f ⋆S UP.unit (src f)"] by presburger qed qed hence "S.cmpUP (trg f, f) ⋅S ((S.UP ε ⋅S S.cmpUP (f, g) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (S.cmpUP (g, f)) ⋅S S.UP η)) ⋅S S.inv (S.cmpUP (f, src f)) = S.cmpUP (trg f, f) ⋅S ((UP.unit (trg f) ⋆S S.UP f) ⋅S (S.UP f ⋆S S.inv (UP.unit (src f)))) ⋅S S.inv (S.cmpUP (f, src f))" by simp thus ?thesis using S.comp_assoc by simp qed qed qed lemma triangle_right_implies_left: assumes "(g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g) = r-1[g] ⋅ l[g]" shows "(ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η) = l-1[f] ⋅ r[f]" proof - have "par ((ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η)) (l-1[f] ⋅ r[f])" using antipar by simp moreover have "S.UP ((ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η)) = S.UP (l-1[f] ⋅ r[f])" using assms UP_triangle(3-5) by simp ultimately show "(ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η) = l-1[f] ⋅ r[f]" using UP.is_faithful by blast qed text ‹ We \emph{really} don't want to go through the ordeal of proving a dual version o ‹UP_triangle(5)›, do we? So let's be smart and dualize via the opposite bicateg › lemma triangle_left_implies_right: assumes "(ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η) = l-1[f] ⋅ r[f]" shows "(g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g) = r-1[g] ⋅ l[g]" proof - interpret Cop: op_bicategory V H a i src trg .. interpret Eop: equivalence_in_bicategory V Cop.H Cop.a i Cop.src Cop.trg g f η ε using antipar unit_in_hom counit_in_hom by (unfold_locales) simp_all have "(ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η) = l-1[f] ⋅ r[f] ==> (g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g) = r-1[g] ⋅ l[g]" using antipar Cop.lunit_ide_simp Cop.runit_ide_simp Cop.assoc_ide_simp VVV.ide_char VVV.arr_charSbC VV.arr_charSbC Eop.triangle_right_implies_left by simp thus ?thesis using assms by simp qed lemma triangle_left_iff_right: shows "(ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η) = l-1[f] ⋅ r[f] ⟷ (g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g) = r-1[g] ⋅ l[g]" using triangle_left_implies_right triangle_right_implies_left by auto end text ‹ We might as well specialize the dual result back to the strict case while we are › context equivalence_in_strict_bicategory begin lemma triangle_left_iff_right: shows "(ε ⋆ f) ⋅ (f ⋆ η) = f ⟷ (g ⋆ ε) ⋅ (η ⋆ g) = g" proof - have "(ε ⋆ f) ⋅ (f ⋆ η) = f ⟷ (ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η) = l-1[f] ⋅ r[f]" proof - have "l-1[f] ⋅ r[f] = f" using strict_lunit strict_runit by simp moreover have "(ε ⋆ f) ⋅ a-1[f, g, f] ⋅ (f ⋆ η) = (ε ⋆ f) ⋅ (f ⋆ η)" using antipar strict_assoc assoc'_in_hom(2) [of f g f] comp_cod_arr by auto ultimately show ?thesis by simp qed also have "... ⟷ (g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g) = r-1[g] ⋅ l[g]" using triangle_left_iff_right by blast also have "... ⟷ (g ⋆ ε) ⋅ (η ⋆ g) = g" proof - have "r-1[g] ⋅ l[g] = g" using strict_lunit strict_runit by simp moreover have "(g ⋆ ε) ⋅ a[g, f, g] ⋅ (η ⋆ g) = (g ⋆ ε) ⋅ (η ⋆ g)" using antipar strict_assoc assoc_in_hom(2) [of g f g] comp_cod_arr by auto ultimately show ?thesis by simp qed finally show ?thesis by simp qed end end
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.306Bemerkung: (vorverarbeitet am 2026-06-10) ¤*Bot Zugriff |
|
||||||||||||||
2026-06-09