Quelle  DerivedMethods.autogen.gi   Sprache: Shell

# SPDX-License-Identifier: GPL-2.0-or-later
# CAP: Categories, Algorithms, Programming
#
# Implementations
#
# THIS FILE IS AUTOMATICALLY GENERATED, SEE CompilerForCAP/tst/generate_opposite_derivations.tst

##
AddDerivationToCAP( AdditionForMorphisms,
                    "dualizing the derivation of AdditionForMorphisms by AdditionForMorphisms(mor1, mor2) as the composition of (mor1,mor2) with the codiagonal morphism",
                    [
                        [ UniversalMorphismFromDirectSum, 1 ],
                        [ IdentityMorphism, 1 ],
                        [ UniversalMorphismIntoDirectSum, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, beta_1 )
    local deduped_1_1, deduped_2_1, deduped_3_1;
    deduped_3_1 := Source( alpha_1 );
    deduped_2_1 := [ deduped_3_1, deduped_3_1 ];
    deduped_1_1 := IdentityMorphism( cat_1, deduped_3_1 );
    return PostCompose( cat_1, UniversalMorphismFromDirectSum( cat_1, deduped_2_1, Range( alpha_1 ), [ alpha_1, beta_1 ] ), UniversalMorphismIntoDirectSum( cat_1, deduped_2_1, deduped_3_1, [ deduped_1_1, deduped_1_1 ] ) );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( AstrictionToCoimage,
                    "dualizing the derivation of CoastrictionToImage by CoastrictionToImage using that image embedding can be seen as a kernel",
                    [
                        [ CoimageProjection, 1 ],
                        [ ColiftAlongEpimorphism, 1 ],
                    ],
                    
  function ( cat_1, alpha_1 )
    return ColiftAlongEpimorphism( cat_1, CoimageProjection( cat_1, alpha_1 ), alpha_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( AstrictionToCoimageWithGivenCoimageObject,
                    "dualizing the derivation of CoastrictionToImageWithGivenImageObject by CoastrictionToImage using that image embedding can be seen as a kernel",
                    [
                        [ CoimageProjectionWithGivenCoimageObject, 1 ],
                        [ ColiftAlongEpimorphism, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, C_1 )
    return ColiftAlongEpimorphism( cat_1, CoimageProjectionWithGivenCoimageObject( cat_1, alpha_1, C_1 ), alpha_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( Coequalizer,
                    "dualizing the derivation of Equalizer by Equalizer as the source of EmbeddingOfEqualizer",
                    [
                        [ ProjectionOntoCoequalizer, 1 ],
                    ],
                    
  function ( cat_1, Y_1, morphisms_1 )
    return Range( ProjectionOntoCoequalizer( cat_1, Y_1, morphisms_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CoequalizerFunctorialWithGivenCoequalizers,
                    "dualizing the derivation of EqualizerFunctorialWithGivenEqualizers by EqualizerFunctorialWithGivenEqualizers using the universality of the limit",
                    [
                        [ UniversalMorphismFromCoequalizerWithGivenCoequalizer, 1 ],
                        [ PostCompose, 1 ],
                        [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ],
                    ],
                    
  function ( cat_1, P_1, morphisms_1, mu_1, morphismsp_1, Pp_1 )
    return UniversalMorphismFromCoequalizerWithGivenCoequalizer( cat_1, Source( mu_1 ), morphisms_1, Pp_1, PostCompose( cat_1, ProjectionOntoCoequalizerWithGivenCoequalizer( cat_1, Range( mu_1 ), morphismsp_1, Pp_1 ), mu_1 ), P_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CoimageObject,
                    "dualizing the derivation of ImageObject by ImageObject as the source of ImageEmbedding",
                    [
                        [ CoimageProjection, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return Range( CoimageProjection( cat_1, arg2_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CoimageObject,
                    "dualizing the derivation of ImageObject by ImageObject as the source of IsomorphismFromImageObjectToKernelOfCokernel",
                    [
                        [ IsomorphismFromCokernelOfKernelToCoimage, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return Range( IsomorphismFromCokernelOfKernelToCoimage( cat_1, arg2_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CoimageObject,
                    "dualizing the derivation of ImageObject by ImageObject as the range of IsomorphismFromKernelOfCokernelToImageObject",
                    [
                        [ IsomorphismFromCoimageToCokernelOfKernel, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return Source( IsomorphismFromCoimageToCokernelOfKernel( cat_1, arg2_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CoimageObjectFunctorialWithGivenCoimageObjects,
                    "dualizing the derivation of ImageObjectFunctorialWithGivenImageObjects by ImageObjectFunctorialWithGivenImageObjects using the universality",
                    [
                        [ ColiftAlongEpimorphism, 1 ],
                        [ CoimageProjectionWithGivenCoimageObject, 2 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, C_1, alpha_1, mu_1, alphap_1, Cp_1 )
    return ColiftAlongEpimorphism( cat_1, CoimageProjectionWithGivenCoimageObject( cat_1, alpha_1, C_1 ), PostCompose( cat_1, CoimageProjectionWithGivenCoimageObject( cat_1, alphap_1, Cp_1 ), mu_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CoimageProjection,
                    "dualizing the derivation of ImageEmbedding by ImageEmbedding as the kernel embedding of the cokernel projection",
                    [
                        [ KernelEmbedding, 1 ],
                        [ CokernelProjection, 1 ],
                        [ IsomorphismFromCokernelOfKernelToCoimage, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, alpha_1 )
    return PostCompose( cat_1, IsomorphismFromCokernelOfKernelToCoimage( cat_1, alpha_1 ), CokernelProjection( cat_1, KernelEmbedding( cat_1, alpha_1 ) ) );
end : CategoryFilter := IsPreAbelianCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CokernelColift,
                    "dualizing the derivation of KernelLift by KernelLift using LiftAlongMonomorphism and KernelEmbedding",
                    [
                        [ ColiftAlongEpimorphism, 1 ],
                        [ CokernelProjection, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, T_1, tau_1 )
    return ColiftAlongEpimorphism( cat_1, CokernelProjection( cat_1, alpha_1 ), tau_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CokernelColiftWithGivenCokernelObject,
                    "dualizing the derivation of KernelLiftWithGivenKernelObject by KernelLift using LiftAlongMonomorphism and KernelEmbedding",
                    [
                        [ ColiftAlongEpimorphism, 1 ],
                        [ CokernelProjectionWithGivenCokernelObject, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, T_1, tau_1, P_1 )
    return ColiftAlongEpimorphism( cat_1, CokernelProjectionWithGivenCokernelObject( cat_1, alpha_1, P_1 ), tau_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CokernelObject,
                    "dualizing the derivation of KernelObject by KernelObject as the source of KernelEmbedding",
                    [
                        [ CokernelProjection, 1 ],
                    ],
                    
  function ( cat_1, alpha_1 )
    return Range( CokernelProjection( cat_1, alpha_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CokernelObjectFunctorialWithGivenCokernelObjects,
                    "dualizing the derivation of KernelObjectFunctorialWithGivenKernelObjects by KernelObjectFunctorialWithGivenKernelObjects using the universality of the limit",
                    [
                        [ CokernelColiftWithGivenCokernelObject, 1 ],
                        [ PostCompose, 1 ],
                        [ CokernelProjectionWithGivenCokernelObject, 1 ],
                    ],
                    
  function ( cat_1, P_1, alpha_1, mu_1, alphap_1, Pp_1 )
    return CokernelColiftWithGivenCokernelObject( cat_1, alpha_1, Pp_1, PostCompose( cat_1, CokernelProjectionWithGivenCokernelObject( cat_1, alphap_1, Pp_1 ), mu_1 ), P_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( ColiftAlongEpimorphism,
                    "dualizing the derivation of LiftAlongMonomorphism by LiftAlongMonomorphism using Lift",
                    [
                        [ Colift, 1 ],
                    ],
                    
  function ( cat_1, epsilon_1, tau_1 )
    return Colift( cat_1, epsilon_1, tau_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( ColiftAlongEpimorphism,
                    "dualizing the derivation of LiftAlongMonomorphism by LiftAlongMonomorphism by inverting the kernel lift from the source to the kernel of the cokernel of a given monomorphism",
                    [
                        [ KernelEmbedding, 1 ],
                        [ CokernelColift, 2 ],
                        [ PostCompose, 1 ],
                        [ InverseForMorphisms, 1 ],
                    ],
                    
  function ( cat_1, epsilon_1, tau_1 )
    local deduped_1_1;
    deduped_1_1 := KernelEmbedding( cat_1, epsilon_1 );
    return PostCompose( cat_1, CokernelColift( cat_1, deduped_1_1, Range( tau_1 ), tau_1 ), InverseForMorphisms( cat_1, CokernelColift( cat_1, deduped_1_1, Range( epsilon_1 ), epsilon_1 ) ) );
end : CategoryFilter := IsAbelianCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( ComponentOfMorphismFromCoproduct,
                    "dualizing the derivation of ComponentOfMorphismIntoDirectProduct by ComponentOfMorphismIntoDirectProduct using ComponentOfMorphismIntoDirectSum",
                    [
                        [ IsomorphismFromDirectSumToCoproduct, 1 ],
                        [ ComponentOfMorphismFromDirectSum, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, I_1, i_1 )
    return ComponentOfMorphismFromDirectSum( cat_1, PostCompose( cat_1, alpha_1, IsomorphismFromDirectSumToCoproduct( cat_1, I_1 ) ), I_1, i_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( ComponentOfMorphismFromCoproduct,
                    "dualizing the derivation of ComponentOfMorphismIntoDirectProduct by ComponentOfMorphismIntoDirectProduct by composing with the direct product projection",
                    [
                        [ InjectionOfCofactorOfCoproduct, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, I_1, i_1 )
    return PostCompose( cat_1, alpha_1, InjectionOfCofactorOfCoproduct( cat_1, I_1, i_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( ComponentOfMorphismFromDirectSum,
                    "dualizing the derivation of ComponentOfMorphismIntoDirectSum by ComponentOfMorphismIntoDirectSum using ComponentOfMorphismIntoDirectProduct",
                    [
                        [ IsomorphismFromCoproductToDirectSum, 1 ],
                        [ ComponentOfMorphismFromCoproduct, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, S_1, i_1 )
    return ComponentOfMorphismFromCoproduct( cat_1, PostCompose( cat_1, alpha_1, IsomorphismFromCoproductToDirectSum( cat_1, S_1 ) ), S_1, i_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( ComponentOfMorphismFromDirectSum,
                    "dualizing the derivation of ComponentOfMorphismIntoDirectSum by ComponentOfMorphismIntoDirectSum by composing with the direct sum projection",
                    [
                        [ InjectionOfCofactorOfDirectSum, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, S_1, i_1 )
    return PostCompose( cat_1, alpha_1, InjectionOfCofactorOfDirectSum( cat_1, S_1, i_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( Coproduct,
                    "dualizing the derivation of DirectProduct by DirectProduct as the source of IsomorphismFromDirectProductToDirectSum",
                    [
                        [ IsomorphismFromDirectSumToCoproduct, 1 ],
                    ],
                    
  function ( cat_1, objects_1 )
    return Range( IsomorphismFromDirectSumToCoproduct( cat_1, objects_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( CoproductFunctorialWithGivenCoproducts,
                    "dualizing the derivation of DirectProductFunctorialWithGivenDirectProducts by DirectProductFunctorialWithGivenDirectProducts using the universality of the limit",
                    [
                        [ UniversalMorphismFromCoproductWithGivenCoproduct, 1 ],
                        [ PostCompose, 2 ],
                        [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ],
                    ],
                    
  function ( cat_1, P_1, objects_1, L_1, objectsp_1, Pp_1 )
    return UniversalMorphismFromCoproductWithGivenCoproduct( cat_1, objects_1, Pp_1, List( [ 1 .. Length( L_1 ) ], function ( i_2 )
              return PostCompose( cat_1, InjectionOfCofactorOfCoproductWithGivenCoproduct( cat_1, objectsp_1, i_2, Pp_1 ), L_1[i_2] );
          end ), P_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( DirectSumFunctorialWithGivenDirectSums,
                    "dualizing the derivation of DirectSumFunctorialWithGivenDirectSums by DirectSumFunctorialWithGivenDirectSums using the universality of the limit",
                    [
                        [ UniversalMorphismFromDirectSumWithGivenDirectSum, 1 ],
                        [ PostCompose, 2 ],
                        [ InjectionOfCofactorOfDirectSumWithGivenDirectSum, 2 ],
                    ],
                    
  function ( cat_1, P_1, objects_1, L_1, objectsp_1, Pp_1 )
    return UniversalMorphismFromDirectSumWithGivenDirectSum( cat_1, objects_1, Pp_1, List( [ 1 .. Length( L_1 ) ], function ( i_2 )
              return PostCompose( cat_1, InjectionOfCofactorOfDirectSumWithGivenDirectSum( cat_1, objectsp_1, i_2, Pp_1 ), L_1[i_2] );
          end ), P_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InitialObject,
                    "dualizing the derivation of TerminalObject by TerminalObject as the source of IsomorphismFromTerminalObjectToZeroObject",
                    [
                        [ IsomorphismFromZeroObjectToInitialObject, 1 ],
                    ],
                    
  function ( cat_1 )
    return Range( IsomorphismFromZeroObjectToInitialObject( cat_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InitialObject,
                    "dualizing the derivation of TerminalObject by TerminalObject as the range of IsomorphismFromZeroObjectToTerminalObject",
                    [
                        [ IsomorphismFromInitialObjectToZeroObject, 1 ],
                    ],
                    
  function ( cat_1 )
    return Source( IsomorphismFromInitialObjectToZeroObject( cat_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InitialObjectFunctorial,
                    "dualizing the derivation of TerminalObjectFunctorial by TerminalObjectFunctorial by taking the identity morphism of TerminalObject",
                    [
                        [ InitialObject, 1 ],
                        [ IdentityMorphism, 1 ],
                    ],
                    
  function ( cat_1 )
    return IdentityMorphism( cat_1, InitialObject( cat_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InitialObjectFunctorialWithGivenInitialObjects,
                    "dualizing the derivation of TerminalObjectFunctorialWithGivenTerminalObjects by TerminalObjectFunctorialWithGivenTerminalObjects using the universality of the limit",
                    [
                        [ UniversalMorphismFromInitialObjectWithGivenInitialObject, 1 ],
                    ],
                    
  function ( cat_1, P_1, Pp_1 )
    return UniversalMorphismFromInitialObjectWithGivenInitialObject( cat_1, Pp_1, P_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InjectionOfCofactorOfCoproduct,
                    "dualizing the derivation of ProjectionInFactorOfDirectProduct by ProjectionInFactorOfDirectProduct using ProjectionInFactorOfDirectSum",
                    [
                        [ IsomorphismFromDirectSumToCoproduct, 1 ],
                        [ InjectionOfCofactorOfDirectSum, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, objects_1, k_1 )
    return PostCompose( cat_1, IsomorphismFromDirectSumToCoproduct( cat_1, objects_1 ), InjectionOfCofactorOfDirectSum( cat_1, objects_1, k_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InjectionOfCofactorOfDirectSum,
                    "dualizing the derivation of ProjectionInFactorOfDirectSum by ProjectionInFactorOfDirectSum using UniversalMorphismFromDirectSum",
                    [
                        [ IdentityMorphism, 1 ],
                        [ ZeroMorphism, 2 ],
                        [ UniversalMorphismIntoDirectSum, 1 ],
                    ],
                    
  function ( cat_1, objects_1, k_1 )
    local hoisted_1_1, deduped_3_1;
    deduped_3_1 := objects_1[k_1];
    hoisted_1_1 := IdentityMorphism( cat_1, deduped_3_1 );
    return UniversalMorphismIntoDirectSum( cat_1, objects_1, deduped_3_1, List( [ 1 .. Length( objects_1 ) ], function ( i_2 )
              if i_2 = k_1 then
                  return hoisted_1_1;
              else
                  return ZeroMorphism( cat_1, deduped_3_1, objects_1[i_2] );
              fi;
              return;
          end ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InjectionOfCofactorOfDirectSum,
                    "dualizing the derivation of ProjectionInFactorOfDirectSum by ProjectionInFactorOfDirectSum using ProjectionInFactorOfDirectProduct",
                    [
                        [ IsomorphismFromCoproductToDirectSum, 1 ],
                        [ InjectionOfCofactorOfCoproduct, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, objects_1, k_1 )
    return PostCompose( cat_1, IsomorphismFromCoproductToDirectSum( cat_1, objects_1 ), InjectionOfCofactorOfCoproduct( cat_1, objects_1, k_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InjectionOfCofactorOfDirectSumWithGivenDirectSum,
                    "dualizing the derivation of ProjectionInFactorOfDirectSumWithGivenDirectSum by ProjectionInFactorOfDirectSum using UniversalMorphismFromDirectSum",
                    [
                        [ IdentityMorphism, 1 ],
                        [ ZeroMorphism, 2 ],
                        [ UniversalMorphismIntoDirectSumWithGivenDirectSum, 1 ],
                    ],
                    
  function ( cat_1, objects_1, k_1, P_1 )
    local hoisted_1_1, deduped_3_1;
    deduped_3_1 := objects_1[k_1];
    hoisted_1_1 := IdentityMorphism( cat_1, deduped_3_1 );
    return UniversalMorphismIntoDirectSumWithGivenDirectSum( cat_1, objects_1, deduped_3_1, List( [ 1 .. Length( objects_1 ) ], function ( i_2 )
              if i_2 = k_1 then
                  return hoisted_1_1;
              else
                  return ZeroMorphism( cat_1, deduped_3_1, objects_1[i_2] );
              fi;
              return;
          end ), P_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InjectionOfCofactorOfPushout,
                    "dualizing the derivation of ProjectionInFactorOfFiberProduct by ProjectionInFactorOfFiberProduct by composing the embedding of equalizer with the direct product projection",
                    [
                        [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ],
                        [ PostCompose, 3 ],
                        [ ProjectionOntoCoequalizer, 1 ],
                        [ Coproduct, 1 ],
                        [ ComponentOfMorphismFromCoproduct, 1 ],
                        [ IsomorphismFromCoequalizerOfCoproductDiagramToPushout, 1 ],
                    ],
                    
  function ( cat_1, morphisms_1, k_1 )
    local deduped_3_1, deduped_4_1;
    deduped_4_1 := List( morphisms_1, Range );
    deduped_3_1 := Coproduct( cat_1, deduped_4_1 );
    return PostCompose( cat_1, IsomorphismFromCoequalizerOfCoproductDiagramToPushout( cat_1, morphisms_1 ), ComponentOfMorphismFromCoproduct( cat_1, ProjectionOntoCoequalizer( cat_1, deduped_3_1, List( [ 1 .. Length( morphisms_1 ) ], function ( i_2 )
                  return PostCompose( cat_1, InjectionOfCofactorOfCoproductWithGivenCoproduct( cat_1, deduped_4_1, i_2, deduped_3_1 ), morphisms_1[i_2] );
              end ) ), deduped_4_1, k_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InjectiveColift,
                    "dualizing the derivation of ProjectiveLift by ProjectiveLift using Lift",
                    [
                        [ Colift, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, beta_1 )
    return Colift( cat_1, alpha_1, beta_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InjectiveEnvelopeObject,
                    "dualizing the derivation of ProjectiveCoverObject by ProjectiveCoverObject as the source of EpimorphismFromProjectiveCoverObject",
                    [
                        [ MonomorphismIntoInjectiveEnvelopeObject, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return Range( MonomorphismIntoInjectiveEnvelopeObject( cat_1, arg2_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( InverseForMorphisms,
                    "dualizing the derivation of InverseForMorphisms by InverseForMorphisms using LiftAlongMonomorphism of an identity morphism",
                    [
                        [ IdentityMorphism, 1 ],
                        [ ColiftAlongEpimorphism, 1 ],
                    ],
                    
  function ( cat_1, alpha_1 )
    return ColiftAlongEpimorphism( cat_1, alpha_1, IdentityMorphism( cat_1, Source( alpha_1 ) ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsCodominating,
                    "dualizing the derivation of IsDominating by IsDominating using IsLiftableAlongMonomorphism",
                    [
                        [ IsColiftableAlongEpimorphism, 1 ],
                    ],
                    
  function ( cat_1, arg2_1, arg3_1 )
    return IsColiftableAlongEpimorphism( cat_1, arg3_1, arg2_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsCodominating,
                    "dualizing the derivation of IsDominating by IsDominating using IsCodominating and duality by cokernel",
                    [
                        [ KernelEmbedding, 2 ],
                        [ IsDominating, 1 ],
                    ],
                    
  function ( cat_1, arg2_1, arg3_1 )
    return IsDominating( cat_1, KernelEmbedding( cat_1, arg3_1 ), KernelEmbedding( cat_1, arg2_1 ) );
end : CategoryFilter := IsAbelianCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsCodominating,
                    "dualizing the derivation of IsDominating by IsDominating(sub1, sub2) by deciding if sub1 composed with CokernelProjection(cat, sub2) is zero",
                    [
                        [ KernelEmbedding, 1 ],
                        [ PostCompose, 1 ],
                        [ IsZeroForMorphisms, 1 ],
                    ],
                    
  function ( cat_1, arg2_1, arg3_1 )
    return IsZeroForMorphisms( cat_1, PostCompose( cat_1, arg2_1, KernelEmbedding( cat_1, arg3_1 ) ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsColiftable,
                    "dualizing the derivation of IsLiftable by Two morphisms with equal targets are mutually liftable in a terminal category",
                    [
                    ],
                    
  function ( cat_1, arg2_1, arg3_1 )
    return true;
end : CategoryFilter := IsTerminalCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsColiftableAlongEpimorphism,
                    "dualizing the derivation of IsLiftableAlongMonomorphism by IsLiftableAlongMonomorphism using IsLiftable",
                    [
                        [ IsColiftable, 1 ],
                    ],
                    
  function ( cat_1, arg2_1, arg3_1 )
    return IsColiftable( cat_1, arg2_1, arg3_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsEpimorphism,
                    "dualizing the derivation of IsMonomorphism by IsMonomorphism by deciding if the kernel is a zero object",
                    [
                        [ IsZeroForObjects, 1 ],
                        [ CokernelObject, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return IsZeroForObjects( cat_1, CokernelObject( cat_1, arg2_1 ) );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsEpimorphism,
                    "dualizing the derivation of IsMonomorphism by IsMonomorphism by deciding if the diagonal morphism is an isomorphism",
                    [
                        [ IsIsomorphism, 1 ],
                        [ IdentityMorphism, 1 ],
                        [ UniversalMorphismFromPushout, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    local deduped_1_1, deduped_2_1;
    deduped_2_1 := Range( arg2_1 );
    deduped_1_1 := IdentityMorphism( cat_1, deduped_2_1 );
    return IsIsomorphism( cat_1, UniversalMorphismFromPushout( cat_1, [ arg2_1, arg2_1 ], deduped_2_1, [ deduped_1_1, deduped_1_1 ] ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsEqualAsFactorobjects,
                    "dualizing the derivation of IsEqualAsSubobjects by IsEqualAsSubobjects(sub1, sub2) if sub1 dominates sub2 and vice versa",
                    [
                        [ IsCodominating, 2 ],
                    ],
                    
  function ( cat_1, arg2_1, arg3_1 )
    return IsCodominating( cat_1, arg2_1, arg3_1 ) and IsCodominating( cat_1, arg3_1, arg2_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsIdempotent,
                    "dualizing the derivation of IsIdempotent by IsIdempotent by comparing the square of the morphism with itself",
                    [
                        [ IsCongruentForMorphisms, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return IsCongruentForMorphisms( cat_1, PostCompose( cat_1, arg2_1, arg2_1 ), arg2_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsInitial,
                    "dualizing the derivation of IsTerminal by IsTerminal using IsZeroForObjects",
                    [
                        [ IsZeroForObjects, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return IsZeroForObjects( cat_1, arg2_1 );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsInitial,
                    "dualizing the derivation of IsTerminal by IsTerminal using IsIsomorphism( cat, UniversalMorphismIntoTerminalObject )",
                    [
                        [ IsIsomorphism, 1 ],
                        [ UniversalMorphismFromInitialObject, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return IsIsomorphism( cat_1, UniversalMorphismFromInitialObject( cat_1, arg2_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsInjective,
                    "dualizing the derivation of IsProjective by IsProjective by checking if the object is a retract of some projective object",
                    [
                        [ MonomorphismIntoSomeInjectiveObject, 1 ],
                        [ IsSplitMonomorphism, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return IsSplitMonomorphism( cat_1, MonomorphismIntoSomeInjectiveObject( cat_1, arg2_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsInjective,
                    "dualizing the derivation of IsProjective by ",
                    [
                        [ MonomorphismIntoInjectiveEnvelopeObject, 1 ],
                        [ IsIsomorphism, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return IsIsomorphism( cat_1, MonomorphismIntoInjectiveEnvelopeObject( cat_1, arg2_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsIsomorphism,
                    "dualizing the derivation of IsIsomorphism by IsIsomorphism by deciding if it is a split mono and an epi",
                    [
                        [ IsSplitEpimorphism, 1 ],
                        [ IsMonomorphism, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return IsSplitEpimorphism( cat_1, arg2_1 ) and IsMonomorphism( cat_1, arg2_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsSplitEpimorphism,
                    "dualizing the derivation of IsSplitMonomorphism by IsSplitMonomorphism by using IsColiftable",
                    [
                        [ IsLiftable, 1 ],
                        [ IdentityMorphism, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return IsLiftable( cat_1, IdentityMorphism( cat_1, Range( arg2_1 ) ), arg2_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromCoequalizerOfCoproductDiagramToPushout,
                    "dualizing the derivation of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram by IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram using the universal property of the equalizer",
                    [
                        [ Coproduct, 1 ],
                        [ PostCompose, 2 ],
                        [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ],
                        [ InjectionOfCofactorOfPushoutWithGivenPushout, 2 ],
                        [ UniversalMorphismFromCoproductWithGivenCoproduct, 1 ],
                        [ Pushout, 1 ],
                        [ UniversalMorphismFromCoequalizer, 1 ],
                    ],
                    
  function ( cat_1, D_1 )
    local deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1;
    deduped_7_1 := Pushout( cat_1, D_1 );
    deduped_6_1 := List( D_1, Range );
    deduped_5_1 := [ 1 .. Length( D_1 ) ];
    deduped_4_1 := Coproduct( cat_1, deduped_6_1 );
    return UniversalMorphismFromCoequalizer( cat_1, deduped_4_1, List( deduped_5_1, function ( i_2 )
              return PostCompose( cat_1, InjectionOfCofactorOfCoproductWithGivenCoproduct( cat_1, deduped_6_1, i_2, deduped_4_1 ), D_1[i_2] );
          end ), deduped_7_1, UniversalMorphismFromCoproductWithGivenCoproduct( cat_1, deduped_6_1, deduped_7_1, List( deduped_5_1, function ( i_2 )
                return InjectionOfCofactorOfPushoutWithGivenPushout( cat_1, D_1, i_2, deduped_7_1 );
            end ), deduped_4_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromCoequalizerOfCoproductDiagramToPushout,
                    "dualizing the derivation of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram by IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram as the inverse of IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct",
                    [
                        [ IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, 1 ],
                        [ InverseForMorphisms, 1 ],
                    ],
                    
  function ( cat_1, D_1 )
    return InverseForMorphisms( cat_1, IsomorphismFromPushoutToCoequalizerOfCoproductDiagram( cat_1, D_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct,
                    "dualizing the derivation of IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer by IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer using the universal property of the equalizer",
                    [
                        [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ],
                        [ CokernelObject, 1 ],
                        [ CokernelProjectionWithGivenCokernelObject, 1 ],
                        [ UniversalMorphismFromCoequalizer, 1 ],
                    ],
                    
  function ( cat_1, A_1, D_1 )
    local deduped_1_1, deduped_2_1;
    deduped_2_1 := JointPairwiseDifferencesOfMorphismsFromCoproduct( cat_1, A_1, D_1 );
    deduped_1_1 := CokernelObject( cat_1, deduped_2_1 );
    return UniversalMorphismFromCoequalizer( cat_1, A_1, D_1, deduped_1_1, CokernelProjectionWithGivenCokernelObject( cat_1, deduped_2_1, deduped_1_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromCoimageToCokernelOfKernel,
                    "dualizing the derivation of IsomorphismFromKernelOfCokernelToImageObject by IsomorphismFromKernelOfCokernelToImageObject as the inverse of IsomorphismFromImageObjectToKernelOfCokernel",
                    [
                        [ InverseForMorphisms, 1 ],
                        [ IsomorphismFromCokernelOfKernelToCoimage, 1 ],
                    ],
                    
  function ( cat_1, alpha_1 )
    return InverseForMorphisms( cat_1, IsomorphismFromCokernelOfKernelToCoimage( cat_1, alpha_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer,
                    "dualizing the derivation of IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct by IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct using the universal property of the kernel",
                    [
                        [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ],
                        [ Coequalizer, 1 ],
                        [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ],
                        [ CokernelColift, 1 ],
                    ],
                    
  function ( cat_1, A_1, D_1 )
    local deduped_1_1;
    deduped_1_1 := Coequalizer( cat_1, A_1, D_1 );
    return CokernelColift( cat_1, JointPairwiseDifferencesOfMorphismsFromCoproduct( cat_1, A_1, D_1 ), deduped_1_1, ProjectionOntoCoequalizerWithGivenCoequalizer( cat_1, A_1, D_1, deduped_1_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromCokernelOfKernelToCoimage,
                    "dualizing the derivation of IsomorphismFromImageObjectToKernelOfCokernel by IsomorphismFromImageObjectToKernelOfCokernel as the inverse of IsomorphismFromKernelOfCokernelToImageObject",
                    [
                        [ InverseForMorphisms, 1 ],
                        [ IsomorphismFromCoimageToCokernelOfKernel, 1 ],
                    ],
                    
  function ( cat_1, alpha_1 )
    return InverseForMorphisms( cat_1, IsomorphismFromCoimageToCokernelOfKernel( cat_1, alpha_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromCokernelOfKernelToCoimage,
                    "dualizing the derivation of IsomorphismFromImageObjectToKernelOfCokernel by IsomorphismFromImageObjectToKernelOfCokernel using the universal property of the image",
                    [
                        [ CokernelProjection, 1 ],
                        [ KernelEmbedding, 1 ],
                        [ ColiftAlongEpimorphism, 1 ],
                        [ UniversalMorphismIntoCoimage, 1 ],
                    ],
                    
  function ( cat_1, alpha_1 )
    local deduped_1_1;
    deduped_1_1 := CokernelProjection( cat_1, KernelEmbedding( cat_1, alpha_1 ) );
    return UniversalMorphismIntoCoimage( cat_1, alpha_1, NTuple( 2, deduped_1_1, ColiftAlongEpimorphism( cat_1, deduped_1_1, alpha_1 ) ) );
end : CategoryFilter := IsAbelianCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromCoproductToDirectSum,
                    "dualizing the derivation of IsomorphismFromDirectSumToDirectProduct by IsomorphismFromDirectSumToDirectProduct using direct sum projections and universal property of direct product",
                    [
                        [ InjectionOfCofactorOfDirectSum, 2 ],
                        [ DirectSum, 1 ],
                        [ UniversalMorphismFromCoproduct, 1 ],
                    ],
                    
  function ( cat_1, D_1 )
    return UniversalMorphismFromCoproduct( cat_1, D_1, DirectSum( cat_1, D_1 ), List( [ 1 .. Length( D_1 ) ], function ( i_2 )
              return InjectionOfCofactorOfDirectSum( cat_1, D_1, i_2 );
          end ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromCoproductToDirectSum,
                    "dualizing the derivation of IsomorphismFromDirectSumToDirectProduct by IsomorphismFromDirectSumToDirectProduct as the inverse of IsomorphismFromDirectProductToDirectSum",
                    [
                        [ InverseForMorphisms, 1 ],
                        [ IsomorphismFromDirectSumToCoproduct, 1 ],
                    ],
                    
  function ( cat_1, D_1 )
    return InverseForMorphisms( cat_1, IsomorphismFromDirectSumToCoproduct( cat_1, D_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromDirectSumToCoproduct,
                    "dualizing the derivation of IsomorphismFromDirectProductToDirectSum by IsomorphismFromDirectProductToDirectSum using direct product projections and universal property of direct sum",
                    [
                        [ InjectionOfCofactorOfCoproduct, 2 ],
                        [ Coproduct, 1 ],
                        [ UniversalMorphismFromDirectSum, 1 ],
                    ],
                    
  function ( cat_1, D_1 )
    return UniversalMorphismFromDirectSum( cat_1, D_1, Coproduct( cat_1, D_1 ), List( [ 1 .. Length( D_1 ) ], function ( i_2 )
              return InjectionOfCofactorOfCoproduct( cat_1, D_1, i_2 );
          end ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromDirectSumToCoproduct,
                    "dualizing the derivation of IsomorphismFromDirectProductToDirectSum by IsomorphismFromDirectProductToDirectSum as the inverse of IsomorphismFromDirectSumToDirectProduct",
                    [
                        [ IsomorphismFromCoproductToDirectSum, 1 ],
                        [ InverseForMorphisms, 1 ],
                    ],
                    
  function ( cat_1, D_1 )
    return InverseForMorphisms( cat_1, IsomorphismFromCoproductToDirectSum( cat_1, D_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromInitialObjectToZeroObject,
                    "dualizing the derivation of IsomorphismFromZeroObjectToTerminalObject by IsomorphismFromZeroObjectToTerminalObject as the unique morphism from zero object to terminal object",
                    [
                        [ UniversalMorphismFromInitialObject, 1 ],
                        [ ZeroObject, 1 ],
                    ],
                    
  function ( cat_1 )
    return UniversalMorphismFromInitialObject( cat_1, ZeroObject( cat_1 ) );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromInitialObjectToZeroObject,
                    "dualizing the derivation of IsomorphismFromZeroObjectToTerminalObject by IsomorphismFromZeroObjectToTerminalObject using the universal property of the zero object",
                    [
                        [ UniversalMorphismIntoZeroObject, 1 ],
                        [ InitialObject, 1 ],
                    ],
                    
  function ( cat_1 )
    return UniversalMorphismIntoZeroObject( cat_1, InitialObject( cat_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromInitialObjectToZeroObject,
                    "dualizing the derivation of IsomorphismFromZeroObjectToTerminalObject by IsomorphismFromZeroObjectToTerminalObject as the inverse of IsomorphismFromTerminalObjectToZeroObject",
                    [
                        [ InverseForMorphisms, 1 ],
                        [ IsomorphismFromZeroObjectToInitialObject, 1 ],
                    ],
                    
  function ( cat_1 )
    return InverseForMorphisms( cat_1, IsomorphismFromZeroObjectToInitialObject( cat_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromPushoutToCoequalizerOfCoproductDiagram,
                    "dualizing the derivation of IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct by IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct using the universal property of the fiber product",
                    [
                        [ PostCompose, 4 ],
                        [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ],
                        [ Coproduct, 1 ],
                        [ Coequalizer, 1 ],
                        [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ],
                        [ UniversalMorphismFromPushout, 1 ],
                    ],
                    
  function ( cat_1, D_1 )
    local hoisted_4_1, deduped_5_1, deduped_6_1, deduped_7_1, deduped_8_1, deduped_9_1;
    deduped_9_1 := List( D_1, Range );
    deduped_8_1 := [ 1 .. Length( D_1 ) ];
    deduped_7_1 := Coproduct( cat_1, deduped_9_1 );
    deduped_6_1 := List( deduped_8_1, function ( i_2 )
            return PostCompose( cat_1, InjectionOfCofactorOfCoproductWithGivenCoproduct( cat_1, deduped_9_1, i_2, deduped_7_1 ), D_1[i_2] );
        end );
    deduped_5_1 := Coequalizer( cat_1, deduped_7_1, deduped_6_1 );
    hoisted_4_1 := ProjectionOntoCoequalizerWithGivenCoequalizer( cat_1, deduped_7_1, deduped_6_1, deduped_5_1 );
    return UniversalMorphismFromPushout( cat_1, D_1, deduped_5_1, List( deduped_8_1, function ( i_2 )
              return PostCompose( cat_1, hoisted_4_1, deduped_6_1[i_2] );
          end ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromPushoutToCoequalizerOfCoproductDiagram,
                    "dualizing the derivation of IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct by IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct as the inverse of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram",
                    [
                        [ IsomorphismFromCoequalizerOfCoproductDiagramToPushout, 1 ],
                        [ InverseForMorphisms, 1 ],
                    ],
                    
  function ( cat_1, D_1 )
    return InverseForMorphisms( cat_1, IsomorphismFromCoequalizerOfCoproductDiagramToPushout( cat_1, D_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromZeroObjectToInitialObject,
                    "dualizing the derivation of IsomorphismFromTerminalObjectToZeroObject by IsomorphismFromTerminalObjectToZeroObject as the inverse of IsomorphismFromZeroObjectToTerminalObject",
                    [
                        [ InverseForMorphisms, 1 ],
                        [ IsomorphismFromInitialObjectToZeroObject, 1 ],
                    ],
                    
  function ( cat_1 )
    return InverseForMorphisms( cat_1, IsomorphismFromInitialObjectToZeroObject( cat_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( IsomorphismFromZeroObjectToInitialObject,
                    "dualizing the derivation of IsomorphismFromTerminalObjectToZeroObject by IsomorphismFromTerminalObjectToZeroObject using the universal property of the zero object",
                    [
                        [ UniversalMorphismFromZeroObject, 1 ],
                        [ InitialObject, 1 ],
                    ],
                    
  function ( cat_1 )
    return UniversalMorphismFromZeroObject( cat_1, InitialObject( cat_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( MorphismFromCoimageToImageWithGivenObjects,
                    "dualizing the derivation of MorphismFromCoimageToImageWithGivenObjects by MorphismFromCoimageToImageWithGivenObjects using that images are given by kernels of cokernels",
                    [
                        [ KernelEmbedding, 1 ],
                        [ CokernelColift, 1 ],
                        [ CoastrictionToImageWithGivenImageObject, 1 ],
                        [ PostCompose, 1 ],
                        [ IsomorphismFromCoimageToCokernelOfKernel, 1 ],
                    ],
                    
  function ( cat_1, C_1, alpha_1, I_1 )
    return PostCompose( cat_1, CokernelColift( cat_1, KernelEmbedding( cat_1, alpha_1 ), I_1, CoastrictionToImageWithGivenImageObject( cat_1, alpha_1, I_1 ) ), IsomorphismFromCoimageToCokernelOfKernel( cat_1, alpha_1 ) );
end : CategoryFilter := IsPreAbelianCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( MorphismFromSourceToCoequalizer,
                    "dualizing the derivation of MorphismFromEqualizerToSink by MorphismFromEqualizerToSink by composing the embedding with the first morphism in the diagram",
                    [
                        [ ProjectionOntoCoequalizer, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, Y_1, morphisms_1 )
    return PostCompose( cat_1, ProjectionOntoCoequalizer( cat_1, Y_1, morphisms_1 ), morphisms_1[1] );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( MorphismFromSourceToCokernelObject,
                    "dualizing the derivation of MorphismFromKernelObjectToSink by MorphismFromKernelObjectToSink as zero morphism from kernel object to range",
                    [
                        [ CokernelObject, 1 ],
                        [ ZeroMorphism, 1 ],
                    ],
                    
  function ( cat_1, alpha_1 )
    return ZeroMorphism( cat_1, Source( alpha_1 ), CokernelObject( cat_1, alpha_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( MorphismFromSourceToPushout,
                    "dualizing the derivation of MorphismFromFiberProductToSink by MorphismFromFiberProductToSink by composing the first projection with the first morphism in the diagram",
                    [
                        [ InjectionOfCofactorOfPushout, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, morphisms_1 )
    return PostCompose( cat_1, InjectionOfCofactorOfPushout( cat_1, morphisms_1, 1 ), morphisms_1[1] );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( PostCompose,
                    "dualizing the derivation of PreCompose by PreCompose using PostCompose and swapping arguments",
                    [
                        [ PreCompose, 1 ],
                    ],
                    
  function ( cat_1, beta_1, alpha_1 )
    return PreCompose( cat_1, alpha_1, beta_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( PostCompose,
                    "dualizing the derivation of PreCompose by PreCompose by wrapping the arguments in a list",
                    [
                        [ PostComposeList, 1 ],
                    ],
                    
  function ( cat_1, beta_1, alpha_1 )
    return PostComposeList( cat_1, Source( alpha_1 ), [ beta_1, alpha_1 ], Range( beta_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( PostComposeList,
                    "dualizing the derivation of PreComposeList by PreComposeList by iterating PreCompose",
                    [
                        [ IdentityMorphism, 2 ],
                        [ PostCompose, 2 ],
                    ],
                    
  function ( cat_1, source_1, list_of_morphisms_1, range_1 )
    return Iterated( list_of_morphisms_1, function ( alpha_2, beta_2 )
            return PostCompose( cat_1, alpha_2, beta_2 );
        end, IdentityMorphism( cat_1, range_1 ), IdentityMorphism( cat_1, source_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( PostInverseForMorphisms,
                    "dualizing the derivation of PreInverseForMorphisms by PreInverseForMorphisms using IdentityMorphism and Lift",
                    [
                        [ IdentityMorphism, 1 ],
                        [ Colift, 1 ],
                    ],
                    
  function ( cat_1, alpha_1 )
    return Colift( cat_1, alpha_1, IdentityMorphism( cat_1, Source( alpha_1 ) ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( ProjectionOntoCoequalizer,
                    "dualizing the derivation of EmbeddingOfEqualizer by EmbeddingOfEqualizer using the kernel embedding of JointPairwiseDifferencesOfMorphismsIntoDirectProduct",
                    [
                        [ CokernelProjection, 1 ],
                        [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ],
                        [ PostCompose, 1 ],
                        [ IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer, 1 ],
                    ],
                    
  function ( cat_1, Y_1, morphisms_1 )
    return PostCompose( cat_1, IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer( cat_1, Y_1, morphisms_1 ), CokernelProjection( cat_1, JointPairwiseDifferencesOfMorphismsFromCoproduct( cat_1, Y_1, morphisms_1 ) ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( Pushout,
                    "dualizing the derivation of FiberProduct by FiberProduct as the source of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram",
                    [
                        [ IsomorphismFromCoequalizerOfCoproductDiagramToPushout, 1 ],
                    ],
                    
  function ( cat_1, morphisms_1 )
    return Range( IsomorphismFromCoequalizerOfCoproductDiagramToPushout( cat_1, morphisms_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( PushoutFunctorialWithGivenPushouts,
                    "dualizing the derivation of FiberProductFunctorialWithGivenFiberProducts by FiberProductFunctorialWithGivenFiberProducts using the universality of the limit",
                    [
                        [ UniversalMorphismFromPushoutWithGivenPushout, 1 ],
                        [ PostCompose, 2 ],
                        [ InjectionOfCofactorOfPushoutWithGivenPushout, 2 ],
                    ],
                    
  function ( cat_1, P_1, morphisms_1, L_1, morphismsp_1, Pp_1 )
    return UniversalMorphismFromPushoutWithGivenPushout( cat_1, morphisms_1, Pp_1, List( [ 1 .. Length( L_1 ) ], function ( i_2 )
              return PostCompose( cat_1, InjectionOfCofactorOfPushoutWithGivenPushout( cat_1, morphismsp_1, i_2, Pp_1 ), L_1[i_2] );
          end ), P_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( SomeInjectiveObject,
                    "dualizing the derivation of SomeProjectiveObject by SomeProjectiveObject as the source of EpimorphismFromSomeProjectiveObject",
                    [
                        [ MonomorphismIntoSomeInjectiveObject, 1 ],
                    ],
                    
  function ( cat_1, arg2_1 )
    return Range( MonomorphismIntoSomeInjectiveObject( cat_1, arg2_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromCoequalizer,
                    "dualizing the derivation of UniversalMorphismIntoEqualizer by UniversalMorphismIntoEqualizer using the universality of the kernel representation of the equalizer",
                    [
                        [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ],
                        [ CokernelColift, 1 ],
                        [ IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, Y_1, morphisms_1, T_1, tau_1 )
    return PostCompose( cat_1, CokernelColift( cat_1, JointPairwiseDifferencesOfMorphismsFromCoproduct( cat_1, Y_1, morphisms_1 ), T_1, tau_1 ), IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct( cat_1, Y_1, morphisms_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromCoequalizer,
                    "dualizing the derivation of UniversalMorphismIntoEqualizer by UniversalMorphismIntoEqualizer using LiftAlongMonomorphism and EmbeddingOfEqualizer",
                    [
                        [ ColiftAlongEpimorphism, 1 ],
                        [ ProjectionOntoCoequalizer, 1 ],
                    ],
                    
  function ( cat_1, Y_1, morphisms_1, T_1, tau_1 )
    return ColiftAlongEpimorphism( cat_1, ProjectionOntoCoequalizer( cat_1, Y_1, morphisms_1 ), tau_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromCoequalizerWithGivenCoequalizer,
                    "dualizing the derivation of UniversalMorphismIntoEqualizerWithGivenEqualizer by UniversalMorphismIntoEqualizer using LiftAlongMonomorphism and EmbeddingOfEqualizer",
                    [
                        [ ColiftAlongEpimorphism, 1 ],
                        [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ],
                    ],
                    
  function ( cat_1, Y_1, morphisms_1, T_1, tau_1, P_1 )
    return ColiftAlongEpimorphism( cat_1, ProjectionOntoCoequalizerWithGivenCoequalizer( cat_1, Y_1, morphisms_1, P_1 ), tau_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromCoproduct,
                    "dualizing the derivation of UniversalMorphismIntoDirectProduct by UniversalMorphismIntoDirectProduct using UniversalMorphismIntoDirectSum",
                    [
                        [ UniversalMorphismFromDirectSum, 1 ],
                        [ IsomorphismFromCoproductToDirectSum, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, objects_1, T_1, tau_1 )
    return PostCompose( cat_1, UniversalMorphismFromDirectSum( cat_1, objects_1, T_1, tau_1 ), IsomorphismFromCoproductToDirectSum( cat_1, objects_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromDirectSum,
                    "dualizing the derivation of UniversalMorphismIntoDirectSum by UniversalMorphismIntoDirectSum using the injections of the direct sum",
                    [
                        [ PostCompose, 2 ],
                        [ ProjectionInFactorOfDirectSum, 2 ],
                        [ SumOfMorphisms, 1 ],
                        [ DirectSum, 1 ],
                    ],
                    
  function ( cat_1, objects_1, T_1, tau_1 )
    return SumOfMorphisms( cat_1, DirectSum( cat_1, objects_1 ), List( [ 1 .. Length( tau_1 ) ], function ( i_2 )
              return PostCompose( cat_1, tau_1[i_2], ProjectionInFactorOfDirectSum( cat_1, objects_1, i_2 ) );
          end ), T_1 );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromDirectSum,
                    "dualizing the derivation of UniversalMorphismIntoDirectSum by UniversalMorphismIntoDirectSum using UniversalMorphismIntoDirectProduct",
                    [
                        [ UniversalMorphismFromCoproduct, 1 ],
                        [ IsomorphismFromDirectSumToCoproduct, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, objects_1, T_1, tau_1 )
    return PostCompose( cat_1, UniversalMorphismFromCoproduct( cat_1, objects_1, T_1, tau_1 ), IsomorphismFromDirectSumToCoproduct( cat_1, objects_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromDirectSumWithGivenDirectSum,
                    "dualizing the derivation of UniversalMorphismIntoDirectSumWithGivenDirectSum by UniversalMorphismIntoDirectSum using the injections of the direct sum",
                    [
                        [ PostCompose, 2 ],
                        [ ProjectionInFactorOfDirectSumWithGivenDirectSum, 2 ],
                        [ SumOfMorphisms, 1 ],
                    ],
                    
  function ( cat_1, objects_1, T_1, tau_1, P_1 )
    return SumOfMorphisms( cat_1, P_1, List( [ 1 .. Length( tau_1 ) ], function ( i_2 )
              return PostCompose( cat_1, tau_1[i_2], ProjectionInFactorOfDirectSumWithGivenDirectSum( cat_1, objects_1, i_2, P_1 ) );
          end ), T_1 );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromInitialObject,
                    "dualizing the derivation of UniversalMorphismIntoTerminalObject by UniversalMorphismIntoTerminalObject computing the zero morphism",
                    [
                        [ InitialObject, 1 ],
                        [ ZeroMorphism, 1 ],
                    ],
                    
  function ( cat_1, T_1 )
    return ZeroMorphism( cat_1, InitialObject( cat_1 ), T_1 );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromInitialObject,
                    "dualizing the derivation of UniversalMorphismIntoTerminalObject by UniversalMorphismFromInitialObject using UniversalMorphismFromZeroObject",
                    [
                        [ UniversalMorphismFromZeroObject, 1 ],
                        [ IsomorphismFromInitialObjectToZeroObject, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, T_1 )
    return PostCompose( cat_1, UniversalMorphismFromZeroObject( cat_1, T_1 ), IsomorphismFromInitialObjectToZeroObject( cat_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromInitialObjectWithGivenInitialObject,
                    "dualizing the derivation of UniversalMorphismIntoTerminalObjectWithGivenTerminalObject by UniversalMorphismIntoTerminalObject computing the zero morphism",
                    [
                        [ ZeroMorphism, 1 ],
                    ],
                    
  function ( cat_1, T_1, P_1 )
    return ZeroMorphism( cat_1, P_1, T_1 );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromPushout,
                    "dualizing the derivation of UniversalMorphismIntoFiberProduct by UniversalMorphismIntoFiberProduct as the universal morphism into equalizer of a univeral morphism into direct product",
                    [
                        [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ],
                        [ PostCompose, 3 ],
                        [ UniversalMorphismFromCoproduct, 1 ],
                        [ UniversalMorphismFromCoequalizer, 1 ],
                        [ Coproduct, 1 ],
                        [ IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, 1 ],
                    ],
                    
  function ( cat_1, morphisms_1, T_1, tau_1 )
    local deduped_3_1, deduped_4_1;
    deduped_4_1 := List( morphisms_1, Range );
    deduped_3_1 := Coproduct( cat_1, deduped_4_1 );
    return PostCompose( cat_1, UniversalMorphismFromCoequalizer( cat_1, deduped_3_1, List( [ 1 .. Length( morphisms_1 ) ], function ( i_2 )
                return PostCompose( cat_1, InjectionOfCofactorOfCoproductWithGivenCoproduct( cat_1, deduped_4_1, i_2, deduped_3_1 ), morphisms_1[i_2] );
            end ), T_1, UniversalMorphismFromCoproduct( cat_1, deduped_4_1, T_1, tau_1 ) ), IsomorphismFromPushoutToCoequalizerOfCoproductDiagram( cat_1, morphisms_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromZeroObject,
                    "dualizing the derivation of UniversalMorphismIntoZeroObject by UniversalMorphismIntoZeroObject computing the zero morphism",
                    [
                        [ ZeroObject, 1 ],
                        [ ZeroMorphism, 1 ],
                    ],
                    
  function ( cat_1, T_1 )
    return ZeroMorphism( cat_1, ZeroObject( cat_1 ), T_1 );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromZeroObject,
                    "dualizing the derivation of UniversalMorphismIntoZeroObject by UniversalMorphismIntoZeroObject using UniversalMorphismIntoTerminalObject",
                    [
                        [ UniversalMorphismFromInitialObject, 1 ],
                        [ IsomorphismFromZeroObjectToInitialObject, 1 ],
                        [ PostCompose, 1 ],
                    ],
                    
  function ( cat_1, T_1 )
    return PostCompose( cat_1, UniversalMorphismFromInitialObject( cat_1, T_1 ), IsomorphismFromZeroObjectToInitialObject( cat_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismFromZeroObjectWithGivenZeroObject,
                    "dualizing the derivation of UniversalMorphismIntoZeroObjectWithGivenZeroObject by UniversalMorphismIntoZeroObject computing the zero morphism",
                    [
                        [ ZeroMorphism, 1 ],
                    ],
                    
  function ( cat_1, T_1, P_1 )
    return ZeroMorphism( cat_1, P_1, T_1 );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismIntoCoimage,
                    "dualizing the derivation of UniversalMorphismFromImage by UniversalMorphismFromImage using ImageEmbedding and LiftAlongMonomorphism",
                    [
                        [ CoimageProjection, 1 ],
                        [ ColiftAlongEpimorphism, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, tau_1 )
    return ColiftAlongEpimorphism( cat_1, tau_1[1], CoimageProjection( cat_1, alpha_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( UniversalMorphismIntoCoimageWithGivenCoimageObject,
                    "dualizing the derivation of UniversalMorphismFromImageWithGivenImageObject by UniversalMorphismFromImageWithGivenImageObject using ImageEmbeddingWithGivenImageObject and LiftAlongMonomorphism",
                    [
                        [ CoimageProjectionWithGivenCoimageObject, 1 ],
                        [ ColiftAlongEpimorphism, 1 ],
                    ],
                    
  function ( cat_1, alpha_1, tau_1, C_1 )
    return ColiftAlongEpimorphism( cat_1, tau_1[1], CoimageProjectionWithGivenCoimageObject( cat_1, alpha_1, C_1 ) );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( ZeroMorphism,
                    "dualizing the derivation of ZeroMorphism by Zero morphism by composition of morphism into and from zero object",
                    [
                        [ PostCompose, 1 ],
                        [ UniversalMorphismFromZeroObject, 1 ],
                        [ UniversalMorphismIntoZeroObject, 1 ],
                    ],
                    
  function ( cat_1, a_1, b_1 )
    return PostCompose( cat_1, UniversalMorphismFromZeroObject( cat_1, b_1 ), UniversalMorphismIntoZeroObject( cat_1, a_1 ) );
end : CategoryFilter := IsAdditiveCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );

##
AddDerivationToCAP( ZeroObjectFunctorialWithGivenZeroObjects,
                    "dualizing the derivation of ZeroObjectFunctorialWithGivenZeroObjects by ZeroObjectFunctorialWithGivenZeroObjects using the universality of the limit",
                    [
                        [ UniversalMorphismFromZeroObjectWithGivenZeroObject, 1 ],
                    ],
                    
  function ( cat_1, P_1, Pp_1 )
    return UniversalMorphismFromZeroObjectWithGivenZeroObject( cat_1, Pp_1, P_1 );
end : CategoryFilter := IsCapCategory,
      Weight := 1,
      is_autogenerated_by_CompilerForCAP := true );