Review of the formalizations of the specifications of CAP operations and properties

[zickgraf]

I have added formalizations of the specifications of various CAP operations and properties in

CAP_project/CompilerForCAP/gap/ProofAssistant.gi

Lines 991 to 1786 in de3e9fa

	BindGlobal( "CAP_JIT_INTERNAL_PROOF_ASSISTANT_LEMMATA", rec(
	PreCompose := rec(
	lemmata := [
	rec(
	description := "the composite of two morphisms defines a morphism",
	input_types := [ "category", "object", "object", "object", "morphism", "morphism" ],
	func := function ( cat, A, B, C, alpha, beta )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, A, PreCompose( cat, alpha, beta ), C );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "B" ),
	rec( src_template := "Range( beta )", dst_template := "C" ),
	],
	),
	rec(
	description := "composition is associative",
	input_types := [ "category", "object", "object", "object", "object", "morphism", "morphism", "morphism" ],
	func := function ( cat, A, B, C, D, alpha, beta, gamma )
	return IsCongruentForMorphisms( cat, PreCompose( cat, PreCompose( cat, alpha, beta ), gamma ), PreCompose( cat, alpha, PreCompose( cat, beta, gamma ) ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "B" ),
	rec( src_template := "Range( beta )", dst_template := "C" ),
	rec( src_template := "Source( gamma )", dst_template := "C" ),
	rec( src_template := "Range( gamma )", dst_template := "D" ),
	],
	),
	],
	),
	IdentityMorphism := rec(
	lemmata := [
	rec(
	description := "the identity on an object defines a morphism",
	input_types := [ "category", "object" ],
	func := function ( cat, A )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, A, IdentityMorphism( cat, A ), A );
	end,
	preconditions := [ ],
	),
	rec(
	description := "identity morphisms are left neutral",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsCongruentForMorphisms( cat, PreCompose( cat, IdentityMorphism( cat, A ), alpha ), alpha );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	rec(
	description := "identity morphisms are right neutral",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsCongruentForMorphisms( cat, PreCompose( cat, alpha, IdentityMorphism( cat, B ) ), alpha );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	],
	),
	AdditionForMorphisms := rec(
	lemmata := [
	rec(
	description := "the addition of morphisms defines a morphism",
	input_types := [ "category", "object", "object", "morphism", "morphism" ],
	func := function ( cat, A, B, alpha, beta )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, A, AdditionForMorphisms( cat, alpha, beta ), B );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "A" ),
	rec( src_template := "Range( beta )", dst_template := "B" ),
	],
	),
	rec(
	description := "addition of morphisms is associative",
	input_types := [ "category", "object", "object", "morphism", "morphism", "morphism" ],
	func := function ( cat, A, B, alpha, beta, gamma )
	return IsCongruentForMorphisms( cat, AdditionForMorphisms( cat, AdditionForMorphisms( cat, alpha, beta ), gamma ), AdditionForMorphisms( cat, alpha, AdditionForMorphisms( cat, beta, gamma ) ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "A" ),
	rec( src_template := "Range( beta )", dst_template := "B" ),
	rec( src_template := "Source( gamma )", dst_template := "A" ),
	rec( src_template := "Range( gamma )", dst_template := "B" ),
	],
	),
	rec(
	description := "addition of morphisms is commutative",
	input_types := [ "category", "object", "object", "morphism", "morphism" ],
	func := function ( cat, A, B, alpha, beta )
	return IsCongruentForMorphisms( cat,
	AdditionForMorphisms( cat, alpha, beta ),
	AdditionForMorphisms( cat, beta, alpha )
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "A" ),
	rec( src_template := "Range( beta )", dst_template := "B" ),
	],
	),
	rec(
	description := "composition is additive in the first component",
	input_types := [ "category", "object", "object", "object", "morphism", "morphism", "morphism" ],
	func := function ( cat, A, B, C, alpha, beta, phi )
	return IsCongruentForMorphisms( cat,
	PreCompose( cat, AdditionForMorphisms( cat, alpha, beta ), phi ),
	AdditionForMorphisms( cat, PreCompose( cat, alpha, phi ), PreCompose( cat, beta, phi ) )
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "A" ),
	rec( src_template := "Range( beta )", dst_template := "B" ),
	rec( src_template := "Source( phi )", dst_template := "B" ),
	rec( src_template := "Range( phi )", dst_template := "C" ),
	],
	),
	rec(
	description := "composition is additive in the second component",
	input_types := [ "category", "object", "object", "object", "morphism", "morphism", "morphism" ],
	func := function ( cat, A, B, C, alpha, beta, phi )
	return IsCongruentForMorphisms( cat,
	PreCompose( cat, phi, AdditionForMorphisms( cat, alpha, beta ) ),
	AdditionForMorphisms( cat, PreCompose( cat, phi, alpha ), PreCompose( cat, phi, beta ) )
	);
	end,
	preconditions := [
	rec( src_template := "Source( phi )", dst_template := "A" ),
	rec( src_template := "Range( phi )", dst_template := "B" ),
	rec( src_template := "Source( alpha )", dst_template := "B" ),
	rec( src_template := "Range( alpha )", dst_template := "C" ),
	rec( src_template := "Source( beta )", dst_template := "B" ),
	rec( src_template := "Range( beta )", dst_template := "C" ),
	],
	),
	],
	),
	ZeroMorphism := rec(
	lemmata := [
	rec(
	description := "the zero morphism between two objects is a morphism",
	input_types := [ "category", "object", "object" ],
	func := function ( cat, A, B )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, A, ZeroMorphism( cat, A, B ), B );
	end,
	preconditions := [ ],
	),
	rec(
	description := "zero morphisms are left neutral",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsCongruentForMorphisms( cat, AdditionForMorphisms( cat, ZeroMorphism( cat, A, B ), alpha ), alpha );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	rec(
	description := "zero morphisms are right neutral",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsCongruentForMorphisms( cat, AdditionForMorphisms( cat, alpha, ZeroMorphism( cat, A, B ) ), alpha );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	],
	),
	AdditiveInverseForMorphisms := rec(
	lemmata := [
	rec(
	description := "the additive inverse of a morphism defines a morphism",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, A, AdditiveInverseForMorphisms( cat, alpha ), B );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	rec(
	description := "additive inverses are left inverse",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsCongruentForMorphisms( cat, AdditionForMorphisms( cat, AdditiveInverseForMorphisms( cat, alpha ), alpha ), ZeroMorphism( cat, A, B ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	rec(
	description := "additive inverses are right inverse",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsCongruentForMorphisms( cat, AdditionForMorphisms( cat, alpha, AdditiveInverseForMorphisms( cat, alpha ) ), ZeroMorphism( cat, A, B ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	],
	),
	MultiplyWithElementOfCommutativeRingForMorphisms := rec(
	lemmata := [
	rec(
	description := "multiplying a morphism by a ring element defines a morphism",
	input_types := [ "category", "object", "object", "element_of_commutative_ring_of_linear_structure", "morphism" ],
	func := function ( cat, A, B, r, alpha )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, A, MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, alpha ), B );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	rec(
	description := "multiplication with ring elements is associative",
	input_types := [ "category", "object", "object", "element_of_commutative_ring_of_linear_structure", "element_of_commutative_ring_of_linear_structure", "morphism" ],
	func := function ( cat, A, B, r, s, alpha )
	return IsCongruentForMorphisms( cat, MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, MultiplyWithElementOfCommutativeRingForMorphisms( s, alpha ) ), MultiplyWithElementOfCommutativeRingForMorphisms( cat, r * s, alpha ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	rec(
	description := "composition distributes over the addition of ring elements",
	input_types := [ "category", "object", "object", "element_of_commutative_ring_of_linear_structure", "element_of_commutative_ring_of_linear_structure", "morphism" ],
	func := function ( cat, A, B, r, s, alpha )
	return IsCongruentForMorphisms( cat, MultiplyWithElementOfCommutativeRingForMorphisms( cat, r + s, alpha ), AdditionForMorphisms( cat, MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, alpha ), MultiplyWithElementOfCommutativeRingForMorphisms( cat, s, alpha ) ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	rec(
	description := "ring multiplication distributes over the addition of morphisms",
	input_types := [ "category", "object", "object", "element_of_commutative_ring_of_linear_structure", "morphism", "morphism" ],
	func := function ( cat, A, B, r, alpha, beta )
	return IsCongruentForMorphisms( cat, MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, AdditionForMorphisms( cat, alpha, beta ) ), AdditionForMorphisms( cat, MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, alpha ), MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, beta ) ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "A" ),
	rec( src_template := "Range( beta )", dst_template := "B" ),
	],
	),
	rec(
	description := "multiplication with ring elements has a neutral element",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsCongruentForMorphisms( cat, MultiplyWithElementOfCommutativeRingForMorphisms( cat, One( CommutativeRingOfLinearCategory( cat ) ), alpha ), alpha );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	rec(
	description := "composition is linear in the first component",
	input_types := [ "category", "object", "object", "object", "element_of_commutative_ring_of_linear_structure", "morphism", "morphism" ],
	func := function ( cat, A, B, C, r, alpha, beta )
	return IsCongruentForMorphisms( cat, PreCompose( cat, MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, alpha ), beta ), MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, PreCompose( cat, alpha, beta ) ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "B" ),
	rec( src_template := "Range( beta )", dst_template := "C" ),
	],
	),
	rec(
	description := "composition is linear in the second component",
	input_types := [ "category", "object", "object", "object", "element_of_commutative_ring_of_linear_structure", "morphism", "morphism" ],
	func := function ( cat, A, B, C, r, alpha, beta )
	return IsCongruentForMorphisms( cat, PreCompose( cat, alpha, MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, beta ) ), MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, PreCompose( cat, alpha, beta ) ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "B" ),
	rec( src_template := "Range( beta )", dst_template := "C" ),
	],
	),
	],
	),
	ZeroObject := rec(
	lemmata := [
	rec(
	description := "the zero object is an object",
	input_types := [ "category" ],
	func := function ( cat )
	return IsWellDefinedForObjects( cat, ZeroObject( cat ) );
	end,
	preconditions := [ ],
	),
	],
	),
	UniversalMorphismIntoZeroObject := rec(
	lemmata := [
	rec(
	description := "the universal morphism into the zero objects defines a morphism",
	input_types := [ "category", "object" ],
	func := function ( cat, A )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, A, UniversalMorphismIntoZeroObject( cat, A ), ZeroObject( cat ) );
	end,
	preconditions := [ ],
	),
	rec(
	description := "the universal morphism into the zero object is unique",
	input_types := [ "category", "object", "morphism" ],
	func := function ( cat, A, u )
	return IsCongruentForMorphisms( cat,
	UniversalMorphismIntoZeroObject( cat, A ),
	u
	);
	end,
	preconditions := [
	rec( src_template := "Source( u )", dst_template := "A" ),
	rec( src_template := "Range( u )", dst_template := "ZeroObject( cat )" ),
	],
	),
	],
	),
	UniversalMorphismFromZeroObject := rec(
	lemmata := [
	rec(
	description := "the universal morphism from the zero objects defines a morphism",
	input_types := [ "category", "object" ],
	func := function ( cat, B )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, ZeroObject( cat ), UniversalMorphismFromZeroObject( cat, B ), B );
	end,
	preconditions := [ ],
	),
	rec(
	description := "the universal morphism from the zero object is unique",
	input_types := [ "category", "object", "morphism" ],
	func := function ( cat, B, u )
	return IsCongruentForMorphisms( cat,
	UniversalMorphismFromZeroObject( cat, B ),
	u
	);
	end,
	preconditions := [
	rec( src_template := "Source( u )", dst_template := "ZeroObject( cat )" ),
	rec( src_template := "Range( u )", dst_template := "B" ),
	],
	),
	],
	),
	KernelObject := rec(
	lemmata := [
	rec(
	description := "kernel objects are objects",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsWellDefinedForObjects( cat, KernelObject( cat, alpha ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	],
	),
	KernelEmbedding := rec(
	lemmata := [
	rec(
	description := "kernel embeddings define morphisms",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, KernelObject( cat, alpha ), KernelEmbedding( cat, alpha ), A );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	rec(
	description := "the kernel embedding composes to zero",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsZeroForMorphisms( cat, PreCompose( cat, KernelEmbedding( cat, alpha ), alpha ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	],
	),
	KernelLift := rec(
	lemmata := [
	rec(
	description := "kernel lifts define morphisms",
	input_types := [ "category", "object", "object", "object", "morphism", "morphism" ],
	func := function ( cat, A, B, T, alpha, tau )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, T, KernelLift( cat, alpha, T, tau ), KernelObject( cat, alpha ) );
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( tau )", dst_template := "T" ),
	rec( src_template := "Range( tau )", dst_template := "A" ),
	rec( src_template := "PreCompose( cat, tau, alpha )", dst_template := "ZeroMorphism( cat, T, B )" ),
	],
	),
	rec(
	description := "taking the kernel lift is an injective operation",
	input_types := [ "category", "object", "object", "object", "morphism", "morphism" ],
	func := function ( cat, A, B, T, alpha, tau )
	return IsCongruentForMorphisms( cat,
	PreCompose( cat, KernelLift( cat, alpha, T, tau ), KernelEmbedding( cat, alpha ) ),
	tau
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( tau )", dst_template := "T" ),
	rec( src_template := "Range( tau )", dst_template := "A" ),
	rec( src_template := "PreCompose( cat, tau, alpha )", dst_template := "ZeroMorphism( cat, T, B )" ),
	],
	),
	rec(
	description := "taking the kernel lift is a surjective operation",
	input_types := [ "category", "object", "object", "object", "morphism", "morphism" ],
	func := function ( cat, A, B, T, alpha, u )
	return IsCongruentForMorphisms( cat,
	KernelLift( cat, alpha, T, PreCompose( cat, u, KernelEmbedding( cat, alpha ) ) ),
	u
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( u )", dst_template := "T" ),
	rec( src_template := "Range( u )", dst_template := "KernelObject( cat, alpha )" ),
	],
	),
	],
	),
	DistinguishedObjectOfHomomorphismStructure := rec(
	lemmata := [
	rec(
	description := "the distinguished object is an object in the range category of the homomorphism structure",
	input_types := [ "category" ],
	func := function ( cat )
	return IsWellDefinedForObjects( RangeCategoryOfHomomorphismStructure( cat ), DistinguishedObjectOfHomomorphismStructure( cat ) );
	end,
	preconditions := [ ],
	),
	],
	),
	HomomorphismStructureOnObjects := rec(
	lemmata := [
	rec(
	description := "the homomorphism structure on objects defines an object in the range category of the homomorphism structure",
	input_types := [ "category", "object", "object" ],
	func := function ( cat, A, B )
	return IsWellDefinedForObjects( RangeCategoryOfHomomorphismStructure( cat ), HomomorphismStructureOnObjects( cat, A, B ) );
	end,
	preconditions := [ ],
	),
	],
	),
	HomomorphismStructureOnMorphisms := rec(
	lemmata := [
	rec(
	description := "the homomorphism structure on morphisms defines a morphism in the range category of the homomorphism structure",
	input_types := [ "category", "object", "object", "object", "object", "morphism", "morphism" ],
	func := function ( cat, A, B, C, D, alpha, beta )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( RangeCategoryOfHomomorphismStructure( cat ),
	HomomorphismStructureOnObjects( cat, B, C ),
	HomomorphismStructureOnMorphisms( cat, alpha, beta ),
	HomomorphismStructureOnObjects( cat, A, D )
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "C" ),
	rec( src_template := "Range( beta )", dst_template := "D" ),
	],
	),
	# H( id, id ) = id
	rec(
	description := "the homomorphism structure preserves identities",
	input_types := [ "category", "object", "object" ],
	func := function ( cat, A, B )
	return IsCongruentForMorphisms( RangeCategoryOfHomomorphismStructure( cat ),
	HomomorphismStructureOnMorphisms( cat, IdentityMorphism( cat, A ), IdentityMorphism( cat, B ) ),
	IdentityMorphism( RangeCategoryOfHomomorphismStructure( cat ), HomomorphismStructureOnObjects( cat, A, B ) )
	);
	end,
	preconditions := [ ],
	),
	# H( α₁, β₁ ) ⋅ H( α₂, β₂ ) = H( α₂ ⋅ α₁, β₁ ⋅ β₂ )
	rec(
	description := "the homomorphism structure is compatible with composition",
	input_types := [ "category", "object", "object", "object", "object", "object", "object", "morphism", "morphism", "morphism", "morphism" ],
	func := function ( cat, A, B, C, D, E, F, alpha_1, alpha_2, beta_1, beta_2 )
	return IsCongruentForMorphisms( RangeCategoryOfHomomorphismStructure( cat ),
	PreCompose( RangeCategoryOfHomomorphismStructure( cat ), HomomorphismStructureOnMorphisms( cat, alpha_1, beta_1 ), HomomorphismStructureOnMorphisms( cat, alpha_2, beta_2 ) ),
	HomomorphismStructureOnMorphisms( cat, PreCompose( cat, alpha_2, alpha_1 ), PreCompose( cat, beta_1, beta_2 ) )
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha_2 )", dst_template := "A" ),
	rec( src_template := "Range( alpha_2 )", dst_template := "B" ),
	rec( src_template := "Source( alpha_1 )", dst_template := "B" ),
	rec( src_template := "Range( alpha_1 )", dst_template := "C" ),
	rec( src_template := "Source( beta_1 )", dst_template := "D" ),
	rec( src_template := "Range( beta_1 )", dst_template := "E" ),
	rec( src_template := "Source( beta_2 )", dst_template := "E" ),
	rec( src_template := "Range( beta_2 )", dst_template := "F" ),
	],
	),
	# H( α₁, β ) + H( α₂, β ) = H( α₁ + α₂, β )
	rec(
	description := "the homomorphism structue is additive in the first component",
	input_types := [ "category", "object", "object", "object", "object", "morphism", "morphism", "morphism" ],
	func := function ( cat, A, B, C, D, alpha_1, alpha_2, beta )
	return IsCongruentForMorphisms( RangeCategoryOfHomomorphismStructure( cat ),
	AdditionForMorphisms( RangeCategoryOfHomomorphismStructure( cat ), HomomorphismStructureOnMorphisms( cat, alpha_1, beta ), HomomorphismStructureOnMorphisms( cat, alpha_2, beta ) ),
	HomomorphismStructureOnMorphisms( cat, AdditionForMorphisms( cat, alpha_1, alpha_2 ), beta )
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha_1 )", dst_template := "A" ),
	rec( src_template := "Range( alpha_1 )", dst_template := "B" ),
	rec( src_template := "Source( alpha_2 )", dst_template := "A" ),
	rec( src_template := "Range( alpha_2 )", dst_template := "B" ),
	rec( src_template := "Source( beta )", dst_template := "C" ),
	rec( src_template := "Range( beta )", dst_template := "D" ),
	],
	category_filter := IsAbCategory,
	),
	# H( α, β₁ ) + H( α, β₂ ) = H( α, β₁ + β₂ )
	rec(
	description := "the homomorphism structure is additive in the second component",
	input_types := [ "category", "object", "object", "object", "object", "morphism", "morphism", "morphism" ],
	func := function ( cat, A, B, C, D, alpha, beta_1, beta_2 )
	return IsCongruentForMorphisms( RangeCategoryOfHomomorphismStructure( cat ),
	AdditionForMorphisms( RangeCategoryOfHomomorphismStructure( cat ), HomomorphismStructureOnMorphisms( cat, alpha, beta_1 ), HomomorphismStructureOnMorphisms( cat, alpha, beta_2 ) ),
	HomomorphismStructureOnMorphisms( cat, alpha, AdditionForMorphisms( cat, beta_1, beta_2 ) )
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( beta_1 )", dst_template := "C" ),
	rec( src_template := "Range( beta_1 )", dst_template := "D" ),
	rec( src_template := "Source( beta_2 )", dst_template := "C" ),
	rec( src_template := "Range( beta_2 )", dst_template := "D" ),
	],
	category_filter := IsAbCategory,
	),
	],
	),
	InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure := rec(
	lemmata := [
	rec(
	description := "interpreting a morphism as a morphism from the distinguished object defines a morphism in the range category of the homomorphism structure",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( RangeCategoryOfHomomorphismStructure( cat ),
	DistinguishedObjectOfHomomorphismStructure( cat ),
	InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( cat, alpha ),
	HomomorphismStructureOnObjects( cat, A, B )
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	# for more, see InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism
	],
	),
	InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism := rec(
	lemmata := [
	rec(
	description := "reinterpreting a morphism from the distinguished morphism as a usual morphism defines a morphism",
	input_types := [ "category", "object", "object", "morphism_in_range_category_of_homomorphism_structure" ],
	func := function ( cat, A, B, alpha )
	return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat,
	A,
	InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( cat, A, B, alpha ),
	B
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "DistinguishedObjectOfHomomorphismStructure( cat )" ),
	rec( src_template := "Range( alpha )", dst_template := "HomomorphismStructureOnObjects( cat, A, B )" ),
	],
	),
	rec(
	# ν⁻¹(ν(α)) = α
	description := "interpreting morphisms as morphisms from the distinguished object is an injective operation",
	input_types := [ "category", "object", "object", "morphism" ],
	func := function ( cat, A, B, alpha )
	return IsCongruentForMorphisms( cat,
	InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( cat, A, B, InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( cat, alpha ) ),
	alpha
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	],
	),
	rec(
	# ν(ν⁻¹(α)) = α
	description := "interpreting morphisms as morphisms from the distinguished object is a surjective operation",
	input_types := [ "category", "object", "object", "morphism_in_range_category_of_homomorphism_structure" ],
	func := function ( cat, S, T, alpha )
	return IsCongruentForMorphisms( RangeCategoryOfHomomorphismStructure( cat ),
	InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( cat, InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( cat, S, T, alpha ) ),
	alpha
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "DistinguishedObjectOfHomomorphismStructure( cat )" ),
	rec( src_template := "Range( alpha )", dst_template := "HomomorphismStructureOnObjects( cat, S, T )" ),
	],
	),
	rec(
	# naturality of ν: ν(α ⋅ ξ ⋅ β) = ν(ξ) ⋅ H(α, β)
	description := "interpreting morphisms as morphisms from the distinguished object is a natural transformation",
	input_types := [ "category", "object", "object", "object", "object", "morphism", "morphism", "morphism" ],
	func := function ( cat, A, B, C, D, alpha, xi, beta )
	return IsCongruentForMorphisms( RangeCategoryOfHomomorphismStructure( cat ),
	InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( cat, PreComposeList( cat, A, [ alpha, xi, beta ], D ) ),
	PreCompose( RangeCategoryOfHomomorphismStructure( cat ), InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( cat, xi ), HomomorphismStructureOnMorphisms( cat, alpha, beta ) )
	);
	end,
	preconditions := [
	rec( src_template := "Source( alpha )", dst_template := "A" ),
	rec( src_template := "Range( alpha )", dst_template := "B" ),
	rec( src_template := "Source( xi )", dst_template := "B" ),
	rec( src_template := "Range( xi )", dst_template := "C" ),
	rec( src_template := "Source( beta )", dst_template := "C" ),
	rec( src_template := "Range( beta )", dst_template := "D" ),
	],
	),
	],
	),
	) );
	BindGlobal( "CAP_JIT_INTERNAL_PROOF_ASSISTANT_PROPOSITIONS", rec(
	is_category := rec(
	description := "is indeed a category",
	operations := [ "PreCompose", "IdentityMorphism" ],
	),
	is_equipped_with_preadditive_structure := rec(
	description := "is equipped with a preadditive structure",
	operations := [ "AdditionForMorphisms", "ZeroMorphism", "AdditiveInverseForMorphisms" ],
	),
	is_equipped_with_linear_structure := rec(
	description := "is equipped with a linear structure",
	operations := [ "MultiplyWithElementOfCommutativeRingForMorphisms" ],
	),
	has_zero_object := rec(
	description := "has a zero object",
	operations := [ "ZeroObject", "UniversalMorphismIntoZeroObject", "UniversalMorphismFromZeroObject" ],
	),
	has_kernels := rec(
	description := "has kernels",
	operations := [ "KernelObject", "KernelEmbedding", "KernelLift" ],
	),
	is_equipped_with_hom_structure := rec(
	description := "is equipped with a homomorphism structure",
	operations := [ "DistinguishedObjectOfHomomorphismStructure", "HomomorphismStructureOnObjects", "HomomorphismStructureOnMorphisms", "InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure", "InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism" ],
	),
	) );

These are crucial for purposes of verification, so it would be nice if another pair of eyes could double check that there are no typos and nothing is missing.