Theory ConcreteBicategory

(*  Title:       ConcreteBicategory
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2021
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

section "Concrete Bicategories"

text ‹
  The locale ‹concrete_bicategory› defined in this section provides a uniform way to construct
  a bicategory from extrinsically specified data comprising: a set of ‹Obj› of ``objects'',
  a ``hom-category'' ‹Hom A B› for each pair of objects ‹A› and ‹B›, an ``identity arrow''
  ‹Id A ∈ Hom A A› for each object ‹A›, ``horizontal composition'' functors
  ‹Comp C B A : Hom B C × Hom A B → Hom A C› indexed by triples of objects,
  together with unit and associativity isomorphisms; the latter subject to naturality and
  coherence conditions.
  We show that the bicategory produced by the construction relates to the given data in the
  expected fashion: the objects of the bicategory are in bijective correspondence with the
  given set ‹Obj›, the hom-categories of the bicategory are isomorphic to the given
  categories ‹Hom A B›, the horizontal composition of the bicategory agrees with the given
  compositions ‹Comp C B A›, and the unit and associativity 2-cells of the bicategory are
  directly defined in terms of the given unit and associativity isomorphisms.
›

theory ConcreteBicategory
imports Bicategory.Bicategory
begin

  locale concrete_bicategory =
  fixes Obj :: "'o set"
  and Hom :: "'o ⇒ 'o ⇒ 'a comp"
  and Id :: "'o ⇒ 'a"
  and Comp :: "'o ⇒ 'o ⇒ 'o ⇒ 'a ⇒ 'a ⇒ 'a"
  and Unit :: "'o ⇒ 'a"
  and Assoc :: "'o ⇒ 'o ⇒ 'o ⇒ 'o ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a"
  assumes category_Hom: "⟦ A ∈ Obj; B ∈ Obj ⟧ ⟹ category (Hom A B)"
  and binary_functor_Comp:
        "⟦ A ∈ Obj; B ∈ Obj; C ∈ Obj ⟧
            ⟹ binary_functor (Hom B C) (Hom A B) (Hom A C) (λ(f, g). Comp C B A f g)"
  and ide_Id: "A ∈ Obj ⟹ partial_composition.ide (Hom A A) (Id A)"
  and Unit_in_hom:
        "A ∈ Obj ⟹
           partial_composition.in_hom (Hom A A) (Unit A) (Comp A A A (Id A) (Id A)) (Id A)"
  and iso_Unit: "A ∈ Obj ⟹ category.iso (Hom A A) (Unit A)"
  and natural_isomorphism_Assoc:
        "⟦ A ∈ Obj; B ∈ Obj; C ∈ Obj; D ∈ Obj ⟧
            ⟹ natural_isomorphism
                  (product_category.comp
                    (Hom C D) (product_category.comp (Hom B C) (Hom A B))) (Hom A D)
                  (λ(f, g, h). Comp D B A (Comp D C B f g) h)
                  (λ(f, g, h). Comp D C A f (Comp C B A g h))
                  (λ(f, g, h). Assoc D C B A f g h)"
  and left_unit_Id:
        "⋀A B. ⟦ A ∈ Obj; B ∈ Obj ⟧
                   ⟹ fully_faithful_functor (Hom A B) (Hom A B)
                         (λf. if partial_composition.arr (Hom A B) f
                              then Comp B B A (Id B) f
                              else partial_magma.null (Hom A B))"
  and right_unit_Id:
        "⋀A B. ⟦ A ∈ Obj; B ∈ Obj ⟧
                   ⟹ fully_faithful_functor (Hom A B) (Hom A B)
                         (λf. if partial_composition.arr (Hom A B) f
                              then Comp B A A f (Id A)
                              else partial_magma.null (Hom A B))"
  and pentagon:
        "⋀A B C D E f g h k.
            ⟦ A ∈ Obj; B ∈ Obj; C ∈ Obj; D ∈ Obj; E ∈ Obj;
              partial_composition.ide (Hom D E) f; partial_composition.ide (Hom C D) g;
              partial_composition.ide (Hom B C) h; partial_composition.ide (Hom A B) k ⟧ ⟹
              Hom A E (Comp E D A f (Assoc D C B A g h k))
                      (Hom A E (Assoc E D B A f (Comp D C B g h) k)
                               (Comp E B A (Assoc E D C B f g h) k)) =
              Hom A E (Assoc E D C A f g (Comp C B A h k))
                      (Assoc E C B A (Comp E D C f g) h k)"
  begin

    text ‹
      We first construct the vertical category.
      Arrows are terms of the form ‹MkCell A B μ›, where ‹A ∈ Obj›, ‹B ∈ Obj›, and where ‹μ›
      is an arrow of ‹Hom A B›.
      Composition requires agreement of the ``source'' ‹A› and ``target'' ‹B› components,
      and is then defined in terms of composition within ‹Hom A B›.
    ›

    datatype ('oo, 'aa) cell =
      Null
    | MkCell 'oo 'oo 'aa

    abbreviation MkObj :: "'o ⇒ ('o, 'a) cell"
    where "MkObj A ≡ MkCell A A (Id A)"

    fun Src :: "('o, 'a) cell ⇒ 'o"
    where "Src (MkCell A _ _) = A"
        | "Src _ = undefined"

    fun Trg
    where "Trg (MkCell _ B _) = B"
        | "Trg _ = undefined"

    fun Map
    where "Map (MkCell _ _ F) = F"
        | "Map _ = undefined"

    abbreviation Cell
    where "Cell μ ≡ μ ≠ Null ∧ Src μ ∈ Obj ∧ Trg μ ∈ Obj ∧
                    partial_composition.arr (Hom (Src μ) (Trg μ)) (Map μ)"

    definition vcomp
    where "vcomp μ ν ≡ if Cell μ ∧ Cell ν ∧ Src μ = Src ν ∧ Trg μ = Trg ν ∧
                           partial_composition.seq (Hom (Src μ) (Trg μ)) (Map μ) (Map ν)
                        then MkCell (Src μ) (Trg μ) (Hom (Src μ) (Trg μ) (Map μ) (Map ν))
                        else Null"

    interpretation partial_composition vcomp
      by (metis partial_composition_def partial_magma_def vcomp_def)

    lemma null_char:
    shows "null = Null"
      using null_is_zero(1) vcomp_def by metis

    lemma MkCell_Map:
    assumes "μ ≠ null"
    shows "μ = MkCell (Src μ) (Trg μ) (Map μ)"
      using assms null_char
      by (metis Map.simps(1) Src.elims Trg.simps(1))

    (*
     * We need to name the following fact so that it does not get
     * hidden when we interpret the category locale, because it is still
     * used in some subsequent proofs.
     *)
    lemma ide_char'':
    shows "ide μ ⟷ Cell μ ∧ partial_composition.ide (Hom (Src μ) (Trg μ)) (Map μ)"
    proof
      show "ide μ ⟹ Cell μ ∧ partial_composition.ide (Hom (Src μ) (Trg μ)) (Map μ)"
      proof
        assume μ: "ide μ"
        show 1: "Cell μ"
          by (metis μ ide_def vcomp_def)
        interpret Hom: category "Hom (Src μ) (Trg μ)"
          using 1 category_Hom by simp
        let ?ν = "MkCell (Src μ) (Trg μ) (Hom.dom (Map μ))"
        have "vcomp μ ?ν = MkCell (Src μ) (Trg μ) (Map μ)"
          using 1 vcomp_def Hom.comp_arr_dom by simp
        moreover have "vcomp μ ?ν = ?ν"
          using μ ide_def null_char
          by (metis MkCell_Map calculation)
        ultimately show "Hom.ide (Map μ)"
          using 1 Hom.ide_dom by fastforce
      qed
      show "Cell μ ∧ partial_composition.ide (Hom (Src μ) (Trg μ)) (Map μ) ⟹ ide μ"
      proof -
        assume μ: "Cell μ ∧ partial_composition.ide (Hom (Src μ) (Trg μ)) (Map μ)"
        interpret Hom: category "Hom (Src μ) (Trg μ)"
          using μ category_Hom by simp
        show "ide μ"
        proof -
          have "vcomp μ μ ≠ null"
            using μ vcomp_def null_char by simp
          moreover have "⋀ν. vcomp ν μ ≠ null ⟹ vcomp ν μ = ν"
            by (metis (full_types) Hom.comp_arr_ide μ MkCell_Map vcomp_def null_char)
          moreover have "⋀ν. vcomp μ ν ≠ null ⟹ vcomp μ ν = ν"
            by (metis Hom.comp_ide_arr MkCell_Map μ null_char vcomp_def)
          ultimately show ?thesis
            unfolding ide_def by simp
        qed
      qed
    qed

    lemma MkCell_in_domains:
    assumes "Cell μ"
    shows "MkCell (Src μ) (Trg μ) (partial_composition.dom (Hom (Src μ) (Trg μ)) (Map μ))
             ∈ domains μ"
    proof -
      interpret Hom: category "Hom (Src μ) (Trg μ)"
        using assms category_Hom by simp
      let ?ν = "MkCell (Src μ) (Trg μ) (Hom.dom (Map μ))"
      have "ide ?ν"
        using assms ide_char'' Hom.arr_dom Hom.ide_dom by simp
      moreover have "vcomp μ ?ν = μ"
        unfolding vcomp_def
        using assms Hom.comp_arr_dom MkCell_Map null_char by auto
      ultimately show ?thesis
          using domains_def by (simp add: assms null_char)
    qed
    
    lemma MkCell_in_codomains:
    assumes "Cell μ"
    shows "MkCell (Src μ) (Trg μ) (partial_composition.cod (Hom (Src μ) (Trg μ)) (Map μ))
             ∈ codomains μ"
    proof -
      interpret Hom: category "Hom (Src μ) (Trg μ)"
        using assms category_Hom by simp
      let ?ν = "MkCell (Src μ) (Trg μ) (Hom.cod (Map μ))"
      have "ide ?ν"
        using assms ide_char'' Hom.arr_dom Hom.ide_dom by simp
      moreover have "vcomp ?ν μ = μ"
        unfolding vcomp_def
        using assms Hom.comp_cod_arr MkCell_Map null_char by auto
      ultimately show ?thesis
          using codomains_def by (simp add: assms null_char)
    qed
  
    lemma has_domain_char:
    shows "domains μ ≠ {} ⟷ Cell μ"
    proof -
      have "¬ Cell μ ⟹ domains μ = {}"
        using vcomp_def domains_def null_char by auto
      moreover have
        "Cell μ ⟹ MkCell (Src μ) (Trg μ) (partial_composition.dom (Hom (Src μ) (Trg μ)) (Map μ))
                       ∈ domains μ"
        using MkCell_in_domains by simp
      ultimately show ?thesis by auto
    qed

    lemma has_codomain_char:
    shows "codomains μ ≠ {} ⟷ Cell μ"
    proof -
      have "¬ Cell μ ⟹ codomains μ = {}"
        using vcomp_def codomains_def null_char by auto
      moreover have
        "Cell μ ⟹ MkCell (Src μ) (Trg μ) (partial_composition.cod (Hom (Src μ) (Trg μ)) (Map μ))
                       ∈ codomains μ"
        using MkCell_in_codomains by simp
      ultimately show ?thesis by auto
    qed

    lemma arr_char:
    shows "arr μ ⟷ Cell μ"
      using arr_def has_domain_char has_codomain_char by simp

    lemma ide_char''':
    shows "ide μ ⟷ arr μ ∧ partial_composition.ide (Hom (Src μ) (Trg μ)) (Map μ)"
      using ide_char'' arr_char by simp

    lemma seq_char:
    shows "seq μ ν ⟷ Cell μ ∧ Cell ν ∧ Src μ = Src ν ∧ Trg μ = Trg ν ∧
                       partial_composition.seq (Hom (Src μ) (Trg μ)) (Map μ) (Map ν)"
      using arr_char vcomp_def by auto

    lemma vcomp_char:
    shows "vcomp μ ν = (if seq μ ν then
                          MkCell (Src μ) (Trg μ) (Hom (Src μ) (Trg μ) (Map μ) (Map ν))
                        else null)"
      by (metis null_char seq_char vcomp_def)

    interpretation category vcomp
    proof
      show "⋀g f. vcomp g f ≠ null ⟹ seq g f"
        using seq_char null_char vcomp_def by metis
      show "⋀f. (domains f ≠ {}) = (codomains f ≠ {})"
        using has_domain_char has_codomain_char by simp
      show "⋀h g f. ⟦seq h g; seq (vcomp h g) f⟧ ⟹ seq g f"
        using vcomp_def
        apply (unfold seq_char, intro conjI)
                  apply auto
        by (meson category.match_1 category_Hom)
      show "⋀h g f. ⟦seq h (vcomp g f); seq g f⟧ ⟹ seq h g"
        using vcomp_def
        apply (unfold seq_char, intro conjI)
                  apply auto
        by (meson category.match_2 category_Hom)
      show "⋀g f h. ⟦seq g f; seq h g⟧ ⟹ seq (vcomp h g) f"
        using vcomp_def
        apply (unfold seq_char, intro conjI)
                  apply auto
        by (meson category.match_3 category_Hom)
      show "⋀g f h. ⟦seq g f; seq h g⟧ ⟹ vcomp (vcomp h g) f = vcomp h (vcomp g f)"
      proof -
        fix f g h
        assume fg: "seq g f" and gh: "seq h g"
        interpret Hom: category ‹Hom (Src f) (Trg f)›
          using fg seq_char category_Hom by simp
        have "vcomp (vcomp h g) f =
              MkCell (Src f) (Trg f)
                                (Hom (Src f) (Trg f)
                                     (Hom (Src f) (Trg f) (Map h) (Map g)) (Map f))"
          using fg gh vcomp_char seq_char null_char Hom.match_3 by auto
        also have "... =
              MkCell (Src f) (Trg f)
                     (Hom (Src f) (Trg f) (Map h)
                          (Hom (Src f) (Trg f) (Map g) (Map f)))"
          using fg gh seq_char Hom.comp_assoc by simp
        also have "... = vcomp h (vcomp g f)"
          using fg gh vcomp_char seq_char null_char Hom.match_4 by auto
        finally show "vcomp (vcomp h g) f = vcomp h (vcomp g f)"
          by blast
      qed
    qed

    lemma arr_eqI:
    assumes "arr f" and "arr f'"
    and "Src f = Src f'" and "Trg f = Trg f'" and "Map f = Map f'"
    shows "f = f'"
      using arr_char MkCell_Map assms null_char by metis

    lemma dom_char:
    shows "dom μ = (if arr μ then
                      MkCell (Src μ) (Trg μ) (partial_composition.dom (Hom (Src μ) (Trg μ)) (Map μ))
                    else Null)"
      by (metis MkCell_in_domains arr_char dom_in_domains domain_unique has_domain_iff_arr
          dom_def null_char)
        
    lemma cod_char:
    shows "cod μ = (if arr μ then
                      MkCell (Src μ) (Trg μ) (partial_composition.cod (Hom (Src μ) (Trg μ)) (Map μ))
                    else Null)"
      by (metis MkCell_in_codomains arr_char cod_def cod_in_codomains codomain_unique
          has_codomain_iff_arr null_char)

    lemma Src_vcomp [simp]:
    assumes "seq μ ν"
    shows "Src (vcomp μ ν) = Src μ"
      using assms seq_char vcomp_def by auto

    lemma Trg_vcomp [simp]:
    assumes "seq μ ν"
    shows "Trg (vcomp μ ν) = Trg μ"
      using assms seq_char vcomp_def by auto

    lemma Map_vcomp [simp]:
    assumes "seq μ ν"
    shows "Map (vcomp μ ν) = Hom (Src μ) (Trg μ) (Map μ) (Map ν)"
      using assms seq_char vcomp_def by auto

    lemma arr_MkCell [simp]:
    assumes "A ∈ Obj" and "B ∈ Obj" and "partial_composition.arr (Hom A B) f"
    shows "arr (MkCell A B f)"
      using assms arr_char by simp

    lemma dom_MkCell [simp]:
    assumes "arr (MkCell A B f)"
    shows "dom (MkCell A B f) = MkCell A B (partial_composition.dom (Hom A B) f)"
      using assms arr_char dom_char by simp

    lemma cod_MkCell [simp]:
    assumes "arr (MkCell A B f)"
    shows "cod (MkCell A B f) = MkCell A B (partial_composition.cod (Hom A B) f)"
      using assms arr_char cod_char by simp

    lemma iso_char:
    shows "iso μ ⟷ arr μ ∧ category.iso (Hom (Src μ) (Trg μ)) (Map μ)"
    proof
      assume μ: "iso μ"
      have 1: "arr μ" using μ by blast
      interpret Hom: category ‹Hom (Src μ) (Trg μ)›
        using 1 arr_char category_Hom by simp
      have 2: "Hom.iso (Map μ)"
      proof -
        obtain ν where ν: "inverse_arrows μ ν"
          using μ by blast
        have "Hom.inverse_arrows (Map μ) (Map ν)"
        proof
          show "Hom.ide (Hom (Src μ) (Trg μ) (Map μ) (Map ν))"
            using ν ide_char'' Src_vcomp Trg_vcomp ideD(1) vcomp_char Map_vcomp
            by (metis inverse_arrowsE)
          show "Hom.ide (Hom (Src μ) (Trg μ) (Map ν) (Map μ))"
          proof -
            have 1: "ide (vcomp ν μ)"
              using ν by auto
            hence "Hom.ide (Map (vcomp ν μ))"
              using ide_char'' Src_vcomp Trg_vcomp ideD(1) seq_char by metis
            thus "Hom.ide (Hom (Src μ) (Trg μ) (Map ν) (Map μ))"
              using ν 1 vcomp_char Map.simps(1) seq_char ideD(1)
              by (metis (no_types, lifting))
          qed
        qed
        thus ?thesis by auto
      qed
      show "arr μ ∧ Hom.iso (Map μ)"
        using 1 2 by simp
      next
      assume μ: "arr μ ∧ category.iso (Hom (Src μ) (Trg μ)) (Map μ)"
      interpret Hom: category ‹Hom (Src μ) (Trg μ)›
        using μ arr_char category_Hom by simp
      obtain f where f: "Hom.inverse_arrows (Map μ) f"
        using μ by auto
      let ?ν = "MkCell (Src μ) (Trg μ) f"
      have 1: "arr ?ν"
        using μ f arr_char by auto
      have "inverse_arrows μ (MkCell (Src μ) (Trg μ) f)"
        using μ f 1 arr_char ide_char'' vcomp_def
        apply (intro inverse_arrowsI) by auto
      thus "iso μ" by auto        
    qed

    text ‹
      Next, we equip each arrow with a source and a target, and show that these assignments
      are functorial.
    ›

    definition src
    where "src μ ≡ if arr μ then MkObj (Src μ) else null"

    definition trg
    where "trg μ ≡ if arr μ then MkObj (Trg μ) else null"

    lemma src_MkCell [simp]:
    assumes "arr (MkCell A B f)"
    shows "src (MkCell A B f) = MkObj A"
      using assms src_def by simp

    lemma trg_MkCell [simp]:
    assumes "arr (MkCell A B f)"
    shows "trg (MkCell A B f) = MkObj B"
      using assms trg_def by simp

    lemma src_dom:
    assumes "arr μ"
    shows "src (dom μ) = src μ"
      using assms dom_char src_def arr_char arr_dom by auto

    lemma src_cod:
    assumes "arr μ"
    shows "src (cod μ) = src μ"
      using assms cod_char src_def arr_char arr_cod by auto

    lemma trg_dom:
    assumes "arr μ"
    shows "trg (dom μ) = trg μ"
      using assms dom_char trg_def arr_char arr_dom by auto

    lemma trg_cod:
    assumes "arr μ"
    shows "trg (cod μ) = trg μ"
      using assms cod_char trg_def arr_char arr_cod by auto

    lemma Src_src [simp]:
    assumes "arr μ"
    shows "Src (src μ) = Src μ"
      using assms src_def by simp

    lemma Trg_src [simp]:
    assumes "arr μ"
    shows "Trg (src μ) = Src μ"
      using assms src_def by simp

    lemma Map_src [simp]:
    assumes "arr μ"
    shows "Map (src μ) = Id (Src μ)"
      using assms src_def by simp

    lemma Src_trg [simp]:
    assumes "arr μ"
    shows "Src (trg μ) = Trg μ"
      using assms trg_def by simp

    lemma Trg_trg [simp]:
    assumes "arr μ"
    shows "Trg (trg μ) = Trg μ"
      using assms trg_def by simp

    lemma Map_trg [simp]:
    assumes "arr μ"
    shows "Map (trg μ) = Id (Trg μ)"
      using assms trg_def by simp

    lemma Src_dom [simp]:
    assumes "arr μ"
    shows "Src (dom μ) = Src μ"
      using assms dom_char src_def arr_char arr_dom by auto

    lemma Src_cod [simp]:
    assumes "arr μ"
    shows "Src (cod μ) = Src μ"
      using assms src_cod src_def arr_char arr_cod by auto

    lemma Trg_dom [simp]:
    assumes "arr μ"
    shows "Trg (dom μ) = Trg μ"
      using assms dom_char trg_def arr_char arr_dom by auto

    lemma Trg_cod [simp]:
    assumes "arr μ"
    shows "Trg (cod μ) = Trg μ"
      using assms cod_char trg_def arr_char arr_cod by auto

    lemma Map_dom [simp]:
    assumes "arr μ"
    shows "Map (dom μ) = partial_composition.dom (Hom (Src μ) (Trg μ)) (Map μ)"
      using assms by (simp add: dom_char)

    lemma Map_cod [simp]:
    assumes "arr μ"
    shows "Map (cod μ) = partial_composition.cod (Hom (Src μ) (Trg μ)) (Map μ)"
      using assms by (simp add: cod_char)

    lemma ide_MkObj:
    assumes "A ∈ Obj"
    shows "ide (MkObj A)"
      using assms ide_char'
      by (metis Map.simps(1) Src.simps(1) Trg.simps(1) category.ideD(1) cell.simps(2)
          category_Hom ide_char'' ide_Id) 

    interpretation src: "functor" vcomp vcomp src
      using src_def arr_char Map.simps(1) Src.simps(1) Trg.simps(1) arr_dom category.ideD(1)
            ide_MkObj src_dom src_cod ide_Id
      apply unfold_locales
          apply auto[1]
         apply (simp add: category.ideD(1) category_Hom)
        apply auto[2]
    proof -
      fix g :: "('o, 'a) cell" and f :: "('o, 'a) cell"
      assume fg: "seq g f"
      thus "src (vcomp g f) = vcomp (src g) (src f)"
        using arr_char ide_MkObj src_dom src_cod src_def
        by (metis Src_vcomp comp_ide_self seqE)
    qed

    interpretation trg: "functor" vcomp vcomp trg
      using trg_def arr_char Map.simps(1) Src.simps(1) Trg.simps(1) arr_dom category.ideD(1)
            ide_MkObj trg_dom trg_cod ide_Id
      apply unfold_locales
          apply auto[1]
         apply (simp add: category.ideD(1) category_Hom)
        apply auto[2]
    proof -
      fix g :: "('o, 'a) cell" and f :: "('o, 'a) cell"
      assume fg: "seq g f"
      thus "trg (vcomp g f) = vcomp (trg g) (trg f)"
        using arr_char ide_MkObj trg_dom trg_cod trg_def
        by (metis Trg_vcomp comp_ide_self seqE)
    qed

    interpretation H: horizontal_homs vcomp src trg
      using ide_MkObj arr_char src_def trg_def src.preserves_arr trg.preserves_arr
      by unfold_locales auto

    lemma obj_MkObj:
    assumes "A ∈ Obj"
    shows "H.obj (MkObj A)"
      using assms src_def H.obj_def ide_MkObj by simp

    lemma MkCell_in_hom [intro]:
    assumes "A ∈ Obj" and "B ∈ Obj" and "partial_composition.arr (Hom A B) f"
    shows "H.in_hhom (MkCell A B f) (MkObj A) (MkObj B)"
    and "«MkCell A B f : MkCell A B (partial_composition.dom (Hom A B) f)
                            ⇒ MkCell A B (partial_composition.cod (Hom A B) f)»"
      using assms by auto

    text ‹
      Horizontal composition of horizontally composable arrows is now defined by applying
      the given function ‹Comp› to the ``Map'' components.
    ›

    definition hcomp
    where "hcomp μ ν ≡ if arr μ ∧ arr ν ∧ src μ = trg ν then
                         MkCell (Src ν) (Trg μ) (Comp (Trg μ) (Trg ν) (Src ν) (Map μ) (Map ν))
                       else
                         null"

    lemma arr_hcomp:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "arr (hcomp μ ν)"
    and "dom (hcomp μ ν) = hcomp (dom μ) (dom ν)"
    and "cod (hcomp μ ν) = hcomp (cod μ) (cod ν)"
    proof -
      have 1: "hcomp μ ν =
               MkCell (Src ν) (Trg μ) (Comp (Trg μ) (Trg ν) (Src ν) (Map μ) (Map ν))"
        using assms hcomp_def by simp
      have 2: "Src μ = Trg ν"
        using assms src_def trg_def by simp
      interpret Hom_μ: category ‹Hom (Src μ) (Trg μ)›
        using assms arr_char category_Hom by simp
      interpret Hom_ν: category ‹Hom (Src ν) (Trg ν)›
        using assms arr_char category_Hom by simp
      interpret Hom_μν: category ‹Hom (Src ν) (Trg μ)›
        using assms arr_char category_Hom by simp
      interpret Comp: binary_functor
                        ‹Hom (Trg ν) (Trg μ)› ‹Hom (Src ν) (Trg ν)› ‹Hom (Src ν) (Trg μ)›
                        ‹λ(f, g). Comp (Trg μ) (Trg ν) (Src ν) f g›
        using assms arr_char 2 binary_functor_Comp [of "Src ν" "Trg ν" "Trg μ"]
        by simp
      have 4: "Comp.A1xA2.arr (Map μ, Map ν)"
        using assms 2 arr_char Comp.A1xA2.arr_char by simp
      show 3: "arr (hcomp μ ν)"
        using assms 1 2 4 arr_char Comp.preserves_arr [of "(Map μ, Map ν)"]
        by simp
      show "dom (hcomp μ ν) = hcomp (dom μ) (dom ν)"
      proof -
        have "dom (hcomp μ ν) =
              MkCell (Src ν) (Trg μ)
                     (Hom_μν.dom (Comp (Trg μ) (Trg ν) (Src ν) (Map μ) (Map ν)))"
          using 1 3 dom_char by simp
        moreover have "Hom_μν.dom (Comp (Trg μ) (Trg ν) (Src ν) (Map μ) (Map ν)) =
                       Comp (Trg μ) (Trg ν) (Src ν) (Hom_μ.dom (Map μ)) (Hom_ν.dom (Map ν))"
          using 2 Comp.preserves_dom ‹Comp.A1xA2.arr (Map μ, Map ν)› by force
        ultimately show ?thesis
          using assms 2 dom_char hcomp_def arr_dom
          by auto metis
      qed
      show "cod (hcomp μ ν) = hcomp (cod μ) (cod ν)"
      proof -
        have "cod (hcomp μ ν) =
              MkCell (Src ν) (Trg μ)
                     (Hom_μν.cod (Comp (Trg μ) (Trg ν) (Src ν) (Map μ) (Map ν)))"
          using 1 3 cod_char by simp
        moreover have "Hom_μν.cod (Comp (Trg μ) (Trg ν) (Src ν) (Map μ) (Map ν)) =
                       Comp (Trg μ) (Trg ν) (Src ν) (Hom_μ.cod (Map μ)) (Hom_ν.cod (Map ν))"
          using 2 Comp.preserves_cod ‹Comp.A1xA2.arr (Map μ, Map ν)› by force
        ultimately show "cod (hcomp μ ν) = hcomp (cod μ) (cod ν)"
          using assms 2 cod_char hcomp_def arr_cod
          by auto metis
      qed
    qed

    lemma src_hcomp:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "src (hcomp μ ν) = src ν"
      using assms hcomp_def src_def arr_hcomp(1) by auto

    lemma trg_hcomp:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "trg (hcomp μ ν) = trg μ"
      using assms hcomp_def trg_def arr_hcomp(1) by auto

    lemma Src_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "Src (hcomp μ ν) = Src ν"
      using assms hcomp_def by simp

    lemma Trg_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "Trg (hcomp μ ν) = Trg μ"
      using assms hcomp_def by simp

    lemma Map_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "Map (hcomp μ ν) = Comp (Trg μ) (Trg ν) (Src ν) (Map μ) (Map ν)"
      using assms hcomp_def by simp

    lemma hcomp_vcomp:
    assumes "H.VV.seq g f"
    shows "hcomp (fst (H.VV.comp g f)) (snd (H.VV.comp g f)) =
           vcomp (hcomp (fst g) (snd g)) (hcomp (fst f) (snd f))"
    proof -
      let ?f1 = "fst f" and ?f2 = "snd f" and ?g1 = "fst g" and ?g2 = "snd g"
      have 1: "Src ?f1 ∈ Obj ∧ Trg ?f1 ∈ Obj ∧ Src ?f2 ∈ Obj ∧ Trg ?f2 ∈ Obj ∧
               Src ?g1 ∈ Obj ∧ Trg ?g1 ∈ Obj ∧ Src ?g2 ∈ Obj ∧ Trg ?g2 ∈ Obj"
        using assms arr_char H.VV.arrE by blast
      interpret Hom_f1: category ‹Hom (Src ?f1) (Trg ?f1)›
        using assms 1 category_Hom by simp
      interpret Hom_f2: category ‹Hom (Src ?f2) (Trg ?f2)›
        using assms 1 category_Hom by simp
      interpret Hom_g1: category ‹Hom (Src ?g1) (Trg ?g1)›
        using assms 1 category_Hom by simp
      interpret Hom_g2: category ‹Hom (Src ?g2) (Trg ?g2)›
        using assms 1 category_Hom by simp
      interpret Hom_f: category ‹Hom (Src ?f2) (Trg ?f1)›
        using assms 1 category_Hom by simp
      interpret Hom_g: category ‹Hom (Src ?g2) (Trg ?g1)›
        using assms 1 category_Hom by simp
      interpret Comp_f: binary_functor ‹Hom (Trg ?f2) (Trg ?f1)› ‹Hom (Src ?f2) (Trg ?f2)›
                          ‹Hom (Src ?f2) (Trg ?f1)›
                          ‹λ(fa, g). Comp (Trg ?f1) (Trg ?f2) (Src ?f2) fa g›
        using assms 1 arr_char binary_functor_Comp by simp

      have "hcomp (fst (H.VV.comp g f)) (snd (H.VV.comp g f)) =
            MkCell (Src (snd (H.VV.comp g f))) (Trg (fst (H.VV.comp g f)))
                   (Comp (Trg (fst (H.VV.comp g f))) (Trg (snd (H.VV.comp g f)))
                         (Src (snd (H.VV.comp g f)))
                         (Map (fst (H.VV.comp g f))) (Map (snd (H.VV.comp g f))))"
        using assms hcomp_def H.VV.arrE
        by (metis (no_types, lifting))
      also have "... = MkCell (Src ?f2) (Trg ?f1)
                              (Hom (Src ?f2) (Trg ?f1)
                                   (Comp (Trg ?f1) (Trg ?g2) (Src ?f2) (Map ?g1) (Map ?g2))
                                   (Comp (Trg ?f1) (Trg ?f2) (Src ?f2) (Map ?f1) (Map ?f2)))"
      proof -
        have "Src (snd (H.VV.comp g f)) = Src ?f2"
          using assms arr_char src_def H.VV.comp_char H.VV.seq_char⇩S⇩b⇩C
          by (metis (no_types, lifting) H.vseq_implies_hpar(1) Src.simps(1) H.VV.arrE
              H.VV.inclusion H.VxV.comp_arr_dom H.VxV.dom_comp H.VxV.seqE⇩P⇩C)
        moreover have "Trg (fst (H.VV.comp g f)) = Trg ?f1"
          by (metis (no_types, lifting) H.VV.comp_arr_dom H.VV.comp_simp H.VV.seq_char⇩S⇩b⇩C
              H.VxV.arr_char H.VxV.cod_comp H.VxV.comp_cod_arr H.VxV.seqE⇩P⇩C
              H.vseq_implies_hpar(2) Src_trg assms)
        moreover have
            "Comp (Trg (fst (H.VV.comp g f))) (Trg (snd (H.VV.comp g f)))
                  (Src (snd (H.VV.comp g f)))
                  (Map (fst (H.VV.comp g f))) (Map (snd (H.VV.comp g f))) =
             Hom (Src ?f2) (Trg ?f1)
                 (Comp (Trg ?f1) (Trg ?g2) (Src ?f2) (Map ?g1) (Map ?g2))
                 (Comp (Trg ?f1) (Trg ?f2) (Src ?f2) (Map ?f1) (Map ?f2))"
        proof -
          have "Comp (Trg (fst (H.VV.comp g f))) (Trg (snd (H.VV.comp g f)))
                     (Src (snd (H.VV.comp g f)))
                     (Map (fst (H.VV.comp g f))) (Map (snd (H.VV.comp g f))) =
                Comp (Trg ?g1) (Trg ?g2) (Src ?g2)
                     (Map (vcomp ?g1 ?f1)) (Map (vcomp ?g2 ?f2))"
            using assms H.VV.comp_char H.VV.arr_char⇩S⇩b⇩C H.VxV.comp_char by auto  (* 10 sec *)
          also have "... = Comp (Trg ?g1) (Trg ?g2) (Src ?g2)
                                (Hom (Src ?g1) (Trg ?g1) (Map ?g1) (Map ?f1))
                                (Hom (Src ?g2) (Trg ?g2) (Map ?g2) (Map ?f2))"
            using assms H.VV.seq_char⇩S⇩b⇩C Map_vcomp H.VxV.seq_char by auto
          also have "... = Hom (Src ?f2) (Trg ?f1)
                               (Comp (Trg ?f1) (Trg ?g2) (Src ?f2)
                                     (Map ?g1) (Map ?g2))
                               (Comp (Trg ?f1) (Trg ?f2) (Src ?f2)
                                     (Map ?f1) (Map ?f2))"
          proof -
            have 2: "Src ?g1 = Trg ?g2"
              using assms H.VV.arr_char⇩S⇩b⇩C [of g] src_def [of "?g1"] trg_def [of "?g2"] by auto
            have "Comp (Trg ?f1) (Trg ?f2) (Src ?f2)
                       (Hom (Trg ?g2) (Trg ?g1) (Map ?g1) (Map ?f1))
                       (Hom (Src ?g2) (Trg ?g2) (Map ?g2) (Map ?f2)) =
                  Hom (Src ?f2) (Trg ?f1)
                      (Comp (Trg ?f1) (Trg ?f2) (Src ?f2)
                            (Map ?g1) (Map ?g2))
                      (Comp (Trg ?f1) (Trg ?f2) (Src ?f2)
                            (Map ?f1) (Map ?f2))"
            proof -
              have "Comp_f.A1xA2.seq (Map ?g1, Map ?g2) (Map ?f1, Map ?f2)"
                using assms 2 H.VV.seq_char⇩S⇩b⇩C
                by (metis (no_types, lifting) Comp_f.A1xA2.seq_char H.VxV.seqE⇩P⇩C
                    fst_conv seq_char snd_conv)
              moreover have
                "Comp_f.A1xA2.comp (Map ?g1, Map ?g2) (Map ?f1, Map ?f2) =
                 (Hom (Src ?g1) (Trg ?g1) (Map ?g1) (Map ?f1),
                  Hom (Src ?g2) (Trg ?g2) (Map ?g2) (Map ?f2))"
                using assms 2 H.VV.seq_char⇩S⇩b⇩C H.VxV.seqE⇩P⇩C seq_char
                by (metis (no_types, lifting) Comp_f.A1xA2.comp_char fst_conv snd_conv)
              ultimately show ?thesis
                by (metis 2 Comp_f.as_nat_trans.preserves_comp_2 old.prod.case)
            qed
            thus ?thesis using assms 2 H.VV.seq_char⇩S⇩b⇩C H.VxV.seqE⇩P⇩C seq_char
              by (metis (no_types, lifting))
          qed
          finally show ?thesis by blast
        qed
        ultimately show ?thesis by blast
      qed
      also have "... = vcomp (hcomp ?g1 ?g2) (hcomp ?f1 ?f2)"
      proof -
        have 2: "Trg ?g1 = Trg ?f1 ∧ Src ?g2 = Src ?f2 ∧ Src ?f1 = Trg ?f2"
          using assms seq_char H.VV.seq_char⇩S⇩b⇩C H.VxV.seqE⇩P⇩C
          by (metis (no_types, lifting) H.VV.arr_char⇩S⇩b⇩C Src_src Src_trg)
        have "Hom_f.seq (Comp (Trg ?f1) (Trg ?g2) (Src ?f2)
                              (Map ?g1) (Map ?g2))
                        (Comp (Trg ?f1) (Trg ?f2) (Src ?f2)
                              (Map ?f1) (Map ?f2))"
          by (metis (no_types, lifting) 2 Comp_f.A1xA2.seqI⇩P⇩C Comp_f.preserves_seq H.VV.seq_char⇩S⇩b⇩C
              H.VxV.seqE⇩P⇩C arr_char assms case_prod_conv vcomp_def)
        moreover have "?f1 ≠ Null ∧ ?f2 ≠ Null ∧ src ?f1 = trg ?f2 ∧
                       ?g1 ≠ Null ∧ ?g2 ≠ Null ∧ src ?g1 = trg ?g2"
          using assms H.VV.arr_char⇩S⇩b⇩C arr_char assms by blast
        moreover have "Hom_f1.arr (Map ?f1) ∧ Hom_f2.arr (Map ?f2)"
          using assms seq_char H.VV.arrE H.VV.seqE arr_char by fast
        moreover have "Hom_g1.arr (Map ?g1) ∧ Hom_g2.arr (Map ?g2)"
          using assms seq_char H.VV.arrE H.VV.seqE arr_char by meson
        ultimately show ?thesis
          using 1 2 arr_char hcomp_def vcomp_def by auto
      qed
      finally show ?thesis by simp
    qed

    interpretation H: "functor" H.VV.comp vcomp ‹λμν. hcomp (fst μν) (snd μν)›
      using hcomp_def arr_hcomp hcomp_vcomp H.VV.arr_char⇩S⇩b⇩C H.VV.dom_char⇩S⇩b⇩C H.VV.cod_char⇩S⇩b⇩C
      by unfold_locales auto

    interpretation H: horizontal_composition vcomp hcomp src trg
      using src_hcomp trg_hcomp arr_char hcomp_def null_char
      by unfold_locales auto

    lemma Map_obj:
    assumes "H.obj a"
    shows "Map a = Id (Src a)" and "Map a = Id (Trg a)"
      using assms H.obj_def Map_src Map_trg H.obj_simps(3) by metis+

    lemma MkCell_simps:
    assumes "A ∈ Obj" and "B ∈ Obj" and "partial_composition.arr (Hom A B) f"
    shows "arr (MkCell A B f)"
    and "src (MkCell A B f) = MkObj A" and "trg (MkCell A B f) = MkObj B"
    and "dom (MkCell A B f) = MkCell A B (partial_composition.dom (Hom A B) f)"
    and "cod (MkCell A B f) = MkCell A B (partial_composition.cod (Hom A B) f)"
      using assms MkCell_in_hom by auto

    text ‹
      Next, define the associativities and show that they are the components of a
      natural isomorphism.
    ›

    definition assoc
    where "assoc f g h ≡
           if H.VVV.ide (f, g, h) then
             MkCell (Src h) (Trg f)
                    (Assoc (Trg f) (Trg g) (Trg h) (Src h) (Map f) (Map g) (Map h))
           else null"

    lemma assoc_in_hom [intro]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "«assoc f g h : hcomp (hcomp f g) h ⇒ hcomp f (hcomp g h)»"
    proof -
      let ?A = "Src h" and ?B = "Trg h" and ?C = "Trg g" and ?D = "Trg f"
      interpret Hom_f: category ‹Hom ?C ?D›
        using assms ide_char arr_char dom_char cod_char category_Hom by simp
      interpret Hom_g: category ‹Hom ?B ?C›
        using assms ide_char arr_char dom_char cod_char category_Hom by simp
      interpret Hom_h: category ‹Hom ?A ?B›
        using assms ide_char arr_char dom_char cod_char category_Hom by simp
      interpret Hom_gh: product_category ‹Hom ?B ?C› ‹Hom ?A ?B› ..
      interpret Hom_f_gh: product_category ‹Hom ?C ?D› Hom_gh.comp ..
      interpret Comp_fg: binary_functor ‹Hom ?C ?D› ‹Hom ?B ?C› ‹Hom ?B ?D›
                           ‹λ(fa, g). Comp ?D ?C ?B fa g›
        using assms arr_char ide_char'' binary_functor_Comp [of ?B ?C ?D] by simp
      interpret α: natural_isomorphism Hom_f_gh.comp ‹Hom (Src h) (Trg f)›
                     ‹λ(fa, ga, ha). Comp ?D ?B ?A (Comp ?D ?C ?B fa ga) ha›
                     ‹λ(fa, ga, ha). Comp ?D ?C ?A fa (Comp ?C ?B ?A ga ha)›
                     ‹λ(fa, ga, ha). Assoc ?D ?C ?B ?A fa ga ha›
        using assms ide_char arr_char natural_isomorphism_Assoc [of ?A ?B ?C ?D]
        by blast
      show ?thesis
      proof
        have 1: "Src f = Trg g ∧ Src g = Trg h"
          using assms src_def trg_def by simp
        have 2: "Hom_f.ide (Map f) ∧ Hom_g.ide (Map g) ∧ Hom_h.ide (Map h)"
          using assms 1 ide_char' [of f] arr_char [of f]
          by (simp add: ide_char'')
        show 3: "arr (assoc f g h)"
          unfolding assoc_def
          using assms arr_char ide_char'' H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C H.VVV.ide_char⇩S⇩b⇩C
                src_def trg_def α.preserves_reflects_arr [of "(Map f, Map g, Map h)"]
                Hom_f_gh.arr_char Hom_gh.arr_char
          by simp
        show "dom (assoc f g h) = hcomp (hcomp f g) h"
        proof -
          have  "arr (MkCell ?B ?D (Comp ?D ?C ?B (Map f) (Map g)))"
            by (metis assms(1-2,4) 1 Map_hcomp Src_hcomp Trg_hcomp arr_MkCell arr_char
                arr_hcomp(1) ideD(1))
          moreover have "MkObj ?B = trg h"
            using assms ide_char'' arr_char MkCell_Map null_char trg_MkCell by metis
          ultimately show ?thesis
            unfolding hcomp_def
            using assms 1 2 3 arr_char ide_char'' assoc_def dom_MkCell H.VV.arr_char⇩S⇩b⇩C
                  H.VVV.arr_char⇩S⇩b⇩C H.VVV.ide_char⇩S⇩b⇩C src_MkCell trg_MkCell α.preserves_dom
            by force
        qed
        show "cod (assoc f g h) = hcomp f (hcomp g h)"
        proof -
          have "trg g = MkObj ?C"
            using assms ide_char'' arr_char MkCell_Map null_char trg_MkCell by metis
          thus ?thesis
            unfolding hcomp_def
            using assms 2 3 α.preserves_cod src_MkCell trg_MkCell H.hseqI' hcomp_def
                  assms arr_char ide_char'' assoc_def cod_MkCell H.VV.arr_char⇩S⇩b⇩C
                  H.VVV.arr_char⇩S⇩b⇩C H.VVV.ide_char⇩S⇩b⇩C
            by force
        qed
      qed
    qed

    lemma assoc_simps [simp]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "arr (assoc f g h)"
    and "dom (assoc f g h) = hcomp (hcomp f g) h"
    and "cod (assoc f g h) = hcomp f (hcomp g h)"
      using assms assoc_in_hom by auto

    lemma assoc_simps' [simp]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "src (assoc f g h) = src h"
    and "trg (assoc f g h) = trg f"
    and "Src (assoc f g h) = Src h"
    and "Trg (assoc f g h) = Trg f"
    and "Map (assoc f g h) = Assoc (Trg f) (Trg g) (Trg h) (Src h) (Map f) (Map g) (Map h)"
    proof -
      show "src (assoc f g h) = src h"
        using assms src_hcomp src_dom src_def src_MkCell assoc_simps(1) assoc_def
        by (metis (no_types, lifting) ideD(1) not_arr_null)
      show "trg (assoc f g h) = trg f"
        using assms trg_hcomp trg_hcomp trg_cod H.hseqI'
        by (metis assoc_simps(1,3) ideD(1))
      show "Src (assoc f g h) = Src h"
        using assms Src_hcomp Src_dom
        by (metis (no_types, lifting) Src.simps(1) arr_char assoc_def assoc_simps(1) null_char)
      show "Trg (assoc f g h) = Trg f"
        using assms Trg_hcomp Trg_dom
        by (metis (no_types, lifting) Trg.simps(1) arr_char assoc_def assoc_simps(1) null_char)
      show "Map (assoc f g h) = Assoc (Trg f) (Trg g) (Trg h) (Src h) (Map f) (Map g) (Map h)"
        using assms Map_hcomp Map_dom
        by (metis (no_types, lifting) Map.simps(1) arr_char assoc_def assoc_simps(1) null_char)
    qed

    lemma iso_assoc:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "iso (assoc f g h)"
    proof -
      let ?A = "Src h" and ?B = "Trg h" and ?C = "Trg g" and ?D = "Trg f"
      interpret Hom_f: category ‹Hom ?C ?D›
        using assms ide_char arr_char dom_char cod_char category_Hom by simp
      interpret Hom_g: category ‹Hom ?B ?C›
        using assms ide_char arr_char dom_char cod_char category_Hom by simp
      interpret Hom_h: category ‹Hom ?A ?B›
        using assms ide_char arr_char dom_char cod_char category_Hom by simp
      interpret Hom_fg: product_category ‹Hom ?C ?D› ‹Hom ?B ?C› ..
      interpret Hom_gh: product_category ‹Hom ?B ?C› ‹Hom ?A ?B› ..
      interpret Hom_f_gh: product_category ‹Hom ?C ?D› Hom_gh.comp ..
      interpret α: natural_isomorphism Hom_f_gh.comp ‹Hom (Src h) (Trg f)›
                     ‹λ(fa, ga, ha). Comp ?D ?B ?A (Comp ?D ?C ?B fa ga) ha›
                     ‹λ(fa, ga, ha). Comp ?D ?C ?A fa (Comp ?C ?B ?A ga ha)›
                     ‹λ(fa, ga, ha). Assoc ?D ?C ?B ?A fa ga ha›
        using assms ide_char arr_char natural_isomorphism_Assoc [of ?A ?B ?C ?D]
        by blast
      show ?thesis
        using assms α.components_are_iso [of "(Map f, Map g, Map h)"]
              iso_char H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C H.VVV.ide_char ide_char''
        by (simp add: src_def trg_def)
    qed

    lemma assoc_naturality:
    assumes "arr f" and "arr g" and "arr h" and "src f = trg g" and "src g = trg h"
    shows "vcomp (H.HoVH (f, g, h)) (assoc (dom f) (dom g) (dom h)) =
           vcomp (assoc (cod f) (cod g) (cod h)) (H.HoHV (f, g, h))"
    proof -
      let ?A = "Src h" and ?B = "Trg h" and ?C = "Trg g" and ?D = "Trg f"
      have 1: "Src f = Trg g ∧ Src g = Trg h"
        using assms src_def trg_def by simp
      interpret Hom_f: category ‹Hom ?C ?D›
        using assms ide_char arr_char dom_char cod_char category_Hom by simp
      interpret Hom_g: category ‹Hom ?B ?C›
        using assms ide_char arr_char dom_char cod_char category_Hom by simp
      interpret Hom_h: category ‹Hom ?A ?B›
        using assms ide_char arr_char dom_char cod_char category_Hom by simp
      interpret Hom_fg: product_category ‹Hom ?C ?D› ‹Hom ?B ?C› ..
      interpret Hom_gh: product_category ‹Hom ?B ?C› ‹Hom ?A ?B› ..
      interpret Hom_fg_h: product_category Hom_fg.comp ‹Hom ?A ?B› ..
      interpret Hom_f_gh: product_category ‹Hom ?C ?D› Hom_gh.comp ..
      interpret Hom: category ‹Hom ?A ?D›
        using assms ide_char arr_char dom_char cod_char category_Hom by simp
      interpret Comp_fg: binary_functor ‹Hom ?C ?D› ‹Hom ?B ?C› ‹Hom ?B ?D›
                           ‹λ(f', g). Comp ?D ?C ?B f' g›
        using assms arr_char ide_char'' binary_functor_Comp [of ?B ?C ?D] by simp
      interpret Comp_gh: binary_functor ‹Hom ?B ?C› ‹Hom ?A ?B› ‹Hom ?A ?C›
                           ‹λ(f', g). Comp ?C ?B ?A f' g›
        using assms arr_char ide_char'' binary_functor_Comp [of ?A ?B ?C] by simp
      interpret Comp_fg_h: binary_functor ‹Hom ?B ?D› ‹Hom ?A ?B› ‹Hom ?A ?D›
                           ‹λ(f', g). Comp ?D ?B ?A f' g›
        using assms arr_char ide_char'' binary_functor_Comp [of ?A ?B ?D] by simp
      interpret Comp_f_gh: binary_functor ‹Hom ?C ?D› ‹Hom ?A ?C› ‹Hom ?A ?D›
                           ‹λ(f', g). Comp ?D ?C ?A f' g›
        using assms arr_char ide_char'' binary_functor_Comp [of ?A ?C ?D] by simp
      interpret α: natural_isomorphism Hom_f_gh.comp ‹Hom ?A ?D›
                     ‹λ(f', g', h'). Comp ?D ?B ?A (Comp ?D ?C ?B f' g') h'›
                     ‹λ(f', g', h'). Comp ?D ?C ?A f' (Comp ?C ?B ?A g' h')›
                     ‹λ(f', g', h'). Assoc ?D ?C ?B ?A f' g' h'›
        using assms ide_char arr_char natural_isomorphism_Assoc [of ?A ?B ?C ?D]
        by blast

      have ide_Map_dom:
             "Hom_f.ide (Map (dom f)) ∧ Hom_g.ide (Map (dom g)) ∧ Hom_h.ide (Map (dom h))"
        using assms 1 ide_char'' arr_char by simp
      have ide_Map_cod:
             "Hom_f.ide (Map (cod f)) ∧ Hom_g.ide (Map (cod g)) ∧ Hom_h.ide (Map (cod h))"
        using assms 1 ide_char'' arr_char by simp

      have "vcomp (H.HoVH (f, g, h)) (assoc (dom f) (dom g) (dom h)) =
            vcomp (hcomp f (hcomp g h))
                  (MkCell (Src (dom h)) (Trg (dom f))
                          (Assoc (Trg (dom f)) (Trg (dom g)) (Trg (dom h)) (Src (dom h))
                                 (Map (dom f)) (Map (dom g)) (Map (dom h))))"
        using assms 1 H.HoVH_def H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C H.VVV.ide_char⇩S⇩b⇩C
              assoc_def assoc_in_hom
         by simp
      also have "... = MkCell (Src (dom h)) (Trg (dom f))
                              (Hom (Src (dom h)) (Trg (dom f))
                                   (Comp (Trg (dom f)) (Trg g) (Src (dom h)) (Map f)
                                         (Comp (Trg g) (Trg h) (Src (dom h)) (Map g) (Map h)))
                                   (Assoc (Trg (dom f)) (Trg (dom g)) (Trg (dom h)) (Src (dom h))
                                          (Map (dom f)) (Map (dom g)) (Map (dom h))))"
      proof -
        have "Hom.seq (Comp ?D ?C ?A (Map f) (Comp ?C ?B ?A (Map g) (Map h)))
                      (Assoc ?D (Trg (dom g)) (Trg (dom h)) ?A
                             (Map (dom f)) (Map (dom g)) (Map (dom h)))"
        proof (intro Hom.seqI)
          show "Hom.arr (Assoc ?D (Trg (dom g)) (Trg (dom h)) ?A
                               (Map (dom f)) (Map (dom g)) (Map (dom h)))"
          proof -
            have "Hom.arr (Assoc ?D (Trg (dom g)) (Trg (dom h)) ?A
                                 (Map (dom f)) (Map (dom g)) (Map (dom h)))"
              using assms 1 arr_char Trg_dom Src_dom ide_Map_dom
                    α.preserves_reflects_arr [of "(Map (dom f), Map (dom g), Map (dom h))"]
              by simp
            thus ?thesis
              using assms 1 arr_char Src_dom Trg_dom assoc_simps(1-2) assoc_def
                    H.VV.ide_char H.VV.arr_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C ide_Map_dom
              by simp
          qed
          show "Hom.arr (Comp ?D ?C ?A (Map f) (Comp ?C ?B ?A (Map g) (Map h)))"
          proof -
            have "Hom.arr (Comp ?D ?C ?A (Map f) (Comp ?C ?B ?A (Map g) (Map h)))"
              using assms 1 arr_char
                    Comp_f_gh.preserves_reflects_arr [of "(Map f, Comp ?C ?B ?A (Map g) (Map h))"]
                    Comp_gh.preserves_reflects_arr [of "(Map g, Map h)"] Src_dom Trg_dom
              by simp
            thus ?thesis
              using assms 1 arr_char Src_dom Trg_dom by simp
          qed
          show "Hom.dom (Comp ?D ?C ?A (Map f) (Comp ?C ?B ?A (Map g) (Map h))) =
                Hom.cod (Assoc ?D (Trg (dom g)) (Trg (dom h)) ?A
                        (Map (dom f)) (Map (dom g)) (Map (dom h)))"
          proof -
            have "Hom.cod (Assoc ?D (Trg (dom g)) (Trg (dom h)) ?A
                          (Map (dom f)) (Map (dom g)) (Map (dom h))) =
                  Hom.cod (Map (assoc (dom f) (dom g) (dom h)))"
              using Src_dom Trg_dom assms(1-5) assoc_simps'(5) ide_dom src_dom trg_dom
              by presburger
            also have "... = Comp ?D ?C ?A
                                  (Map (dom f))
                                  (Comp ?C ?B ?A (Map (dom g)) (Map (dom h)))"
            proof -
              have "dom f ≠ Null ∧ dom g ≠ Null ∧ dom h ≠ Null"
                using arr_dom assms not_arr_null null_char by fastforce
              moreover have "Hom.cod (Map (assoc (dom f) (dom g) (dom h))) =
                             Comp ?D ?C ?A
                                  (Map (dom f))
                                  (Comp ?C ?B ?A (Map (dom g)) (Map (dom h)))"
                using assms assoc_simps'(5) ide_Map_dom
                      α.preserves_cod [of "(Map (dom f), Map (dom g), Map (dom h))"]
                by simp
              ultimately show ?thesis
                using assms 1 arr_char assoc_def H.VV.ide_char H.VV.arr_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C
                      Src_dom Trg_dom ide_Map_dom null_char assoc_simps'(5)
                by simp
            qed
            also have "... =
                       Hom.dom (Comp ?D ?C ?A (Map f) (Comp ?C ?B ?A (Map g) (Map h)))"
            proof -
              have "arr (MkCell ?A ?C (Comp ?C ?B ?A (Map g) (Map h)))"
                using assms 1 arr_char arr_MkCell
                      Comp_gh.preserves_reflects_arr [of "(Map g, Map h)"]
                by simp
              thus ?thesis
                using assms arr_char 1 Map_dom
                      Comp_f_gh.preserves_dom [of "(Map f, Comp ?C ?B ?A (Map g) (Map h))"]
                      Comp_gh.preserves_dom [of "(Map g, Map h)"]
                by simp
            qed
            finally show ?thesis by argo
          qed
        qed
        thus ?thesis
          using assms(1-5) H.hseqI' arr_char vcomp_def by auto
      qed
      also have "... = MkCell (Src h) (Trg f)
                              (Hom (Src h) (Trg f)
                                   (Assoc (Trg f) (Trg (cod g)) (Trg (cod h)) (Src h)
                                          (Map (cod f)) (Map (cod g)) (Map (cod h)))
                                   (Comp (Trg f) (Trg h) (Src h)
                                         (Comp (Trg f) (Trg g) (Src g) (Map f) (Map g)) (Map h)))"
        using assms 1 arr_char α.naturality [of "(Map f, Map g, Map h)"] by simp
      also have "... = vcomp (MkCell (Src (cod h)) (Trg (cod f))
                                     (Assoc (Trg (cod f)) (Trg (cod g)) (Trg (cod h)) (Src (cod h))
                                            (Map (cod f)) (Map (cod g)) (Map (cod h))))
                             (hcomp (hcomp f g) h)"
      proof -
        have "arr (MkCell ?B ?D (Comp ?D ?C ?B (Map f) (Map g)))"
          using assms 1 arr_char arr_MkCell
                Comp_fg.preserves_reflects_arr [of "(Map f, Map g)"]
          by simp
        moreover have
                   "Hom.arr (Comp ?D ?B ?A (Comp ?D ?C ?B (Map f) (Map g)) (Map h))"
          using assms 1 arr_char Comp_fg.preserves_reflects_arr [of "(Map f, Map g)"]
                Comp_fg_h.preserves_reflects_arr [of "(Comp ?D ?C ?B (Map f) (Map g), Map h)"]
          by simp
        moreover have "Hom.arr (Assoc ?D (Trg (cod g)) (Trg (cod h)) ?A
                                         (Map (cod f)) (Map (cod g)) (Map (cod h)))"
          using assms 1 arr_char Trg_cod ide_Map_cod
                α.preserves_reflects_arr [of "(Map (cod f), Map (cod g), Map (cod h))"]
          by simp
        moreover have "Hom.seq (Assoc ?D (Trg (cod g)) (Trg (cod h)) ?A
                                      (Map (cod f)) (Map (cod g)) (Map (cod h)))
                               (Comp ?D ?B ?A (Comp ?D ?C ?B (Map f) (Map g)) (Map h))"
        proof (intro Hom.seqI)
          show "Hom.arr (Comp ?D ?B ?A (Comp ?D ?C ?B (Map f) (Map g)) (Map h))"
            using assms 1 arr_char Comp_fg.preserves_reflects_arr [of "(Map f, Map g)"]
                  Comp_fg_h.preserves_reflects_arr [of "(Comp ?D ?C ?B (Map f) (Map g), Map h)"]
            by simp
          show "Hom.arr (Assoc ?D (Trg (cod g)) (Trg (cod h)) ?A
                            (Map (cod f)) (Map (cod g)) (Map (cod h)))"
            using assms 1 arr_char Trg_cod ide_Map_cod
                  α.preserves_reflects_arr [of "(Map (cod f), Map (cod g), Map (cod h))"]
            by simp
          show "Hom.dom (Assoc ?D (Trg (cod g)) (Trg (cod h)) ?A
                        (Map (cod f)) (Map (cod g)) (Map (cod h))) =
                Hom.cod (Comp ?D ?B ?A (Comp ?D ?C ?B (Map f) (Map g)) (Map h))"
          proof -
            have "Hom.dom (Assoc ?D (Trg (cod g)) (Trg (cod h)) ?A
                          (Map (cod f)) (Map (cod g)) (Map (cod h))) =
                  Hom.dom (Map (assoc (cod f) (cod g) (cod h)))"
              using H.cod_trg Src_cod Trg_cod assms(1-5) assoc_simps'(5) ide_cod src_cod
                    trg.preserves_cod
              by presburger
            also have "... = Comp ?D ?B ?A
                                  (Comp ?D ?C ?B (Map (cod f)) (Map (cod g))) (Map (cod h))"
            proof -
              have "cod f ≠ Null ∧ cod g ≠ Null ∧ cod h ≠ Null"
                using arr_cod assms not_arr_null null_char by fastforce
              moreover have "Hom.dom (Map (assoc (cod f) (cod g) (cod h))) =
                             Comp ?D ?B ?A
                                  (Comp ?D ?C ?B (Map (cod f)) (Map (cod g))) (Map (cod h))"
                using assms assoc_simps'(5) ide_Map_cod
                      α.preserves_dom [of "(Map (cod f), Map (cod g), Map (cod h))"]
                by simp
              ultimately show ?thesis
                using assms 1 arr_char assoc_def H.VV.ide_char H.VV.arr_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C
                      Src_cod Trg_cod ide_Map_cod null_char assoc_simps'(5)
                by simp
            qed
            also have "... =
                       Hom.cod (Comp ?D ?B ?A (Comp ?D ?C ?B (Map f) (Map g)) (Map h))"
              using assms arr_char 1 Map_cod arr_MkCell
                    Comp_fg_h.preserves_cod [of "(Comp ?D ?C ?B (Map f) (Map g), Map h)"]
                    Comp_fg.preserves_cod [of "(Map f, Map g)"]
                    Comp_fg.preserves_reflects_arr [of "(Map f, Map g)"]
              by simp
            finally show ?thesis by blast
          qed
        qed
        ultimately show ?thesis
          using assms arr_char vcomp_def hcomp_def Src_cod Trg_cod
                H.VV.ide_char H.VV.arr_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C src_def trg_def
          by simp
      qed
      also have "... = vcomp (assoc (cod f) (cod g) (cod h)) (H.HoHV (f, g, h))"
        using assms 1 H.HoHV_def H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C H.VVV.ide_char⇩S⇩b⇩C
              assoc_def assoc_in_hom
         by simp
      finally show "vcomp (H.HoVH (f, g, h)) (assoc (dom f) (dom g) (dom h)) =
                    vcomp (assoc (cod f) (cod g) (cod h)) (H.HoHV (f, g, h))"
        by blast
    qed

    interpretation α⇩0: transformation_by_components H.VVV.comp vcomp H.HoHV H.HoVH
                         ‹λ(f, g, h). assoc f g h›
    proof
      fix fgh
      show "H.VVV.ide fgh ⟹
              «case fgh of (f, g, h) ⇒ assoc f g h : H.HoHV fgh ⇒ H.HoVH fgh»"
        using assoc_in_hom H.HoHV_def H.HoVH_def H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C H.VVV.ide_char⇩S⇩b⇩C
        by (cases fgh) simp
      assume fgh: "H.VVV.arr fgh"
      show "vcomp (case H.VVV.cod fgh of (f, g, h) ⇒ assoc f g h) (H.HoHV fgh) =
            vcomp (H.HoVH fgh) (case H.VVV.dom fgh of (f, g, h) ⇒ assoc f g h)"
        using fgh assoc_simps H.HoHV_def assoc_naturality
              H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C H.VVV.dom_char⇩S⇩b⇩C H.VVV.cod_char⇩S⇩b⇩C
        by (cases fgh) simp
    qed

    definition 𝖺  ("𝖺[_,_,_]")
    where "𝖺 f g h == α⇩0.map (f, g, h)"

    lemma 𝖺_simp_ide:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "𝖺[f, g, h] =
           MkCell (Src h) (Trg f)
                  (Assoc (Trg f) (Trg g) (Trg h) (Src h) (Map f) (Map g) (Map h))"
      using assms 𝖺_def assoc_def assoc_simps' MkCell_Map not_arr_null
            α⇩0.map_simp_ide H.VVV.ide_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C
      by simp

    interpretation α: natural_isomorphism H.VVV.comp vcomp H.HoHV H.HoVH
                        ‹λfgh. 𝖺 (fst fgh) (fst (snd fgh)) (snd (snd fgh))›
    proof -
      interpret α: natural_isomorphism H.VVV.comp vcomp H.HoHV H.HoVH α⇩0.map
        using α⇩0.map_simp_ide iso_assoc H.VVV.ide_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C
        by unfold_locales auto
      show "natural_isomorphism H.VVV.comp vcomp H.HoHV H.HoVH
              (λfgh. 𝖺 (fst fgh) (fst (snd fgh)) (snd (snd fgh)))"
        using α.natural_isomorphism_axioms 𝖺_def by simp
    qed

    text ‹
      What remains is to show that horizontal composition with source or target defines
      fully faithful functors.
    ›

    interpretation endofunctor vcomp H.L
        using H.endofunctor_L by auto
    interpretation endofunctor vcomp H.R
      using H.endofunctor_R by auto

    interpretation R: fully_faithful_functor vcomp vcomp H.R
    proof
      show "⋀f f'. ⟦par f f'; H.R f = H.R f'⟧ ⟹ f = f'"
      proof -
        fix μ μ'
        assume par: "par μ μ'"
        and eq: "H.R μ = H.R μ'"
        have 1: "Src μ' = Src μ ∧ Trg μ' = Trg μ"
          using par by (metis Src_dom Trg_dom)
        interpret Hom: category ‹Hom (Src μ) (Trg μ)›
          using par arr_char category_Hom by simp
        let ?R = "λf. if Hom.arr f
                      then Comp (Trg μ) (Src μ) (Src μ) f (Id (Src μ))
                      else Hom.null"
        interpret R: fully_faithful_functor ‹Hom (Src μ) (Trg μ)› ‹Hom (Src μ) (Trg μ)› ?R
          using par arr_char right_unit_Id by simp
        have Rμ: "H.R μ = MkCell (Src μ) (Trg μ)
                                 (Comp (Trg μ) (Src μ) (Src μ) (Map μ) (Id (Src μ)))"
          unfolding hcomp_def
          using par src_def null_char H.trg_src src.preserves_arr by simp
        have Rμ': "H.R μ' = MkCell (Src μ) (Trg μ)
                                   (Comp (Trg μ) (Src μ) (Src μ) (Map μ') (Id (Src μ)))"
          unfolding hcomp_def
          using par 1 src_def null_char H.trg_src src.preserves_arr by simp
        have "Map μ = Map μ'"
          using Rμ Rμ' eq par arr_char eq R.is_faithful
          by (metis "1" Map_cod Map_dom cell.inject)
        thus "μ = μ'"
          using 1 par MkCell_Map by (metis arr_char null_char)
      qed
      show "⋀f g ν. ⟦ide f; ide g; «ν : H.R f ⇒ H.R g»⟧ ⟹ ∃μ. «μ : f ⇒ g» ∧ H.R μ = ν"
      proof -
        fix f g ν
        assume f: "ide f" and g: "ide g" and ν: "«ν : H.R f ⇒ H.R g»"
        interpret Hom: category ‹Hom (Src ν) (Trg ν)›
          using ν arr_char category_Hom by auto
        let ?R = "λf. if Hom.arr f
                      then Comp (Trg ν) (Src ν) (Src ν) f (Id (Src ν))
                      else Hom.null"
        interpret R: fully_faithful_functor ‹Hom (Src ν) (Trg ν)› ‹Hom (Src ν) (Trg ν)› ?R
          using ν arr_char right_unit_Id by auto
        have 0: "Src f = Src ν ∧ Trg f = Trg ν ∧ Src g = Src ν ∧ Trg g = Trg ν"
        proof (intro conjI)
          show "Trg f = Trg ν"
            using f ν Trg_dom Trg_hcomp by fastforce
          show "Trg g = Trg ν"
            using g ν Trg_cod Trg_hcomp by fastforce
          show "Src f = Src ν"
          proof -
            have 1: "arr f ∧ dom f = f ∧ cod f = f"
              by (meson f ide_char)
            hence "hcomp f (src f) = dom ν"
              using ν by fastforce
            thus ?thesis
              using 1
              by (metis (no_types) H.trg_src Src.simps(1) Src_hcomp ν dom_char in_homE
                  src.preserves_arr src_def)
          qed
          show "Src g = Src ν"
          proof -
            have 1: "arr g ∧ dom g = g ∧ cod g = g"
              by (meson g ide_char)
            hence "hcomp g (src g) = cod ν"
              using ν by fastforce
            thus ?thesis
              using 1
              by (metis (no_types) H.trg_src Src.simps(1) Src_hcomp ν cod_char in_homE
                  src.preserves_arr src_def)
          qed
        qed
        have 1: "Hom.in_hom (Map ν) (?R (Map f)) (?R (Map g))"
        proof
          show "Hom.arr (Map ν)"
            using ν arr_char by auto
          show "Hom.dom (Map ν) = ?R (Map f)"
          proof -
            have 1: "arr f ∧ dom f = f ∧ cod f = f"
              using f ide_char by blast
            have "dom ν = MkCell (Src ν) (Trg ν) (Hom.dom (Map ν))"
              by (meson ν dom_char in_homE)
            thus ?thesis
              using 1 H.trg_src ν arr_char hcomp_def src.preserves_arr src_def by fastforce
          qed
          show "Hom.cod (Map ν) = ?R (Map g)"
          proof -
            have 1: "arr g ∧ dom g = g ∧ cod g = g"
              using g ide_char by blast
            have "cod ν = MkCell (Src ν) (Trg ν) (Hom.cod (Map ν))"
              by (meson ν cod_char in_homE)
            thus ?thesis
              using 1 H.trg_src ν arr_char hcomp_def src.preserves_arr src_def by fastforce
          qed
        qed
        have 2: "Hom.ide (Map f) ∧ Hom.ide (Map g)"
          using 0 f g arr_char ide_char'' by simp
        obtain x where x: "Hom.in_hom x (Map f) (Map g) ∧ ?R x = Map ν"
          using ν 1 2 R.is_full by blast
        have "«MkCell (Src ν) (Trg ν) x : f ⇒ g»"
        proof -
          have "arr (MkCell (Src ν) (Trg ν) x)"
            using ν arr_char x by auto
          thus ?thesis
            by (metis 0 Hom.in_homE Map.simps(1) Src.simps(1) Trg.simps(1)
                      cod_char dom_char f g ide_char in_homI x)
        qed
        moreover have "H.R (MkCell (Src ν) (Trg ν) x) = ν"
          using MkCell_Map ν arrI arr_char hcomp_def null_char src.preserves_arr x by auto
        ultimately show "∃μ. «μ : f ⇒ g» ∧ H.R μ = ν" by auto
      qed
    qed

    interpretation L: fully_faithful_functor vcomp vcomp H.L
    proof
      show "⋀f f'. ⟦par f f'; H.L f = H.L f'⟧ ⟹ f = f'"
      proof -
        fix μ μ'
        assume par: "par μ μ'"
        and eq: "H.L μ = H.L μ'"
        have 1: "Src μ' = Src μ ∧ Trg μ' = Trg μ"
          using par by (metis Src_dom Trg_dom)
        interpret Hom: category ‹Hom (Src μ) (Trg μ)›
          using par arr_char category_Hom by simp
        let ?L = "λf. if Hom.arr f
                      then Comp (Trg μ) (Trg μ) (Src μ) (Id (Trg μ)) f
                      else Hom.null"
        interpret L: fully_faithful_functor ‹Hom (Src μ) (Trg μ)› ‹Hom (Src μ) (Trg μ)› ?L
          using par arr_char left_unit_Id [of "Src μ" "Trg μ"] by simp
        have Lμ: "H.L μ = MkCell (Src μ) (Trg μ)
                                 (Comp (Trg μ) (Trg μ) (Src μ) (Id (Trg μ)) (Map μ))"
          unfolding hcomp_def
          using par trg_def null_char H.src_trg trg.preserves_arr by simp
        have Lμ': "H.L μ' = MkCell (Src μ) (Trg μ)
                                   (Comp (Trg μ) (Trg μ) (Src μ) (Id (Trg μ)) (Map μ'))"
          unfolding hcomp_def
          using par 1 trg_def null_char H.src_trg trg.preserves_arr by simp
        have "Map μ = Map μ'"
          using Lμ Lμ' eq par arr_char eq L.is_faithful
          by (metis "1" Map.simps(1) Map_cod Map_dom)
        thus "μ = μ'"
          using 1 par MkCell_Map
          by (metis arr_char null_char)
      qed
      show "⋀f g ν. ⟦ide f; ide g; «ν : H.L f ⇒ H.L g»⟧ ⟹ ∃μ. «μ : f ⇒ g» ∧ H.L μ = ν"
      proof -
        fix f g ν
        assume f: "ide f" and g: "ide g" and ν: "«ν : H.L f ⇒ H.L g»"
        interpret Hom: category ‹Hom (Src ν) (Trg ν)›
          using ν arr_char category_Hom by auto
        let ?L = "λf. if Hom.arr f
                      then Comp (Trg ν) (Trg ν) (Src ν) (Id (Trg ν)) f
                      else Hom.null"
        interpret L: fully_faithful_functor ‹Hom (Src ν) (Trg ν)› ‹Hom (Src ν) (Trg ν)› ?L
          using ν arr_char left_unit_Id by auto
        have 0: "Src f = Src ν ∧ Trg f = Trg ν ∧ Src g = Src ν ∧ Trg g = Trg ν"
        proof (intro conjI)
          show "Src f = Src ν"
            using Src_dom Src_hcomp ν f by fastforce
          show "Src g = Src ν"
            using ν g Src_cod Src_hcomp by fastforce
          show "Trg f = Trg ν"
          proof -
            have 1: "arr f ∧ dom f = f ∧ cod f = f"
              by (meson f ide_char)
            hence "hcomp (trg f) f = dom ν"
              using ν by fastforce
            thus ?thesis
              using 1
              by (metis (no_types) H.src_trg Trg.simps(1) Trg_hcomp ν dom_char in_homE
                  trg.preserves_arr trg_def)
          qed
          show "Trg g = Trg ν"
          proof -
            have 1: "arr g ∧ dom g = g ∧ cod g = g"
              by (meson g ide_char)
            hence "hcomp (trg g) g = cod ν"
              using ν by fastforce
            thus ?thesis
              using 1
              by (metis (no_types) H.src_trg Trg.simps(1) Trg_hcomp ν cod_char in_homE
                  trg.preserves_arr trg_def)
          qed
        qed
        have 1: "Hom.in_hom (Map ν) (?L (Map f)) (?L (Map g))"
        proof
          show "Hom.arr (Map ν)"
            using ν arr_char by auto
          show "Hom.dom (Map ν) = ?L (Map f)"
          proof -
            have "dom ν = MkCell (Src ν) (Trg ν) (Hom.dom (Map ν))"
              using ν dom_char [of ν] by auto
            hence "Hom.dom (Map ν) = Map (dom ν)"
              by simp
            also have "... = ?L (Map f)"
              using 0 f ν left_unit_Id [of "Src f" "Trg f"]
              apply (simp add: ide_char'')
              by (metis (no_types, lifting) H.src_trg Map.simps(1) Map_hcomp Trg.simps(1)
                  f ide_char in_homE trg.preserves_arr trg_def)
            finally show ?thesis by blast
          qed
          show "Hom.cod (Map ν) = ?L (Map g)"
          proof -
            have "cod ν = MkCell (Src ν) (Trg ν) (Hom.cod (Map ν))"
              using ν cod_char [of ν] by auto
            hence "Hom.cod (Map ν) = Map (cod ν)"
              by simp
            also have "... = ?L (Map g)"
              using 0 g ν left_unit_Id [of "Src g" "Trg g"]
              apply (simp add: ide_char'')
              by (metis (no_types, lifting) H.src_trg Map.simps(1) Map_hcomp Trg.simps(1)
                  g ide_char in_homE trg.preserves_arr trg_def)
            finally show ?thesis by blast
          qed
        qed
        have 2: "Hom.ide (Map f) ∧ Hom.ide (Map g)"
          using 0 f g arr_char ide_char'' by simp
        obtain x where x: "Hom.in_hom x (Map f) (Map g) ∧ ?L x = Map ν"
          using ν 1 2 L.is_full by blast
        have "«MkCell (Src ν) (Trg ν) x : f ⇒ g»"
        proof -
          have "arr (MkCell (Src ν) (Trg ν) x)"
            using ν arr_char x by auto
          thus ?thesis
            by (metis 0 Hom.in_homE Map.simps(1) Src.simps(1) Trg.simps(1)
                      cod_char dom_char f g ide_char in_homI x)
        qed
        moreover have "H.L (MkCell (Src ν) (Trg ν) x) = ν"
          using MkCell_Map ν arrI arr_char hcomp_def null_char trg.preserves_arr x by auto
        ultimately show "∃μ. «μ : f ⇒ g» ∧ H.L μ = ν" by auto
      qed
    qed

    text ‹
      The unit isomorphisms are defined in terms of the specified function ‹Unit›.
    ›

    definition 𝗂  ("𝗂[_]")
    where "𝗂[a] ≡ MkCell (Src a) (Src a) (Unit (Src a))"

    lemma 𝗂_simps [simp]:
    assumes "H.obj a"
    shows "Src 𝗂[a] = Src a" and "Trg 𝗂[a] = Trg a" and "Map 𝗂[a] = Unit (Src a)"
      using assms 𝗂_def H.obj_def src_def trg_def
       apply auto
      by (metis Trg.simps(1))

    text ‹
      The main result: the construction produces a bicategory.
    ›

    proposition induces_bicategory:
    shows "bicategory vcomp hcomp 𝖺 𝗂 src trg"
    proof
      fix a
      assume a: "H.obj a"
      have Src_a: "Src a ∈ Obj"
        using a ide_char'' by auto
      interpret Hom: category ‹Hom (Src a) (Src a)›
        using Src_a category_Hom by auto
      show "«𝗂 a : hcomp a a ⇒ a»"
      proof -
        have "«𝗂 a : MkCell (Src a) (Src a) (Hom.dom (Unit (Src a)))
                       ⇒ MkCell (Src a) (Src a) (Hom.cod (Unit (Src a)))»"
          using a Src_a MkCell_in_hom Unit_in_hom [of "Src a"] 𝗂_def
          by simp (metis Hom.in_homE)
        moreover have "MkCell (Src a) (Src a) (Hom.cod (Unit (Src a))) = a"
          using a MkCell_Map H.obj_def Map_obj src_def Src_a Unit_in_hom by force
        moreover have "MkCell (Src a) (Src a) (Hom.dom (Unit (Src a))) = hcomp a a"
          using a H.obj_def Map_hcomp [of a a] Map_obj Src_a Unit_in_hom Src_hcomp Trg_hcomp
          by (metis H.objE Hom.in_homE Trg.simps(1) calculation(2) hcomp_def)
        ultimately show ?thesis by simp
      qed
      show "iso (𝗂 a)"
        using a Src_a iso_Unit [of "Src a"] ‹«𝗂 a : hcomp a a ⇒ a»› iso_char 𝗂_def by auto
      next
      show "⋀f g h k. ⟦ide f; ide g; ide h; ide k; src f = trg g; src g = trg h; src h = trg k⟧
              ⟹ vcomp (hcomp f (𝖺 g h k)) (vcomp (𝖺 f (hcomp g h) k) (hcomp (𝖺 f g h) k)) =
                  vcomp (𝖺 f g (hcomp h k)) (𝖺 (hcomp f g) h k)"
      proof (intro arr_eqI)
        fix f g h k
        assume f: "ide f" and g: "ide g" and h: "ide h" and k: "ide k"
        and fg: "src f = trg g" and gh: "src g = trg h" and hk: "src h = trg k"
        have 1: "«hcomp f (𝖺 g h k) :
                    hcomp f (hcomp (hcomp g h) k) ⇒ hcomp f (hcomp g (hcomp h k))»"
          using f g h k fg gh hk H.VV.in_hom_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C
                assoc_simps α⇩0.map_simp_ide H.VVV.ide_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C
                H.preserves_hom 𝖺_def
            by auto
        have 2: "«hcomp (𝖺 f g h) k :
                    hcomp (hcomp (hcomp f g) h) k ⇒ hcomp (hcomp f (hcomp g h)) k»"
          using f g h k fg gh hk H.VV.in_hom_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C
                assoc_simps α⇩0.map_simp_ide H.VVV.ide_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C
                H.preserves_hom 𝖺_def
          by auto
        have 3: "«𝖺 f (hcomp g h) k :
                    hcomp (hcomp f (hcomp g h)) k ⇒ hcomp f (hcomp (hcomp g h) k)»"
          using f g h k fg gh hk H.VV.in_hom_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C
                assoc_simps α⇩0.map_simp_ide H.VVV.ide_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C
                H.preserves_hom 𝖺_def
          by auto
        have 4: "seq (hcomp f (𝖺 g h k)) (vcomp (𝖺 f (hcomp g h) k) (hcomp (𝖺 f g h) k))"
          using 1 2 3 by auto
        have 5: "seq (𝖺 f (hcomp g h) k) (hcomp (𝖺 f g h) k)"
          using 2 3 by auto
        have 6: "seq (𝖺 f g (hcomp h k)) (𝖺 (hcomp f g) h k)"
          using f g h k fg gh hk H.VV.in_hom_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C
                assoc_simps α⇩0.map_simp_ide H.VVV.ide_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C
                H.preserves_hom 𝖺_def
          by simp

        let ?LHS = "vcomp (hcomp f (𝖺 g h k)) (vcomp (𝖺 f (hcomp g h) k) (hcomp (𝖺 f g h) k))"
        let ?RHS = "vcomp (𝖺 f g (hcomp h k)) (𝖺 (hcomp f g) h k)"
        show "arr ?LHS"
          using 4 by simp
        show "arr ?RHS"
          using 6 by simp
        show "Src ?LHS = Src ?RHS"
          using 4 6 f g h k fg gh hk Src_vcomp Src_hcomp
                α⇩0.map_simp_ide H.VVV.ide_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C
                assoc_simps assoc_simps' assoc_def 𝖺_def
          by simp
        show "Trg ?LHS = Trg ?RHS"
          using 4 6 f g h k fg gh hk Trg_vcomp Trg_hcomp
                α⇩0.map_simp_ide H.VVV.ide_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C
                assoc_simps assoc_simps' assoc_def 𝖺_def
          by simp
        show "Map ?LHS = Map ?RHS"
          using 4 5 6 f g h k fg gh hk α⇩0.map_simp_ide H.VVV.ide_char⇩S⇩b⇩C
                H.VV.arr_char⇩S⇩b⇩C H.VVV.arr_char⇩S⇩b⇩C 𝖺_def
          apply simp
          using Trg_src Trg_trg pentagon ideD(1) ide_char''
          by (metis (no_types, lifting))
      qed
    qed

    sublocale bicategory vcomp hcomp 𝖺 𝗂 src trg
      using induces_bicategory by simp

  end

  text ‹
    We now establish some correspondences between the constructed bicategory and the
    originally given data, to provide some assurance that the construction really is doing
    what we think it is.
  ›

  context concrete_bicategory
  begin

    lemma Src_in_Obj:
    assumes "arr μ"
    shows "Src μ ∈ Obj"
      using assms arr_char by simp

    lemma Trg_in_Obj:
    assumes "arr μ"
    shows "Trg μ ∈ Obj"
      using assms arr_char by simp

    lemma arr_Map:
    assumes "arr μ"
    shows "partial_composition.arr (Hom (Src μ) (Trg μ)) (Map μ)"
      using assms arr_char by simp

    lemma obj_MkObj_Src:
    assumes "arr μ"
    shows "obj (MkObj (Src μ))"
      using assms by (simp add: Src_in_Obj obj_MkObj)

    lemma obj_MkObj_Trg:
    assumes "arr μ"
    shows "obj (MkObj (Trg μ))"
      using assms by (simp add: Trg_in_Obj obj_MkObj)

    lemma vcomp_MkCell [simp]:
    assumes "arr (MkCell A B f)" and "arr (MkCell A B g)"
    and "partial_composition.seq (Hom A B) f g"
    shows "vcomp (MkCell A B f) (MkCell A B g) = MkCell A B (Hom A B f g)"
      using assms(1-3) arr_char vcomp_def by fastforce

    lemma hcomp_MkCell [simp]:
    assumes "arr (MkCell B C f)" and "arr (MkCell A B g)"
    shows "hcomp (MkCell B C f) (MkCell A B g) = MkCell A C (Comp C B A f g)"
      by (simp add: assms(1-2) hcomp_def)

    text ‹
      The objects of the constructed bicategory are in bijective correspondence with
      the originally given set ‹Obj›, via the inverse mappings ‹MkObj› and ‹Src›.
    ›

    proposition bij_betw_obj_Obj:
    shows "MkObj ∈ Obj → Collect obj"
    and "Src ∈ Collect obj → Obj"
    and "A ∈ Obj ⟹ Src (MkObj A) = A"
    and "a ∈ Collect obj ⟹ MkObj (Src a) = a"
    and "bij_betw MkObj Obj (Collect obj)"
      using obj_MkObj obj_def Src_in_Obj src_def
          apply auto
      by (intro bij_betwI) auto

    lemma obj_char:
    shows "obj a ⟷ Src a ∈ Obj ∧ a = MkCell (Src a) (Src a) (Id (Src a))"
      using Src_in_Obj bij_betw_obj_Obj(4) obj_MkObj by force

    lemma Map_in_Hom:
    assumes "arr μ"
    shows "partial_composition.in_hom (Hom (Src μ) (Trg μ)) (Map μ) (Map (dom μ)) (Map (cod μ))"
      by (simp add: Src_in_Obj Trg_in_Obj arr_Map assms category.in_homI category_Hom)

    text ‹
      For each pair of objects ‹a› and ‹b›, the hom-category ‹hhom a b› of the constructed
      bicategory is isomorphic to the originally given category ‹Hom (Src a) (Src b)›.
    ›

    proposition isomorphic_hhom_Hom:
    assumes "obj a" and "obj b"
    shows "isomorphic_categories
             (subcategory.comp vcomp (λf. f ∈ hhom a b)) (Hom (Src a) (Src b))"
    proof -
      interpret hom: subcategory vcomp ‹λf. f ∈ hhom a b›
        using assms by unfold_locales auto
      interpret Hom: category ‹Hom (Src a) (Src b)›
        using assms category_Hom Src_in_Obj obj_def by simp
      let ?Map = "λμ. if μ ∈ hhom a b then Map μ else Hom.null"
      let ?MkCell = "λμ. if Hom.arr μ then MkCell (Src a) (Src b) μ else hom.null"
      interpret Map: "functor" hom.comp ‹Hom (Src a) (Src b)› ?Map
      proof
        fix μ
        show "¬ hom.arr μ ⟹ ?Map μ = Hom.null"
          using hom.inclusion [of μ] hom.arr_char⇩S⇩b⇩C by auto
        assume μ: "hom.arr μ"
        have 0: "src μ = a ∧ trg μ = b"
          using μ hom.arrE src_def trg_def
          by (metis in_hhomE mem_Collect_eq)
        have 1: "arr μ"
          using μ hom.inclusion hom.arrE by blast
        have 2: "Src μ = Src a ∧ Trg μ = Trg b"
          using μ 0
          by (metis Src_src Trg_trg hom.arr_char⇩S⇩b⇩C hom.inclusion)
        show "Hom.arr (?Map μ)"
          using 0 1 arr_Map [of μ] μ by auto
        show "Hom.dom (?Map μ) = ?Map (hom.dom μ)"
        proof -
          have "Hom.dom (?Map μ) = Map (dom μ)"
            using μ hom.arrE by fastforce
          thus ?thesis
            by (metis μ hom.arrE hom.arr_dom hom.dom_simp)
        qed
        show "Hom.cod (?Map μ) = ?Map (hom.cod μ)"
        proof -
          have "Hom.cod (?Map μ) = Map (cod μ)"
            using μ hom.arrE by fastforce
          thus ?thesis
            by (metis μ hom.arrE hom.arr_cod hom.cod_simp)
        qed
        next
        fix μ ν
        assume μν: "hom.seq μ ν"
        show "?Map (hom.comp μ ν) = Hom (Src a) (Src b) (?Map μ) (?Map ν)"
        proof -
          have 1: "hom.arr ν ∧ hom.arr μ ∧ seq μ ν"
            using μν hom.seq_char⇩S⇩b⇩C by blast
          hence 2: "hom.comp μ ν = vcomp μ ν"
            using hom.comp_char by auto
          have 3: "μ ∈ hhom a b"
            using 1 hom.arrE by blast
          have "Src a = Src μ"
            using 3 by (metis Trg_src in_hhomE mem_Collect_eq obj_def)
          moreover have "Src b = Trg μ"
            using 3 by (metis Trg_src Trg_trg in_hhomE mem_Collect_eq obj_def)
          ultimately show ?thesis
            using 1 2 Map_vcomp μν hom.arrE by presburger
        qed
      qed
      interpret MkCell: "functor" ‹Hom (Src a) (Src b)› hom.comp ?MkCell
      proof
        fix μ
        show "¬ Hom.arr μ ⟹ ?MkCell μ = hom.null"
          by simp
        assume μ: "Hom.arr μ"
        show 1: "hom.arr (?MkCell μ)"
          using assms obj_def μ hom.arr_char⇩S⇩b⇩C arr_MkCell src_def arr_char by auto
        show "hom.dom (?MkCell μ) = ?MkCell (Hom.dom μ)"
              using assms 1 μ hom.dom_char⇩S⇩b⇩C src_def arr_char obj_def Src_in_Obj by simp
        show "hom.cod (?MkCell μ) = ?MkCell (Hom.cod μ)"
              using assms 1 μ hom.cod_char⇩S⇩b⇩C src_def arr_char obj_def Src_in_Obj by simp
        next
        fix μ ν
        assume μν: "Hom.seq μ ν"
        have 1: "hom.arr (?MkCell μ)"
          using assms obj_def μν hom.arr_char⇩S⇩b⇩C src_def arr_char by auto
        have 2: "hom.arr (?MkCell ν)"
          using assms obj_def μν hom.arr_char⇩S⇩b⇩C src_def arr_char by auto
        have 3: "hom.dom (?MkCell μ) = hom.cod (?MkCell ν)"
          using μν 1 2 hom.dom_char⇩S⇩b⇩C dom_char hom.cod_char⇩S⇩b⇩C cod_char arr_char by auto
        have 4: "seq (?MkCell μ) (?MkCell ν)"
          by (metis 1 2 3 hom.arrE hom.cod_simp hom.comp_closed hom.dom_simp hom.inclusion)
        have "hom.comp (?MkCell μ) (?MkCell ν) =
               vcomp (MkCell (Src a) (Src b) μ) (MkCell (Src a) (Src b) ν)"
          using μν 1 2 4 hom.comp_char by auto
        also have "... = MkCell (Src a) (Src b) (Hom (Src a) (Src b) μ ν)"
          using μν 4 vcomp_char [of "MkCell (Src a) (Src b) μ" "MkCell (Src a) (Src b) ν"]
          by auto
        also have "... = ?MkCell (Hom (Src a) (Src b) μ ν)"
          using μν by simp
        finally show "?MkCell (Hom (Src a) (Src b) μ ν) = hom.comp (?MkCell μ) (?MkCell ν)"
          by simp
      qed
      interpret inverse_functors hom.comp ‹Hom (Src a) (Src b)› ?MkCell ?Map
      proof
        show "?MkCell o ?Map = hom.map"
        proof
          fix μ
          have "μ ∉ hhom a b ⟹ (?MkCell o ?Map) μ = hom.map μ"
            using o_apply hom.is_extensional hom.arr_char⇩S⇩b⇩C by simp
          moreover have "μ ∈ hhom a b ⟹ (?MkCell o ?Map) μ = hom.map μ"
          proof -
            assume μ: "μ ∈ hhom a b"
            have "(?MkCell o ?Map) μ = MkCell (Src a) (Src b) (Map μ)"
              using μ arr_char src_def trg_def by auto
            also have "... = μ"
              using μ MkCell_Map arr_char null_char by auto
            also have "... = hom.map μ"
              using μ hom.arrI⇩S⇩b⇩C hom.map_def by presburger
            finally show "(?MkCell o ?Map) μ = hom.map μ"
              by simp
          qed
          ultimately show "(?MkCell o ?Map) μ = hom.map μ"
            by blast
        qed
        show "?Map o ?MkCell = Hom.map"
        proof
          fix μ
          have "¬ Hom.arr μ ⟹ (?Map o ?MkCell) μ = Hom.map μ"
            using Hom.is_extensional hom.null_char by auto
          moreover have "Hom.arr μ ⟹ (?Map o ?MkCell) μ = Hom.map μ"
          proof -
            assume μ: "Hom.arr μ"
            have "in_hhom (MkCell (Src a) (Src b) μ) a b"
              using μ MkCell.preserves_reflects_arr [of μ] hom.arr_char⇩S⇩b⇩C by simp
            thus "(?Map o ?MkCell) μ = Hom.map μ"
              using μ by simp
          qed
          ultimately show "(?Map o ?MkCell) μ = Hom.map μ"
            by blast
        qed
      qed
      show ?thesis ..
    qed

  end

end