# SPDX-License-Identifier: GPL-2.0-or-later
# CAP: Categories, Algorithms, Programming
#
# Implementations
#
# THIS FILE IS AUTOMATICALLY GENERATED, SEE LimitConvenience.gi

##
InstallMethod( UniversalMorphismIntoDirectProduct,
               [ IsList ],
               
  function( list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismIntoDirectProduct( CapCategory( list[1] ), list );
    
end );

##
InstallOtherMethod( UniversalMorphismIntoDirectProduct,
               [ IsCapCategory, IsList ],
               
  function( cat, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismIntoDirectProduct( cat, List( list, Range ), list );
    
end );

##
InstallOtherMethod( UniversalMorphismIntoDirectProduct,
               [ IsCapCategoryObject, IsList ],
               
  function( test_object, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismIntoDirectProduct( CapCategory( test_object ), test_object, list );
    
end );

##
InstallOtherMethod( UniversalMorphismIntoDirectProduct,
               [ IsCapCategory, IsCapCategoryObject, IsList ],
               
  function( cat, test_object, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismIntoDirectProduct( cat, List( list, Range ), test_object, list );
    
end );

InstallOtherMethod( UniversalMorphismIntoDirectProduct,
                    [ IsList, IsList ],
                    
    function( objects, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoDirectProduct( objects, Source( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismIntoDirectProduct,
                    [ IsCapCategory, IsList, IsList ],
                    
    function( cat, objects, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoDirectProduct( cat, objects, Source( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismIntoDirectProductWithGivenDirectProduct,
                    [ IsList, IsList, IsCapCategoryObject ],
                    
    function( objects, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoDirectProductWithGivenDirectProduct( objects, Source( tau[1] ), tau, P );
        
end );

InstallOtherMethod( UniversalMorphismIntoDirectProductWithGivenDirectProduct,
                    [ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
                    
    function( cat, objects, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoDirectProductWithGivenDirectProduct( cat, objects, Source( tau[1] ), tau, P );
        
end );

##
InstallMethod( UniversalMorphismFromCoproduct,
               [ IsList ],
               
  function( list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismFromCoproduct( CapCategory( list[1] ), list );
    
end );

##
InstallOtherMethod( UniversalMorphismFromCoproduct,
               [ IsCapCategory, IsList ],
               
  function( cat, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismFromCoproduct( cat, List( list, Source ), list );
    
end );

##
InstallOtherMethod( UniversalMorphismFromCoproduct,
               [ IsCapCategoryObject, IsList ],
               
  function( test_object, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismFromCoproduct( CapCategory( test_object ), test_object, list );
    
end );

##
InstallOtherMethod( UniversalMorphismFromCoproduct,
               [ IsCapCategory, IsCapCategoryObject, IsList ],
               
  function( cat, test_object, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismFromCoproduct( cat, List( list, Source ), test_object, list );
    
end );

InstallOtherMethod( UniversalMorphismFromCoproduct,
                    [ IsList, IsList ],
                    
    function( objects, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromCoproduct( objects, Range( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismFromCoproduct,
                    [ IsCapCategory, IsList, IsList ],
                    
    function( cat, objects, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromCoproduct( cat, objects, Range( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismFromCoproductWithGivenCoproduct,
                    [ IsList, IsList, IsCapCategoryObject ],
                    
    function( objects, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromCoproductWithGivenCoproduct( objects, Range( tau[1] ), tau, P );
        
end );

InstallOtherMethod( UniversalMorphismFromCoproductWithGivenCoproduct,
                    [ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
                    
    function( cat, objects, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromCoproductWithGivenCoproduct( cat, objects, Range( tau[1] ), tau, P );
        
end );

##
InstallOtherMethod( DirectProductFunctorial,
                    [ IsList ],
               
  function( L )
    
    return DirectProductFunctorial( List( L, Source ), L, List( L, Range ) );
    
end );

##
InstallOtherMethodForCompilerForCAP( DirectProductFunctorial,
                                     [ IsCapCategory, IsList ],
                    
  function( cat, L )
    
    return DirectProductFunctorial( cat, List( L, Source ), L, List( L, Range ) );
    
end );

##
InstallOtherMethod( DirectProductFunctorialWithGivenDirectProducts,
               [ IsCapCategoryObject, IsList, IsCapCategoryObject ],
               
  function( source, L, range )
    
    return DirectProductFunctorialWithGivenDirectProducts( source, List( L, Source ), L, List( L, Range ), range );
    
end );

##
InstallOtherMethodForCompilerForCAP( DirectProductFunctorialWithGivenDirectProducts,
                                     [ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryObject ],
               
  function( cat, source, L, range )
    
    return DirectProductFunctorialWithGivenDirectProducts( cat, source, List( L, Source ), L, List( L, Range ), range );
    
end );

##
AddDerivationToCAP( DirectProductFunctorialWithGivenDirectProducts,
                    "DirectProductFunctorialWithGivenDirectProducts using the universality of the limit",
                    [ [UniversalMorphismIntoDirectProductWithGivenDirectProduct, 1 ], [ PreCompose, 2 ], [ ProjectionInFactorOfDirectProductWithGivenDirectProduct, 2 ] ],
                    
  function( cat, P, objects, L, objectsp, Pp )
    
    return UniversalMorphismIntoDirectProductWithGivenDirectProduct( cat, objectsp, P, List( [ 1 .. Length( L ) ], i -> PreCompose( cat, ProjectionInFactorOfDirectProductWithGivenDirectProduct( cat, objects, i, P ), L[i] ) ), Pp );
    
end );

##
InstallOtherMethod( CoproductFunctorial,
                    [ IsList ],
               
  function( L )
    
    return CoproductFunctorial( List( L, Source ), L, List( L, Range ) );
    
end );

##
InstallOtherMethodForCompilerForCAP( CoproductFunctorial,
                                     [ IsCapCategory, IsList ],
                    
  function( cat, L )
    
    return CoproductFunctorial( cat, List( L, Source ), L, List( L, Range ) );
    
end );

##
InstallOtherMethod( CoproductFunctorialWithGivenCoproducts,
               [ IsCapCategoryObject, IsList, IsCapCategoryObject ],
               
  function( source, L, range )
    
    return CoproductFunctorialWithGivenCoproducts( source, List( L, Source ), L, List( L, Range ), range );
    
end );

##
InstallOtherMethodForCompilerForCAP( CoproductFunctorialWithGivenCoproducts,
                                     [ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryObject ],
               
  function( cat, source, L, range )
    
    return CoproductFunctorialWithGivenCoproducts( cat, source, List( L, Source ), L, List( L, Range ), range );
    
end );

##
InstallMethod( UniversalMorphismIntoDirectSum,
               [ IsList ],
               
  function( list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismIntoDirectSum( CapCategory( list[1] ), list );
    
end );

##
InstallOtherMethod( UniversalMorphismIntoDirectSum,
               [ IsCapCategory, IsList ],
               
  function( cat, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismIntoDirectSum( cat, List( list, Range ), list );
    
end );

##
InstallOtherMethod( UniversalMorphismIntoDirectSum,
               [ IsCapCategoryObject, IsList ],
               
  function( test_object, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismIntoDirectSum( CapCategory( test_object ), test_object, list );
    
end );

##
InstallOtherMethod( UniversalMorphismIntoDirectSum,
               [ IsCapCategory, IsCapCategoryObject, IsList ],
               
  function( cat, test_object, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismIntoDirectSum( cat, List( list, Range ), test_object, list );
    
end );

InstallOtherMethod( UniversalMorphismIntoDirectSum,
                    [ IsList, IsList ],
                    
    function( objects, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoDirectSum( objects, Source( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismIntoDirectSum,
                    [ IsCapCategory, IsList, IsList ],
                    
    function( cat, objects, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoDirectSum( cat, objects, Source( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismIntoDirectSumWithGivenDirectSum,
                    [ IsList, IsList, IsCapCategoryObject ],
                    
    function( objects, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoDirectSumWithGivenDirectSum( objects, Source( tau[1] ), tau, P );
        
end );

InstallOtherMethod( UniversalMorphismIntoDirectSumWithGivenDirectSum,
                    [ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
                    
    function( cat, objects, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoDirectSumWithGivenDirectSum( cat, objects, Source( tau[1] ), tau, P );
        
end );

##
InstallMethod( UniversalMorphismFromDirectSum,
               [ IsList ],
               
  function( list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismFromDirectSum( CapCategory( list[1] ), list );
    
end );

##
InstallOtherMethod( UniversalMorphismFromDirectSum,
               [ IsCapCategory, IsList ],
               
  function( cat, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismFromDirectSum( cat, List( list, Source ), list );
    
end );

##
InstallOtherMethod( UniversalMorphismFromDirectSum,
               [ IsCapCategoryObject, IsList ],
               
  function( test_object, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismFromDirectSum( CapCategory( test_object ), test_object, list );
    
end );

##
InstallOtherMethod( UniversalMorphismFromDirectSum,
               [ IsCapCategory, IsCapCategoryObject, IsList ],
               
  function( cat, test_object, list )
    #% CAP_JIT_RESOLVE_FUNCTION
    
    return UniversalMorphismFromDirectSum( cat, List( list, Source ), test_object, list );
    
end );

InstallOtherMethod( UniversalMorphismFromDirectSum,
                    [ IsList, IsList ],
                    
    function( objects, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromDirectSum( objects, Range( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismFromDirectSum,
                    [ IsCapCategory, IsList, IsList ],
                    
    function( cat, objects, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromDirectSum( cat, objects, Range( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismFromDirectSumWithGivenDirectSum,
                    [ IsList, IsList, IsCapCategoryObject ],
                    
    function( objects, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromDirectSumWithGivenDirectSum( objects, Range( tau[1] ), tau, P );
        
end );

InstallOtherMethod( UniversalMorphismFromDirectSumWithGivenDirectSum,
                    [ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
                    
    function( cat, objects, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromDirectSumWithGivenDirectSum( cat, objects, Range( tau[1] ), tau, P );
        
end );

##
InstallOtherMethod( DirectSumFunctorial,
                    [ IsList ],
               
  function( L )
    
    return DirectSumFunctorial( List( L, Source ), L, List( L, Range ) );
    
end );

##
InstallOtherMethodForCompilerForCAP( DirectSumFunctorial,
                                     [ IsCapCategory, IsList ],
                    
  function( cat, L )
    
    return DirectSumFunctorial( cat, List( L, Source ), L, List( L, Range ) );
    
end );

##
InstallOtherMethod( DirectSumFunctorialWithGivenDirectSums,
               [ IsCapCategoryObject, IsList, IsCapCategoryObject ],
               
  function( source, L, range )
    
    return DirectSumFunctorialWithGivenDirectSums( source, List( L, Source ), L, List( L, Range ), range );
    
end );

##
InstallOtherMethodForCompilerForCAP( DirectSumFunctorialWithGivenDirectSums,
                                     [ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryObject ],
               
  function( cat, source, L, range )
    
    return DirectSumFunctorialWithGivenDirectSums( cat, source, List( L, Source ), L, List( L, Range ), range );
    
end );

##
AddDerivationToCAP( DirectSumFunctorialWithGivenDirectSums,
                    "DirectSumFunctorialWithGivenDirectSums using the universality of the limit",
                    [ [UniversalMorphismIntoDirectSumWithGivenDirectSum, 1 ], [ PreCompose, 2 ], [ ProjectionInFactorOfDirectSumWithGivenDirectSum, 2 ] ],
                    
  function( cat, P, objects, L, objectsp, Pp )
    
    return UniversalMorphismIntoDirectSumWithGivenDirectSum( cat, objectsp, P, List( [ 1 .. Length( L ) ], i -> PreCompose( cat, ProjectionInFactorOfDirectSumWithGivenDirectSum( cat, objects, i, P ), L[i] ) ), Pp );
    
end );

InstallOtherMethod( UniversalMorphismIntoFiberProduct,
                    [ IsList, IsList ],
                    
    function( morphisms, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoFiberProduct( morphisms, Source( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismIntoFiberProduct,
                    [ IsCapCategory, IsList, IsList ],
                    
    function( cat, morphisms, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoFiberProduct( cat, morphisms, Source( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismIntoFiberProductWithGivenFiberProduct,
                    [ IsList, IsList, IsCapCategoryObject ],
                    
    function( morphisms, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoFiberProductWithGivenFiberProduct( morphisms, Source( tau[1] ), tau, P );
        
end );

InstallOtherMethod( UniversalMorphismIntoFiberProductWithGivenFiberProduct,
                    [ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
                    
    function( cat, morphisms, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoFiberProductWithGivenFiberProduct( cat, morphisms, Source( tau[1] ), tau, P );
        
end );

InstallOtherMethod( UniversalMorphismFromPushout,
                    [ IsList, IsList ],
                    
    function( morphisms, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromPushout( morphisms, Range( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismFromPushout,
                    [ IsCapCategory, IsList, IsList ],
                    
    function( cat, morphisms, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromPushout( cat, morphisms, Range( tau[1] ), tau );
        
end );

InstallOtherMethod( UniversalMorphismFromPushoutWithGivenPushout,
                    [ IsList, IsList, IsCapCategoryObject ],
                    
    function( morphisms, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromPushoutWithGivenPushout( morphisms, Range( tau[1] ), tau, P );
        
end );

InstallOtherMethod( UniversalMorphismFromPushoutWithGivenPushout,
                    [ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
                    
    function( cat, morphisms, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromPushoutWithGivenPushout( cat, morphisms, Range( tau[1] ), tau, P );
        
end );

##
AddDerivationToCAP( FiberProductFunctorialWithGivenFiberProducts,
                    "FiberProductFunctorialWithGivenFiberProducts using the universality of the limit",
                    [ [UniversalMorphismIntoFiberProductWithGivenFiberProduct, 1 ], [ PreCompose, 2 ], [ ProjectionInFactorOfFiberProductWithGivenFiberProduct, 2 ] ],
                    
  function( cat, P, morphisms, L, morphismsp, Pp )
    
    return UniversalMorphismIntoFiberProductWithGivenFiberProduct( cat, morphismsp, P, List( [ 1 .. Length( L ) ], i -> PreCompose( cat, ProjectionInFactorOfFiberProductWithGivenFiberProduct( cat, morphisms, i, P ), L[i] ) ), Pp );
    
end );

InstallOtherMethod( UniversalMorphismIntoEqualizer,
                    [ IsCapCategoryObject, IsList, IsCapCategoryMorphism ],
                    
    function( Y, morphisms, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoEqualizer( Y, morphisms, Source( tau ), tau );
        
end );

InstallOtherMethod( UniversalMorphismIntoEqualizer,
                    [ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryMorphism ],
                    
    function( cat, Y, morphisms, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoEqualizer( cat, Y, morphisms, Source( tau ), tau );
        
end );

InstallOtherMethod( UniversalMorphismIntoEqualizerWithGivenEqualizer,
                    [ IsCapCategoryObject, IsList, IsCapCategoryMorphism, IsCapCategoryObject ],
                    
    function( Y, morphisms, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoEqualizerWithGivenEqualizer( Y, morphisms, Source( tau ), tau, P );
        
end );

InstallOtherMethod( UniversalMorphismIntoEqualizerWithGivenEqualizer,
                    [ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryMorphism, IsCapCategoryObject ],
                    
    function( cat, Y, morphisms, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismIntoEqualizerWithGivenEqualizer( cat, Y, morphisms, Source( tau ), tau, P );
        
end );

InstallOtherMethod( UniversalMorphismFromCoequalizer,
                    [ IsCapCategoryObject, IsList, IsCapCategoryMorphism ],
                    
    function( Y, morphisms, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromCoequalizer( Y, morphisms, Range( tau ), tau );
        
end );

InstallOtherMethod( UniversalMorphismFromCoequalizer,
                    [ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryMorphism ],
                    
    function( cat, Y, morphisms, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromCoequalizer( cat, Y, morphisms, Range( tau ), tau );
        
end );

InstallOtherMethod( UniversalMorphismFromCoequalizerWithGivenCoequalizer,
                    [ IsCapCategoryObject, IsList, IsCapCategoryMorphism, IsCapCategoryObject ],
                    
    function( Y, morphisms, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromCoequalizerWithGivenCoequalizer( Y, morphisms, Range( tau ), tau, P );
        
end );

InstallOtherMethod( UniversalMorphismFromCoequalizerWithGivenCoequalizer,
                    [ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryMorphism, IsCapCategoryObject ],
                    
    function( cat, Y, morphisms, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return UniversalMorphismFromCoequalizerWithGivenCoequalizer( cat, Y, morphisms, Range( tau ), tau, P );
        
end );

##
AddDerivationToCAP( EqualizerFunctorialWithGivenEqualizers,
                    "EqualizerFunctorialWithGivenEqualizers using the universality of the limit",
                    [ [UniversalMorphismIntoEqualizerWithGivenEqualizer, 1 ], [ PreCompose, 1 ], [ EmbeddingOfEqualizerWithGivenEqualizer, 1 ] ],
                    
  function( cat, P, morphisms, mu, morphismsp, Pp )
    local Y, Yp;
    
    Y := Source( mu );
    Yp := Range( mu );
    
    return UniversalMorphismIntoEqualizerWithGivenEqualizer( cat, Yp, morphismsp, P, PreCompose( cat, EmbeddingOfEqualizerWithGivenEqualizer( cat, Y, morphisms, P ), mu ), Pp );
    
end );

InstallOtherMethod( KernelLift,
                    [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
                    
    function( alpha, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return KernelLift( alpha, Source( tau ), tau );
        
end );

InstallOtherMethod( KernelLift,
                    [ IsCapCategory, IsCapCategoryMorphism, IsCapCategoryMorphism ],
                    
    function( cat, alpha, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return KernelLift( cat, alpha, Source( tau ), tau );
        
end );

InstallOtherMethod( KernelLiftWithGivenKernelObject,
                    [ IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryObject ],
                    
    function( alpha, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return KernelLiftWithGivenKernelObject( alpha, Source( tau ), tau, P );
        
end );

InstallOtherMethod( KernelLiftWithGivenKernelObject,
                    [ IsCapCategory, IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryObject ],
                    
    function( cat, alpha, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return KernelLiftWithGivenKernelObject( cat, alpha, Source( tau ), tau, P );
        
end );

InstallOtherMethod( CokernelColift,
                    [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
                    
    function( alpha, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return CokernelColift( alpha, Range( tau ), tau );
        
end );

InstallOtherMethod( CokernelColift,
                    [ IsCapCategory, IsCapCategoryMorphism, IsCapCategoryMorphism ],
                    
    function( cat, alpha, tau )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return CokernelColift( cat, alpha, Range( tau ), tau );
        
end );

InstallOtherMethod( CokernelColiftWithGivenCokernelObject,
                    [ IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryObject ],
                    
    function( alpha, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return CokernelColiftWithGivenCokernelObject( alpha, Range( tau ), tau, P );
        
end );

InstallOtherMethod( CokernelColiftWithGivenCokernelObject,
                    [ IsCapCategory, IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryObject ],
                    
    function( cat, alpha, tau, P )
        #% CAP_JIT_RESOLVE_FUNCTION
        
        return CokernelColiftWithGivenCokernelObject( cat, alpha, Range( tau ), tau, P );
        
end );

##
AddDerivationToCAP( KernelObjectFunctorialWithGivenKernelObjects,
                    "KernelObjectFunctorialWithGivenKernelObjects using the universality of the limit",
                    [ [KernelLiftWithGivenKernelObject, 1 ], [ PreCompose, 1 ], [ KernelEmbeddingWithGivenKernelObject, 1 ] ],
                    
  function( cat, P, alpha, mu, alphap, Pp )
    
    return KernelLiftWithGivenKernelObject( cat, alphap, P, PreCompose( cat, KernelEmbeddingWithGivenKernelObject( cat, alpha, P ), mu ), Pp );
    
end );

##
AddDerivationToCAP( TerminalObjectFunctorialWithGivenTerminalObjects,
                    "TerminalObjectFunctorialWithGivenTerminalObjects using the universality of the limit",
                    [ [UniversalMorphismIntoTerminalObjectWithGivenTerminalObject, 1 ] ],
                    
  function( cat, P, Pp )
    
    return UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( cat, P, Pp );
    
end );

##
AddDerivationToCAP( TerminalObjectFunctorial,
                    "TerminalObjectFunctorial by taking the identity morphism of TerminalObject",
                    [ [ TerminalObject, 1 ],
                      [ IdentityMorphism, 1 ] ],
                    
  function( cat )
    
    return IdentityMorphism( cat, TerminalObject( cat ) );
    
end );

##
AddDerivationToCAP( ZeroObjectFunctorialWithGivenZeroObjects,
                    "ZeroObjectFunctorialWithGivenZeroObjects using the universality of the limit",
                    [ [UniversalMorphismIntoZeroObjectWithGivenZeroObject, 1 ] ],
                    
  function( cat, P, Pp )
    
    return UniversalMorphismIntoZeroObjectWithGivenZeroObject( cat, P, Pp );
    
end );

##
AddDerivationToCAP( ZeroObjectFunctorial,
                    "ZeroObjectFunctorial by taking the identity morphism of ZeroObject",
                    [ [ ZeroObject, 1 ],
                      [ IdentityMorphism, 1 ] ],
                    
  function( cat )
    
    return IdentityMorphism( cat, ZeroObject( cat ) );
    
end );