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_34 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → () Source #

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

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

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

du_zero'35'_40 ∷ T_RawSuccessorSet_10 → AgdaAny Source #

d_Homomorphic'8320'_58 ∷ 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'_60 ∷ 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_68 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSuccessorSetHomomorphism_68 Source #

d_isRelHomomorphism_78 ∷ T_IsSuccessorSetHomomorphism_68 → T_IsRelHomomorphism_42 Source #

d_suc'35''45'homo_80 ∷ T_IsSuccessorSetHomomorphism_68 → AgdaAny → AgdaAny Source #

d_zero'35''45'homo_82 ∷ T_IsSuccessorSetHomomorphism_68 → AgdaAny Source #

d_IsSuccessorSetMonomorphism_88 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSuccessorSetMonomorphism_88 Source #

d_isSuccessorSetHomomorphism_96 ∷ T_IsSuccessorSetMonomorphism_88 → T_IsSuccessorSetHomomorphism_68 Source #

d_injective_98 ∷ T_IsSuccessorSetMonomorphism_88 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_102 ∷ T_IsSuccessorSetMonomorphism_88 → T_IsRelHomomorphism_42 Source #

d_suc'35''45'homo_104 ∷ T_IsSuccessorSetMonomorphism_88 → AgdaAny → AgdaAny Source #

d_zero'35''45'homo_106 ∷ T_IsSuccessorSetMonomorphism_88 → AgdaAny Source #

d_isRelMonomorphism_108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → (AgdaAny → AgdaAny) → T_IsSuccessorSetMonomorphism_88 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_108 ∷ T_IsSuccessorSetMonomorphism_88 → T_IsRelMonomorphism_66 Source #

d_IsSuccessorSetIsomorphism_114 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSuccessorSetIsomorphism_114 Source #

d_isSuccessorSetMonomorphism_122 ∷ T_IsSuccessorSetIsomorphism_114 → T_IsSuccessorSetMonomorphism_88 Source #

d_surjective_124 ∷ T_IsSuccessorSetIsomorphism_114 → AgdaAny → T_Σ_14 Source #

d_injective_128 ∷ T_IsSuccessorSetIsomorphism_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_130 ∷ T_IsSuccessorSetIsomorphism_114 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → (AgdaAny → AgdaAny) → T_IsSuccessorSetIsomorphism_114 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_132 ∷ T_IsSuccessorSetIsomorphism_114 → T_IsRelMonomorphism_66 Source #

d_isSuccessorSetHomomorphism_134 ∷ T_IsSuccessorSetIsomorphism_114 → T_IsSuccessorSetHomomorphism_68 Source #

d_suc'35''45'homo_136 ∷ T_IsSuccessorSetIsomorphism_114 → AgdaAny → AgdaAny Source #

d_zero'35''45'homo_138 ∷ T_IsSuccessorSetIsomorphism_114 → AgdaAny Source #

d_isRelIsomorphism_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSuccessorSet_10 → T_RawSuccessorSet_10 → (AgdaAny → AgdaAny) → T_IsSuccessorSetIsomorphism_114 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_140 ∷ T_IsSuccessorSetIsomorphism_114 → T_IsRelIsomorphism_98 Source #

d__'8729'__160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_44 → T_RawMagma_44 → AgdaAny → AgdaAny → AgdaAny Source #

du__'8729'__160 ∷ T_RawMagma_44 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_44 → T_RawMagma_44 → AgdaAny → AgdaAny → () Source #

d_Carrier_166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_44 → T_RawMagma_44 → () Source #

d_Homomorphic'8322'_188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_44 → T_RawMagma_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsMagmaHomomorphism_194 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_202 ∷ T_IsMagmaHomomorphism_194 → T_IsRelHomomorphism_42 Source #

d_homo_204 ∷ T_IsMagmaHomomorphism_194 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_208 ∷ T_IsMagmaHomomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMagmaMonomorphism_214 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMagmaMonomorphism_214 Source #

d_isMagmaHomomorphism_222 ∷ T_IsMagmaMonomorphism_214 → T_IsMagmaHomomorphism_194 Source #

d_injective_224 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_228 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_230 ∷ T_IsMagmaMonomorphism_214 → T_IsRelHomomorphism_42 Source #

d_cong_232 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelMonomorphism_234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_44 → T_RawMagma_44 → (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_214 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_234 ∷ T_IsMagmaMonomorphism_214 → T_IsRelMonomorphism_66 Source #

d_IsMagmaIsomorphism_240 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMagmaIsomorphism_240 Source #

d_isMagmaMonomorphism_248 ∷ T_IsMagmaIsomorphism_240 → T_IsMagmaMonomorphism_214 Source #

d_surjective_250 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → T_Σ_14 Source #

d_homo_254 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_256 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_258 ∷ T_IsMagmaIsomorphism_240 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_260 ∷ T_IsMagmaIsomorphism_240 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_44 → T_RawMagma_44 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_262 ∷ T_IsMagmaIsomorphism_240 → T_IsRelMonomorphism_66 Source #

d_cong_264 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelIsomorphism_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMagma_44 → T_RawMagma_44 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_266 ∷ T_IsMagmaIsomorphism_240 → T_IsRelIsomorphism_98 Source #

d__'8776'__288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → AgdaAny → AgdaAny → () Source #

d_Carrier_292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → () Source #

d_ε_296 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → AgdaAny Source #

du_ε_296 ∷ T_RawMonoid_74 → AgdaAny Source #

d_Homomorphic'8320'_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_IsMagmaHomomorphism_324 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaIsomorphism_328 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaMonomorphism_332 ∷ p → p → p → p → p → p → p → () Source #

d_homo_338 ∷ T_IsMagmaHomomorphism_194 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_340 ∷ T_IsMagmaHomomorphism_194 → T_IsRelHomomorphism_42 Source #

d_cong_342 ∷ T_IsMagmaHomomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_346 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_348 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_350 ∷ T_IsMagmaIsomorphism_240 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_352 ∷ T_IsMagmaIsomorphism_240 → T_IsMagmaMonomorphism_214 Source #

d_isRelHomomorphism_354 ∷ T_IsMagmaIsomorphism_240 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_356 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_356 ∷ (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_358 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_358 ∷ T_IsMagmaIsomorphism_240 → T_IsRelMonomorphism_66 Source #

d_surjective_360 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → T_Σ_14 Source #

d_cong_362 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_366 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_368 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_370 ∷ T_IsMagmaMonomorphism_214 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_372 ∷ T_IsMagmaMonomorphism_214 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_374 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_214 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_374 ∷ (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_214 → T_IsRelMonomorphism_66 Source #

d_cong_376 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoidHomomorphism_380 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMonoidHomomorphism_380 Source #

d_isMagmaHomomorphism_388 ∷ T_IsMonoidHomomorphism_380 → T_IsMagmaHomomorphism_194 Source #

d_ε'45'homo_390 ∷ T_IsMonoidHomomorphism_380 → AgdaAny Source #

d_homo_394 ∷ T_IsMonoidHomomorphism_380 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_396 ∷ T_IsMonoidHomomorphism_380 → T_IsRelHomomorphism_42 Source #

d_cong_398 ∷ T_IsMonoidHomomorphism_380 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoidMonomorphism_404 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMonoidMonomorphism_404 Source #

d_isMonoidHomomorphism_412 ∷ T_IsMonoidMonomorphism_404 → T_IsMonoidHomomorphism_380 Source #

d_injective_414 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_418 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_420 ∷ T_IsMonoidMonomorphism_404 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_422 ∷ T_IsMonoidMonomorphism_404 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_424 ∷ T_IsMonoidMonomorphism_404 → AgdaAny Source #

d_cong_426 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaMonomorphism_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_428 ∷ T_IsMonoidMonomorphism_404 → T_IsMagmaMonomorphism_214 Source #

d_isRelMonomorphism_432 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_432 ∷ T_IsMonoidMonomorphism_404 → T_IsRelMonomorphism_66 Source #

d_IsMonoidIsomorphism_438 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMonoidIsomorphism_438 Source #

d_isMonoidMonomorphism_446 ∷ T_IsMonoidIsomorphism_438 → T_IsMonoidMonomorphism_404 Source #

d_surjective_448 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → T_Σ_14 Source #

d_homo_452 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_454 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_456 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_458 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_460 ∷ T_IsMonoidIsomorphism_438 → T_IsMonoidHomomorphism_380 Source #

d_isRelHomomorphism_462 ∷ T_IsMonoidIsomorphism_438 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_464 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_464 ∷ T_IsMonoidIsomorphism_438 → T_IsRelMonomorphism_66 Source #

d_ε'45'homo_466 ∷ T_IsMonoidIsomorphism_438 → AgdaAny Source #

d_cong_468 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaIsomorphism_470 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_470 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaIsomorphism_240 Source #

d_isRelIsomorphism_474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawMonoid_74 → T_RawMonoid_74 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_474 ∷ T_IsMonoidIsomorphism_438 → T_IsRelIsomorphism_98 Source #

d__'8315''185'_494 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → AgdaAny → AgdaAny Source #

du__'8315''185'_494 ∷ T_RawGroup_108 → AgdaAny → AgdaAny Source #

d__'8776'__498 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → AgdaAny → AgdaAny → () Source #

d_Carrier_502 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → () Source #

d_Homomorphic'8321'_532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_IsMagmaHomomorphism_540 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaIsomorphism_544 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaMonomorphism_548 ∷ p → p → p → p → p → p → p → () Source #

d_homo_554 ∷ T_IsMagmaHomomorphism_194 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_556 ∷ T_IsMagmaHomomorphism_194 → T_IsRelHomomorphism_42 Source #

d_cong_558 ∷ T_IsMagmaHomomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_562 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_564 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_566 ∷ T_IsMagmaIsomorphism_240 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_568 ∷ T_IsMagmaIsomorphism_240 → T_IsMagmaMonomorphism_214 Source #

d_isRelHomomorphism_570 ∷ T_IsMagmaIsomorphism_240 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_572 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_572 ∷ (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_574 ∷ T_IsMagmaIsomorphism_240 → T_IsRelMonomorphism_66 Source #

d_surjective_576 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → T_Σ_14 Source #

d_cong_578 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_582 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_584 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_586 ∷ T_IsMagmaMonomorphism_214 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_588 ∷ T_IsMagmaMonomorphism_214 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_590 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_214 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_590 ∷ (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_214 → T_IsRelMonomorphism_66 Source #

d_cong_592 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoidHomomorphism_596 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidIsomorphism_600 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidMonomorphism_604 ∷ p → p → p → p → p → p → p → () Source #

d_homo_610 ∷ T_IsMonoidHomomorphism_380 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_612 ∷ T_IsMonoidHomomorphism_380 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_614 ∷ T_IsMonoidHomomorphism_380 → T_IsRelHomomorphism_42 Source #

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

d_cong_618 ∷ T_IsMonoidHomomorphism_380 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_622 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_624 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_626 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaIsomorphism_628 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_628 ∷ (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaIsomorphism_240 Source #

d_isMagmaMonomorphism_630 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_630 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_632 ∷ T_IsMonoidIsomorphism_438 → T_IsMonoidHomomorphism_380 Source #

d_isMonoidMonomorphism_634 ∷ T_IsMonoidIsomorphism_438 → T_IsMonoidMonomorphism_404 Source #

d_isRelHomomorphism_636 ∷ T_IsMonoidIsomorphism_438 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_638 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_638 ∷ T_IsMonoidIsomorphism_438 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_640 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_640 ∷ T_IsMonoidIsomorphism_438 → T_IsRelMonomorphism_66 Source #

d_surjective_642 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_644 ∷ T_IsMonoidIsomorphism_438 → AgdaAny Source #

d_cong_646 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_650 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_652 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_654 ∷ T_IsMonoidMonomorphism_404 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_656 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_656 ∷ (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_658 ∷ T_IsMonoidMonomorphism_404 → T_IsMonoidHomomorphism_380 Source #

d_isRelHomomorphism_660 ∷ T_IsMonoidMonomorphism_404 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_662 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_662 ∷ T_IsMonoidMonomorphism_404 → T_IsRelMonomorphism_66 Source #

d_ε'45'homo_664 ∷ T_IsMonoidMonomorphism_404 → AgdaAny Source #

d_cong_666 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsGroupHomomorphism_670 ∷ p → p → p → p → p → p → p → () Source #

data T_IsGroupHomomorphism_670 Source #

d_isMonoidHomomorphism_678 ∷ T_IsGroupHomomorphism_670 → T_IsMonoidHomomorphism_380 Source #

d_'8315''185''45'homo_680 ∷ T_IsGroupHomomorphism_670 → AgdaAny → AgdaAny Source #

d_homo_684 ∷ T_IsGroupHomomorphism_670 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_686 ∷ T_IsGroupHomomorphism_670 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_688 ∷ T_IsGroupHomomorphism_670 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_690 ∷ T_IsGroupHomomorphism_670 → AgdaAny Source #

d_cong_692 ∷ T_IsGroupHomomorphism_670 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsGroupMonomorphism_698 ∷ p → p → p → p → p → p → p → () Source #

data T_IsGroupMonomorphism_698 Source #

d_isGroupHomomorphism_706 ∷ T_IsGroupMonomorphism_698 → T_IsGroupHomomorphism_670 Source #

d_injective_708 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_712 ∷ T_IsGroupMonomorphism_698 → T_IsMagmaHomomorphism_194 Source #

d_isMonoidHomomorphism_714 ∷ T_IsGroupMonomorphism_698 → T_IsMonoidHomomorphism_380 Source #

d_isRelHomomorphism_716 ∷ T_IsGroupMonomorphism_698 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_718 ∷ T_IsGroupMonomorphism_698 → AgdaAny Source #

d_'8315''185''45'homo_720 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny Source #

d_homo_722 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_724 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMonoidMonomorphism_726 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsMonoidMonomorphism_404 Source #

du_isMonoidMonomorphism_726 ∷ T_IsGroupMonomorphism_698 → T_IsMonoidMonomorphism_404 Source #

d_isMagmaMonomorphism_730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_730 ∷ T_IsGroupMonomorphism_698 → T_IsMagmaMonomorphism_214 Source #

d_isRelMonomorphism_732 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_732 ∷ T_IsGroupMonomorphism_698 → T_IsRelMonomorphism_66 Source #

d_IsGroupIsomorphism_738 ∷ p → p → p → p → p → p → p → () Source #

data T_IsGroupIsomorphism_738 Source #

d_isGroupMonomorphism_746 ∷ T_IsGroupIsomorphism_738 → T_IsGroupMonomorphism_698 Source #

d_surjective_748 ∷ T_IsGroupIsomorphism_738 → AgdaAny → T_Σ_14 Source #

d_injective_752 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroupHomomorphism_754 ∷ T_IsGroupIsomorphism_738 → T_IsGroupHomomorphism_670 Source #

d_isMagmaHomomorphism_756 ∷ T_IsGroupIsomorphism_738 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_758 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_758 ∷ T_IsGroupIsomorphism_738 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_760 ∷ T_IsGroupIsomorphism_738 → T_IsMonoidHomomorphism_380 Source #

d_isMonoidMonomorphism_762 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMonoidMonomorphism_404 Source #

du_isMonoidMonomorphism_762 ∷ T_IsGroupIsomorphism_738 → T_IsMonoidMonomorphism_404 Source #

d_isRelHomomorphism_764 ∷ T_IsGroupIsomorphism_738 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_766 ∷ T_IsGroupIsomorphism_738 → T_IsRelMonomorphism_66 Source #

d_ε'45'homo_768 ∷ T_IsGroupIsomorphism_738 → AgdaAny Source #

d_'8315''185''45'homo_770 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny Source #

d_homo_772 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_774 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMonoidIsomorphism_776 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMonoidIsomorphism_438 Source #

du_isMonoidIsomorphism_776 ∷ T_IsGroupIsomorphism_738 → T_IsMonoidIsomorphism_438 Source #

d_isMagmaIsomorphism_780 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_780 ∷ T_IsGroupIsomorphism_738 → T_IsMagmaIsomorphism_240 Source #

d_isRelIsomorphism_782 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawGroup_108 → T_RawGroup_108 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_782 ∷ T_IsGroupIsomorphism_738 → T_IsRelIsomorphism_98 Source #

d__'42'__802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → AgdaAny → AgdaAny → AgdaAny Source #

du__'42'__802 ∷ T_RawNearSemiring_148 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → AgdaAny → AgdaAny → () Source #

d_Carrier_818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → () Source #

d_IsMonoidHomomorphism_842 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidIsomorphism_846 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidMonomorphism_850 ∷ p → p → p → p → p → p → p → () Source #

d_homo_856 ∷ T_IsMonoidHomomorphism_380 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_858 ∷ T_IsMonoidHomomorphism_380 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_860 ∷ T_IsMonoidHomomorphism_380 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_862 ∷ T_IsMonoidHomomorphism_380 → AgdaAny Source #

d_cong_864 ∷ T_IsMonoidHomomorphism_380 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_868 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_870 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_872 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaIsomorphism_874 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_874 ∷ (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaIsomorphism_240 Source #

d_isMagmaMonomorphism_876 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_876 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_878 ∷ T_IsMonoidIsomorphism_438 → T_IsMonoidHomomorphism_380 Source #

d_isMonoidMonomorphism_880 ∷ T_IsMonoidIsomorphism_438 → T_IsMonoidMonomorphism_404 Source #

d_isRelHomomorphism_882 ∷ T_IsMonoidIsomorphism_438 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_884 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_884 ∷ T_IsMonoidIsomorphism_438 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_886 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_886 ∷ T_IsMonoidIsomorphism_438 → T_IsRelMonomorphism_66 Source #

d_surjective_888 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_890 ∷ T_IsMonoidIsomorphism_438 → AgdaAny Source #

d_cong_892 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_896 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_898 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_900 ∷ T_IsMonoidMonomorphism_404 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_902 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_902 ∷ (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_904 ∷ T_IsMonoidMonomorphism_404 → T_IsMonoidHomomorphism_380 Source #

d_isRelHomomorphism_906 ∷ T_IsMonoidMonomorphism_404 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_908 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_908 ∷ T_IsMonoidMonomorphism_404 → T_IsRelMonomorphism_66 Source #

d_ε'45'homo_910 ∷ T_IsMonoidMonomorphism_404 → AgdaAny Source #

d_cong_912 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMagmaHomomorphism_916 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaIsomorphism_920 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaMonomorphism_924 ∷ p → p → p → p → p → p → p → () Source #

d_homo_930 ∷ T_IsMagmaHomomorphism_194 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_932 ∷ T_IsMagmaHomomorphism_194 → T_IsRelHomomorphism_42 Source #

d_cong_934 ∷ T_IsMagmaHomomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_938 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_940 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_942 ∷ T_IsMagmaIsomorphism_240 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_944 ∷ T_IsMagmaIsomorphism_240 → T_IsMagmaMonomorphism_214 Source #

d_isRelHomomorphism_946 ∷ T_IsMagmaIsomorphism_240 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_948 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_948 ∷ (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_950 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_950 ∷ T_IsMagmaIsomorphism_240 → T_IsRelMonomorphism_66 Source #

d_surjective_952 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → T_Σ_14 Source #

d_cong_954 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_958 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_960 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_962 ∷ T_IsMagmaMonomorphism_214 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_964 ∷ T_IsMagmaMonomorphism_214 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_214 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_966 ∷ (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_214 → T_IsRelMonomorphism_66 Source #

d_cong_968 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Homomorphic'8322'_976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsNearSemiringHomomorphism_982 ∷ p → p → p → p → p → p → p → () Source #

data T_IsNearSemiringHomomorphism_982 Source #

d_'43''45'isMonoidHomomorphism_990 ∷ T_IsNearSemiringHomomorphism_982 → T_IsMonoidHomomorphism_380 Source #

d_'42''45'homo_992 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_996 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_998 ∷ T_IsNearSemiringHomomorphism_982 → T_IsMagmaHomomorphism_194 Source #

d_ε'45'homo_1000 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny Source #

d_isRelHomomorphism_1002 ∷ T_IsNearSemiringHomomorphism_982 → T_IsRelHomomorphism_42 Source #

d_cong_1004 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1006 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringHomomorphism_982 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1006 ∷ T_IsNearSemiringHomomorphism_982 → T_IsMagmaHomomorphism_194 Source #

d_IsNearSemiringMonomorphism_1012 ∷ p → p → p → p → p → p → p → () Source #

data T_IsNearSemiringMonomorphism_1012 Source #

d_isNearSemiringHomomorphism_1020 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsNearSemiringHomomorphism_982 Source #

d_injective_1022 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1026 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1028 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMagmaHomomorphism_194 Source #

d_homo_1030 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1032 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMagmaHomomorphism_194 Source #

d_'43''45'isMonoidHomomorphism_1034 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMonoidHomomorphism_380 Source #

d_ε'45'homo_1036 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny Source #

d_isRelHomomorphism_1038 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsRelHomomorphism_42 Source #

d_cong_1040 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isMonoidMonomorphism_1042 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMonoidMonomorphism_404 Source #

du_'43''45'isMonoidMonomorphism_1042 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMonoidMonomorphism_404 Source #

d_isMagmaMonomorphism_1046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1046 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

d_isRelMonomorphism_1048 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1048 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsRelMonomorphism_66 Source #

d_'42''45'isMagmaMonomorphism_1050 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

du_'42''45'isMagmaMonomorphism_1050 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

d_IsNearSemiringIsomorphism_1056 ∷ p → p → p → p → p → p → p → () Source #

data T_IsNearSemiringIsomorphism_1056 Source #

d_isNearSemiringMonomorphism_1064 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsNearSemiringMonomorphism_1012 Source #

d_surjective_1066 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → T_Σ_14 Source #

d_'42''45'homo_1070 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1072 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1072 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaHomomorphism_194 Source #

d_'42''45'isMagmaMonomorphism_1074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

du_'42''45'isMagmaMonomorphism_1074 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

d_homo_1076 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1078 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_1080 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1080 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

d_'43''45'isMonoidHomomorphism_1082 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMonoidHomomorphism_380 Source #

d_'43''45'isMonoidMonomorphism_1084 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMonoidMonomorphism_404 Source #

du_'43''45'isMonoidMonomorphism_1084 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMonoidMonomorphism_404 Source #

d_ε'45'homo_1086 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny Source #

d_injective_1088 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1090 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsNearSemiringHomomorphism_982 Source #

d_isRelHomomorphism_1092 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1094 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1094 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsRelMonomorphism_66 Source #

d_cong_1096 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isMonoidIsomorphism_1098 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMonoidIsomorphism_438 Source #

du_'43''45'isMonoidIsomorphism_1098 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMonoidIsomorphism_438 Source #

d_isMagmaIsomorphism_1102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_1102 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

d_isRelIsomorphism_1104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_1104 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsRelIsomorphism_98 Source #

d_'42''45'isMagmaIsomorphism_1106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawNearSemiring_148 → T_RawNearSemiring_148 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

du_'42''45'isMagmaIsomorphism_1106 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

d__'8776'__1130 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → AgdaAny → AgdaAny → () Source #

d_1'35'_1144 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → AgdaAny Source #

du_1'35'_1144 ∷ T_RawSemiring_190 → AgdaAny Source #

d_Carrier_1146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → () Source #

d_IsMonoidHomomorphism_1178 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidIsomorphism_1182 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidMonomorphism_1186 ∷ p → p → p → p → p → p → p → () Source #

d_homo_1192 ∷ T_IsMonoidHomomorphism_380 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1194 ∷ T_IsMonoidHomomorphism_380 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_1196 ∷ T_IsMonoidHomomorphism_380 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_1198 ∷ T_IsMonoidHomomorphism_380 → AgdaAny Source #

d_cong_1200 ∷ T_IsMonoidHomomorphism_380 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1204 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1206 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1208 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaIsomorphism_1210 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_1210 ∷ (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaIsomorphism_240 Source #

d_isMagmaMonomorphism_1212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1212 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_1214 ∷ T_IsMonoidIsomorphism_438 → T_IsMonoidHomomorphism_380 Source #

d_isMonoidMonomorphism_1216 ∷ T_IsMonoidIsomorphism_438 → T_IsMonoidMonomorphism_404 Source #

d_isRelHomomorphism_1218 ∷ T_IsMonoidIsomorphism_438 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1220 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_1220 ∷ T_IsMonoidIsomorphism_438 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_1222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1222 ∷ T_IsMonoidIsomorphism_438 → T_IsRelMonomorphism_66 Source #

d_surjective_1224 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_1226 ∷ T_IsMonoidIsomorphism_438 → AgdaAny Source #

d_cong_1228 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1232 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1234 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1236 ∷ T_IsMonoidMonomorphism_404 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_1238 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1238 ∷ (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_1240 ∷ T_IsMonoidMonomorphism_404 → T_IsMonoidHomomorphism_380 Source #

d_isRelHomomorphism_1242 ∷ T_IsMonoidMonomorphism_404 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsMonoidMonomorphism_404 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1244 ∷ T_IsMonoidMonomorphism_404 → T_IsRelMonomorphism_66 Source #

d_ε'45'homo_1246 ∷ T_IsMonoidMonomorphism_404 → AgdaAny Source #

d_cong_1248 ∷ T_IsMonoidMonomorphism_404 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Homomorphic'8320'_1252 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_IsNearSemiringHomomorphism_1262 ∷ p → p → p → p → p → p → p → () Source #

d_IsNearSemiringIsomorphism_1266 ∷ p → p → p → p → p → p → p → () Source #

d_IsNearSemiringMonomorphism_1270 ∷ p → p → p → p → p → p → p → () Source #

d_'42''45'homo_1276 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringHomomorphism_982 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1278 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringHomomorphism_982 → T_IsMagmaHomomorphism_194 Source #

d_homo_1280 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1282 ∷ T_IsNearSemiringHomomorphism_982 → T_IsMagmaHomomorphism_194 Source #

d_'43''45'isMonoidHomomorphism_1284 ∷ T_IsNearSemiringHomomorphism_982 → T_IsMonoidHomomorphism_380 Source #

d_ε'45'homo_1286 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny Source #

d_isRelHomomorphism_1288 ∷ T_IsNearSemiringHomomorphism_982 → T_IsRelHomomorphism_42 Source #

d_cong_1290 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1294 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1296 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1296 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaHomomorphism_194 Source #

d_'42''45'isMagmaIsomorphism_1298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

du_'42''45'isMagmaIsomorphism_1298 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

d_'42''45'isMagmaMonomorphism_1300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

du_'42''45'isMagmaMonomorphism_1300 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

d_homo_1302 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1304 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaIsomorphism_1306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_1306 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

d_isMagmaMonomorphism_1308 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1308 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

d_'43''45'isMonoidHomomorphism_1310 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMonoidHomomorphism_380 Source #

d_'43''45'isMonoidIsomorphism_1312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMonoidIsomorphism_438 Source #

du_'43''45'isMonoidIsomorphism_1312 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMonoidIsomorphism_438 Source #

d_'43''45'isMonoidMonomorphism_1314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMonoidMonomorphism_404 Source #

du_'43''45'isMonoidMonomorphism_1314 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMonoidMonomorphism_404 Source #

d_ε'45'homo_1316 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny Source #

d_injective_1318 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1320 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsNearSemiringHomomorphism_982 Source #

d_isNearSemiringMonomorphism_1322 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsNearSemiringMonomorphism_1012 Source #

d_isRelHomomorphism_1324 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1326 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_1326 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_1328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1328 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsRelMonomorphism_66 Source #

d_surjective_1330 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → T_Σ_14 Source #

d_cong_1332 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1336 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1338 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1338 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMagmaHomomorphism_194 Source #

d_'42''45'isMagmaMonomorphism_1340 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

du_'42''45'isMagmaMonomorphism_1340 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

d_homo_1342 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1344 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_1346 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1346 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

d_'43''45'isMonoidHomomorphism_1348 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMonoidHomomorphism_380 Source #

d_'43''45'isMonoidMonomorphism_1350 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMonoidMonomorphism_404 Source #

du_'43''45'isMonoidMonomorphism_1350 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMonoidMonomorphism_404 Source #

d_ε'45'homo_1352 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny Source #

d_injective_1354 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1356 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsNearSemiringHomomorphism_982 Source #

d_isRelHomomorphism_1358 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1360 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1360 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsRelMonomorphism_66 Source #

d_cong_1362 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSemiringHomomorphism_1366 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSemiringHomomorphism_1366 Source #

d_isNearSemiringHomomorphism_1374 ∷ T_IsSemiringHomomorphism_1366 → T_IsNearSemiringHomomorphism_982 Source #

d_1'35''45'homo_1376 ∷ T_IsSemiringHomomorphism_1366 → AgdaAny Source #

d_'42''45'homo_1380 ∷ T_IsSemiringHomomorphism_1366 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringHomomorphism_1366 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1382 ∷ T_IsSemiringHomomorphism_1366 → T_IsMagmaHomomorphism_194 Source #

d_homo_1384 ∷ T_IsSemiringHomomorphism_1366 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1386 ∷ T_IsSemiringHomomorphism_1366 → T_IsMagmaHomomorphism_194 Source #

d_'43''45'isMonoidHomomorphism_1388 ∷ T_IsSemiringHomomorphism_1366 → T_IsMonoidHomomorphism_380 Source #

d_ε'45'homo_1390 ∷ T_IsSemiringHomomorphism_1366 → AgdaAny Source #

d_isRelHomomorphism_1392 ∷ T_IsSemiringHomomorphism_1366 → T_IsRelHomomorphism_42 Source #

d_cong_1394 ∷ T_IsSemiringHomomorphism_1366 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMonoidHomomorphism_1396 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringHomomorphism_1366 → T_IsMonoidHomomorphism_380 Source #

du_'42''45'isMonoidHomomorphism_1396 ∷ T_IsSemiringHomomorphism_1366 → T_IsMonoidHomomorphism_380 Source #

d_IsSemiringMonomorphism_1402 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSemiringMonomorphism_1402 Source #

d_isSemiringHomomorphism_1410 ∷ T_IsSemiringMonomorphism_1402 → T_IsSemiringHomomorphism_1366 Source #

d_injective_1412 ∷ T_IsSemiringMonomorphism_1402 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1416 ∷ T_IsSemiringMonomorphism_1402 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1418 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1402 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1418 ∷ T_IsSemiringMonomorphism_1402 → T_IsMagmaHomomorphism_194 Source #

d_'42''45'isMonoidHomomorphism_1420 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1402 → T_IsMonoidHomomorphism_380 Source #

du_'42''45'isMonoidHomomorphism_1420 ∷ T_IsSemiringMonomorphism_1402 → T_IsMonoidHomomorphism_380 Source #

d_homo_1422 ∷ T_IsSemiringMonomorphism_1402 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1424 ∷ T_IsSemiringMonomorphism_1402 → T_IsMagmaHomomorphism_194 Source #

d_'43''45'isMonoidHomomorphism_1426 ∷ T_IsSemiringMonomorphism_1402 → T_IsMonoidHomomorphism_380 Source #

d_ε'45'homo_1428 ∷ T_IsSemiringMonomorphism_1402 → AgdaAny Source #

d_1'35''45'homo_1430 ∷ T_IsSemiringMonomorphism_1402 → AgdaAny Source #

d_isNearSemiringHomomorphism_1432 ∷ T_IsSemiringMonomorphism_1402 → T_IsNearSemiringHomomorphism_982 Source #

d_isRelHomomorphism_1434 ∷ T_IsSemiringMonomorphism_1402 → T_IsRelHomomorphism_42 Source #

d_cong_1436 ∷ T_IsSemiringMonomorphism_1402 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringMonomorphism_1438 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1402 → T_IsNearSemiringMonomorphism_1012 Source #

du_isNearSemiringMonomorphism_1438 ∷ T_IsSemiringMonomorphism_1402 → T_IsNearSemiringMonomorphism_1012 Source #

d_'42''45'isMagmaMonomorphism_1442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1402 → T_IsMagmaMonomorphism_214 Source #

du_'42''45'isMagmaMonomorphism_1442 ∷ T_IsSemiringMonomorphism_1402 → T_IsMagmaMonomorphism_214 Source #

d_'43''45'isMonoidMonomorphism_1444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1402 → T_IsMonoidMonomorphism_404 Source #

du_'43''45'isMonoidMonomorphism_1444 ∷ T_IsSemiringMonomorphism_1402 → T_IsMonoidMonomorphism_404 Source #

d_'42''45'isMonoidMonomorphism_1446 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringMonomorphism_1402 → T_IsMonoidMonomorphism_404 Source #

du_'42''45'isMonoidMonomorphism_1446 ∷ T_IsSemiringMonomorphism_1402 → T_IsMonoidMonomorphism_404 Source #

d_IsSemiringIsomorphism_1452 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSemiringIsomorphism_1452 Source #

d_isSemiringMonomorphism_1460 ∷ T_IsSemiringIsomorphism_1452 → T_IsSemiringMonomorphism_1402 Source #

d_surjective_1462 ∷ T_IsSemiringIsomorphism_1452 → AgdaAny → T_Σ_14 Source #

d_'42''45'homo_1466 ∷ T_IsSemiringIsomorphism_1452 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1468 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1452 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1468 ∷ T_IsSemiringIsomorphism_1452 → T_IsMagmaHomomorphism_194 Source #

d_'42''45'isMagmaMonomorphism_1470 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1452 → T_IsMagmaMonomorphism_214 Source #

du_'42''45'isMagmaMonomorphism_1470 ∷ T_IsSemiringIsomorphism_1452 → T_IsMagmaMonomorphism_214 Source #

d_'42''45'isMonoidHomomorphism_1472 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1452 → T_IsMonoidHomomorphism_380 Source #

du_'42''45'isMonoidHomomorphism_1472 ∷ T_IsSemiringIsomorphism_1452 → T_IsMonoidHomomorphism_380 Source #

d_'42''45'isMonoidMonomorphism_1474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1452 → T_IsMonoidMonomorphism_404 Source #

du_'42''45'isMonoidMonomorphism_1474 ∷ T_IsSemiringIsomorphism_1452 → T_IsMonoidMonomorphism_404 Source #

d_homo_1476 ∷ T_IsSemiringIsomorphism_1452 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1478 ∷ T_IsSemiringIsomorphism_1452 → T_IsMagmaHomomorphism_194 Source #

d_'43''45'isMonoidHomomorphism_1480 ∷ T_IsSemiringIsomorphism_1452 → T_IsMonoidHomomorphism_380 Source #

d_'43''45'isMonoidMonomorphism_1482 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1452 → T_IsMonoidMonomorphism_404 Source #

du_'43''45'isMonoidMonomorphism_1482 ∷ T_IsSemiringIsomorphism_1452 → T_IsMonoidMonomorphism_404 Source #

d_ε'45'homo_1484 ∷ T_IsSemiringIsomorphism_1452 → AgdaAny Source #

d_1'35''45'homo_1486 ∷ T_IsSemiringIsomorphism_1452 → AgdaAny Source #

d_injective_1488 ∷ T_IsSemiringIsomorphism_1452 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1490 ∷ T_IsSemiringIsomorphism_1452 → T_IsNearSemiringHomomorphism_982 Source #

d_isNearSemiringMonomorphism_1492 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1452 → T_IsNearSemiringMonomorphism_1012 Source #

du_isNearSemiringMonomorphism_1492 ∷ T_IsSemiringIsomorphism_1452 → T_IsNearSemiringMonomorphism_1012 Source #

d_isRelHomomorphism_1494 ∷ T_IsSemiringIsomorphism_1452 → T_IsRelHomomorphism_42 Source #

d_isSemiringHomomorphism_1496 ∷ T_IsSemiringIsomorphism_1452 → T_IsSemiringHomomorphism_1366 Source #

d_cong_1498 ∷ T_IsSemiringIsomorphism_1452 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringIsomorphism_1500 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1452 → T_IsNearSemiringIsomorphism_1056 Source #

du_isNearSemiringIsomorphism_1500 ∷ T_IsSemiringIsomorphism_1452 → T_IsNearSemiringIsomorphism_1056 Source #

d_'42''45'isMagmaIsomorphism_1504 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1452 → T_IsMagmaIsomorphism_240 Source #

du_'42''45'isMagmaIsomorphism_1504 ∷ T_IsSemiringIsomorphism_1452 → T_IsMagmaIsomorphism_240 Source #

d_'43''45'isMonoidIsomorphism_1506 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1452 → T_IsMonoidIsomorphism_438 Source #

du_'43''45'isMonoidIsomorphism_1506 ∷ T_IsSemiringIsomorphism_1452 → T_IsMonoidIsomorphism_438 Source #

d_'42''45'isMonoidIsomorphism_1508 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawSemiring_190 → T_RawSemiring_190 → (AgdaAny → AgdaAny) → T_IsSemiringIsomorphism_1452 → T_IsMonoidIsomorphism_438 Source #

du_'42''45'isMonoidIsomorphism_1508 ∷ T_IsSemiringIsomorphism_1452 → T_IsMonoidIsomorphism_438 Source #

d__'42'__1528 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → AgdaAny → AgdaAny → AgdaAny Source #

du__'42'__1528 ∷ T_RawRingWithoutOne_240 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → AgdaAny → AgdaAny → () Source #

d_Carrier_1548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → () Source #

d_IsGroupHomomorphism_1580 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroupIsomorphism_1584 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroupMonomorphism_1588 ∷ p → p → p → p → p → p → p → () Source #

d_homo_1594 ∷ T_IsGroupHomomorphism_670 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1596 ∷ T_IsGroupHomomorphism_670 → T_IsMagmaHomomorphism_194 Source #

d_isMonoidHomomorphism_1598 ∷ T_IsGroupHomomorphism_670 → T_IsMonoidHomomorphism_380 Source #

d_isRelHomomorphism_1600 ∷ T_IsGroupHomomorphism_670 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_1602 ∷ T_IsGroupHomomorphism_670 → AgdaAny Source #

d_'8315''185''45'homo_1604 ∷ T_IsGroupHomomorphism_670 → AgdaAny → AgdaAny Source #

d_cong_1606 ∷ T_IsGroupHomomorphism_670 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1610 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroupHomomorphism_1612 ∷ T_IsGroupIsomorphism_738 → T_IsGroupHomomorphism_670 Source #

d_isGroupMonomorphism_1614 ∷ T_IsGroupIsomorphism_738 → T_IsGroupMonomorphism_698 Source #

d_isMagmaHomomorphism_1616 ∷ T_IsGroupIsomorphism_738 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaIsomorphism_1618 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_1618 ∷ T_IsGroupIsomorphism_738 → T_IsMagmaIsomorphism_240 Source #

d_isMagmaMonomorphism_1620 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1620 ∷ T_IsGroupIsomorphism_738 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_1622 ∷ T_IsGroupIsomorphism_738 → T_IsMonoidHomomorphism_380 Source #

d_isMonoidIsomorphism_1624 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMonoidIsomorphism_438 Source #

du_isMonoidIsomorphism_1624 ∷ (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMonoidIsomorphism_438 Source #

d_isMonoidMonomorphism_1626 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMonoidMonomorphism_404 Source #

du_isMonoidMonomorphism_1626 ∷ T_IsGroupIsomorphism_738 → T_IsMonoidMonomorphism_404 Source #

d_isRelHomomorphism_1628 ∷ T_IsGroupIsomorphism_738 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1630 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_1630 ∷ T_IsGroupIsomorphism_738 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_1632 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1632 ∷ T_IsGroupIsomorphism_738 → T_IsRelMonomorphism_66 Source #

d_surjective_1634 ∷ T_IsGroupIsomorphism_738 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_1636 ∷ T_IsGroupIsomorphism_738 → AgdaAny Source #

d_'8315''185''45'homo_1638 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny Source #

d_homo_1640 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_1642 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1646 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroupHomomorphism_1648 ∷ T_IsGroupMonomorphism_698 → T_IsGroupHomomorphism_670 Source #

d_isMagmaHomomorphism_1650 ∷ T_IsGroupMonomorphism_698 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_1652 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1652 ∷ T_IsGroupMonomorphism_698 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_1654 ∷ T_IsGroupMonomorphism_698 → T_IsMonoidHomomorphism_380 Source #

d_isMonoidMonomorphism_1656 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsMonoidMonomorphism_404 Source #

du_isMonoidMonomorphism_1656 ∷ (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsMonoidMonomorphism_404 Source #

d_isRelHomomorphism_1658 ∷ T_IsGroupMonomorphism_698 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1660 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1660 ∷ T_IsGroupMonomorphism_698 → T_IsRelMonomorphism_66 Source #

d_ε'45'homo_1662 ∷ T_IsGroupMonomorphism_698 → AgdaAny Source #

d_'8315''185''45'homo_1664 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny Source #

d_homo_1666 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_1668 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMagmaHomomorphism_1672 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaIsomorphism_1676 ∷ p → p → p → p → p → p → p → () Source #

d_IsMagmaMonomorphism_1680 ∷ p → p → p → p → p → p → p → () Source #

d_homo_1686 ∷ T_IsMagmaHomomorphism_194 → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_1688 ∷ T_IsMagmaHomomorphism_194 → T_IsRelHomomorphism_42 Source #

d_cong_1690 ∷ T_IsMagmaHomomorphism_194 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1694 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1696 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1698 ∷ T_IsMagmaIsomorphism_240 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_1700 ∷ T_IsMagmaIsomorphism_240 → T_IsMagmaMonomorphism_214 Source #

d_isRelHomomorphism_1702 ∷ T_IsMagmaIsomorphism_240 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_1704 ∷ (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_1706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsMagmaIsomorphism_240 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1706 ∷ T_IsMagmaIsomorphism_240 → T_IsRelMonomorphism_66 Source #

d_surjective_1708 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → T_Σ_14 Source #

d_cong_1710 ∷ T_IsMagmaIsomorphism_240 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1714 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_1716 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1718 ∷ T_IsMagmaMonomorphism_214 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_1720 ∷ T_IsMagmaMonomorphism_214 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_214 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1722 ∷ (AgdaAny → AgdaAny) → T_IsMagmaMonomorphism_214 → T_IsRelMonomorphism_66 Source #

d_cong_1724 ∷ T_IsMagmaMonomorphism_214 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsNearSemiringHomomorphism_1728 ∷ p → p → p → p → p → p → p → () Source #

d_IsNearSemiringIsomorphism_1732 ∷ p → p → p → p → p → p → p → () Source #

d_IsNearSemiringMonomorphism_1736 ∷ p → p → p → p → p → p → p → () Source #

d_'42''45'homo_1742 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1744 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringHomomorphism_982 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1744 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringHomomorphism_982 → T_IsMagmaHomomorphism_194 Source #

d_homo_1746 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1748 ∷ T_IsNearSemiringHomomorphism_982 → T_IsMagmaHomomorphism_194 Source #

d_'43''45'isMonoidHomomorphism_1750 ∷ T_IsNearSemiringHomomorphism_982 → T_IsMonoidHomomorphism_380 Source #

d_ε'45'homo_1752 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny Source #

d_isRelHomomorphism_1754 ∷ T_IsNearSemiringHomomorphism_982 → T_IsRelHomomorphism_42 Source #

d_cong_1756 ∷ T_IsNearSemiringHomomorphism_982 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1760 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1762 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1762 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaHomomorphism_194 Source #

d_'42''45'isMagmaIsomorphism_1764 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

du_'42''45'isMagmaIsomorphism_1764 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

d_'42''45'isMagmaMonomorphism_1766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

du_'42''45'isMagmaMonomorphism_1766 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

d_homo_1768 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1770 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaIsomorphism_1772 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_1772 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaIsomorphism_240 Source #

d_isMagmaMonomorphism_1774 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1774 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMagmaMonomorphism_214 Source #

d_'43''45'isMonoidHomomorphism_1776 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMonoidHomomorphism_380 Source #

d_'43''45'isMonoidIsomorphism_1778 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMonoidIsomorphism_438 Source #

du_'43''45'isMonoidIsomorphism_1778 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMonoidIsomorphism_438 Source #

d_'43''45'isMonoidMonomorphism_1780 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsMonoidMonomorphism_404 Source #

du_'43''45'isMonoidMonomorphism_1780 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsMonoidMonomorphism_404 Source #

d_ε'45'homo_1782 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny Source #

d_injective_1784 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1786 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsNearSemiringHomomorphism_982 Source #

d_isNearSemiringMonomorphism_1788 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsNearSemiringMonomorphism_1012 Source #

d_isRelHomomorphism_1790 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_1792 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_1794 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringIsomorphism_1056 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1794 ∷ T_IsNearSemiringIsomorphism_1056 → T_IsRelMonomorphism_66 Source #

d_surjective_1796 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → T_Σ_14 Source #

d_cong_1798 ∷ T_IsNearSemiringIsomorphism_1056 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1802 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1804 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMagmaHomomorphism_194 Source #

d_'42''45'isMagmaMonomorphism_1806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

du_'42''45'isMagmaMonomorphism_1806 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

d_homo_1808 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1810 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_1812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1812 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMagmaMonomorphism_214 Source #

d_'43''45'isMonoidHomomorphism_1814 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsMonoidHomomorphism_380 Source #

d_'43''45'isMonoidMonomorphism_1816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMonoidMonomorphism_404 Source #

du_'43''45'isMonoidMonomorphism_1816 ∷ (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsMonoidMonomorphism_404 Source #

d_ε'45'homo_1818 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny Source #

d_injective_1820 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1822 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsNearSemiringHomomorphism_982 Source #

d_isRelHomomorphism_1824 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsNearSemiringMonomorphism_1012 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1826 ∷ T_IsNearSemiringMonomorphism_1012 → T_IsRelMonomorphism_66 Source #

d_cong_1828 ∷ T_IsNearSemiringMonomorphism_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Homomorphic'8322'_1836 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsRingWithoutOneHomomorphism_1842 ∷ p → p → p → p → p → p → p → () Source #

data T_IsRingWithoutOneHomomorphism_1842 Source #

d_'43''45'isGroupHomomorphism_1850 ∷ T_IsRingWithoutOneHomomorphism_1842 → T_IsGroupHomomorphism_670 Source #

d_'42''45'homo_1852 ∷ T_IsRingWithoutOneHomomorphism_1842 → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_1856 ∷ T_IsRingWithoutOneHomomorphism_1842 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_1858 ∷ T_IsRingWithoutOneHomomorphism_1842 → T_IsMagmaHomomorphism_194 Source #

d_isMonoidHomomorphism_1860 ∷ T_IsRingWithoutOneHomomorphism_1842 → T_IsMonoidHomomorphism_380 Source #

d_ε'45'homo_1862 ∷ T_IsRingWithoutOneHomomorphism_1842 → AgdaAny Source #

d_isRelHomomorphism_1864 ∷ T_IsRingWithoutOneHomomorphism_1842 → T_IsRelHomomorphism_42 Source #

d_'8315''185''45'homo_1866 ∷ T_IsRingWithoutOneHomomorphism_1842 → AgdaAny → AgdaAny Source #

d_cong_1868 ∷ T_IsRingWithoutOneHomomorphism_1842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1870 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneHomomorphism_1842 → T_IsNearSemiringHomomorphism_982 Source #

du_isNearSemiringHomomorphism_1870 ∷ T_IsRingWithoutOneHomomorphism_1842 → T_IsNearSemiringHomomorphism_982 Source #

d_'42''45'isMagmaHomomorphism_1872 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneHomomorphism_1842 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1872 ∷ T_IsRingWithoutOneHomomorphism_1842 → T_IsMagmaHomomorphism_194 Source #

d_IsRingWithoutOneMonomorphism_1878 ∷ p → p → p → p → p → p → p → () Source #

data T_IsRingWithoutOneMonomorphism_1878 Source #

d_isRingWithoutOneHomomorphism_1886 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsRingWithoutOneHomomorphism_1842 Source #

d_injective_1888 ∷ T_IsRingWithoutOneMonomorphism_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'homo_1892 ∷ T_IsRingWithoutOneMonomorphism_1878 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1894 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1878 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1894 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsMagmaHomomorphism_194 Source #

d_homo_1896 ∷ T_IsRingWithoutOneMonomorphism_1878 → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isGroupHomomorphism_1898 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsGroupHomomorphism_670 Source #

d_isMagmaHomomorphism_1900 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsMagmaHomomorphism_194 Source #

d_isMonoidHomomorphism_1902 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsMonoidHomomorphism_380 Source #

d_ε'45'homo_1904 ∷ T_IsRingWithoutOneMonomorphism_1878 → AgdaAny Source #

d_isNearSemiringHomomorphism_1906 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1878 → T_IsNearSemiringHomomorphism_982 Source #

du_isNearSemiringHomomorphism_1906 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsNearSemiringHomomorphism_982 Source #

d_isRelHomomorphism_1908 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsRelHomomorphism_42 Source #

d_'8315''185''45'homo_1910 ∷ T_IsRingWithoutOneMonomorphism_1878 → AgdaAny → AgdaAny Source #

d_cong_1912 ∷ T_IsRingWithoutOneMonomorphism_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isGroupMonomorphism_1914 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1878 → T_IsGroupMonomorphism_698 Source #

du_'43''45'isGroupMonomorphism_1914 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsGroupMonomorphism_698 Source #

d_isMagmaMonomorphism_1918 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1878 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1918 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidMonomorphism_1920 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1878 → T_IsMonoidMonomorphism_404 Source #

du_isMonoidMonomorphism_1920 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsMonoidMonomorphism_404 Source #

d_isRelMonomorphism_1922 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1878 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1922 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsRelMonomorphism_66 Source #

d_'42''45'isMagmaMonomorphism_1924 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneMonomorphism_1878 → T_IsMagmaMonomorphism_214 Source #

du_'42''45'isMagmaMonomorphism_1924 ∷ T_IsRingWithoutOneMonomorphism_1878 → T_IsMagmaMonomorphism_214 Source #

d_IsRingWithoutOneIsoMorphism_1930 ∷ p → p → p → p → p → p → p → () Source #

data T_IsRingWithoutOneIsoMorphism_1930 Source #

d_isRingWithoutOneMonomorphism_1938 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsRingWithoutOneMonomorphism_1878 Source #

d_surjective_1940 ∷ T_IsRingWithoutOneIsoMorphism_1930 → AgdaAny → T_Σ_14 Source #

d_'42''45'homo_1944 ∷ T_IsRingWithoutOneIsoMorphism_1930 → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1946 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaHomomorphism_194 Source #

du_'42''45'isMagmaHomomorphism_1946 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaHomomorphism_194 Source #

d_'42''45'isMagmaMonomorphism_1948 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaMonomorphism_214 Source #

du_'42''45'isMagmaMonomorphism_1948 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaMonomorphism_214 Source #

d_homo_1950 ∷ T_IsRingWithoutOneIsoMorphism_1930 → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isGroupHomomorphism_1952 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsGroupHomomorphism_670 Source #

d_'43''45'isGroupMonomorphism_1954 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsGroupMonomorphism_698 Source #

du_'43''45'isGroupMonomorphism_1954 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsGroupMonomorphism_698 Source #

d_isMagmaHomomorphism_1956 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_1958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_1958 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_1960 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsMonoidHomomorphism_380 Source #

d_isMonoidMonomorphism_1962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsMonoidMonomorphism_404 Source #

du_isMonoidMonomorphism_1962 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsMonoidMonomorphism_404 Source #

d_ε'45'homo_1964 ∷ T_IsRingWithoutOneIsoMorphism_1930 → AgdaAny Source #

d_injective_1966 ∷ T_IsRingWithoutOneIsoMorphism_1930 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isNearSemiringHomomorphism_1968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsNearSemiringHomomorphism_982 Source #

du_isNearSemiringHomomorphism_1968 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsNearSemiringHomomorphism_982 Source #

d_isRelHomomorphism_1970 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_1972 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsRelMonomorphism_66 Source #

d_isRingWithoutOneHomomorphism_1974 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsRingWithoutOneHomomorphism_1842 Source #

d_'8315''185''45'homo_1976 ∷ T_IsRingWithoutOneIsoMorphism_1930 → AgdaAny → AgdaAny Source #

d_cong_1978 ∷ T_IsRingWithoutOneIsoMorphism_1930 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isGroupIsomorphism_1980 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsGroupIsomorphism_738 Source #

du_'43''45'isGroupIsomorphism_1980 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsGroupIsomorphism_738 Source #

d_isMagmaIsomorphism_1984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_1984 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaIsomorphism_240 Source #

d_isMonoidIsomorphism_1986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsMonoidIsomorphism_438 Source #

du_isMonoidIsomorphism_1986 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsMonoidIsomorphism_438 Source #

d_isRelIsomorphism_1988 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_1988 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsRelIsomorphism_98 Source #

d_'42''45'isMagmaIsomorphism_1990 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRingWithoutOne_240 → T_RawRingWithoutOne_240 → (AgdaAny → AgdaAny) → T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaIsomorphism_240 Source #

du_'42''45'isMagmaIsomorphism_1990 ∷ T_IsRingWithoutOneIsoMorphism_1930 → T_IsMagmaIsomorphism_240 Source #

d__'8776'__2014 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → AgdaAny → AgdaAny → () Source #

d_'45'__2028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → AgdaAny → AgdaAny Source #

du_'45'__2028 ∷ T_RawRing_290 → AgdaAny → AgdaAny Source #

d_Carrier_2034 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → () Source #

d_IsGroupHomomorphism_2074 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroupIsomorphism_2078 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroupMonomorphism_2082 ∷ p → p → p → p → p → p → p → () Source #

d_homo_2088 ∷ T_IsGroupHomomorphism_670 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_2090 ∷ T_IsGroupHomomorphism_670 → T_IsMagmaHomomorphism_194 Source #

d_isMonoidHomomorphism_2092 ∷ T_IsGroupHomomorphism_670 → T_IsMonoidHomomorphism_380 Source #

d_isRelHomomorphism_2094 ∷ T_IsGroupHomomorphism_670 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_2096 ∷ T_IsGroupHomomorphism_670 → AgdaAny Source #

d_'8315''185''45'homo_2098 ∷ T_IsGroupHomomorphism_670 → AgdaAny → AgdaAny Source #

d_cong_2100 ∷ T_IsGroupHomomorphism_670 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_2104 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroupHomomorphism_2106 ∷ T_IsGroupIsomorphism_738 → T_IsGroupHomomorphism_670 Source #

d_isGroupMonomorphism_2108 ∷ T_IsGroupIsomorphism_738 → T_IsGroupMonomorphism_698 Source #

d_isMagmaHomomorphism_2110 ∷ T_IsGroupIsomorphism_738 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaIsomorphism_2112 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_2112 ∷ T_IsGroupIsomorphism_738 → T_IsMagmaIsomorphism_240 Source #

d_isMagmaMonomorphism_2114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_2114 ∷ T_IsGroupIsomorphism_738 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_2116 ∷ T_IsGroupIsomorphism_738 → T_IsMonoidHomomorphism_380 Source #

d_isMonoidIsomorphism_2118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMonoidIsomorphism_438 Source #

du_isMonoidIsomorphism_2118 ∷ (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMonoidIsomorphism_438 Source #

d_isMonoidMonomorphism_2120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsMonoidMonomorphism_404 Source #

du_isMonoidMonomorphism_2120 ∷ T_IsGroupIsomorphism_738 → T_IsMonoidMonomorphism_404 Source #

d_isRelHomomorphism_2122 ∷ T_IsGroupIsomorphism_738 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_2124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_2124 ∷ T_IsGroupIsomorphism_738 → T_IsRelIsomorphism_98 Source #

d_isRelMonomorphism_2126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsGroupIsomorphism_738 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_2126 ∷ T_IsGroupIsomorphism_738 → T_IsRelMonomorphism_66 Source #

d_surjective_2128 ∷ T_IsGroupIsomorphism_738 → AgdaAny → T_Σ_14 Source #

d_ε'45'homo_2130 ∷ T_IsGroupIsomorphism_738 → AgdaAny Source #

d_'8315''185''45'homo_2132 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny Source #

d_homo_2134 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_2136 ∷ T_IsGroupIsomorphism_738 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_2140 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isGroupHomomorphism_2142 ∷ T_IsGroupMonomorphism_698 → T_IsGroupHomomorphism_670 Source #

d_isMagmaHomomorphism_2144 ∷ T_IsGroupMonomorphism_698 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaMonomorphism_2146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_2146 ∷ T_IsGroupMonomorphism_698 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_2148 ∷ T_IsGroupMonomorphism_698 → T_IsMonoidHomomorphism_380 Source #

d_isMonoidMonomorphism_2150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsMonoidMonomorphism_404 Source #

du_isMonoidMonomorphism_2150 ∷ (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsMonoidMonomorphism_404 Source #

d_isRelHomomorphism_2152 ∷ T_IsGroupMonomorphism_698 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_2154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsGroupMonomorphism_698 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_2154 ∷ T_IsGroupMonomorphism_698 → T_IsRelMonomorphism_66 Source #

d_ε'45'homo_2156 ∷ T_IsGroupMonomorphism_698 → AgdaAny Source #

d_'8315''185''45'homo_2158 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny Source #

d_homo_2160 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_2162 ∷ T_IsGroupMonomorphism_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoidHomomorphism_2166 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidIsomorphism_2170 ∷ p → p → p → p → p → p → p → () Source #

d_IsMonoidMonomorphism_2174 ∷ p → p → p → p → p → p → p → () Source #

d_homo_2180 ∷ T_IsMonoidHomomorphism_380 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_2182 ∷ T_IsMonoidHomomorphism_380 → T_IsMagmaHomomorphism_194 Source #

d_isRelHomomorphism_2184 ∷ T_IsMonoidHomomorphism_380 → T_IsRelHomomorphism_42 Source #

d_ε'45'homo_2186 ∷ T_IsMonoidHomomorphism_380 → AgdaAny Source #

d_cong_2188 ∷ T_IsMonoidHomomorphism_380 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_homo_2192 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_2194 ∷ T_IsMonoidIsomorphism_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagmaHomomorphism_2196 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaHomomorphism_194 Source #

d_isMagmaIsomorphism_2198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaIsomorphism_240 Source #

du_isMagmaIsomorphism_2198 ∷ (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaIsomorphism_240 Source #

d_isMagmaMonomorphism_2200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsMagmaMonomorphism_214 Source #

du_isMagmaMonomorphism_2200 ∷ T_IsMonoidIsomorphism_438 → T_IsMagmaMonomorphism_214 Source #

d_isMonoidHomomorphism_2202 ∷ T_IsMonoidIsomorphism_438 → T_IsMonoidHomomorphism_380 Source #

d_isMonoidMonomorphism_2204 ∷ T_IsMonoidIsomorphism_438 → T_IsMonoidMonomorphism_404 Source #

d_isRelHomomorphism_2206 ∷ T_IsMonoidIsomorphism_438 → T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_2208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_RawRing_290 → T_RawRing_290 → (AgdaAny → AgdaAny) → T_IsMonoidIsomorphism_438 → T_IsRelIsomorphism_98 Source #