Theory NaturalTransformation

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

chapter NaturalTransformation

theory NaturalTransformation
imports Functor
begin

  section "Definition of a Natural Transformation"
    
  text‹
    As is the case for functors, the ``object-free'' definition of category
    makes it possible to view natural transformations as functions on arrows.
    In particular, a natural transformation between functors
    @{term F} and @{term G} from @{term A} to @{term B} can be represented by
    the map that takes each arrow @{term f} of @{term A} to the diagonal of the
    square in @{term B} corresponding to the transformation of @{term "F f"}
    to @{term "G f"}.  The images of the identities of @{term A} under this
    map are the usual components of the natural transformation.
    This representation exhibits natural transformations as a kind of generalization
    of functors, and in fact we can directly identify functors with identity
    natural transformations.
    However, functors are still necessary to state the defining conditions for
    a natural transformation, as the domain and codomain of a natural transformation
    cannot be recovered from the map on arrows that represents it.

    Like functors, natural transformations preserve arrows and map non-arrows to null.
    Natural transformations also ``preserve'' domain and codomain, but in a more general
    sense than functors. The naturality conditions, which express the two ways of factoring
    the diagonal of a commuting square, are degenerate in the case of an identity transformation.
›

  locale natural_transformation =
    A: category A +
    B: category B + 
    F: "functor" A B F +
    G: "functor" A B G
  for A :: "'a comp"      (infixr A 55)
  and B :: "'b comp"      (infixr B 55)
  and F :: "'a  'b"
  and G :: "'a  'b"
  and τ :: "'a  'b" +
  assumes is_extensional: "¬A.arr f  τ f = B.null"
  and preserves_dom [iff]: "A.arr f  B.dom (τ f) = F (A.dom f)"
  and preserves_cod [iff]: "A.arr f  B.cod (τ f) = G (A.cod f)"
  and is_natural_1 [iff]: "A.arr f  G f B τ (A.dom f) = τ f"
  and is_natural_2 [iff]: "A.arr f  τ (A.cod f) B F f = τ f"
  begin

    lemma naturality:
    assumes "A.arr f"
    shows "τ (A.cod f) B F f = G f B τ (A.dom f)"
      using assms is_natural_1 is_natural_2 by simp

    text‹
      The following fact for natural transformations provides us with the same advantages
      as the corresponding fact for functors.
›

    lemma preserves_reflects_arr [iff]:
    shows "B.arr (τ f)  A.arr f"
      using is_extensional A.arr_cod_iff_arr B.arr_cod_iff_arr preserves_cod by force

    lemma preserves_hom [intro]:
    assumes "«f : a A b»"
    shows "«τ f : F a B G b»"
      using assms
      by (metis A.in_homE B.arr_cod_iff_arr B.in_homI G.preserves_arr G.preserves_cod
          preserves_cod preserves_dom)

    lemma preserves_comp_1:
    assumes "A.seq f' f"
    shows "τ (f' A f) = G f' B τ f"
      using assms
      by (metis A.seqE A.dom_comp B.comp_assoc G.preserves_comp is_natural_1)

    lemma preserves_comp_2:
    assumes "A.seq f' f"
    shows "τ (f' A f) = τ f' B F f"
      using assms
      by (metis A.arr_cod_iff_arr A.cod_comp B.comp_assoc F.preserves_comp is_natural_2)

    text‹
      A natural transformation that also happens to be a functor is equal to
      its own domain and codomain.
›

    lemma functor_implies_equals_dom:
    assumes "functor A B τ"
    shows "F = τ"
    proof
      interpret τ: "functor" A B τ using assms by auto
      fix f
      show "F f = τ f"
        using assms
        by (metis A.dom_cod B.comp_cod_arr F.is_extensional F.preserves_arr F.preserves_cod
            τ.preserves_dom is_extensional is_natural_2 preserves_dom)
    qed

    lemma functor_implies_equals_cod:
    assumes "functor A B τ"
    shows "G = τ"
    proof
      interpret τ: "functor" A B τ using assms by auto
      fix f
      show "G f = τ f"
        using assms
        by (metis A.cod_dom B.comp_arr_dom G.is_extensional G.preserves_arr
            G.preserves_dom B.cod_dom functor_implies_equals_dom is_extensional
            is_natural_1 preserves_cod preserves_dom)
    qed
          
  end

  section "Components of a Natural Transformation"

  text‹
    The values taken by a natural transformation on identities are the \emph{components}
    of the transformation.  We have the following basic technique for proving two natural
    transformations equal: show that they have the same components.
›

  lemma eqI:
  assumes "natural_transformation A B F G σ" and "natural_transformation A B F G σ'"
  and "a. partial_composition.ide A a  σ a = σ' a"
  shows "σ = σ'"
  proof -
    interpret A: category A using assms(1) natural_transformation_def by blast
    interpret σ: natural_transformation A B F G σ using assms(1) by auto
    interpret σ': natural_transformation A B F G σ' using assms(2) by auto
    have "f. σ f = σ' f"
      using assms(3) σ.is_natural_2 σ'.is_natural_2 σ.is_extensional σ'.is_extensional A.ide_cod
      by metis
    thus ?thesis by auto
  qed

  text‹
    As equality of natural transformations is determined by equality of components,
    a natural transformation may be uniquely defined by specifying its components.
    The extension to all arrows is given by @{prop is_natural_1} or equivalently
    by @{prop is_natural_2}.
›

  locale transformation_by_components =
    A: category A +
    B: category B + 
    F: "functor" A B F +
    G: "functor" A B G
  for A :: "'a comp"      (infixr A 55)
  and B :: "'b comp"      (infixr B 55)
  and F :: "'a  'b"
  and G :: "'a  'b"
  and t :: "'a  'b" +
  assumes maps_ide_in_hom [intro]: "A.ide a  «t a : F a B G a»"
  and is_natural: "A.arr f  t (A.cod f) B F f = G f B t (A.dom f)"
  begin

    definition map
    where "map f = (if A.arr f then t (A.cod f) B F f else B.null)"

    lemma map_simp_ide [simp]:
    assumes "A.ide a"
    shows "map a = t a"
      using assms map_def B.comp_arr_dom [of "t a"] maps_ide_in_hom by fastforce

    lemma is_natural_transformation:
    shows "natural_transformation A B F G map"
      using map_def is_natural
      apply (unfold_locales, simp_all)
         apply (metis A.ide_dom B.dom_comp B.seqI
                      G.preserves_arr G.preserves_dom B.in_homE maps_ide_in_hom)
        apply (metis A.ide_dom B.arrI B.cod_comp B.in_homE B.seqI
                     G.preserves_arr G.preserves_cod G.preserves_dom maps_ide_in_hom)
       apply (metis A.ide_dom B.comp_arr_dom B.in_homE maps_ide_in_hom)
      by (metis B.comp_assoc A.comp_cod_arr F.preserves_comp)

  end

  sublocale transformation_by_components  natural_transformation A B F G map
    using is_natural_transformation by auto

  lemma transformation_by_components_idem [simp]:
  assumes "natural_transformation A B F G τ"
  shows "transformation_by_components.map A B F τ = τ"
  proof -
    interpret τ: natural_transformation A B F G τ using assms by blast
    interpret τ': transformation_by_components A B F G τ
      by (unfold_locales, auto) 
    show ?thesis
      using assms τ'.map_simp_ide τ'.is_natural_transformation eqI by blast
  qed

  section "Functors as Natural Transformations"

  text‹
    A functor is a special case of a natural transformation, in the sense that the same map
    that defines the functor also defines an identity natural transformation.
›

  lemma functor_is_transformation [simp]:
  assumes "functor A B F"
  shows "natural_transformation A B F F F"
  proof -
    interpret "functor" A B F using assms by auto
    show "natural_transformation A B F F F"
      using is_extensional B.comp_arr_dom B.comp_cod_arr
      by (unfold_locales, simp_all)
  qed

  sublocale "functor"  as_nat_trans: natural_transformation A B F F F
    by (simp add: functor_axioms)

  section "Constant Natural Transformations"

  text‹
    A constant natural transformation is one whose components are all the same arrow.
›

  locale constant_transformation =
    A: category A +
    B: category B +
    F: constant_functor A B "B.dom g" +
    G: constant_functor A B "B.cod g"
  for A :: "'a comp"      (infixr A 55)
  and B :: "'b comp"      (infixr B 55)
  and g :: 'b +
  assumes value_is_arr: "B.arr g"
  begin

    definition map
    where "map f  if A.arr f then g else B.null"

    lemma map_simp [simp]:
    assumes "A.arr f"
    shows "map f = g"
      using assms map_def by auto

    lemma is_natural_transformation:
    shows "natural_transformation A B F.map G.map map"
      apply unfold_locales
      using map_def value_is_arr B.comp_arr_dom B.comp_cod_arr by auto

    lemma is_functor_if_value_is_ide:
    assumes "B.ide g"
    shows "functor A B map"
      apply unfold_locales using assms map_def by auto

  end

  sublocale constant_transformation  natural_transformation A B F.map G.map map
    using is_natural_transformation by auto

  context constant_transformation
  begin

    lemma equals_dom_if_value_is_ide:
    assumes "B.ide g"
    shows "map = F.map"
      using assms functor_implies_equals_dom is_functor_if_value_is_ide by auto

    lemma equals_cod_if_value_is_ide:
    assumes "B.ide g"
    shows "map = G.map"
      using assms functor_implies_equals_dom is_functor_if_value_is_ide by auto

  end

  section "Vertical Composition"

  text‹
    Vertical composition is a way of composing natural transformations σ: F → G›
    and τ: G → H›, between parallel functors @{term F}, @{term G}, and @{term H}
    to obtain a natural transformation from @{term F} to @{term H}.
    The composite is traditionally denoted by τ o σ›, however in the present
    setting this notation is misleading because it is horizontal composite, rather than
    vertical composite, that coincides with composition of natural transformations as
    functions on arrows.
›

  locale vertical_composite =
    A: category A +
    B: category B +
    F: "functor" A B F +
    G: "functor" A B G +
    H: "functor" A B H +
    σ: natural_transformation A B F G σ +
    τ: natural_transformation A B G H τ
  for A :: "'a comp"      (infixr A 55)
  and B :: "'b comp"      (infixr B 55)
  and F :: "'a  'b"
  and G :: "'a  'b"
  and H :: "'a  'b"
  and σ :: "'a  'b"
  and τ :: "'a  'b"
  begin

    text‹
      Vertical composition takes an arrow @{term "A.in_hom a b f"} to an arrow in
      @{term "B.hom (F a) (G b)"}, which we can obtain by forming either of
      the composites @{term "B (τ b) (σ f)"} or @{term "B (τ f) (σ a)"}, which are
      equal to each other.
›

    definition map
    where "map f = (if A.arr f then τ (A.cod f) B σ f else B.null)"

    lemma map_seq:
    assumes "A.arr f"
    shows "B.seq (τ (A.cod f)) (σ f)"
      using assms by auto

    lemma map_simp_ide:
    assumes "A.ide a"
    shows "map a = τ a B σ a"
      using assms map_def by auto

    lemma map_simp_1:
    assumes "A.arr f"
    shows "map f = τ (A.cod f) B σ f"
      using assms by (simp add: map_def)

    lemma map_simp_2:
    assumes "A.arr f"
    shows "map f = τ f B σ (A.dom f)"
      using assms
      by (metis B.comp_assoc σ.is_natural_2 σ.naturality τ.is_natural_1 τ.naturality map_simp_1)

    lemma is_natural_transformation:
    shows "natural_transformation A B F H map"
      using map_def map_simp_1 map_simp_2 map_seq B.comp_assoc
      apply (unfold_locales, simp_all)
      by (metis B.comp_assoc τ.is_natural_1)

  end

  sublocale vertical_composite  natural_transformation A B F H map
    using is_natural_transformation by auto

  text‹
    Functors are the identities for vertical composition.
›

  lemma vcomp_ide_dom [simp]:
  assumes "natural_transformation A B F G τ"
  shows "vertical_composite.map A B F τ = τ"
    using assms apply (intro eqI)
      apply auto[2]
     apply (meson functor_is_transformation natural_transformation_def vertical_composite.intro
                  vertical_composite.is_natural_transformation)
  proof -
    fix a :: 'a
    have "vertical_composite A B F F G F τ"
      by (meson assms functor_is_transformation natural_transformation.axioms(1-4)
                vertical_composite.intro)
    thus "vertical_composite.map A B F τ a = τ a"
      using assms natural_transformation.is_extensional natural_transformation.is_natural_2
            vertical_composite.map_def
      by fastforce
  qed
    
  lemma vcomp_ide_cod [simp]:
  assumes "natural_transformation A B F G τ"
  shows "vertical_composite.map A B τ G = τ"
    using assms apply (intro eqI)
      apply auto[2]
     apply (meson functor_is_transformation natural_transformation_def vertical_composite.intro
                  vertical_composite.is_natural_transformation)
  proof -
    fix a :: 'a
    assume a: "partial_composition.ide A a"
    interpret Goτ: vertical_composite A B F G G τ G
      by (meson assms functor_is_transformation natural_transformation.axioms(1-4)
                vertical_composite.intro)
    show "vertical_composite.map A B τ G a = τ a"
      using assms a natural_transformation.is_extensional natural_transformation.is_natural_1
            Goτ.map_simp_ide Goτ.B.comp_cod_arr
      by simp
  qed

  text‹
    Vertical composition is associative.
›

  lemma vcomp_assoc [simp]:
  assumes "natural_transformation A B F G ρ"
  and "natural_transformation A B G H σ"
  and "natural_transformation A B H K τ"
  shows "vertical_composite.map A B (vertical_composite.map A B ρ σ) τ
            = vertical_composite.map A B ρ (vertical_composite.map A B σ τ)"
  proof -
    interpret A: category A
      using assms(1) natural_transformation_def functor_def by blast
    interpret B: category B
      using assms(1) natural_transformation_def functor_def by blast
    interpret ρ: natural_transformation A B F G ρ using assms(1) by auto
    interpret σ: natural_transformation A B G H σ using assms(2) by auto
    interpret τ: natural_transformation A B H K τ using assms(3) by auto
    interpret ρσ: vertical_composite A B F G H ρ σ ..
    interpret στ: vertical_composite A B G H K σ τ ..
    interpret ρ_στ: vertical_composite A B F G K ρ στ.map ..
    interpret ρσ_τ: vertical_composite A B F H K ρσ.map τ ..
    show ?thesis
      using ρσ_τ.is_natural_transformation ρ_στ.natural_transformation_axioms
            ρσ.map_simp_ide ρσ_τ.map_simp_ide ρ_στ.map_simp_ide στ.map_simp_ide B.comp_assoc
      by (intro eqI, auto)
  qed

  section "Natural Isomorphisms"

  text‹
    A natural isomorphism is a natural transformation each of whose components
    is an isomorphism.  Equivalently, a natural isomorphism is a natural transformation
    that is invertible with respect to vertical composition.
›

  locale natural_isomorphism = natural_transformation A B F G τ
  for A :: "'a comp"      (infixr A 55)
  and B :: "'b comp"      (infixr B 55)
  and F :: "'a  'b"
  and G :: "'a  'b"
  and τ :: "'a  'b" +
  assumes components_are_iso [simp]: "A.ide a  B.iso (τ a)"
  begin

    lemma inv_naturality:
    assumes "A.arr f"
    shows "F f B B.inv (τ (A.dom f)) = B.inv (τ (A.cod f)) B G f"
      using assms is_natural_1 is_natural_2 components_are_iso B.invert_side_of_triangle
            B.comp_assoc A.ide_cod A.ide_dom preserves_reflects_arr
      by fastforce

    text ‹
      Natural isomorphisms preserve isomorphisms, in the sense that the sides of
      of the naturality square determined by an isomorphism are all isomorphisms,
      so the diagonal is, as well.
›

    lemma preserves_iso:
    assumes "A.iso f"
    shows "B.iso (τ f)"
      using assms
      by (metis A.ide_dom A.iso_is_arr B.isos_compose G.preserves_iso components_are_iso
          is_natural_2 naturality preserves_reflects_arr)

  end

  text ‹
    Since the function that represents a functor is formally identical to the function
    that represents the corresponding identity natural transformation, no additional locale
    is needed for identity natural transformations.  However, an identity natural transformation
    is also a natural isomorphism, so it is useful for @{locale functor} to inherit from the
    @{locale natural_isomorphism} locale.
›

  sublocale "functor"  as_nat_iso: natural_isomorphism A B F F F
    apply unfold_locales
    using preserves_ide B.ide_is_iso by simp

  definition naturally_isomorphic
  where "naturally_isomorphic A B F G = (τ. natural_isomorphism A B F G τ)"

  lemma naturally_isomorphic_respects_full_functor:
  assumes "naturally_isomorphic A B F G"
  and "full_functor A B F"
  shows "full_functor A B G"
  proof -
    obtain φ where φ: "natural_isomorphism A B F G φ"
      using assms naturally_isomorphic_def by blast
    interpret φ: natural_isomorphism A B F G φ
      using φ by auto
    interpret φ.F: full_functor A B F
      using assms by auto
    write A (infixr A 55)
    write B (infixr B 55)
    write φ.A.in_hom («_ : _ A _»)
    write φ.B.in_hom («_ : _ B _»)
    show "full_functor A B G"
    proof
      fix a a' g
      assume a': "φ.A.ide a'" and a: "φ.A.ide a"
      and g: "«g : G a' B G a»"
      show "f. «f : a' A a»  G f = g"
      proof -
        let ?g' = "φ.B.inv (φ a) B g B φ a'"
        have g': "«?g' : F a' B F a»"
          using a a' g φ.preserves_hom φ.components_are_iso φ.B.inv_in_hom by force
        obtain f' where f': "«f' : a' A a»  F f' = ?g'"
          using a a' g' φ.F.is_full [of a a' ?g'] by blast
        moreover have "G f' = g"
          by (metis f' φ.A.arrI φ.B.arrI φ.B.inv_inv φ.B.invert_side_of_triangle(1-2)
              φ.B.iso_inv_iso φ.G.as_nat_trans.natural_transformation_axioms
              φ.components_are_iso φ.naturality a a' category.in_homE f' g'
              natural_transformation.axioms(1))
        ultimately show ?thesis by auto
      qed
    qed
  qed

  lemma naturally_isomorphic_respects_faithful_functor:
  assumes "naturally_isomorphic A B F G"
  and "faithful_functor A B F"
  shows "faithful_functor A B G"
  proof -
    obtain φ where φ: "natural_isomorphism A B F G φ"
      using assms naturally_isomorphic_def by blast
    interpret φ: natural_isomorphism A B F G φ
      using φ by auto
    interpret φ.F: faithful_functor A B F
      using assms by auto
    show "faithful_functor A B G"
      using φ.naturality φ.components_are_iso φ.B.iso_is_section φ.B.section_is_mono
            φ.B.monoE φ.F.is_faithful φ.is_natural_1 φ.natural_transformation_axioms
            φ.preserves_reflects_arr φ.A.ide_cod
      by (unfold_locales, metis)
  qed

  locale inverse_transformation =
    A: category A +
    B: category B +
    F: "functor" A B F +
    G: "functor" A B G +
    τ: natural_isomorphism A B F G τ
  for A :: "'a comp"      (infixr A 55)
  and B :: "'b comp"      (infixr B 55)
  and F :: "'a  'b"
  and G :: "'a  'b"
  and τ :: "'a  'b"
  begin

    interpretation τ': transformation_by_components A B G F λa. B.inv (τ a)
    proof
      fix f :: 'a
      show "A.ide f  «B.inv (τ f) : G f B F f»"
        using B.inv_in_hom τ.components_are_iso A.ide_in_hom by blast
      show "A.arr f  B.inv (τ (A.cod f)) B G f = F f B B.inv (τ (A.dom f))"
        by (metis A.ide_cod A.ide_dom B.invert_opposite_sides_of_square τ.components_are_iso
            τ.is_natural_2 τ.naturality τ.preserves_reflects_arr)
    qed

    definition map
    where "map = τ'.map"

    lemma map_ide_simp [simp]:
    assumes "A.ide a"
    shows "map a = B.inv (τ a)"
      using assms map_def by fastforce

    lemma map_simp:
    assumes "A.arr f"
    shows "map f = B.inv (τ (A.cod f)) B G f"
      using assms map_def by (simp add: τ'.map_def)

    lemma is_natural_transformation:
    shows "natural_transformation A B G F map"
      by (simp add: τ'.natural_transformation_axioms map_def)

    lemma inverts_components:
    assumes "A.ide a"
    shows "B.inverse_arrows (τ a) (map a)"
      using assms τ.components_are_iso B.ide_is_iso B.inv_is_inverse B.inverse_arrows_def map_def
      by (metis τ'.map_simp_ide)

  end

  sublocale inverse_transformation  natural_transformation A B G F map
    using is_natural_transformation by auto

  sublocale inverse_transformation  natural_isomorphism A B G F map
    by (simp add: natural_isomorphism.intro natural_isomorphism_axioms.intro
        natural_transformation_axioms)

  lemma inverse_inverse_transformation [simp]:
  assumes "natural_isomorphism A B F G τ"
  shows "inverse_transformation.map A B F (inverse_transformation.map A B G τ) = τ"
  proof -
    interpret τ: natural_isomorphism A B F G τ
      using assms by auto
    interpret τ': inverse_transformation A B F G τ ..
    interpret τ'': inverse_transformation A B G F τ'.map ..
    show "τ''.map = τ"
      using τ.natural_transformation_axioms τ''.natural_transformation_axioms   
      by (intro eqI, auto)
  qed

  locale inverse_transformations =
    A: category A +
    B: category B +
    F: "functor" A B F +
    G: "functor" A B G +
    τ: natural_transformation A B F G τ +
    τ': natural_transformation A B G F τ'
  for A :: "'a comp"      (infixr A 55)
  and B :: "'b comp"      (infixr B 55)
  and F :: "'a  'b"
  and G :: "'a  'b"
  and τ :: "'a  'b"
  and τ' :: "'a  'b" +
  assumes inv: "A.ide a  B.inverse_arrows (τ a) (τ' a)"

  sublocale inverse_transformations  natural_isomorphism A B F G τ
    by (meson B.category_axioms τ.natural_transformation_axioms B.iso_def inv
              natural_isomorphism.intro natural_isomorphism_axioms.intro)
  sublocale inverse_transformations  natural_isomorphism A B G F τ'
    by (meson category.inverse_arrows_sym category.iso_def inverse_transformations_axioms
              inverse_transformations_axioms_def inverse_transformations_def
              natural_isomorphism.intro natural_isomorphism_axioms.intro)

  lemma inverse_transformations_sym:
  assumes "inverse_transformations A B F G σ σ'"
  shows "inverse_transformations A B G F σ' σ"
    using assms
    by (simp add: category.inverse_arrows_sym inverse_transformations_axioms_def
                  inverse_transformations_def)

  lemma inverse_transformations_inverse:
  assumes "inverse_transformations A B F G σ σ'"
  shows "vertical_composite.map A B σ σ' = F"
  and "vertical_composite.map A B σ' σ = G"
  proof -
    interpret A: category A
      using assms(1) inverse_transformations_def natural_transformation_def by blast
    interpret inv: inverse_transformations A B F G σ σ' using assms by auto
    interpret σσ': vertical_composite A B F G F σ σ' ..
    show "vertical_composite.map A B σ σ' = F"
      using σσ'.is_natural_transformation inv.F.as_nat_trans.natural_transformation_axioms
            σσ'.map_simp_ide inv.B.comp_inv_arr inv.inv
      by (intro eqI, simp_all)
    interpret inv': inverse_transformations A B G F σ' σ
      using assms inverse_transformations_sym by blast
    interpret σ'σ: vertical_composite A B G F G σ' σ ..
    show "vertical_composite.map A B σ' σ = G"
      using σ'σ.is_natural_transformation inv.G.as_nat_trans.natural_transformation_axioms
            σ'σ.map_simp_ide inv'.inv inv.B.comp_inv_arr
      by (intro eqI, simp_all)
  qed

  lemma inverse_transformations_compose:
  assumes "inverse_transformations A B F G σ σ'"
  and "inverse_transformations A B G H τ τ'"
  shows "inverse_transformations A B F H
           (vertical_composite.map A B σ τ) (vertical_composite.map A B τ' σ')"
  proof -
    interpret A: category A using assms(1) inverse_transformations_def by blast
    interpret B: category B using assms(1) inverse_transformations_def by blast
    interpret σσ': inverse_transformations A B F G σ σ' using assms(1) by auto
    interpret ττ': inverse_transformations A B G H τ τ' using assms(2) by auto
    interpret στ: vertical_composite A B F G H σ τ ..
    interpret τ'σ': vertical_composite A B H G F τ' σ' ..
    show ?thesis
      using B.inverse_arrows_compose σσ'.inv στ.map_simp_ide τ'σ'.map_simp_ide ττ'.inv
      by (unfold_locales, auto)
  qed

  lemma vertical_composite_iso_inverse [simp]:
  assumes "natural_isomorphism A B F G τ"
  shows "vertical_composite.map A B τ (inverse_transformation.map A B G τ) = F"
  proof -
    interpret τ: natural_isomorphism A B F G τ using assms by auto
    interpret τ': inverse_transformation A B F G τ ..
    interpret ττ': vertical_composite A B F G F τ τ'.map ..
    show ?thesis
      using ττ'.is_natural_transformation τ.F.as_nat_trans.natural_transformation_axioms
            τ'.inverts_components τ.B.comp_inv_arr ττ'.map_simp_ide
      by (intro eqI, auto)
  qed

  lemma vertical_composite_inverse_iso [simp]:
  assumes "natural_isomorphism A B F G τ"
  shows "vertical_composite.map A B (inverse_transformation.map A B G τ) τ = G"
  proof -
    interpret τ: natural_isomorphism A B F G τ using assms by auto
    interpret τ': inverse_transformation A B F G τ ..
    interpret τ'τ: vertical_composite A B G F G τ'.map τ ..    
    show ?thesis
      using τ'τ.is_natural_transformation τ.G.as_nat_trans.natural_transformation_axioms
            τ'.inverts_components τ'τ.map_simp_ide τ.B.comp_arr_inv
      by (intro eqI, auto)
  qed

  lemma natural_isomorphisms_compose:
  assumes "natural_isomorphism A B F G σ" and "natural_isomorphism A B G H τ"
  shows "natural_isomorphism A B F H (vertical_composite.map A B σ τ)"
  proof -
    interpret A: category A
      using assms(1) natural_isomorphism_def natural_transformation_def by blast
    interpret B: category B
      using assms(1) natural_isomorphism_def natural_transformation_def by blast
    interpret σ: natural_isomorphism A B F G σ using assms(1) by auto
    interpret τ: natural_isomorphism A B G H τ using assms(2) by auto
    interpret στ: vertical_composite A B F G H σ τ ..
    interpret natural_isomorphism A B F H στ.map
      using στ.map_simp_ide by (unfold_locales, auto)
    show ?thesis ..
  qed

  lemma naturally_isomorphic_reflexive:
  assumes "functor A B F"
  shows "naturally_isomorphic A B F F"
  proof -
    interpret F: "functor" A B F using assms by auto
    have "natural_isomorphism A B F F F" ..
    thus ?thesis using naturally_isomorphic_def by blast
  qed

  lemma naturally_isomorphic_symmetric:
  assumes "naturally_isomorphic A B F G"
  shows "naturally_isomorphic A B G F"
  proof -
    obtain φ where φ: "natural_isomorphism A B F G φ"
      using assms naturally_isomorphic_def by blast
    interpret φ: natural_isomorphism A B F G φ
      using φ by auto
    interpret ψ: inverse_transformation A B F G φ ..
    have "natural_isomorphism A B G F ψ.map" ..
    thus ?thesis using naturally_isomorphic_def by blast
  qed

  lemma naturally_isomorphic_transitive [trans]:
  assumes "naturally_isomorphic A B F G"
  and "naturally_isomorphic A B G H"
  shows "naturally_isomorphic A B F H"
  proof -
    obtain φ where φ: "natural_isomorphism A B F G φ"
      using assms naturally_isomorphic_def by blast
    interpret φ: natural_isomorphism A B F G φ
      using φ by auto
    obtain ψ where ψ: "natural_isomorphism A B G H ψ"
      using assms naturally_isomorphic_def by blast
    interpret ψ: natural_isomorphism A B G H ψ
      using ψ by auto
    interpret ψφ: vertical_composite A B F G H φ ψ ..
    have "natural_isomorphism A B F H ψφ.map"
      using φ ψ natural_isomorphisms_compose by blast
    thus ?thesis
      using naturally_isomorphic_def by blast
  qed

  section "Horizontal Composition"

  text‹
    Horizontal composition is a way of composing parallel natural transformations
    @{term σ} from @{term F} to @{term G} and @{term τ} from @{term H} to @{term K},
    where functors @{term F} and @{term G} map @{term A} to @{term B} and
    @{term H} and @{term K} map @{term B} to @{term C}, to obtain a natural transformation
    from @{term "H o F"} to @{term "K o G"}.

    Since horizontal composition turns out to coincide with ordinary composition of
    natural transformations as functions, there is little point in defining a cumbersome
    locale for horizontal composite.
›

  lemma horizontal_composite:
  assumes "natural_transformation A B F G σ"
  and "natural_transformation B C H K τ"
  shows "natural_transformation A C (H o F) (K o G) (τ o σ)"
  proof -
    interpret σ: natural_transformation A B F G σ
      using assms(1) by simp
    interpret τ: natural_transformation B C H K τ
      using assms(2) by simp
    interpret HF: composite_functor A B C F H ..
    interpret KG: composite_functor A B C G K ..
    show "natural_transformation A C (H o F) (K o G) (τ o σ)"
      using σ.is_extensional τ.is_extensional
      apply (unfold_locales, auto)
       apply (metis σ.is_natural_1 σ.preserves_reflects_arr τ.preserves_comp_1)
      by (metis σ.is_natural_2 σ.preserves_reflects_arr τ.preserves_comp_2)
  qed

  lemma hcomp_ide_dom [simp]:
  assumes "natural_transformation A B F G τ"
  shows "τ o (identity_functor.map A) = τ"
  proof -
    interpret τ: natural_transformation A B F G τ using assms by auto
    show "τ o τ.A.map = τ"
      using τ.A.map_def τ.is_extensional by fastforce
  qed

  lemma hcomp_ide_cod [simp]:
  assumes "natural_transformation A B F G τ"
  shows "(identity_functor.map B) o τ = τ"
  proof -
    interpret τ: natural_transformation A B F G τ using assms by auto
    show "τ.B.map o τ = τ"
      using τ.B.map_def τ.is_extensional by auto
  qed

  text‹
    Horizontal composition of a functor with a vertical composite.
›

  lemma whisker_right:
  assumes "functor A B F"
  and "natural_transformation B C H K τ" and "natural_transformation B C K L τ'"
  shows "(vertical_composite.map B C τ τ') o F = vertical_composite.map A C (τ o F) (τ' o F)"
  proof -
    interpret F: "functor" A B F using assms(1) by auto
    interpret τ: natural_transformation B C H K τ using assms(2) by auto
    interpret τ': natural_transformation B C K L τ' using assms(3) by auto
    interpret τoF: natural_transformation A C H o F K o F τ o F
      using τ.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
            horizontal_composite
      by blast
    interpret τ'oF: natural_transformation A C K o F L o F τ' o F
      using τ'.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
            horizontal_composite
      by blast
    interpret τ'τ: vertical_composite B C H K L τ τ' ..
    interpret τ'τoF: natural_transformation A C H o F L o F τ'τ.map o F
      using τ'τ.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
            horizontal_composite
      by blast
    interpret τ'oF_τoF: vertical_composite A C H o F K o F L o F τ o F τ' o F ..
    show ?thesis
      using τ'oF_τoF.map_def τ'τ.map_def τ'τoF.is_extensional by auto
  qed

  text‹
    Horizontal composition of a vertical composite with a functor.
›

  lemma whisker_left:
  assumes "functor B C K"
  and "natural_transformation A B F G τ" and "natural_transformation A B G H τ'"
  shows "K o (vertical_composite.map A B τ τ') = vertical_composite.map A C (K o τ) (K o τ')"
  proof -
    interpret K: "functor" B C K using assms(1) by auto
    interpret τ: natural_transformation A B F G τ using assms(2) by auto
    interpret τ': natural_transformation A B G H τ' using assms(3) by auto
    interpret τ'τ: vertical_composite A B F G H τ τ' ..
    interpret Koτ: natural_transformation A C K o F K o G K o τ
      using τ.natural_transformation_axioms K.as_nat_trans.natural_transformation_axioms
            horizontal_composite
      by blast
    interpret Koτ': natural_transformation A C K o G K o H K o τ'
      using τ'.natural_transformation_axioms K.as_nat_trans.natural_transformation_axioms
            horizontal_composite
      by blast
    interpret Koτ'τ: natural_transformation A C K o F K o H K o τ'τ.map
      using τ'τ.natural_transformation_axioms K.as_nat_trans.natural_transformation_axioms
            horizontal_composite
      by blast
    interpret Koτ'_Koτ: vertical_composite A C K o F K o G K o H K o τ K o τ' ..
    show "K o τ'τ.map = Koτ'_Koτ.map"
      using Koτ'_Koτ.map_def τ'τ.map_def Koτ'τ.is_extensional Koτ'_Koτ.map_simp_1 τ'τ.map_simp_1
      by auto
  qed

  text‹
    The interchange law for horizontal and vertical composition.
›

  lemma interchange:
  assumes "natural_transformation B C F G τ" and "natural_transformation B C G H ν"
  and "natural_transformation C D K L σ" and "natural_transformation C D L M μ"
  shows "vertical_composite.map C D σ μ  vertical_composite.map B C τ ν =
         vertical_composite.map B D (σ  τ) (μ  ν)"
  proof -
    interpret τ: natural_transformation B C F G τ
       using assms(1) by auto
    interpret ν: natural_transformation B C G H ν
       using assms(2) by auto
    interpret σ: natural_transformation C D K L σ
       using assms(3) by auto
    interpret μ: natural_transformation C D L M μ
       using assms(4) by auto
    interpret ντ: vertical_composite B C F G H τ ν ..
    interpret μσ: vertical_composite C D K L M σ μ ..
    interpret σoτ: natural_transformation B D K o F L o G σ o τ
      using σ.natural_transformation_axioms τ.natural_transformation_axioms
            horizontal_composite
      by blast
    interpret μoν: natural_transformation B D L o G M o H μ o ν
      using μ.natural_transformation_axioms ν.natural_transformation_axioms
            horizontal_composite
      by blast
    interpret μσoντ: natural_transformation B D K o F M o H μσ.map o ντ.map
      using μσ.natural_transformation_axioms ντ.natural_transformation_axioms
            horizontal_composite
      by blast
    interpret μoν_σoτ: vertical_composite B D K o F L o G M o H σ o τ μ o ν ..
    show "μσ.map o ντ.map = μoν_σoτ.map"
    proof (intro eqI)
      show "natural_transformation B D (K  F) (M  H) (μσ.map o ντ.map)" ..
      show "natural_transformation B D (K  F) (M  H) μoν_σoτ.map" ..
      show "a. τ.A.ide a  (μσ.map o ντ.map) a = μoν_σoτ.map a"
      proof -
        fix a
        assume a: "τ.A.ide a"
        have "(μσ.map o ντ.map) a = D (μ (H a)) (σ (C (ν a) (τ a)))"
          using a μσ.map_simp_1 ντ.map_simp_2 by simp
        also have "... = D (μ (ν a)) (σ (τ a))"
          using a
          by (metis (full_types) μ.is_natural_1 μσ.map_simp_1 μσ.preserves_comp_1
              ντ.map_seq ντ.map_simp_1 ντ.preserves_cod σ.B.comp_assoc τ.A.ide_char τ.B.seqE)
        also have "... = μoν_σoτ.map a"
          using a μoν_σoτ.map_simp_ide by simp
        finally show "(μσ.map o ντ.map) a = μoν_σoτ.map a" by blast
      qed
    qed
  qed

  text‹
    A special-case of the interchange law in which two of the natural transformations
    are functors.  It comes up reasonably often, and the reasoning is awkward.
›

  lemma interchange_spc:
  assumes "natural_transformation B C F G σ"
  and "natural_transformation C D H K τ"
  shows "τ  σ = vertical_composite.map B D (H o σ) (τ o G)"
  and "τ  σ = vertical_composite.map B D (τ o F) (K o σ)"
  proof -
    show "τ  σ = vertical_composite.map B D (H  σ) (τ  G)"
    proof -
      have "vertical_composite.map C D H τ  vertical_composite.map B C σ G =
            vertical_composite.map B D (H  σ) (τ  G)"
        by (meson assms functor_is_transformation interchange natural_transformation.axioms(3-4))
      thus ?thesis
        using assms by force
    qed
    show "τ  σ = vertical_composite.map B D (τ  F) (K  σ)"
    proof -
      have "vertical_composite.map C D τ K  vertical_composite.map B C F σ =
            vertical_composite.map B D (τ  F) (K  σ)"
        by (meson assms functor_is_transformation interchange natural_transformation.axioms(3-4))
      thus ?thesis
        using assms by force
    qed
  qed

end