Grace/Cumulus/Category/Functor.g17

Open in Workbench Download source

Imports

Terminal

Declarations

Source

1-- Functors between small categories2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Category.Functor8import Terminal910-- A functor is a structure of its object map, its morphism map, and its11-- source and target categories. Under a hypothesis F : C ⥤ D the values12-- F.obj(a) and F.map(f) are written F(a) and F(f): the elaborator reads off13-- whether the argument is an object or a morphism of C. Functor(F, C, D),14-- written F : C ⥤ D, says that the source and target of F are the15-- categories C and D, that the object map sends C.obj to D.obj and the16-- morphism map C.mor to D.mor, and that the maps preserve endpoints,17-- identities, and composition.18structure Functor (C D : Set)19  | obj map src tgt : Set20  where21    source_category : Category(C)22    target_category : Category(D)23    objects : obj : C.obj → D.obj24    morphisms : map : C.mor → D.mor25    homs : ∀ (a b ∈ C.obj) (f : a ⟶ b), map(f) : obj(a) ⟶ obj(b)26    identities : ∀ a ∈ C.obj, map(C.id(a)) = D.id(obj(a))27    composites : ∀ (a b c ∈ C.obj) (f : a ⟶ b) (g : b ⟶ c),28      map(g ∘ f) = map(g) ∘ map(f)29    source : src = C30    target : tgt = D3132tactic functor_projections := simp [Functor.mk.obj, Functor.mk.map, Functor.mk.src, Functor.mk.tgt]3334-- A functor hypothesis is a transparent guard, and it supplies both35-- compositions and both arrows: g ∘ f for morphisms of the source, F(g) ∘36-- F(f) for morphisms of the target, f : a ⟶ b for objects of C, and37-- F(f) : F(a) ⟶ F(b) in D.38notation guard "_ : _ ⥤ _" => Functor39notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis Functor(F, C, D) for C.mor40notation infixr 70 "∘" => call2(D.comp, _, _) via hypothesis Functor(F, C, D) for D.mor41notation mixfix "_ : _ ⟶ _" => Morphism(C, _, _, _) via hypothesis Functor(F, C, D) for C.obj, C.mor42notation mixfix "_ : _ ⟶ _" => Morphism(D, _, _, _) via hypothesis Functor(F, C, D) for D.obj, D.mor4344-- Faithful: injective on each hom-set. Full: surjective onto each hom-set45-- between images.46predicate Faithful (F C D : Set) :=47  Functor(F, C, D) ∧ (∀ (a b ∈ obj(C)) (f g : a ⟶ b), F(f) = F(g) → f = g)4849predicate Full (F C D : Set) :=50  Functor(F, C, D) ∧ (∀ (a b ∈ obj(C)) (h : F(a) ⟶ F(b)), ∃ (f : a ⟶ b), F(f) = h)5152section FunctorLaws53variable (F C D : Set)54hypothesis functor : F : C ⥤ D5556theorem Functor.source57  shows src(F) = C58proof59  obtain ⟨shape, source, target, objects, morphisms, homs, identities,60    composites, srcF, tgtF⟩ := functor61  exact srcF6263theorem Functor.target64  shows tgt(F) = D65proof66  obtain ⟨shape, source, target, objects, morphisms, homs, identities,67    composites, srcF, tgtF⟩ := functor68  exact tgtF6970theorem Functor.source_category71  shows Category(C)72proof73  obtain ⟨shape, source, rest⟩ := functor74  exact source7576theorem Functor.target_category77  shows Category(D)78proof79  obtain ⟨shape, source, target, rest⟩ := functor80  exact target8182theorem Functor.data83  shows Functor.Data(F)84proof85  obtain ⟨shape, rest⟩ := functor86  exact shape8788theorem Functor.self89  shows Functor(F, src(F), tgt(F))90proof91  have srcF := Functor.source with functor92  have tgtF := Functor.target with functor93  rw [srcF, tgtF]94  exact functor9596theorem Functor.object_function97  shows obj(F) : obj(C) → obj(D)98proof99  obtain ⟨shape, source, target, objects, rest⟩ := functor100  exact objects101102theorem Functor.morphism_function103  shows map(F) : mor(C) → mor(D)104proof105  obtain ⟨shape, source, target, objects, morphisms, rest⟩ := functor106  exact morphisms107108theorem Functor.object_closed (a : Set)109  requires aInO : a ∈ obj(C)110  shows F(a) ∈ obj(D)111proof112  have function := Functor.object_function with functor113  exact FunctionBetween.apply_closed with function, aInO114115theorem Functor.morphism_closed (f : Set)116  requires fInM : f ∈ mor(C)117  shows F(f) ∈ mor(D)118proof119  have function := Functor.morphism_function with functor120  exact FunctionBetween.apply_closed with function, fInM121122-- The functor laws on hom-typed binders.123instance Functor.map_hom (a b ∈ obj(C)) (f : a ⟶ b)124  shows F(f) : F(a) ⟶ F(b)125proof126  obtain ⟨shape, source, target, objects, morphisms, homs, rest⟩ := functor127  exact homs with a, assumption, b, assumption, f, assumption128129theorem Functor.map_id (a : Set)130  requires aInO : a ∈ obj(C)131  shows F(id(C)(a)) = id(D)(F(a))132proof133  obtain ⟨shape, source, target, objects, morphisms, homs, identities, rest⟩ := functor134  exact identities with a, aInO135136theorem Functor.map_comp (a b c ∈ obj(C)) (f : a ⟶ b) (g : b ⟶ c)137  shows F(g ∘ f) = F(g) ∘ F(f)138proof139  obtain ⟨shape, source, target, objects, morphisms, homs, identities,140    composites, rest⟩ := functor141  exact composites with a, assumption, b, assumption, c, assumption, f, assumption, g, assumption142143-- The same laws on bare morphisms and on hom-sets.144theorem Functor.dom (f : Set)145  requires fInM : f ∈ mor(C)146  shows dom(D)(F(f)) = F(dom(C)(f))147proof148  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *149  have image : F(f) : F(dom(C)(f)) ⟶ F(cod(C)(f)) := Functor.map_hom with *150  cc151152theorem Functor.cod (f : Set)153  requires fInM : f ∈ mor(C)154  shows cod(D)(F(f)) = F(cod(C)(f))155proof156  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *157  have image : F(f) : F(dom(C)(f)) ⟶ F(cod(C)(f)) := Functor.map_hom with *158  cc159160theorem Functor.comp (g f : Set)161  requires gInM : g ∈ mor(C)162  requires fInM : f ∈ mor(C)163  requires composable : dom(C)(g) = cod(C)(f)164  shows F(g ∘ f) = F(g) ∘ F(f)165proof166  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *167  have gHom : g : cod(C)(f) ⟶ cod(C)(g) := Morphism.of_composable with *168  exact Functor.map_comp with *169170theorem Functor.composable (g f : Set)171  requires gInM : g ∈ mor(C)172  requires fInM : f ∈ mor(C)173  requires composable : dom(C)(g) = cod(C)(f)174  shows dom(D)(F(g)) = cod(D)(F(f))175proof176  have domG := Functor.dom with functor, gInM177  have codF := Functor.cod with functor, fInM178  cc179180theorem Functor.hom (a b f : Set)181  requires fHom : f ∈ hom(C, a, b)182  shows F(f) ∈ hom(D, F(a), F(b))183proof184  have typed : f : a ⟶ b := Morphism.of_hom with fHom185  have image : F(f) : F(a) ⟶ F(b) := Functor.map_hom with *186  exact Morphism.hom with image187188-- Functors preserve commutative triangles and squares.189theorem Functor.triangle (a b c ∈ obj(C)) (f : a ⟶ b) (g : b ⟶ c) (h : a ⟶ c)190  requires commutes : g ∘ f = h191  shows F(g) ∘ F(f) = F(h)192proof193  calc194    F(g) ∘ F(f) = F(g ∘ f) := by rw Functor.map_comp195    _ = F(h) := by rw commutes196197theorem Functor.square (a b c d ∈ obj(C)) (f : a ⟶ b) (g : b ⟶ d) (h : a ⟶ c) (k : c ⟶ d)198  requires commutes : g ∘ f = k ∘ h199  shows F(g) ∘ F(f) = F(k) ∘ F(h)200proof201  calc202    F(g) ∘ F(f) = F(g ∘ f) := by rw Functor.map_comp203    _ = F(k ∘ h) := by rw commutes204    _ = F(k) ∘ F(h) := by rw Functor.map_comp205206-- Functors preserve inverse pairs, isomorphisms, retractions, and sections.207theorem Functor.inverse_pair (f g : Set)208  requires pair : InversePair(C, f, g)209  shows InversePair(D, F(f), F(g))210proof211  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := InversePair.hom with *212  have gHom : g : cod(C)(f) ⟶ dom(C)(f) := InversePair.inverse_hom with *213  have gf : g ∘ f = id(C)(dom(C)(f)) := InversePair.left with pair214  have fg : f ∘ g = id(C)(cod(C)(f)) := InversePair.right with pair215  have fImage : F(f) : F(dom(C)(f)) ⟶ F(cod(C)(f)) := Functor.map_hom with *216  have gImage : F(g) : F(cod(C)(f)) ⟶ F(dom(C)(f)) := Functor.map_hom with *217  unfold InversePair218  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩219  . cc220  . cc221  . cc222  . cc223  . calc224      F(g) ∘ F(f) = F(g ∘ f) := by rw Functor.map_comp225      _ = F(id(C)(dom(C)(f))) := by rw gf226      _ = id(D)(F(dom(C)(f))) := by rw Functor.map_id227      _ = id(D)(dom(D)(F(f))) := by cc228  . calc229      F(f) ∘ F(g) = F(f ∘ g) := by rw Functor.map_comp230      _ = F(id(C)(cod(C)(f))) := by rw fg231      _ = id(D)(F(cod(C)(f))) := by rw Functor.map_id232      _ = id(D)(cod(D)(F(f))) := by cc233234theorem Functor.isomorphism (f : Set)235  requires iso : Isomorphism(C, f)236  shows Isomorphism(D, F(f))237proof238  obtain ⟨g, pair⟩ := iso239  have image := Functor.inverse_pair with functor, pair240  exact Isomorphism.of_pair with image241242theorem Functor.isomorphic (a b : Set)243  requires iso : Isomorphic(C, a, b)244  shows Isomorphic(D, F(a), F(b))245proof246  obtain ⟨f, fHom, fIso⟩ := iso247  have imageHom := Functor.hom with functor, fHom248  have imageIso := Functor.isomorphism with functor, fIso249  exact Isomorphic.of_hom with imageHom, imageIso250251theorem Functor.retraction (f r : Set)252  requires retraction : Retraction(C, f, r)253  shows Retraction(D, F(f), F(r))254proof255  obtain ⟨fInM, rInM, domR, codR, law⟩ := retraction256  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *257  have rHom : r : cod(C)(f) ⟶ dom(C)(f) := Morphism.of_dom_cod with *258  have fImage : F(f) : F(dom(C)(f)) ⟶ F(cod(C)(f)) := Functor.map_hom with *259  have rImage : F(r) : F(cod(C)(f)) ⟶ F(dom(C)(f)) := Functor.map_hom with *260  unfold Retraction261  refine ⟨?_, ?_, ?_, ?_, ?_⟩262  . cc263  . cc264  . cc265  . cc266  . calc267      F(r) ∘ F(f) = F(r ∘ f) := by rw Functor.map_comp268      _ = F(id(C)(dom(C)(f))) := by rw law269      _ = id(D)(F(dom(C)(f))) := by rw Functor.map_id270      _ = id(D)(dom(D)(F(f))) := by cc271272theorem Functor.section (f s : Set)273  requires section : SectionOf(C, f, s)274  shows SectionOf(D, F(f), F(s))275proof276  obtain ⟨fInM, sInM, domS, codS, law⟩ := section277  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *278  have sHom : s : cod(C)(f) ⟶ dom(C)(f) := Morphism.of_dom_cod with *279  have fImage : F(f) : F(dom(C)(f)) ⟶ F(cod(C)(f)) := Functor.map_hom with *280  have sImage : F(s) : F(cod(C)(f)) ⟶ F(dom(C)(f)) := Functor.map_hom with *281  unfold SectionOf282  refine ⟨?_, ?_, ?_, ?_, ?_⟩283  . cc284  . cc285  . cc286  . cc287  . calc288      F(f) ∘ F(s) = F(f ∘ s) := by rw Functor.map_comp289      _ = F(id(C)(cod(C)(f))) := by rw law290      _ = id(D)(F(cod(C)(f))) := by rw Functor.map_id291      _ = id(D)(cod(D)(F(f))) := by cc292293theorem Functor.split_mono (f : Set)294  requires split : SplitMonomorphism(C, f)295  shows SplitMonomorphism(D, F(f))296proof297  obtain ⟨r, retraction⟩ := split298  have image := Functor.retraction with functor, retraction299  exact SplitMonomorphism.of_retraction with image300301theorem Functor.split_epi (f : Set)302  requires split : SplitEpimorphism(C, f)303  shows SplitEpimorphism(D, F(f))304proof305  obtain ⟨s, section⟩ := split306  have image := Functor.section with functor, section307  exact SplitEpimorphism.of_section with image308309end FunctorLaws310311-- Faithful and full functors.312theorem Faithful.functor (F C D : Set)313  requires faithful : Faithful(F, C, D)314  shows F : C ⥤ D315proof316  obtain ⟨functor, cancel⟩ := faithful317  exact functor318319theorem Full.functor (F C D : Set)320  requires full : Full(F, C, D)321  shows F : C ⥤ D322proof323  obtain ⟨functor, lift⟩ := full324  exact functor325326section FullFaithful327variable (F C D : Set)328hypothesis functor : F : C ⥤ D329330theorem Faithful.cancel (a b ∈ obj(C)) (f g : a ⟶ b)331  requires faithful : Faithful(F, C, D)332  requires sameImage : F(f) = F(g)333  shows f = g334proof335  obtain ⟨functorF, cancel⟩ := faithful336  exact cancel with a, assumption, b, assumption, f, assumption, g, assumption, sameImage337338theorem Full.lift (a b ∈ obj(C)) (h : F(a) ⟶ F(b))339  requires full : Full(F, C, D)340  shows ∃ (f : a ⟶ b), F(f) = h341proof342  obtain ⟨functorF, lift⟩ := full343  exact lift with a, assumption, b, assumption, h, assumption344345end FullFaithful346347-- The identity functor.348def identityFunctor (C : Set) : Set :=349  Functor.mk(identity(Category.obj(C)), identity(Category.mor(C)), C, C)350351theorem identityFunctor.obj (C a : Set)352  requires aInO : a ∈ Category.obj(C)353  shows obj(identityFunctor(C))(a) = a354proof355  have value := identity.apply with aInO356  simp [identityFunctor, Functor.mk.obj, value]357358theorem identityFunctor.map (C f : Set)359  requires fInM : f ∈ Category.mor(C)360  shows map(identityFunctor(C))(f) = f361proof362  have value := identity.apply with fInM363  simp [identityFunctor, Functor.mk.map, value]364365theorem identityFunctor.src (C : Set)366  shows src(identityFunctor(C)) = C367proof368  unfold identityFunctor369  exact Functor.mk.src at identity(Category.obj(C)), identity(Category.mor(C)), C, C370371theorem identityFunctor.tgt (C : Set)372  shows tgt(identityFunctor(C)) = C373proof374  unfold identityFunctor375  exact Functor.mk.tgt at identity(Category.obj(C)), identity(Category.mor(C)), C, C376377theorem identityFunctor.object_function (C : Set)378  shows obj(identityFunctor(C)) : Category.obj(C) → Category.obj(C)379proof380  unfold identityFunctor381  rw Functor.mk.obj382  exact identity.function at Category.obj(C)383384theorem identityFunctor.morphism_function (C : Set)385  shows map(identityFunctor(C)) : Category.mor(C) → Category.mor(C)386proof387  unfold identityFunctor388  rw Functor.mk.map389  exact identity.function at Category.mor(C)390391section IdentityFunctor392variable (C : Set)393hypothesis category : Category(C)394395theorem Functor.identity396  shows identityFunctor(C) : C ⥤ C397proof398  have objects := identity.function at obj(C)399  have morphisms := identity.function at mor(C)400  unfold identityFunctor401  apply Functor.intro with category, category, objects, morphisms402  . intros a aIn b bIn f fHom403    simpa [identity.apply] using fHom404  . intros a aIn405    simp [identity.apply]406  . intros a aIn b bIn c cIn f fHom g gHom407    simp [identity.apply]408  . rfl409  . rfl410411theorem Faithful.identity412  shows Faithful(identityFunctor(C), C, C)413proof414  have functor := Functor.identity with category415  unfold Faithful416  refine ⟨functor, ?_⟩417  intros a aIn b bIn f fHom g gHom same418  simp [identityFunctor.map] at same419  exact same420421theorem Full.identity422  shows Full(identityFunctor(C), C, C)423proof424  have functor := Functor.identity with category425  unfold Full426  refine ⟨functor, ?_⟩427  intros a aIn b bIn h hHom428  simp [identityFunctor.obj] at hHom429  refine ⟨h, hHom, ?_⟩430  simp [identityFunctor.map]431432end IdentityFunctor433434-- Composition of functors, written F ⋙ G for F followed by G.435def composeFunctor (F G : Set) : Set :=436  Functor.mk(437    compose(Functor.obj(G), Functor.obj(F),438      Category.obj(src(F)), Category.obj(tgt(F)), Category.obj(tgt(G))),439    compose(Functor.map(G), Functor.map(F), mor(src(F)), mor(tgt(F)), mor(tgt(G))),440    src(F), tgt(G))441442notation infixl 80 "⋙" => composeFunctor443444section FunctorComposition445variable (F G C D E : Set)446hypothesis functorF : F : C ⥤ D447hypothesis functorG : G : D ⥤ E448449theorem composeFunctor.src450  shows src(F ⋙ G) = C451proof452  have srcF := Functor.source with functorF453  simp [composeFunctor, Functor.mk.src, srcF]454455theorem composeFunctor.tgt456  shows tgt(F ⋙ G) = E457proof458  have tgtG := Functor.target with functorG459  simp [composeFunctor, Functor.mk.tgt, tgtG]460461theorem composeFunctor.object_function462  shows obj(F ⋙ G) : obj(C) → obj(E)463proof464  have srcF := Functor.source with functorF465  have tgtF := Functor.target with functorF466  have tgtG := Functor.target with functorG467  have objectsF := Functor.object_function with functorF468  have objectsG := Functor.object_function with functorG469  have composed := compose.function with objectsF, objectsG470  unfold composeFunctor471  rw [Functor.mk.obj, srcF, tgtF, tgtG]472  exact composed473474theorem composeFunctor.morphism_function475  shows map(F ⋙ G) : mor(C) → mor(E)476proof477  have srcF := Functor.source with functorF478  have tgtF := Functor.target with functorF479  have tgtG := Functor.target with functorG480  have morphismsF := Functor.morphism_function with functorF481  have morphismsG := Functor.morphism_function with functorG482  have composed := compose.function with morphismsF, morphismsG483  unfold composeFunctor484  rw [Functor.mk.map, srcF, tgtF, tgtG]485  exact composed486487theorem composeFunctor.obj_apply (a : Set)488  requires aInO : a ∈ obj(C)489  shows obj(F ⋙ G)(a) = G(F(a))490proof491  have srcF := Functor.source with functorF492  have tgtF := Functor.target with functorF493  have tgtG := Functor.target with functorG494  have objectsF := Functor.object_function with functorF495  have objectsG := Functor.object_function with functorG496  have value := compose.apply with objectsF, objectsG, aInO497  simp [composeFunctor, Functor.mk.obj, srcF, tgtF, tgtG, value]498499theorem composeFunctor.map_apply (f : Set)500  requires fInM : f ∈ mor(C)501  shows map(F ⋙ G)(f) = G(F(f))502proof503  have srcF := Functor.source with functorF504  have tgtF := Functor.target with functorF505  have tgtG := Functor.target with functorG506  have morphismsF := Functor.morphism_function with functorF507  have morphismsG := Functor.morphism_function with functorG508  have value := compose.apply with morphismsF, morphismsG, fInM509  simp [composeFunctor, Functor.mk.map, srcF, tgtF, tgtG, value]510511-- The data of the composite: its shape, its categories, its two maps, and512-- its source and target, in the order the Functor predicate lists them.513theorem composeFunctor.data514  shows Functor.Data(F ⋙ G) ∧ Category(C) ∧ Category(E) ∧515    (obj(F ⋙ G) : obj(C) → obj(E)) ∧ (map(F ⋙ G) : mor(C) → mor(E)) ∧516    src(F ⋙ G) = C ∧ tgt(F ⋙ G) = E517proof518  have shape : Functor.Data(F ⋙ G) by simp [composeFunctor, Functor.mk.data]519  have source := Functor.source_category with functorF520  have target := Functor.target_category with functorG521  have objects : obj(F ⋙ G) : obj(C) → obj(E) := composeFunctor.object_function with *522  have morphisms : map(F ⋙ G) : mor(C) → mor(E) := composeFunctor.morphism_function with *523  have srcLaw : src(F ⋙ G) = C := composeFunctor.src with *524  have tgtLaw : tgt(F ⋙ G) = E := composeFunctor.tgt with *525  refine ⟨shape, source, target, objects, morphisms, srcLaw, tgtLaw⟩526527theorem Functor.compose528  shows F ⋙ G : C ⥤ E529proof530  obtain ⟨shape, source, target, objects, morphisms, srcLaw, tgtLaw⟩ :=531    composeFunctor.data with functorF, functorG532  unfold Functor533  refine ⟨shape, source, target, objects, morphisms, ?_, ?_, ?_, srcLaw, tgtLaw⟩534  . intros a aIn b bIn f fHom535    simp [composeFunctor.obj_apply, composeFunctor.map_apply]536  . intros a aIn537    simp [composeFunctor.obj_apply, composeFunctor.map_apply, Functor.map_id]538  . intros a aIn b bIn c cIn f fHom g gHom539    simp [composeFunctor.obj_apply, composeFunctor.map_apply, Functor.map_comp]540541-- Faithful functors compose, and so do full functors.542theorem Faithful.compose543  requires faithfulF : Faithful(F, C, D)544  requires faithfulG : Faithful(G, D, E)545  shows Faithful(F ⋙ G, C, E)546proof547  have functor := Functor.compose with functorF, functorG548  unfold Faithful549  refine ⟨functor, ?_⟩550  intros a aIn b bIn f fHom g gHom same551  simp [composeFunctor.map_apply] at same552  have aImage := Functor.object_closed with functorF, aIn553  have bImage := Functor.object_closed with functorF, bIn554  have fImage : F(f) : F(a) ⟶ F(b) := Functor.map_hom with *555  have gImage : F(g) : F(a) ⟶ F(b) := Functor.map_hom with *556  have innerSame : F(f) = F(g) := Faithful.cancel with557    aImage, bImage, fImage, gImage, functorG, faithfulG, same558  exact Faithful.cancel with aIn, bIn, fHom, gHom, functorF, faithfulF, innerSame559560theorem Full.compose561  requires fullF : Full(F, C, D)562  requires fullG : Full(G, D, E)563  shows Full(F ⋙ G, C, E)564proof565  have functor := Functor.compose with functorF, functorG566  unfold Full567  refine ⟨functor, ?_⟩568  intros a aIn b bIn h hHom569  have aImage := Functor.object_closed with functorF, aIn570  have bImage := Functor.object_closed with functorF, bIn571  have objA := composeFunctor.obj_apply with functorF, functorG, aIn572  have objB := composeFunctor.obj_apply with functorF, functorG, bIn573  rw [objA, objB] at hHom574  obtain ⟨k, kHom, kImage⟩ := Full.lift with aImage, bImage, hHom, functorG, fullG575  obtain ⟨f, fHom, fImage⟩ := Full.lift with aIn, bIn, kHom, functorF, fullF576  refine ⟨f, fHom, ?_⟩577  simp [composeFunctor.map_apply, fImage, kImage]578579end FunctorComposition580