|
178 | 178 |
|
179 | 179 | ######## |
180 | 180 | function ( cat_1, Y_1, morphisms_1 ) |
181 | | - return CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( SKELETAL_FIN_SETS_ExplicitCoequalizer( Y_1, morphisms_1 ) ) ) ); |
| 181 | + local hoisted_2_1, deduped_3_1, deduped_4_1; |
| 182 | + deduped_4_1 := [ ]; |
| 183 | + deduped_3_1 := Length( Y_1 ); |
| 184 | + hoisted_2_1 := deduped_3_1 - 1; |
| 185 | + return CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( CapFixpoint( function ( coeq_old_2, coeq_2 ) |
| 186 | + return Length( coeq_2[1] ) = deduped_3_1; |
| 187 | + end, function ( coeq_2 ) |
| 188 | + local deduped_2_2, deduped_3_2, deduped_4_2, deduped_5_2; |
| 189 | + deduped_5_2 := coeq_2[1]; |
| 190 | + deduped_4_2 := SafeFirst( [ coeq_2[2] + 1 .. hoisted_2_1 ], function ( y_3 ) |
| 191 | + return not y_3 in deduped_5_2; |
| 192 | + end ); |
| 193 | + deduped_3_2 := CapFixpoint( function ( eq_class_old_3, eq_class_3 ) |
| 194 | + return Length( eq_class_old_3[1] ) = Length( eq_class_3[1] ); |
| 195 | + end, function ( eq_class_3 ) |
| 196 | + local deduped_3_3, deduped_4_3, deduped_5_3, deduped_6_3; |
| 197 | + deduped_6_3 := eq_class_3[2]; |
| 198 | + deduped_5_3 := eq_class_3[1]; |
| 199 | + deduped_4_3 := [ 1 .. Length( deduped_6_3 ) ]; |
| 200 | + deduped_3_3 := PositionsProperty( deduped_4_3, function ( j_4 ) |
| 201 | + return Length( Intersection( deduped_5_3, deduped_6_3[j_4] ) ) > 0; |
| 202 | + end ); |
| 203 | + return NTuple( 2, SSortedList( Concatenation( deduped_5_3, Concatenation( deduped_6_3{deduped_3_3} ) ) ), deduped_6_3{Difference( deduped_4_3, deduped_3_3 )} ); |
| 204 | + end, NTuple( 2, [ deduped_4_2 ], coeq_2[3] ) ); |
| 205 | + deduped_2_2 := deduped_3_2[1]; |
| 206 | + return NTuple( 4, SSortedList( Concatenation( deduped_5_2, deduped_2_2 ) ), deduped_4_2, deduped_3_2[2], Concatenation( coeq_2[4], [ deduped_2_2 ] ) ); |
| 207 | + end, NTuple( 4, deduped_4_1, -1, List( [ 0 .. CAP_JIT_INCOMPLETE_LOGIC( Length( AsList( CAP_JIT_INCOMPLETE_LOGIC( morphisms_1[1] ) ) ) ) - 1 ], function ( x_2 ) |
| 208 | + local hoisted_1_2; |
| 209 | + hoisted_1_2 := 1 + x_2; |
| 210 | + return SSortedList( List( morphisms_1, function ( logic_new_func_x_3 ) |
| 211 | + return AsList( logic_new_func_x_3 )[hoisted_1_2]; |
| 212 | + end ) ); |
| 213 | + end ), deduped_4_1 ) )[4] ) ) ); |
182 | 214 | end |
183 | 215 | ######## |
184 | 216 |
|
@@ -726,10 +758,41 @@ end |
726 | 758 |
|
727 | 759 | ######## |
728 | 760 | function ( cat_1, Y_1, morphisms_1, P_1 ) |
729 | | - local hoisted_1_1; |
730 | | - hoisted_1_1 := SKELETAL_FIN_SETS_ExplicitCoequalizer( Y_1, morphisms_1 ); |
731 | | - return CreateCapCategoryMorphismWithAttributes( cat_1, Y_1, P_1, AsList, List( [ 0 .. Length( Y_1 ) - 1 ], function ( x_2 ) |
732 | | - return -1 + BigInt( SafeUniquePositionProperty( hoisted_1_1, function ( c_3 ) |
| 761 | + local hoisted_2_1, hoisted_3_1, deduped_4_1, deduped_5_1; |
| 762 | + deduped_5_1 := [ ]; |
| 763 | + deduped_4_1 := Length( Y_1 ); |
| 764 | + hoisted_2_1 := deduped_4_1 - 1; |
| 765 | + hoisted_3_1 := CapFixpoint( function ( coeq_old_2, coeq_2 ) |
| 766 | + return Length( coeq_2[1] ) = deduped_4_1; |
| 767 | + end, function ( coeq_2 ) |
| 768 | + local deduped_2_2, deduped_3_2, deduped_4_2, deduped_5_2; |
| 769 | + deduped_5_2 := coeq_2[1]; |
| 770 | + deduped_4_2 := SafeFirst( [ coeq_2[2] + 1 .. hoisted_2_1 ], function ( y_3 ) |
| 771 | + return not y_3 in deduped_5_2; |
| 772 | + end ); |
| 773 | + deduped_3_2 := CapFixpoint( function ( eq_class_old_3, eq_class_3 ) |
| 774 | + return Length( eq_class_old_3[1] ) = Length( eq_class_3[1] ); |
| 775 | + end, function ( eq_class_3 ) |
| 776 | + local deduped_3_3, deduped_4_3, deduped_5_3, deduped_6_3; |
| 777 | + deduped_6_3 := eq_class_3[2]; |
| 778 | + deduped_5_3 := eq_class_3[1]; |
| 779 | + deduped_4_3 := [ 1 .. Length( deduped_6_3 ) ]; |
| 780 | + deduped_3_3 := PositionsProperty( deduped_4_3, function ( j_4 ) |
| 781 | + return Length( Intersection( deduped_5_3, deduped_6_3[j_4] ) ) > 0; |
| 782 | + end ); |
| 783 | + return NTuple( 2, SSortedList( Concatenation( deduped_5_3, Concatenation( deduped_6_3{deduped_3_3} ) ) ), deduped_6_3{Difference( deduped_4_3, deduped_3_3 )} ); |
| 784 | + end, NTuple( 2, [ deduped_4_2 ], coeq_2[3] ) ); |
| 785 | + deduped_2_2 := deduped_3_2[1]; |
| 786 | + return NTuple( 4, SSortedList( Concatenation( deduped_5_2, deduped_2_2 ) ), deduped_4_2, deduped_3_2[2], Concatenation( coeq_2[4], [ deduped_2_2 ] ) ); |
| 787 | + end, NTuple( 4, deduped_5_1, -1, List( [ 0 .. CAP_JIT_INCOMPLETE_LOGIC( Length( AsList( CAP_JIT_INCOMPLETE_LOGIC( morphisms_1[1] ) ) ) ) - 1 ], function ( x_2 ) |
| 788 | + local hoisted_1_2; |
| 789 | + hoisted_1_2 := 1 + x_2; |
| 790 | + return SSortedList( List( morphisms_1, function ( logic_new_func_x_3 ) |
| 791 | + return AsList( logic_new_func_x_3 )[hoisted_1_2]; |
| 792 | + end ) ); |
| 793 | + end ), deduped_5_1 ) )[4]; |
| 794 | + return CreateCapCategoryMorphismWithAttributes( cat_1, Y_1, P_1, AsList, List( Y_1, function ( x_2 ) |
| 795 | + return -1 + BigInt( SafeUniquePositionProperty( hoisted_3_1, function ( c_3 ) |
733 | 796 | return (x_2 in c_3); |
734 | 797 | end ) ); |
735 | 798 | end ) ); |
@@ -874,10 +937,41 @@ end |
874 | 937 |
|
875 | 938 | ######## |
876 | 939 | function ( cat_1, Y_1, morphisms_1, T_1, tau_1, P_1 ) |
877 | | - local hoisted_1_1; |
878 | | - hoisted_1_1 := AsList( tau_1 ); |
879 | | - return CreateCapCategoryMorphismWithAttributes( cat_1, P_1, Range( tau_1 ), AsList, List( SKELETAL_FIN_SETS_ExplicitCoequalizer( Y_1, morphisms_1 ), function ( x_2 ) |
880 | | - return hoisted_1_1[1 + x_2[1]]; |
| 940 | + local hoisted_2_1, hoisted_3_1, deduped_4_1, deduped_5_1; |
| 941 | + deduped_5_1 := [ ]; |
| 942 | + deduped_4_1 := Length( Y_1 ); |
| 943 | + hoisted_3_1 := AsList( tau_1 ); |
| 944 | + hoisted_2_1 := deduped_4_1 - 1; |
| 945 | + return CreateCapCategoryMorphismWithAttributes( cat_1, P_1, Range( tau_1 ), AsList, List( CapFixpoint( function ( coeq_old_2, coeq_2 ) |
| 946 | + return Length( coeq_2[1] ) = deduped_4_1; |
| 947 | + end, function ( coeq_2 ) |
| 948 | + local deduped_2_2, deduped_3_2, deduped_4_2, deduped_5_2; |
| 949 | + deduped_5_2 := coeq_2[1]; |
| 950 | + deduped_4_2 := SafeFirst( [ coeq_2[2] + 1 .. hoisted_2_1 ], function ( y_3 ) |
| 951 | + return not y_3 in deduped_5_2; |
| 952 | + end ); |
| 953 | + deduped_3_2 := CapFixpoint( function ( eq_class_old_3, eq_class_3 ) |
| 954 | + return Length( eq_class_old_3[1] ) = Length( eq_class_3[1] ); |
| 955 | + end, function ( eq_class_3 ) |
| 956 | + local deduped_3_3, deduped_4_3, deduped_5_3, deduped_6_3; |
| 957 | + deduped_6_3 := eq_class_3[2]; |
| 958 | + deduped_5_3 := eq_class_3[1]; |
| 959 | + deduped_4_3 := [ 1 .. Length( deduped_6_3 ) ]; |
| 960 | + deduped_3_3 := PositionsProperty( deduped_4_3, function ( j_4 ) |
| 961 | + return Length( Intersection( deduped_5_3, deduped_6_3[j_4] ) ) > 0; |
| 962 | + end ); |
| 963 | + return NTuple( 2, SSortedList( Concatenation( deduped_5_3, Concatenation( deduped_6_3{deduped_3_3} ) ) ), deduped_6_3{Difference( deduped_4_3, deduped_3_3 )} ); |
| 964 | + end, NTuple( 2, [ deduped_4_2 ], coeq_2[3] ) ); |
| 965 | + deduped_2_2 := deduped_3_2[1]; |
| 966 | + return NTuple( 4, SSortedList( Concatenation( deduped_5_2, deduped_2_2 ) ), deduped_4_2, deduped_3_2[2], Concatenation( coeq_2[4], [ deduped_2_2 ] ) ); |
| 967 | + end, NTuple( 4, deduped_5_1, -1, List( [ 0 .. CAP_JIT_INCOMPLETE_LOGIC( Length( AsList( CAP_JIT_INCOMPLETE_LOGIC( morphisms_1[1] ) ) ) ) - 1 ], function ( x_2 ) |
| 968 | + local hoisted_1_2; |
| 969 | + hoisted_1_2 := 1 + x_2; |
| 970 | + return SSortedList( List( morphisms_1, function ( logic_new_func_x_3 ) |
| 971 | + return AsList( logic_new_func_x_3 )[hoisted_1_2]; |
| 972 | + end ) ); |
| 973 | + end ), deduped_5_1 ) )[4], function ( x_2 ) |
| 974 | + return hoisted_3_1[1 + x_2[1]]; |
881 | 975 | end ) ); |
882 | 976 | end |
883 | 977 | ######## |
|
0 commit comments