Documentation

d__'8776'__30 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → AgdaAny → AgdaAny → () Source #

d_Carrier_32 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → () Source #

d_suc'35'_34 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → AgdaAny → AgdaAny Source #

du_suc'35'_34 ∷ T_RawSuccessorSet_10 → AgdaAny → AgdaAny Source #

d_zero'35'_36 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → AgdaAny Source #

du_zero'35'_36 ∷ T_RawSuccessorSet_10 → AgdaAny Source #

d_Homomorphic'8320'_50 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_52 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_IsSuccessorSetHomomorphism_60 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSuccessorSetHomomorphism_60 Source #

d_isRelHomomorphism_70 ∷ T_IsSuccessorSetHomomorphism_60 → T_IsRelHomomorphism_42 Source #

d_suc'35''45'homo_72 ∷ T_IsSuccessorSetHomomorphism_60 → AgdaAny → AgdaAny Source #

d_zero'35''45'homo_74 ∷ T_IsSuccessorSetHomomorphism_60 → AgdaAny Source #

d_IsSuccessorSetMonomorphism_78 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSuccessorSetMonomorphism_78 Source #

d_isSuccessorSetHomomorphism_86 ∷ T_IsSuccessorSetMonomorphism_78 → T_IsSuccessorSetHomomorphism_60 Source #

d_injective_88 ∷ T_IsSuccessorSetMonomorphism_78 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_92 ∷ T_IsSuccessorSetMonomorphism_78 → T_IsRelHomomorphism_42 Source #

d_suc'35''45'homo_94 ∷ T_IsSuccessorSetMonomorphism_78 → AgdaAny → AgdaAny Source #

d_zero'35''45'homo_96 ∷ T_IsSuccessorSetMonomorphism_78 → AgdaAny Source #

d_isRelMonomorphism_98 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → (AgdaAny → AgdaAny) → T_IsSuccessorSetMonomorphism_78 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_98 ∷ T_IsSuccessorSetMonomorphism_78 → T_IsRelMonomorphism_64 Source #

d_IsSuccessorSetIsomorphism_102 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSuccessorSetIsomorphism_102 Source #

d_isSuccessorSetMonomorphism_110 ∷ T_IsSuccessorSetIsomorphism_102 → T_IsSuccessorSetMonomorphism_78 Source #

d_surjective_112 ∷ T_IsSuccessorSetIsomorphism_102 → AgdaAny → T_Σ_14 Source #

d_injective_116 ∷ T_IsSuccessorSetIsomorphism_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_118 ∷ T_IsSuccessorSetIsomorphism_102 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → (AgdaAny → AgdaAny) → T_IsSuccessorSetIsomorphism_102 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_120 ∷ T_IsSuccessorSetIsomorphism_102 → T_IsRelMonomorphism_64 Source #

d_isSuccessorSetHomomorphism_122 ∷ T_IsSuccessorSetIsomorphism_102 → T_IsSuccessorSetHomomorphism_60 Source #

d_suc'35''45'homo_124 ∷ T_IsSuccessorSetIsomorphism_102 → AgdaAny → AgdaAny Source #

d_zero'35''45'homo_126 ∷ T_IsSuccessorSetIsomorphism_102 → AgdaAny Source #

d_isRelIsomorphism_128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → (AgdaAny → AgdaAny) → T_IsSuccessorSetIsomorphism_102 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_128 ∷ T_IsSuccessorSetIsomorphism_102 → T_IsRelIsomorphism_94 Source #

d__'8729'__146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_36 → T_RawMagma_36 → AgdaAny → AgdaAny → AgdaAny Source #

du__'8729'__146 ∷ T_RawMagma_36 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_36 → T_RawMagma_36 → AgdaAny → AgdaAny → () Source #

d_Carrier_152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_36 → T_RawMagma_36 → () Source #

d_Homomorphic'8322'_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_36 → T_RawMagma_36 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsMagmaHomomorphism_176 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_184 ∷ T_IsMagmaHomomorphism_176 → T_IsRelHomomorphism_42 Source #

d_homo_186 ∷ T_IsMagmaHomomorphism_176 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_190 ∷ T_IsMagmaHomomorphism_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMagmaMonomorphism_194 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMagmaMonomorphism_194 Source #

d_isMagmaHomomorphism_202 ∷ T_IsMagmaMonomorphism_194 → T_IsMagmaHomomorphism_176 Source #

d_injective_204 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_208 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_210 ∷ T_IsMagmaMonomorphism_194 → T_IsRelHomomorphism_42 Source #

d_cong_212 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelMonomorphism_214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_36 → T_RawMagma_36 → (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_194 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_214 ∷ T_IsMagmaMonomorphism_194 → T_IsRelMonomorphism_64 Source #

d_IsMagmaIsomorphism_218 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMagmaIsomorphism_218 Source #

d_isMagmaMonomorphism_226 ∷ T_IsMagmaIsomorphism_218 → T_IsMagmaMonomorphism_194 Source #

d_surjective_228 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → T_Σ_14 Source #

d_homo_232 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_234 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_236 ∷ T_IsMagmaIsomorphism_218 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_238 ∷ T_IsMagmaIsomorphism_218 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_240 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_36 → T_RawMagma_36 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_240 ∷ T_IsMagmaIsomorphism_218 → T_IsRelMonomorphism_64 Source #

d_cong_242 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelIsomorphism_244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_36 → T_RawMagma_36 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_244 ∷ T_IsMagmaIsomorphism_218 → T_IsRelIsomorphism_94 Source #

d__'8776'__264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → AgdaAny → AgdaAny → () Source #

d_Carrier_268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → () Source #

d_ε_272 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → AgdaAny Source #

du_ε_272 ∷ T_RawMonoid_64 → AgdaAny Source #

d_Homomorphic'8320'_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_IsMagmaHomomorphism_300 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaIsomorphism_302 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaMonomorphism_304 ∷ p → p → p → p → p → p → p → () Source #

d_homo_308 ∷ T_IsMagmaHomomorphism_176 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_310 ∷ T_IsMagmaHomomorphism_176 → T_IsRelHomomorphism_42 Source #

d_cong_312 ∷ T_IsMagmaHomomorphism_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_316 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_318 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_320 ∷ T_IsMagmaIsomorphism_218 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_322 ∷ T_IsMagmaIsomorphism_218 → T_IsMagmaMonomorphism_194 Source #

d_isRelHomomorphism_324 ∷ T_IsMagmaIsomorphism_218 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_326 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_326 ∷ (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_328 ∷ T_IsMagmaIsomorphism_218 → T_IsRelMonomorphism_64 Source #

d_surjective_330 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → T_Σ_14 Source #

d_cong_332 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_336 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_338 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_340 ∷ T_IsMagmaMonomorphism_194 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_342 ∷ T_IsMagmaMonomorphism_194 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_344 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_194 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_344 ∷ (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_194 → T_IsRelMonomorphism_64 Source #

d_cong_346 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoidHomomorphism_350 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMonoidHomomorphism_350 Source #

d_isMagmaHomomorphism_358 ∷ T_IsMonoidHomomorphism_350 → T_IsMagmaHomomorphism_176 Source #

d_ε'45'homo_360 ∷ T_IsMonoidHomomorphism_350 → AgdaAny Source #

d_homo_364 ∷ T_IsMonoidHomomorphism_350 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_366 ∷ T_IsMonoidHomomorphism_350 → T_IsRelHomomorphism_42 Source #

d_cong_368 ∷ T_IsMonoidHomomorphism_350 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoidMonomorphism_372 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMonoidMonomorphism_372 Source #

d_isMonoidHomomorphism_380 ∷ T_IsMonoidMonomorphism_372 → T_IsMonoidHomomorphism_350 Source #

d_injective_382 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_386 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_388 ∷ T_IsMonoidMonomorphism_372 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_390 ∷ T_IsMonoidMonomorphism_372 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_392 ∷ T_IsMonoidMonomorphism_372 → AgdaAny Source #

d_cong_394 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaMonomorphism_396 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_396 ∷ T_IsMonoidMonomorphism_372 → T_IsMagmaMonomorphism_194 Source #

d_isRelMonomorphism_400 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_400 ∷ T_IsMonoidMonomorphism_372 → T_IsRelMonomorphism_64 Source #

d_IsMonoidIsomorphism_404 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMonoidIsomorphism_404 Source #

d_isMonoidMonomorphism_412 ∷ T_IsMonoidIsomorphism_404 → T_IsMonoidMonomorphism_372 Source #

d_surjective_414 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → T_Σ_14 Source #

d_homo_418 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_420 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_422 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_424 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_424 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_426 ∷ T_IsMonoidIsomorphism_404 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_428 ∷ T_IsMonoidIsomorphism_404 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_430 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_430 ∷ T_IsMonoidIsomorphism_404 → T_IsRelMonomorphism_64 Source #

d_ε'45'homo_432 ∷ T_IsMonoidIsomorphism_404 → AgdaAny Source #

d_cong_434 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaIsomorphism_436 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_436 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaIsomorphism_218 Source #

d_isRelIsomorphism_440 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_64 → T_RawMonoid_64 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_440 ∷ T_IsMonoidIsomorphism_404 → T_IsRelIsomorphism_94 Source #

d__'8315''185'_458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → AgdaAny → AgdaAny Source #

du__'8315''185'_458 ∷ T_RawGroup_96 → AgdaAny → AgdaAny Source #

d__'8776'__462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → AgdaAny → AgdaAny → () Source #

d_Carrier_466 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → () Source #

d_Homomorphic'8321'_496 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_IsMagmaHomomorphism_504 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaIsomorphism_506 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaMonomorphism_508 ∷ p → p → p → p → p → p → p → () Source #

d_homo_512 ∷ T_IsMagmaHomomorphism_176 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_514 ∷ T_IsMagmaHomomorphism_176 → T_IsRelHomomorphism_42 Source #

d_cong_516 ∷ T_IsMagmaHomomorphism_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_520 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_522 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_524 ∷ T_IsMagmaIsomorphism_218 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_526 ∷ T_IsMagmaIsomorphism_218 → T_IsMagmaMonomorphism_194 Source #

d_isRelHomomorphism_528 ∷ T_IsMagmaIsomorphism_218 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_530 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_530 ∷ (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_532 ∷ T_IsMagmaIsomorphism_218 → T_IsRelMonomorphism_64 Source #

d_surjective_534 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → T_Σ_14 Source #

d_cong_536 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_540 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_542 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_544 ∷ T_IsMagmaMonomorphism_194 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_546 ∷ T_IsMagmaMonomorphism_194 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_194 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_548 ∷ (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_194 → T_IsRelMonomorphism_64 Source #

d_cong_550 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoidHomomorphism_554 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidIsomorphism_556 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidMonomorphism_558 ∷ p → p → p → p → p → p → p → () Source #

d_homo_562 ∷ T_IsMonoidHomomorphism_350 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_564 ∷ T_IsMonoidHomomorphism_350 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_566 ∷ T_IsMonoidHomomorphism_350 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_568 ∷ T_IsMonoidHomomorphism_350 → AgdaAny Source #

d_cong_570 ∷ T_IsMonoidHomomorphism_350 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_574 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_576 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_578 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaIsomorphism_580 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_580 ∷ (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaIsomorphism_218 Source #

d_isMagmaMonomorphism_582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_582 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_584 ∷ T_IsMonoidIsomorphism_404 → T_IsMonoidHomomorphism_350 Source #

d_isMonoidMonomorphism_586 ∷ T_IsMonoidIsomorphism_404 → T_IsMonoidMonomorphism_372 Source #

d_isRelHomomorphism_588 ∷ T_IsMonoidIsomorphism_404 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_590 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_590 ∷ T_IsMonoidIsomorphism_404 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_592 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_592 ∷ T_IsMonoidIsomorphism_404 → T_IsRelMonomorphism_64 Source #

d_surjective_594 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_596 ∷ T_IsMonoidIsomorphism_404 → AgdaAny Source #

d_cong_598 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_602 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_604 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_606 ∷ T_IsMonoidMonomorphism_372 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_608 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_608 ∷ (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_610 ∷ T_IsMonoidMonomorphism_372 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_612 ∷ T_IsMonoidMonomorphism_372 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_614 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_614 ∷ T_IsMonoidMonomorphism_372 → T_IsRelMonomorphism_64 Source #

d_ε'45'homo_616 ∷ T_IsMonoidMonomorphism_372 → AgdaAny Source #

d_cong_618 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsGroupHomomorphism_622 ∷ p → p → p → p → p → p → p → () Source #

data T_IsGroupHomomorphism_622 Source #

d_isMonoidHomomorphism_630 ∷ T_IsGroupHomomorphism_622 → T_IsMonoidHomomorphism_350 Source #

d_'8315''185''45'homo_632 ∷ T_IsGroupHomomorphism_622 → AgdaAny → AgdaAny Source #

d_homo_636 ∷ T_IsGroupHomomorphism_622 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_638 ∷ T_IsGroupHomomorphism_622 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_640 ∷ T_IsGroupHomomorphism_622 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_642 ∷ T_IsGroupHomomorphism_622 → AgdaAny Source #

d_cong_644 ∷ T_IsGroupHomomorphism_622 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsGroupMonomorphism_648 ∷ p → p → p → p → p → p → p → () Source #

data T_IsGroupMonomorphism_648 Source #

d_isGroupHomomorphism_656 ∷ T_IsGroupMonomorphism_648 → T_IsGroupHomomorphism_622 Source #

d_injective_658 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_662 ∷ T_IsGroupMonomorphism_648 → T_IsMagmaHomomorphism_176 Source #

d_isMonoidHomomorphism_664 ∷ T_IsGroupMonomorphism_648 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_666 ∷ T_IsGroupMonomorphism_648 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_668 ∷ T_IsGroupMonomorphism_648 → AgdaAny Source #

d_'8315''185''45'homo_670 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny Source #

d_homo_672 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_674 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMonoidMonomorphism_676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsMonoidMonomorphism_372 Source #

du_isMonoidMonomorphism_676 ∷ T_IsGroupMonomorphism_648 → T_IsMonoidMonomorphism_372 Source #

d_isMagmaMonomorphism_680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_680 ∷ T_IsGroupMonomorphism_648 → T_IsMagmaMonomorphism_194 Source #

d_isRelMonomorphism_682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_682 ∷ T_IsGroupMonomorphism_648 → T_IsRelMonomorphism_64 Source #

d_IsGroupIsomorphism_686 ∷ p → p → p → p → p → p → p → () Source #

data T_IsGroupIsomorphism_686 Source #

d_isGroupMonomorphism_694 ∷ T_IsGroupIsomorphism_686 → T_IsGroupMonomorphism_648 Source #

d_surjective_696 ∷ T_IsGroupIsomorphism_686 → AgdaAny → T_Σ_14 Source #

d_injective_700 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroupHomomorphism_702 ∷ T_IsGroupIsomorphism_686 → T_IsGroupHomomorphism_622 Source #

d_isMagmaHomomorphism_704 ∷ T_IsGroupIsomorphism_686 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_706 ∷ T_IsGroupIsomorphism_686 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_708 ∷ T_IsGroupIsomorphism_686 → T_IsMonoidHomomorphism_350 Source #

d_isMonoidMonomorphism_710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMonoidMonomorphism_372 Source #

du_isMonoidMonomorphism_710 ∷ T_IsGroupIsomorphism_686 → T_IsMonoidMonomorphism_372 Source #

d_isRelHomomorphism_712 ∷ T_IsGroupIsomorphism_686 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_714 ∷ T_IsGroupIsomorphism_686 → T_IsRelMonomorphism_64 Source #

d_ε'45'homo_716 ∷ T_IsGroupIsomorphism_686 → AgdaAny Source #

d_'8315''185''45'homo_718 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny Source #

d_homo_720 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_722 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMonoidIsomorphism_724 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMonoidIsomorphism_404 Source #

du_isMonoidIsomorphism_724 ∷ T_IsGroupIsomorphism_686 → T_IsMonoidIsomorphism_404 Source #

d_isMagmaIsomorphism_728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_728 ∷ T_IsGroupIsomorphism_686 → T_IsMagmaIsomorphism_218 Source #

d_isRelIsomorphism_730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_96 → T_RawGroup_96 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_730 ∷ T_IsGroupIsomorphism_686 → T_IsRelIsomorphism_94 Source #

d__'42'__748 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → AgdaAny → AgdaAny → AgdaAny Source #

du__'42'__748 ∷ T_RawNearSemiring_134 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__752 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → AgdaAny → AgdaAny → () Source #

d_Carrier_764 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → () Source #

d_IsMonoidHomomorphism_788 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidIsomorphism_790 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidMonomorphism_792 ∷ p → p → p → p → p → p → p → () Source #

d_homo_796 ∷ T_IsMonoidHomomorphism_350 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_798 ∷ T_IsMonoidHomomorphism_350 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_800 ∷ T_IsMonoidHomomorphism_350 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_802 ∷ T_IsMonoidHomomorphism_350 → AgdaAny Source #

d_cong_804 ∷ T_IsMonoidHomomorphism_350 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_808 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_810 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_812 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaIsomorphism_814 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_814 ∷ (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaIsomorphism_218 Source #

d_isMagmaMonomorphism_816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_816 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_818 ∷ T_IsMonoidIsomorphism_404 → T_IsMonoidHomomorphism_350 Source #

d_isMonoidMonomorphism_820 ∷ T_IsMonoidIsomorphism_404 → T_IsMonoidMonomorphism_372 Source #

d_isRelHomomorphism_822 ∷ T_IsMonoidIsomorphism_404 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_824 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_824 ∷ T_IsMonoidIsomorphism_404 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_826 ∷ T_IsMonoidIsomorphism_404 → T_IsRelMonomorphism_64 Source #

d_surjective_828 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_830 ∷ T_IsMonoidIsomorphism_404 → AgdaAny Source #

d_cong_832 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_836 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_838 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_840 ∷ T_IsMonoidMonomorphism_372 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_842 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_842 ∷ (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_844 ∷ T_IsMonoidMonomorphism_372 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_846 ∷ T_IsMonoidMonomorphism_372 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_848 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_848 ∷ T_IsMonoidMonomorphism_372 → T_IsRelMonomorphism_64 Source #

d_ε'45'homo_850 ∷ T_IsMonoidMonomorphism_372 → AgdaAny Source #

d_cong_852 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMagmaHomomorphism_856 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaIsomorphism_858 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaMonomorphism_860 ∷ p → p → p → p → p → p → p → () Source #

d_homo_864 ∷ T_IsMagmaHomomorphism_176 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_866 ∷ T_IsMagmaHomomorphism_176 → T_IsRelHomomorphism_42 Source #

d_cong_868 ∷ T_IsMagmaHomomorphism_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_872 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_874 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_876 ∷ T_IsMagmaIsomorphism_218 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_878 ∷ T_IsMagmaIsomorphism_218 → T_IsMagmaMonomorphism_194 Source #

d_isRelHomomorphism_880 ∷ T_IsMagmaIsomorphism_218 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_882 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_882 ∷ (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_884 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_884 ∷ T_IsMagmaIsomorphism_218 → T_IsRelMonomorphism_64 Source #

d_surjective_886 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → T_Σ_14 Source #

d_cong_888 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_892 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_894 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_896 ∷ T_IsMagmaMonomorphism_194 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_898 ∷ T_IsMagmaMonomorphism_194 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_900 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_194 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_900 ∷ (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_194 → T_IsRelMonomorphism_64 Source #

d_cong_902 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Homomorphic'8322'_910 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsNearSemiringHomomorphism_916 ∷ p → p → p → p → p → p → p → () Source #

data T_IsNearSemiringHomomorphism_916 Source #

d_'43''45'isMonoidHomomorphism_924 ∷ T_IsNearSemiringHomomorphism_916 → T_IsMonoidHomomorphism_350 Source #

d_'42''45'homo_926 ∷ T_IsNearSemiringHomomorphism_916 → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_930 ∷ T_IsNearSemiringHomomorphism_916 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_932 ∷ T_IsNearSemiringHomomorphism_916 → T_IsMagmaHomomorphism_176 Source #

d_ε'45'homo_934 ∷ T_IsNearSemiringHomomorphism_916 → AgdaAny Source #

d_isRelHomomorphism_936 ∷ T_IsNearSemiringHomomorphism_916 → T_IsRelHomomorphism_42 Source #

d_cong_938 ∷ T_IsNearSemiringHomomorphism_916 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_940 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringHomomorphism_916 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_940 ∷ T_IsNearSemiringHomomorphism_916 → T_IsMagmaHomomorphism_176 Source #

d_IsNearSemiringMonomorphism_944 ∷ p → p → p → p → p → p → p → () Source #

data T_IsNearSemiringMonomorphism_944 Source #

d_isNearSemiringHomomorphism_952 ∷ T_IsNearSemiringMonomorphism_944 → T_IsNearSemiringHomomorphism_916 Source #

d_injective_954 ∷ T_IsNearSemiringMonomorphism_944 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_958 ∷ T_IsNearSemiringMonomorphism_944 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_960 ∷ T_IsNearSemiringMonomorphism_944 → T_IsMagmaHomomorphism_176 Source #

d_homo_962 ∷ T_IsNearSemiringMonomorphism_944 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_964 ∷ T_IsNearSemiringMonomorphism_944 → T_IsMagmaHomomorphism_176 Source #

d_'43''45'isMonoidHomomorphism_966 ∷ T_IsNearSemiringMonomorphism_944 → T_IsMonoidHomomorphism_350 Source #

d_ε'45'homo_968 ∷ T_IsNearSemiringMonomorphism_944 → AgdaAny Source #

d_isRelHomomorphism_970 ∷ T_IsNearSemiringMonomorphism_944 → T_IsRelHomomorphism_42 Source #

d_cong_972 ∷ T_IsNearSemiringMonomorphism_944 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isMonoidMonomorphism_974 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsMonoidMonomorphism_372 Source #

du_'43''45'isMonoidMonomorphism_974 ∷ T_IsNearSemiringMonomorphism_944 → T_IsMonoidMonomorphism_372 Source #

d_isMagmaMonomorphism_978 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_978 ∷ T_IsNearSemiringMonomorphism_944 → T_IsMagmaMonomorphism_194 Source #

d_isRelMonomorphism_980 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_980 ∷ T_IsNearSemiringMonomorphism_944 → T_IsRelMonomorphism_64 Source #

d_'42''45'isMagmaMonomorphism_982 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsMagmaMonomorphism_194 Source #

du_'42''45'isMagmaMonomorphism_982 ∷ T_IsNearSemiringMonomorphism_944 → T_IsMagmaMonomorphism_194 Source #

d_IsNearSemiringIsomorphism_986 ∷ p → p → p → p → p → p → p → () Source #

data T_IsNearSemiringIsomorphism_986 Source #

d_isNearSemiringMonomorphism_994 ∷ T_IsNearSemiringIsomorphism_986 → T_IsNearSemiringMonomorphism_944 Source #

d_surjective_996 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny → T_Σ_14 Source #

d_'42''45'homo_1000 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1002 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_1002 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaHomomorphism_176 Source #

d_'42''45'isMagmaMonomorphism_1004 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaMonomorphism_194 Source #

du_'42''45'isMagmaMonomorphism_1004 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaMonomorphism_194 Source #

d_homo_1006 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1008 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_1010 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1010 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaMonomorphism_194 Source #

d_'43''45'isMonoidHomomorphism_1012 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMonoidHomomorphism_350 Source #

d_'43''45'isMonoidMonomorphism_1014 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMonoidMonomorphism_372 Source #

du_'43''45'isMonoidMonomorphism_1014 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMonoidMonomorphism_372 Source #

d_ε'45'homo_1016 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny Source #

d_injective_1018 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1020 ∷ T_IsNearSemiringIsomorphism_986 → T_IsNearSemiringHomomorphism_916 Source #

d_isRelHomomorphism_1022 ∷ T_IsNearSemiringIsomorphism_986 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1024 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1024 ∷ T_IsNearSemiringIsomorphism_986 → T_IsRelMonomorphism_64 Source #

d_cong_1026 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isMonoidIsomorphism_1028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMonoidIsomorphism_404 Source #

du_'43''45'isMonoidIsomorphism_1028 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMonoidIsomorphism_404 Source #

d_isMagmaIsomorphism_1032 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_1032 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaIsomorphism_218 Source #

d_isRelIsomorphism_1034 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1034 ∷ T_IsNearSemiringIsomorphism_986 → T_IsRelIsomorphism_94 Source #

d_'42''45'isMagmaIsomorphism_1036 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_134 → T_RawNearSemiring_134 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaIsomorphism_218 Source #

du_'42''45'isMagmaIsomorphism_1036 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaIsomorphism_218 Source #

d__'8776'__1058 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → AgdaAny → AgdaAny → () Source #

d_1'35'_1072 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → AgdaAny Source #

du_1'35'_1072 ∷ T_RawSemiring_174 → AgdaAny Source #

d_Carrier_1074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → () Source #

d_IsMonoidHomomorphism_1106 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidIsomorphism_1108 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidMonomorphism_1110 ∷ p → p → p → p → p → p → p → () Source #

d_homo_1114 ∷ T_IsMonoidHomomorphism_350 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1116 ∷ T_IsMonoidHomomorphism_350 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_1118 ∷ T_IsMonoidHomomorphism_350 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_1120 ∷ T_IsMonoidHomomorphism_350 → AgdaAny Source #

d_cong_1122 ∷ T_IsMonoidHomomorphism_350 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1126 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1128 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1130 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaIsomorphism_1132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_1132 ∷ (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaIsomorphism_218 Source #

d_isMagmaMonomorphism_1134 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1134 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_1136 ∷ T_IsMonoidIsomorphism_404 → T_IsMonoidHomomorphism_350 Source #

d_isMonoidMonomorphism_1138 ∷ T_IsMonoidIsomorphism_404 → T_IsMonoidMonomorphism_372 Source #

d_isRelHomomorphism_1140 ∷ T_IsMonoidIsomorphism_404 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1142 ∷ T_IsMonoidIsomorphism_404 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_1144 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1144 ∷ T_IsMonoidIsomorphism_404 → T_IsRelMonomorphism_64 Source #

d_surjective_1146 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_1148 ∷ T_IsMonoidIsomorphism_404 → AgdaAny Source #

d_cong_1150 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1154 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1156 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1158 ∷ T_IsMonoidMonomorphism_372 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_1160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1160 ∷ (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_1162 ∷ T_IsMonoidMonomorphism_372 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_1164 ∷ T_IsMonoidMonomorphism_372 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1166 ∷ T_IsMonoidMonomorphism_372 → T_IsRelMonomorphism_64 Source #

d_ε'45'homo_1168 ∷ T_IsMonoidMonomorphism_372 → AgdaAny Source #

d_cong_1170 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Homomorphic'8320'_1174 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_IsNearSemiringHomomorphism_1184 ∷ p → p → p → p → p → p → p → () Source #

d_IsNearSemiringIsomorphism_1186 ∷ p → p → p → p → p → p → p → () Source #

d_IsNearSemiringMonomorphism_1188 ∷ p → p → p → p → p → p → p → () Source #

d_'42''45'homo_1192 ∷ T_IsNearSemiringHomomorphism_916 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringHomomorphism_916 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_1194 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringHomomorphism_916 → T_IsMagmaHomomorphism_176 Source #

d_homo_1196 ∷ T_IsNearSemiringHomomorphism_916 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1198 ∷ T_IsNearSemiringHomomorphism_916 → T_IsMagmaHomomorphism_176 Source #

d_'43''45'isMonoidHomomorphism_1200 ∷ T_IsNearSemiringHomomorphism_916 → T_IsMonoidHomomorphism_350 Source #

d_ε'45'homo_1202 ∷ T_IsNearSemiringHomomorphism_916 → AgdaAny Source #

d_isRelHomomorphism_1204 ∷ T_IsNearSemiringHomomorphism_916 → T_IsRelHomomorphism_42 Source #

d_cong_1206 ∷ T_IsNearSemiringHomomorphism_916 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1210 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_1212 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaHomomorphism_176 Source #

d_'42''45'isMagmaIsomorphism_1214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaIsomorphism_218 Source #

du_'42''45'isMagmaIsomorphism_1214 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaIsomorphism_218 Source #

d_'42''45'isMagmaMonomorphism_1216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaMonomorphism_194 Source #

du_'42''45'isMagmaMonomorphism_1216 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaMonomorphism_194 Source #

d_homo_1218 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1220 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaIsomorphism_1222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_1222 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaIsomorphism_218 Source #

d_isMagmaMonomorphism_1224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1224 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMagmaMonomorphism_194 Source #

d_'43''45'isMonoidHomomorphism_1226 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMonoidHomomorphism_350 Source #

d_'43''45'isMonoidIsomorphism_1228 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMonoidIsomorphism_404 Source #

du_'43''45'isMonoidIsomorphism_1228 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMonoidIsomorphism_404 Source #

d_'43''45'isMonoidMonomorphism_1230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsMonoidMonomorphism_372 Source #

du_'43''45'isMonoidMonomorphism_1230 ∷ T_IsNearSemiringIsomorphism_986 → T_IsMonoidMonomorphism_372 Source #

d_ε'45'homo_1232 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny Source #

d_injective_1234 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1236 ∷ T_IsNearSemiringIsomorphism_986 → T_IsNearSemiringHomomorphism_916 Source #

d_isNearSemiringMonomorphism_1238 ∷ T_IsNearSemiringIsomorphism_986 → T_IsNearSemiringMonomorphism_944 Source #

d_isRelHomomorphism_1240 ∷ T_IsNearSemiringIsomorphism_986 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1242 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1242 ∷ T_IsNearSemiringIsomorphism_986 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_1244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_986 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1244 ∷ T_IsNearSemiringIsomorphism_986 → T_IsRelMonomorphism_64 Source #

d_surjective_1246 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny → T_Σ_14 Source #

d_cong_1248 ∷ T_IsNearSemiringIsomorphism_986 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1252 ∷ T_IsNearSemiringMonomorphism_944 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_1254 ∷ T_IsNearSemiringMonomorphism_944 → T_IsMagmaHomomorphism_176 Source #

d_'42''45'isMagmaMonomorphism_1256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsMagmaMonomorphism_194 Source #

du_'42''45'isMagmaMonomorphism_1256 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsMagmaMonomorphism_194 Source #

d_homo_1258 ∷ T_IsNearSemiringMonomorphism_944 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1260 ∷ T_IsNearSemiringMonomorphism_944 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_1262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1262 ∷ T_IsNearSemiringMonomorphism_944 → T_IsMagmaMonomorphism_194 Source #

d_'43''45'isMonoidHomomorphism_1264 ∷ T_IsNearSemiringMonomorphism_944 → T_IsMonoidHomomorphism_350 Source #

d_'43''45'isMonoidMonomorphism_1266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsMonoidMonomorphism_372 Source #

du_'43''45'isMonoidMonomorphism_1266 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsMonoidMonomorphism_372 Source #

d_ε'45'homo_1268 ∷ T_IsNearSemiringMonomorphism_944 → AgdaAny Source #

d_injective_1270 ∷ T_IsNearSemiringMonomorphism_944 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1272 ∷ T_IsNearSemiringMonomorphism_944 → T_IsNearSemiringHomomorphism_916 Source #

d_isRelHomomorphism_1274 ∷ T_IsNearSemiringMonomorphism_944 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_944 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1276 ∷ T_IsNearSemiringMonomorphism_944 → T_IsRelMonomorphism_64 Source #

d_cong_1278 ∷ T_IsNearSemiringMonomorphism_944 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSemiringHomomorphism_1282 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSemiringHomomorphism_1282 Source #

d_isNearSemiringHomomorphism_1290 ∷ T_IsSemiringHomomorphism_1282 → T_IsNearSemiringHomomorphism_916 Source #

d_1'35''45'homo_1292 ∷ T_IsSemiringHomomorphism_1282 → AgdaAny Source #

d_'42''45'homo_1296 ∷ T_IsSemiringHomomorphism_1282 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringHomomorphism_1282 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_1298 ∷ T_IsSemiringHomomorphism_1282 → T_IsMagmaHomomorphism_176 Source #

d_homo_1300 ∷ T_IsSemiringHomomorphism_1282 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1302 ∷ T_IsSemiringHomomorphism_1282 → T_IsMagmaHomomorphism_176 Source #

d_'43''45'isMonoidHomomorphism_1304 ∷ T_IsSemiringHomomorphism_1282 → T_IsMonoidHomomorphism_350 Source #

d_ε'45'homo_1306 ∷ T_IsSemiringHomomorphism_1282 → AgdaAny Source #

d_isRelHomomorphism_1308 ∷ T_IsSemiringHomomorphism_1282 → T_IsRelHomomorphism_42 Source #

d_cong_1310 ∷ T_IsSemiringHomomorphism_1282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMonoidHomomorphism_1312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringHomomorphism_1282 → T_IsMonoidHomomorphism_350 Source #

du_'42''45'isMonoidHomomorphism_1312 ∷ T_IsSemiringHomomorphism_1282 → T_IsMonoidHomomorphism_350 Source #

d_IsSemiringMonomorphism_1316 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSemiringMonomorphism_1316 Source #

d_isSemiringHomomorphism_1324 ∷ T_IsSemiringMonomorphism_1316 → T_IsSemiringHomomorphism_1282 Source #

d_injective_1326 ∷ T_IsSemiringMonomorphism_1316 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1330 ∷ T_IsSemiringMonomorphism_1316 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1332 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1316 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_1332 ∷ T_IsSemiringMonomorphism_1316 → T_IsMagmaHomomorphism_176 Source #

d_'42''45'isMonoidHomomorphism_1334 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1316 → T_IsMonoidHomomorphism_350 Source #

du_'42''45'isMonoidHomomorphism_1334 ∷ T_IsSemiringMonomorphism_1316 → T_IsMonoidHomomorphism_350 Source #

d_homo_1336 ∷ T_IsSemiringMonomorphism_1316 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1338 ∷ T_IsSemiringMonomorphism_1316 → T_IsMagmaHomomorphism_176 Source #

d_'43''45'isMonoidHomomorphism_1340 ∷ T_IsSemiringMonomorphism_1316 → T_IsMonoidHomomorphism_350 Source #

d_ε'45'homo_1342 ∷ T_IsSemiringMonomorphism_1316 → AgdaAny Source #

d_1'35''45'homo_1344 ∷ T_IsSemiringMonomorphism_1316 → AgdaAny Source #

d_isNearSemiringHomomorphism_1346 ∷ T_IsSemiringMonomorphism_1316 → T_IsNearSemiringHomomorphism_916 Source #

d_isRelHomomorphism_1348 ∷ T_IsSemiringMonomorphism_1316 → T_IsRelHomomorphism_42 Source #

d_cong_1350 ∷ T_IsSemiringMonomorphism_1316 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringMonomorphism_1352 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1316 → T_IsNearSemiringMonomorphism_944 Source #

du_isNearSemiringMonomorphism_1352 ∷ T_IsSemiringMonomorphism_1316 → T_IsNearSemiringMonomorphism_944 Source #

d_'42''45'isMagmaMonomorphism_1356 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1316 → T_IsMagmaMonomorphism_194 Source #

du_'42''45'isMagmaMonomorphism_1356 ∷ T_IsSemiringMonomorphism_1316 → T_IsMagmaMonomorphism_194 Source #

d_'43''45'isMonoidMonomorphism_1358 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1316 → T_IsMonoidMonomorphism_372 Source #

du_'43''45'isMonoidMonomorphism_1358 ∷ T_IsSemiringMonomorphism_1316 → T_IsMonoidMonomorphism_372 Source #

d_'42''45'isMonoidMonomorphism_1360 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1316 → T_IsMonoidMonomorphism_372 Source #

du_'42''45'isMonoidMonomorphism_1360 ∷ T_IsSemiringMonomorphism_1316 → T_IsMonoidMonomorphism_372 Source #

d_IsSemiringIsomorphism_1364 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSemiringIsomorphism_1364 Source #

d_isSemiringMonomorphism_1372 ∷ T_IsSemiringIsomorphism_1364 → T_IsSemiringMonomorphism_1316 Source #

d_surjective_1374 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny → T_Σ_14 Source #

d_'42''45'homo_1378 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1380 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_1380 ∷ T_IsSemiringIsomorphism_1364 → T_IsMagmaHomomorphism_176 Source #

d_'42''45'isMagmaMonomorphism_1382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMagmaMonomorphism_194 Source #

du_'42''45'isMagmaMonomorphism_1382 ∷ T_IsSemiringIsomorphism_1364 → T_IsMagmaMonomorphism_194 Source #

d_'42''45'isMonoidHomomorphism_1384 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidHomomorphism_350 Source #

du_'42''45'isMonoidHomomorphism_1384 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidHomomorphism_350 Source #

d_'42''45'isMonoidMonomorphism_1386 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidMonomorphism_372 Source #

du_'42''45'isMonoidMonomorphism_1386 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidMonomorphism_372 Source #

d_homo_1388 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1390 ∷ T_IsSemiringIsomorphism_1364 → T_IsMagmaHomomorphism_176 Source #

d_'43''45'isMonoidHomomorphism_1392 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidHomomorphism_350 Source #

d_'43''45'isMonoidMonomorphism_1394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidMonomorphism_372 Source #

du_'43''45'isMonoidMonomorphism_1394 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidMonomorphism_372 Source #

d_ε'45'homo_1396 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny Source #

d_1'35''45'homo_1398 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny Source #

d_injective_1400 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1402 ∷ T_IsSemiringIsomorphism_1364 → T_IsNearSemiringHomomorphism_916 Source #

d_isNearSemiringMonomorphism_1404 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsNearSemiringMonomorphism_944 Source #

du_isNearSemiringMonomorphism_1404 ∷ T_IsSemiringIsomorphism_1364 → T_IsNearSemiringMonomorphism_944 Source #

d_isRelHomomorphism_1406 ∷ T_IsSemiringIsomorphism_1364 → T_IsRelHomomorphism_42 Source #

d_isSemiringHomomorphism_1408 ∷ T_IsSemiringIsomorphism_1364 → T_IsSemiringHomomorphism_1282 Source #

d_cong_1410 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringIsomorphism_1412 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsNearSemiringIsomorphism_986 Source #

du_isNearSemiringIsomorphism_1412 ∷ T_IsSemiringIsomorphism_1364 → T_IsNearSemiringIsomorphism_986 Source #

d_'42''45'isMagmaIsomorphism_1416 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMagmaIsomorphism_218 Source #

du_'42''45'isMagmaIsomorphism_1416 ∷ T_IsSemiringIsomorphism_1364 → T_IsMagmaIsomorphism_218 Source #

d_'43''45'isMonoidIsomorphism_1418 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidIsomorphism_404 Source #

du_'43''45'isMonoidIsomorphism_1418 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidIsomorphism_404 Source #

d_'42''45'isMonoidIsomorphism_1420 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_174 → T_RawSemiring_174 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidIsomorphism_404 Source #

du_'42''45'isMonoidIsomorphism_1420 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidIsomorphism_404 Source #

d__'42'__1438 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → AgdaAny → AgdaAny → AgdaAny Source #

du__'42'__1438 ∷ T_RawRingWithoutOne_222 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → AgdaAny → AgdaAny → () Source #

d_Carrier_1458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → () Source #

d_IsGroupHomomorphism_1486 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroupIsomorphism_1488 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroupMonomorphism_1490 ∷ p → p → p → p → p → p → p → () Source #

d_homo_1494 ∷ T_IsGroupHomomorphism_622 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1496 ∷ T_IsGroupHomomorphism_622 → T_IsMagmaHomomorphism_176 Source #

d_isMonoidHomomorphism_1498 ∷ T_IsGroupHomomorphism_622 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_1500 ∷ T_IsGroupHomomorphism_622 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_1502 ∷ T_IsGroupHomomorphism_622 → AgdaAny Source #

d_'8315''185''45'homo_1504 ∷ T_IsGroupHomomorphism_622 → AgdaAny → AgdaAny Source #

d_cong_1506 ∷ T_IsGroupHomomorphism_622 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1510 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroupHomomorphism_1512 ∷ T_IsGroupIsomorphism_686 → T_IsGroupHomomorphism_622 Source #

d_isGroupMonomorphism_1514 ∷ T_IsGroupIsomorphism_686 → T_IsGroupMonomorphism_648 Source #

d_isMagmaHomomorphism_1516 ∷ T_IsGroupIsomorphism_686 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaIsomorphism_1518 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_1518 ∷ T_IsGroupIsomorphism_686 → T_IsMagmaIsomorphism_218 Source #

d_isMagmaMonomorphism_1520 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1520 ∷ T_IsGroupIsomorphism_686 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_1522 ∷ T_IsGroupIsomorphism_686 → T_IsMonoidHomomorphism_350 Source #

d_isMonoidIsomorphism_1524 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMonoidIsomorphism_404 Source #

du_isMonoidIsomorphism_1524 ∷ (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMonoidIsomorphism_404 Source #

d_isMonoidMonomorphism_1526 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMonoidMonomorphism_372 Source #

du_isMonoidMonomorphism_1526 ∷ T_IsGroupIsomorphism_686 → T_IsMonoidMonomorphism_372 Source #

d_isRelHomomorphism_1528 ∷ T_IsGroupIsomorphism_686 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1530 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1530 ∷ T_IsGroupIsomorphism_686 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_1532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1532 ∷ T_IsGroupIsomorphism_686 → T_IsRelMonomorphism_64 Source #

d_surjective_1534 ∷ T_IsGroupIsomorphism_686 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_1536 ∷ T_IsGroupIsomorphism_686 → AgdaAny Source #

d_'8315''185''45'homo_1538 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny Source #

d_homo_1540 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_1542 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1546 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroupHomomorphism_1548 ∷ T_IsGroupMonomorphism_648 → T_IsGroupHomomorphism_622 Source #

d_isMagmaHomomorphism_1550 ∷ T_IsGroupMonomorphism_648 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_1552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1552 ∷ T_IsGroupMonomorphism_648 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_1554 ∷ T_IsGroupMonomorphism_648 → T_IsMonoidHomomorphism_350 Source #

d_isMonoidMonomorphism_1556 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsMonoidMonomorphism_372 Source #

du_isMonoidMonomorphism_1556 ∷ (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsMonoidMonomorphism_372 Source #

d_isRelHomomorphism_1558 ∷ T_IsGroupMonomorphism_648 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1560 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1560 ∷ T_IsGroupMonomorphism_648 → T_IsRelMonomorphism_64 Source #

d_ε'45'homo_1562 ∷ T_IsGroupMonomorphism_648 → AgdaAny Source #

d_'8315''185''45'homo_1564 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny Source #

d_homo_1566 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_1568 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMagmaHomomorphism_1572 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaIsomorphism_1574 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaMonomorphism_1576 ∷ p → p → p → p → p → p → p → () Source #

d_homo_1580 ∷ T_IsMagmaHomomorphism_176 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_1582 ∷ T_IsMagmaHomomorphism_176 → T_IsRelHomomorphism_42 Source #

d_cong_1584 ∷ T_IsMagmaHomomorphism_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1588 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1590 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1592 ∷ T_IsMagmaIsomorphism_218 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_1594 ∷ T_IsMagmaIsomorphism_218 → T_IsMagmaMonomorphism_194 Source #

d_isRelHomomorphism_1596 ∷ T_IsMagmaIsomorphism_218 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1598 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1598 ∷ (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_1600 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_218 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1600 ∷ T_IsMagmaIsomorphism_218 → T_IsRelMonomorphism_64 Source #

d_surjective_1602 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → T_Σ_14 Source #

d_cong_1604 ∷ T_IsMagmaIsomorphism_218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1608 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1610 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1612 ∷ T_IsMagmaMonomorphism_194 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_1614 ∷ T_IsMagmaMonomorphism_194 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1616 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_194 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1616 ∷ (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_194 → T_IsRelMonomorphism_64 Source #

d_cong_1618 ∷ T_IsMagmaMonomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Homomorphic'8322'_1626 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsRingWithoutOneHomomorphism_1632 ∷ p → p → p → p → p → p → p → () Source #

data T_IsRingWithoutOneHomomorphism_1632 Source #

d_'43''45'isGroupHomomorphism_1640 ∷ T_IsRingWithoutOneHomomorphism_1632 → T_IsGroupHomomorphism_622 Source #

d_'42''45'homo_1642 ∷ T_IsRingWithoutOneHomomorphism_1632 → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1646 ∷ T_IsRingWithoutOneHomomorphism_1632 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1648 ∷ T_IsRingWithoutOneHomomorphism_1632 → T_IsMagmaHomomorphism_176 Source #

d_ε'45'homo_1650 ∷ T_IsRingWithoutOneHomomorphism_1632 → AgdaAny Source #

d_isMonoidHomomorphism_1652 ∷ T_IsRingWithoutOneHomomorphism_1632 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_1654 ∷ T_IsRingWithoutOneHomomorphism_1632 → T_IsRelHomomorphism_42 Source #

d_'8315''185''45'homo_1656 ∷ T_IsRingWithoutOneHomomorphism_1632 → AgdaAny → AgdaAny Source #

d_cong_1658 ∷ T_IsRingWithoutOneHomomorphism_1632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1660 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneHomomorphism_1632 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_1660 ∷ T_IsRingWithoutOneHomomorphism_1632 → T_IsMagmaHomomorphism_176 Source #

d_IsRingWithoutOneMonomorphism_1664 ∷ p → p → p → p → p → p → p → () Source #

data T_IsRingWithoutOneMonomorphism_1664 Source #

d_isRingWithoutOneHomomorphism_1672 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsRingWithoutOneHomomorphism_1632 Source #

d_injective_1674 ∷ T_IsRingWithoutOneMonomorphism_1664 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1678 ∷ T_IsRingWithoutOneMonomorphism_1664 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1664 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_1680 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsMagmaHomomorphism_176 Source #

d_homo_1682 ∷ T_IsRingWithoutOneMonomorphism_1664 → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isGroupHomomorphism_1684 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsGroupHomomorphism_622 Source #

d_isMagmaHomomorphism_1686 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsMagmaHomomorphism_176 Source #

d_ε'45'homo_1688 ∷ T_IsRingWithoutOneMonomorphism_1664 → AgdaAny Source #

d_isMonoidHomomorphism_1690 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_1692 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsRelHomomorphism_42 Source #

d_'8315''185''45'homo_1694 ∷ T_IsRingWithoutOneMonomorphism_1664 → AgdaAny → AgdaAny Source #

d_cong_1696 ∷ T_IsRingWithoutOneMonomorphism_1664 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isGroupMonomorphism_1698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1664 → T_IsGroupMonomorphism_648 Source #

du_'43''45'isGroupMonomorphism_1698 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsGroupMonomorphism_648 Source #

d_isMagmaMonomorphism_1702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1664 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1702 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidMonomorphism_1704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1664 → T_IsMonoidMonomorphism_372 Source #

du_isMonoidMonomorphism_1704 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsMonoidMonomorphism_372 Source #

d_isRelMonomorphism_1706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1664 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1706 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsRelMonomorphism_64 Source #

d_'42''45'isMagmaMonomorphism_1708 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1664 → T_IsMagmaMonomorphism_194 Source #

du_'42''45'isMagmaMonomorphism_1708 ∷ T_IsRingWithoutOneMonomorphism_1664 → T_IsMagmaMonomorphism_194 Source #

d_IsRingWithoutOneIsoMorphism_1712 ∷ p → p → p → p → p → p → p → () Source #

data T_IsRingWithoutOneIsoMorphism_1712 Source #

d_isRingWithoutOneMonomorphism_1720 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsRingWithoutOneMonomorphism_1664 Source #

d_surjective_1722 ∷ T_IsRingWithoutOneIsoMorphism_1712 → AgdaAny → T_Σ_14 Source #

d_'42''45'homo_1726 ∷ T_IsRingWithoutOneIsoMorphism_1712 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_1728 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaHomomorphism_176 Source #

d_'42''45'isMagmaMonomorphism_1730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaMonomorphism_194 Source #

du_'42''45'isMagmaMonomorphism_1730 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaMonomorphism_194 Source #

d_homo_1732 ∷ T_IsRingWithoutOneIsoMorphism_1712 → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isGroupHomomorphism_1734 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsGroupHomomorphism_622 Source #

d_'43''45'isGroupMonomorphism_1736 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsGroupMonomorphism_648 Source #

du_'43''45'isGroupMonomorphism_1736 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsGroupMonomorphism_648 Source #

d_isMagmaHomomorphism_1738 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_1740 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1740 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidMonomorphism_1742 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsMonoidMonomorphism_372 Source #

du_isMonoidMonomorphism_1742 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsMonoidMonomorphism_372 Source #

d_ε'45'homo_1744 ∷ T_IsRingWithoutOneIsoMorphism_1712 → AgdaAny Source #

d_injective_1746 ∷ T_IsRingWithoutOneIsoMorphism_1712 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMonoidHomomorphism_1748 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_1750 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1752 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1752 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsRelMonomorphism_64 Source #

d_isRingWithoutOneHomomorphism_1754 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsRingWithoutOneHomomorphism_1632 Source #

d_'8315''185''45'homo_1756 ∷ T_IsRingWithoutOneIsoMorphism_1712 → AgdaAny → AgdaAny Source #

d_cong_1758 ∷ T_IsRingWithoutOneIsoMorphism_1712 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isGroupIsomorphism_1760 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsGroupIsomorphism_686 Source #

du_'43''45'isGroupIsomorphism_1760 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsGroupIsomorphism_686 Source #

d_isMagmaIsomorphism_1764 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_1764 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaIsomorphism_218 Source #

d_isMonoidIsomorphism_1766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsMonoidIsomorphism_404 Source #

du_isMonoidIsomorphism_1766 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsMonoidIsomorphism_404 Source #

d_isRelIsomorphism_1768 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1768 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsRelIsomorphism_94 Source #

d_'42''45'isMagmaIsomorphism_1770 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_222 → T_RawRingWithoutOne_222 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaIsomorphism_218 Source #

du_'42''45'isMagmaIsomorphism_1770 ∷ T_IsRingWithoutOneIsoMorphism_1712 → T_IsMagmaIsomorphism_218 Source #

d__'8776'__1792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → AgdaAny → AgdaAny → () Source #

d_'45'__1806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → AgdaAny → AgdaAny Source #

du_'45'__1806 ∷ T_RawRing_268 → AgdaAny → AgdaAny Source #

d_Carrier_1812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → () Source #

d_IsGroupHomomorphism_1852 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroupIsomorphism_1854 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroupMonomorphism_1856 ∷ p → p → p → p → p → p → p → () Source #

d_homo_1860 ∷ T_IsGroupHomomorphism_622 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1862 ∷ T_IsGroupHomomorphism_622 → T_IsMagmaHomomorphism_176 Source #

d_isMonoidHomomorphism_1864 ∷ T_IsGroupHomomorphism_622 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_1866 ∷ T_IsGroupHomomorphism_622 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_1868 ∷ T_IsGroupHomomorphism_622 → AgdaAny Source #

d_'8315''185''45'homo_1870 ∷ T_IsGroupHomomorphism_622 → AgdaAny → AgdaAny Source #

d_cong_1872 ∷ T_IsGroupHomomorphism_622 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1876 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroupHomomorphism_1878 ∷ T_IsGroupIsomorphism_686 → T_IsGroupHomomorphism_622 Source #

d_isGroupMonomorphism_1880 ∷ T_IsGroupIsomorphism_686 → T_IsGroupMonomorphism_648 Source #

d_isMagmaHomomorphism_1882 ∷ T_IsGroupIsomorphism_686 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaIsomorphism_1884 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_1884 ∷ T_IsGroupIsomorphism_686 → T_IsMagmaIsomorphism_218 Source #

d_isMagmaMonomorphism_1886 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1886 ∷ T_IsGroupIsomorphism_686 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_1888 ∷ T_IsGroupIsomorphism_686 → T_IsMonoidHomomorphism_350 Source #

d_isMonoidIsomorphism_1890 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMonoidIsomorphism_404 Source #

du_isMonoidIsomorphism_1890 ∷ (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMonoidIsomorphism_404 Source #

d_isMonoidMonomorphism_1892 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsMonoidMonomorphism_372 Source #

du_isMonoidMonomorphism_1892 ∷ T_IsGroupIsomorphism_686 → T_IsMonoidMonomorphism_372 Source #

d_isRelHomomorphism_1894 ∷ T_IsGroupIsomorphism_686 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1896 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1896 ∷ T_IsGroupIsomorphism_686 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_1898 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_686 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1898 ∷ T_IsGroupIsomorphism_686 → T_IsRelMonomorphism_64 Source #

d_surjective_1900 ∷ T_IsGroupIsomorphism_686 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_1902 ∷ T_IsGroupIsomorphism_686 → AgdaAny Source #

d_'8315''185''45'homo_1904 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny Source #

d_homo_1906 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_1908 ∷ T_IsGroupIsomorphism_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1912 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroupHomomorphism_1914 ∷ T_IsGroupMonomorphism_648 → T_IsGroupHomomorphism_622 Source #

d_isMagmaHomomorphism_1916 ∷ T_IsGroupMonomorphism_648 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_1918 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1918 ∷ T_IsGroupMonomorphism_648 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_1920 ∷ T_IsGroupMonomorphism_648 → T_IsMonoidHomomorphism_350 Source #

d_isMonoidMonomorphism_1922 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsMonoidMonomorphism_372 Source #

du_isMonoidMonomorphism_1922 ∷ (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsMonoidMonomorphism_372 Source #

d_isRelHomomorphism_1924 ∷ T_IsGroupMonomorphism_648 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1926 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_648 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1926 ∷ T_IsGroupMonomorphism_648 → T_IsRelMonomorphism_64 Source #

d_ε'45'homo_1928 ∷ T_IsGroupMonomorphism_648 → AgdaAny Source #

d_'8315''185''45'homo_1930 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny Source #

d_homo_1932 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_1934 ∷ T_IsGroupMonomorphism_648 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoidHomomorphism_1938 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidIsomorphism_1940 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidMonomorphism_1942 ∷ p → p → p → p → p → p → p → () Source #

d_homo_1946 ∷ T_IsMonoidHomomorphism_350 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1948 ∷ T_IsMonoidHomomorphism_350 → T_IsMagmaHomomorphism_176 Source #

d_isRelHomomorphism_1950 ∷ T_IsMonoidHomomorphism_350 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_1952 ∷ T_IsMonoidHomomorphism_350 → AgdaAny Source #

d_cong_1954 ∷ T_IsMonoidHomomorphism_350 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1958 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1960 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1962 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaIsomorphism_1964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaIsomorphism_218 Source #

du_isMagmaIsomorphism_1964 ∷ (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaIsomorphism_218 Source #

d_isMagmaMonomorphism_1966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1966 ∷ T_IsMonoidIsomorphism_404 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_1968 ∷ T_IsMonoidIsomorphism_404 → T_IsMonoidHomomorphism_350 Source #

d_isMonoidMonomorphism_1970 ∷ T_IsMonoidIsomorphism_404 → T_IsMonoidMonomorphism_372 Source #

d_isRelHomomorphism_1972 ∷ T_IsMonoidIsomorphism_404 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1974 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1974 ∷ T_IsMonoidIsomorphism_404 → T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_1976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_404 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1976 ∷ T_IsMonoidIsomorphism_404 → T_IsRelMonomorphism_64 Source #

d_surjective_1978 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_1980 ∷ T_IsMonoidIsomorphism_404 → AgdaAny Source #

d_cong_1982 ∷ T_IsMonoidIsomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1986 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1988 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1990 ∷ T_IsMonoidMonomorphism_372 → T_IsMagmaHomomorphism_176 Source #

d_isMagmaMonomorphism_1992 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsMagmaMonomorphism_194 Source #

du_isMagmaMonomorphism_1992 ∷ (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsMagmaMonomorphism_194 Source #

d_isMonoidHomomorphism_1994 ∷ T_IsMonoidMonomorphism_372 → T_IsMonoidHomomorphism_350 Source #

d_isRelHomomorphism_1996 ∷ T_IsMonoidMonomorphism_372 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1998 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_372 → T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1998 ∷ T_IsMonoidMonomorphism_372 → T_IsRelMonomorphism_64 Source #

d_ε'45'homo_2000 ∷ T_IsMonoidMonomorphism_372 → AgdaAny Source #

d_cong_2002 ∷ T_IsMonoidMonomorphism_372 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Homomorphic'8321'_2008 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_IsSemiringHomomorphism_2016 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringIsomorphism_2018 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringMonomorphism_2020 ∷ p → p → p → p → p → p → p → () Source #

d_'42''45'homo_2024 ∷ T_IsSemiringHomomorphism_1282 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_2026 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringHomomorphism_1282 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_2026 ∷ T_IsSemiringHomomorphism_1282 → T_IsMagmaHomomorphism_176 Source #

d_'42''45'isMonoidHomomorphism_2028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringHomomorphism_1282 → T_IsMonoidHomomorphism_350 Source #

du_'42''45'isMonoidHomomorphism_2028 ∷ (AgdaAny → AgdaAny) → T_IsSemiringHomomorphism_1282 → T_IsMonoidHomomorphism_350 Source #

d_homo_2030 ∷ T_IsSemiringHomomorphism_1282 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_2032 ∷ T_IsSemiringHomomorphism_1282 → T_IsMagmaHomomorphism_176 Source #

d_'43''45'isMonoidHomomorphism_2034 ∷ T_IsSemiringHomomorphism_1282 → T_IsMonoidHomomorphism_350 Source #

d_ε'45'homo_2036 ∷ T_IsSemiringHomomorphism_1282 → AgdaAny Source #

d_1'35''45'homo_2038 ∷ T_IsSemiringHomomorphism_1282 → AgdaAny Source #

d_isNearSemiringHomomorphism_2040 ∷ T_IsSemiringHomomorphism_1282 → T_IsNearSemiringHomomorphism_916 Source #

d_isRelHomomorphism_2042 ∷ T_IsSemiringHomomorphism_1282 → T_IsRelHomomorphism_42 Source #

d_cong_2044 ∷ T_IsSemiringHomomorphism_1282 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_2048 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_2050 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMagmaHomomorphism_176 Source #

du_'42''45'isMagmaHomomorphism_2050 ∷ T_IsSemiringIsomorphism_1364 → T_IsMagmaHomomorphism_176 Source #

d_'42''45'isMagmaIsomorphism_2052 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMagmaIsomorphism_218 Source #

du_'42''45'isMagmaIsomorphism_2052 ∷ T_IsSemiringIsomorphism_1364 → T_IsMagmaIsomorphism_218 Source #

d_'42''45'isMagmaMonomorphism_2054 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMagmaMonomorphism_194 Source #

du_'42''45'isMagmaMonomorphism_2054 ∷ T_IsSemiringIsomorphism_1364 → T_IsMagmaMonomorphism_194 Source #

d_'42''45'isMonoidHomomorphism_2056 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidHomomorphism_350 Source #

du_'42''45'isMonoidHomomorphism_2056 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidHomomorphism_350 Source #

d_'42''45'isMonoidIsomorphism_2058 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidIsomorphism_404 Source #

du_'42''45'isMonoidIsomorphism_2058 ∷ (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidIsomorphism_404 Source #

d_'42''45'isMonoidMonomorphism_2060 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidMonomorphism_372 Source #

du_'42''45'isMonoidMonomorphism_2060 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidMonomorphism_372 Source #

d_homo_2062 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_2064 ∷ T_IsSemiringIsomorphism_1364 → T_IsMagmaHomomorphism_176 Source #

d_'43''45'isMonoidHomomorphism_2066 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidHomomorphism_350 Source #

d_'43''45'isMonoidIsomorphism_2068 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidIsomorphism_404 Source #

du_'43''45'isMonoidIsomorphism_2068 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidIsomorphism_404 Source #

d_'43''45'isMonoidMonomorphism_2070 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsMonoidMonomorphism_372 Source #

du_'43''45'isMonoidMonomorphism_2070 ∷ T_IsSemiringIsomorphism_1364 → T_IsMonoidMonomorphism_372 Source #

d_ε'45'homo_2072 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny Source #

d_1'35''45'homo_2074 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny Source #

d_injective_2076 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_2078 ∷ T_IsSemiringIsomorphism_1364 → T_IsNearSemiringHomomorphism_916 Source #

d_isNearSemiringIsomorphism_2080 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsNearSemiringIsomorphism_986 Source #

du_isNearSemiringIsomorphism_2080 ∷ (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsNearSemiringIsomorphism_986 Source #

d_isNearSemiringMonomorphism_2082 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_268 → T_RawRing_268 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1364 → T_IsNearSemiringMonomorphism_944 Source #

du_isNearSemiringMonomorphism_2082 ∷ T_IsSemiringIsomorphism_1364 → T_IsNearSemiringMonomorphism_944 Source #

d_isRelHomomorphism_2084 ∷ T_IsSemiringIsomorphism_1364 → T_IsRelHomomorphism_42 Source #

d_isSemiringHomomorphism_2086 ∷ T_IsSemiringIsomorphism_1364 → T_IsSemiringHomomorphism_1282 Source #

d_isSemiringMonomorphism_2088 ∷ T_IsSemiringIsomorphism_1364 → T_IsSemiringMonomorphism_1316 Source #

d_surjective_2090 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny → T_Σ_14 Source #

d_cong_2092 ∷ T_IsSemiringIsomorphism_1364 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #