Safe Haskell	None

MAlonzo.Code.Algebra.Morphism.Structures

Documentation

d__'8729'__30 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMagma_8 -> T_RawMagma_8 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'8729'__30 :: T_RawMagma_8 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__32 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMagma_8 -> T_RawMagma_8 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_36 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMagma_8 -> T_RawMagma_8 -> () Source #

d_Homomorphic'8322'_54 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMagma_8 -> T_RawMagma_8 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Injective_64 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMagma_8 -> T_RawMagma_8 -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_72 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMagma_8 -> T_RawMagma_8 -> (AgdaAny -> AgdaAny) -> () Source #

d_IsMagmaHomomorphism_76 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsMagmaHomomorphism_76 Source #

Constructors

C_IsMagmaHomomorphism'46'constructor_757 T_IsRelHomomorphism_42 (AgdaAny -> AgdaAny -> AgdaAny)

d_isRelHomomorphism_84 :: T_IsMagmaHomomorphism_76 -> T_IsRelHomomorphism_42 Source #

d_homo_86 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_90 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMagmaMonomorphism_94 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsMagmaMonomorphism_94 Source #

Constructors

C_IsMagmaMonomorphism'46'constructor_1391 T_IsMagmaHomomorphism_76 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isMagmaHomomorphism_102 :: T_IsMagmaMonomorphism_94 -> T_IsMagmaHomomorphism_76 Source #

d_injective_104 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_108 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_110 :: T_IsMagmaMonomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_cong_112 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelMonomorphism_114 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMagma_8 -> T_RawMagma_8 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_114 :: T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_IsMagmaIsomorphism_118 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsMagmaIsomorphism_118 Source #

Constructors

C_IsMagmaIsomorphism'46'constructor_2309 T_IsMagmaMonomorphism_94 (AgdaAny -> T_Σ_14)

d_isMagmaMonomorphism_126 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaMonomorphism_94 Source #

d_surjective_128 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> T_Σ_14 Source #

d_homo_132 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_134 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_136 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_138 :: T_IsMagmaIsomorphism_118 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_140 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMagma_8 -> T_RawMagma_8 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_140 :: T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

d_cong_142 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelIsomorphism_144 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMagma_8 -> T_RawMagma_8 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_144 :: T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

d_Carrier_168 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> () Source #

d_ε_172 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> AgdaAny Source #

du_ε_172 :: T_RawMonoid_402 -> AgdaAny Source #

d_Homomorphic'8320'_190 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Injective_204 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_212 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> () Source #

d_IsMagmaHomomorphism_216 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaIsomorphism_218 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaMonomorphism_220 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_224 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_226 :: T_IsMagmaHomomorphism_76 -> T_IsRelHomomorphism_42 Source #

d_cong_228 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_232 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_234 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_236 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_238 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaMonomorphism_94 Source #

d_isRelHomomorphism_240 :: T_IsMagmaIsomorphism_118 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_242 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_242 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_244 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_244 :: T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

d_surjective_246 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> T_Σ_14 Source #

d_cong_248 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_252 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_254 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_256 :: T_IsMagmaMonomorphism_94 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_258 :: T_IsMagmaMonomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_260 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_260 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_cong_262 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMonoidHomomorphism_266 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsMonoidHomomorphism_266 Source #

Constructors

C_IsMonoidHomomorphism'46'constructor_4403 T_IsMagmaHomomorphism_76 AgdaAny

d_isMagmaHomomorphism_274 :: T_IsMonoidHomomorphism_266 -> T_IsMagmaHomomorphism_76 Source #

d_ε'45'homo_276 :: T_IsMonoidHomomorphism_266 -> AgdaAny Source #

d_homo_280 :: T_IsMonoidHomomorphism_266 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_282 :: T_IsMonoidHomomorphism_266 -> T_IsRelHomomorphism_42 Source #

d_cong_284 :: T_IsMonoidHomomorphism_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMonoidMonomorphism_288 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsMonoidMonomorphism_288 Source #

Constructors

C_IsMonoidMonomorphism'46'constructor_4857 T_IsMonoidHomomorphism_266 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isMonoidHomomorphism_296 :: T_IsMonoidMonomorphism_288 -> T_IsMonoidHomomorphism_266 Source #

d_injective_298 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_302 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_304 :: T_IsMonoidMonomorphism_288 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_306 :: T_IsMonoidMonomorphism_288 -> T_IsRelHomomorphism_42 Source #

d_ε'45'homo_308 :: T_IsMonoidMonomorphism_288 -> AgdaAny Source #

d_cong_310 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaMonomorphism_312 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_312 :: T_IsMonoidMonomorphism_288 -> T_IsMagmaMonomorphism_94 Source #

d_isRelMonomorphism_316 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_316 :: T_IsMonoidMonomorphism_288 -> T_IsRelMonomorphism_64 Source #

d_IsMonoidIsomorphism_320 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsMonoidIsomorphism_320 Source #

Constructors

C_IsMonoidIsomorphism'46'constructor_5773 T_IsMonoidMonomorphism_288 (AgdaAny -> T_Σ_14)

d_isMonoidMonomorphism_328 :: T_IsMonoidIsomorphism_320 -> T_IsMonoidMonomorphism_288 Source #

d_surjective_330 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> T_Σ_14 Source #

d_homo_334 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_336 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_338 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_340 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_340 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_342 :: T_IsMonoidIsomorphism_320 -> T_IsMonoidHomomorphism_266 Source #

d_isRelHomomorphism_344 :: T_IsMonoidIsomorphism_320 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_346 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_346 :: T_IsMonoidIsomorphism_320 -> T_IsRelMonomorphism_64 Source #

d_ε'45'homo_348 :: T_IsMonoidIsomorphism_320 -> AgdaAny Source #

d_cong_350 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaIsomorphism_352 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_352 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaIsomorphism_118 Source #

d_isRelIsomorphism_356 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawMonoid_402 -> T_RawMonoid_402 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_356 :: T_IsMonoidIsomorphism_320 -> T_IsRelIsomorphism_94 Source #

d__'8315''185'_374 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> AgdaAny -> AgdaAny Source #

du__'8315''185'_374 :: T_RawGroup_868 -> AgdaAny -> AgdaAny Source #

d_Carrier_382 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> () Source #

d_Homomorphic'8321'_412 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Injective_424 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_432 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> () Source #

d_IsMagmaHomomorphism_436 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaIsomorphism_438 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaMonomorphism_440 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_444 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_446 :: T_IsMagmaHomomorphism_76 -> T_IsRelHomomorphism_42 Source #

d_cong_448 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_452 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_454 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_456 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_458 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaMonomorphism_94 Source #

d_isRelHomomorphism_460 :: T_IsMagmaIsomorphism_118 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_462 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_462 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_464 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_464 :: T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

d_surjective_466 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> T_Σ_14 Source #

d_cong_468 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_472 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_474 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_476 :: T_IsMagmaMonomorphism_94 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_478 :: T_IsMagmaMonomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_480 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_480 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_cong_482 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMonoidHomomorphism_486 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMonoidIsomorphism_488 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMonoidMonomorphism_490 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_494 :: T_IsMonoidHomomorphism_266 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_496 :: T_IsMonoidHomomorphism_266 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_498 :: T_IsMonoidHomomorphism_266 -> T_IsRelHomomorphism_42 Source #

d_ε'45'homo_500 :: T_IsMonoidHomomorphism_266 -> AgdaAny Source #

d_cong_502 :: T_IsMonoidHomomorphism_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_506 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_508 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_510 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaIsomorphism_512 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_512 :: (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaIsomorphism_118 Source #

d_isMagmaMonomorphism_514 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_514 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_516 :: T_IsMonoidIsomorphism_320 -> T_IsMonoidHomomorphism_266 Source #

d_isMonoidMonomorphism_518 :: T_IsMonoidIsomorphism_320 -> T_IsMonoidMonomorphism_288 Source #

d_isRelHomomorphism_520 :: T_IsMonoidIsomorphism_320 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_522 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_522 :: T_IsMonoidIsomorphism_320 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_524 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_524 :: T_IsMonoidIsomorphism_320 -> T_IsRelMonomorphism_64 Source #

d_surjective_526 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> T_Σ_14 Source #

d_ε'45'homo_528 :: T_IsMonoidIsomorphism_320 -> AgdaAny Source #

d_cong_530 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_534 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_536 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_538 :: T_IsMonoidMonomorphism_288 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_540 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_540 :: (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_542 :: T_IsMonoidMonomorphism_288 -> T_IsMonoidHomomorphism_266 Source #

d_isRelHomomorphism_544 :: T_IsMonoidMonomorphism_288 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_546 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_546 :: T_IsMonoidMonomorphism_288 -> T_IsRelMonomorphism_64 Source #

d_ε'45'homo_548 :: T_IsMonoidMonomorphism_288 -> AgdaAny Source #

d_cong_550 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsGroupHomomorphism_554 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsGroupHomomorphism_554 Source #

Constructors

C_IsGroupHomomorphism'46'constructor_8617 T_IsMonoidHomomorphism_266 (AgdaAny -> AgdaAny)

d_isMonoidHomomorphism_562 :: T_IsGroupHomomorphism_554 -> T_IsMonoidHomomorphism_266 Source #

d_'8315''185''45'homo_564 :: T_IsGroupHomomorphism_554 -> AgdaAny -> AgdaAny Source #

d_homo_568 :: T_IsGroupHomomorphism_554 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_570 :: T_IsGroupHomomorphism_554 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_572 :: T_IsGroupHomomorphism_554 -> T_IsRelHomomorphism_42 Source #

d_ε'45'homo_574 :: T_IsGroupHomomorphism_554 -> AgdaAny Source #

d_cong_576 :: T_IsGroupHomomorphism_554 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsGroupMonomorphism_580 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsGroupMonomorphism_580 Source #

Constructors

C_IsGroupMonomorphism'46'constructor_9197 T_IsGroupHomomorphism_554 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isGroupHomomorphism_588 :: T_IsGroupMonomorphism_580 -> T_IsGroupHomomorphism_554 Source #

d_injective_590 :: T_IsGroupMonomorphism_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_594 :: T_IsGroupMonomorphism_580 -> T_IsMagmaHomomorphism_76 Source #

d_isMonoidHomomorphism_596 :: T_IsGroupMonomorphism_580 -> T_IsMonoidHomomorphism_266 Source #

d_isRelHomomorphism_598 :: T_IsGroupMonomorphism_580 -> T_IsRelHomomorphism_42 Source #

d_ε'45'homo_600 :: T_IsGroupMonomorphism_580 -> AgdaAny Source #

d_'8315''185''45'homo_602 :: T_IsGroupMonomorphism_580 -> AgdaAny -> AgdaAny Source #

d_homo_604 :: T_IsGroupMonomorphism_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_606 :: T_IsGroupMonomorphism_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMonoidMonomorphism_608 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_580 -> T_IsMonoidMonomorphism_288 Source #

du_isMonoidMonomorphism_608 :: T_IsGroupMonomorphism_580 -> T_IsMonoidMonomorphism_288 Source #

d_isMagmaMonomorphism_612 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_580 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_612 :: T_IsGroupMonomorphism_580 -> T_IsMagmaMonomorphism_94 Source #

d_isRelMonomorphism_614 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_580 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_614 :: T_IsGroupMonomorphism_580 -> T_IsRelMonomorphism_64 Source #

d_IsGroupIsomorphism_618 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsGroupIsomorphism_618 Source #

Constructors

C_IsGroupIsomorphism'46'constructor_10289 T_IsGroupMonomorphism_580 (AgdaAny -> T_Σ_14)

d_isGroupMonomorphism_626 :: T_IsGroupIsomorphism_618 -> T_IsGroupMonomorphism_580 Source #

d_surjective_628 :: T_IsGroupIsomorphism_618 -> AgdaAny -> T_Σ_14 Source #

d_injective_632 :: T_IsGroupIsomorphism_618 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isGroupHomomorphism_634 :: T_IsGroupIsomorphism_618 -> T_IsGroupHomomorphism_554 Source #

d_isMagmaHomomorphism_636 :: T_IsGroupIsomorphism_618 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_638 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_638 :: T_IsGroupIsomorphism_618 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_640 :: T_IsGroupIsomorphism_618 -> T_IsMonoidHomomorphism_266 Source #

d_isMonoidMonomorphism_642 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsMonoidMonomorphism_288 Source #

du_isMonoidMonomorphism_642 :: T_IsGroupIsomorphism_618 -> T_IsMonoidMonomorphism_288 Source #

d_isRelHomomorphism_644 :: T_IsGroupIsomorphism_618 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_646 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_646 :: T_IsGroupIsomorphism_618 -> T_IsRelMonomorphism_64 Source #

d_ε'45'homo_648 :: T_IsGroupIsomorphism_618 -> AgdaAny Source #

d_'8315''185''45'homo_650 :: T_IsGroupIsomorphism_618 -> AgdaAny -> AgdaAny Source #

d_homo_652 :: T_IsGroupIsomorphism_618 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_654 :: T_IsGroupIsomorphism_618 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMonoidIsomorphism_656 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsMonoidIsomorphism_320 Source #

du_isMonoidIsomorphism_656 :: T_IsGroupIsomorphism_618 -> T_IsMonoidIsomorphism_320 Source #

d_isMagmaIsomorphism_660 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_660 :: T_IsGroupIsomorphism_618 -> T_IsMagmaIsomorphism_118 Source #

d_isRelIsomorphism_662 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawGroup_868 -> T_RawGroup_868 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_662 :: T_IsGroupIsomorphism_618 -> T_IsRelIsomorphism_94 Source #

d__'42'__680 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'42'__680 :: T_RawNearSemiring_1304 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_Carrier_696 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> () Source #

d_IsMonoidHomomorphism_720 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMonoidIsomorphism_722 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMonoidMonomorphism_724 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_728 :: T_IsMonoidHomomorphism_266 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_730 :: T_IsMonoidHomomorphism_266 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_732 :: T_IsMonoidHomomorphism_266 -> T_IsRelHomomorphism_42 Source #

d_ε'45'homo_734 :: T_IsMonoidHomomorphism_266 -> AgdaAny Source #

d_cong_736 :: T_IsMonoidHomomorphism_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_740 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_742 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_744 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaIsomorphism_746 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_746 :: (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaIsomorphism_118 Source #

d_isMagmaMonomorphism_748 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_748 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_750 :: T_IsMonoidIsomorphism_320 -> T_IsMonoidHomomorphism_266 Source #

d_isMonoidMonomorphism_752 :: T_IsMonoidIsomorphism_320 -> T_IsMonoidMonomorphism_288 Source #

d_isRelHomomorphism_754 :: T_IsMonoidIsomorphism_320 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_756 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_756 :: T_IsMonoidIsomorphism_320 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_758 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_758 :: T_IsMonoidIsomorphism_320 -> T_IsRelMonomorphism_64 Source #

d_surjective_760 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> T_Σ_14 Source #

d_ε'45'homo_762 :: T_IsMonoidIsomorphism_320 -> AgdaAny Source #

d_cong_764 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_768 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_770 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_772 :: T_IsMonoidMonomorphism_288 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_774 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_774 :: (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_776 :: T_IsMonoidMonomorphism_288 -> T_IsMonoidHomomorphism_266 Source #

d_isRelHomomorphism_778 :: T_IsMonoidMonomorphism_288 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_780 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_780 :: T_IsMonoidMonomorphism_288 -> T_IsRelMonomorphism_64 Source #

d_ε'45'homo_782 :: T_IsMonoidMonomorphism_288 -> AgdaAny Source #

d_cong_784 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMagmaHomomorphism_788 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaIsomorphism_790 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaMonomorphism_792 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_796 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_798 :: T_IsMagmaHomomorphism_76 -> T_IsRelHomomorphism_42 Source #

d_cong_800 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_804 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_806 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_808 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_810 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaMonomorphism_94 Source #

d_isRelHomomorphism_812 :: T_IsMagmaIsomorphism_118 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_814 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_814 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_816 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_816 :: T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

d_surjective_818 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> T_Σ_14 Source #

d_cong_820 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_824 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_826 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_828 :: T_IsMagmaMonomorphism_94 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_830 :: T_IsMagmaMonomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_832 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_832 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_cong_834 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_Homomorphic'8322'_842 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Injective_852 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_860 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> () Source #

d_IsNearSemiringHomomorphism_864 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsNearSemiringHomomorphism_864 Source #

Constructors

C_IsNearSemiringHomomorphism'46'constructor_13157 T_IsMonoidHomomorphism_266 (AgdaAny -> AgdaAny -> AgdaAny)

d_'43''45'isMonoidHomomorphism_872 :: T_IsNearSemiringHomomorphism_864 -> T_IsMonoidHomomorphism_266 Source #

d_'42''45'homo_874 :: T_IsNearSemiringHomomorphism_864 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_878 :: T_IsNearSemiringHomomorphism_864 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_880 :: T_IsNearSemiringHomomorphism_864 -> T_IsMagmaHomomorphism_76 Source #

d_ε'45'homo_882 :: T_IsNearSemiringHomomorphism_864 -> AgdaAny Source #

d_isRelHomomorphism_884 :: T_IsNearSemiringHomomorphism_864 -> T_IsRelHomomorphism_42 Source #

d_cong_886 :: T_IsNearSemiringHomomorphism_864 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_888 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringHomomorphism_864 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_888 :: T_IsNearSemiringHomomorphism_864 -> T_IsMagmaHomomorphism_76 Source #

d_IsNearSemiringMonomorphism_892 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsNearSemiringMonomorphism_892 Source #

Constructors

C_IsNearSemiringMonomorphism'46'constructor_13899 T_IsNearSemiringHomomorphism_864 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isNearSemiringHomomorphism_900 :: T_IsNearSemiringMonomorphism_892 -> T_IsNearSemiringHomomorphism_864 Source #

d_injective_902 :: T_IsNearSemiringMonomorphism_892 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'homo_906 :: T_IsNearSemiringMonomorphism_892 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_908 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_908 :: T_IsNearSemiringMonomorphism_892 -> T_IsMagmaHomomorphism_76 Source #

d_homo_910 :: T_IsNearSemiringMonomorphism_892 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_912 :: T_IsNearSemiringMonomorphism_892 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_914 :: T_IsNearSemiringMonomorphism_892 -> T_IsMonoidHomomorphism_266 Source #

d_ε'45'homo_916 :: T_IsNearSemiringMonomorphism_892 -> AgdaAny Source #

d_isRelHomomorphism_918 :: T_IsNearSemiringMonomorphism_892 -> T_IsRelHomomorphism_42 Source #

d_cong_920 :: T_IsNearSemiringMonomorphism_892 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'43''45'isMonoidMonomorphism_922 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsMonoidMonomorphism_288 Source #

du_'43''45'isMonoidMonomorphism_922 :: T_IsNearSemiringMonomorphism_892 -> T_IsMonoidMonomorphism_288 Source #

d_isMagmaMonomorphism_926 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_926 :: T_IsNearSemiringMonomorphism_892 -> T_IsMagmaMonomorphism_94 Source #

d_isRelMonomorphism_928 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_928 :: T_IsNearSemiringMonomorphism_892 -> T_IsRelMonomorphism_64 Source #

d_'42''45'isMagmaMonomorphism_930 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsMagmaMonomorphism_94 Source #

du_'42''45'isMagmaMonomorphism_930 :: T_IsNearSemiringMonomorphism_892 -> T_IsMagmaMonomorphism_94 Source #

d_IsNearSemiringIsomorphism_934 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsNearSemiringIsomorphism_934 Source #

Constructors

C_IsNearSemiringIsomorphism'46'constructor_15287 T_IsNearSemiringMonomorphism_892 (AgdaAny -> T_Σ_14)

d_isNearSemiringMonomorphism_942 :: T_IsNearSemiringIsomorphism_934 -> T_IsNearSemiringMonomorphism_892 Source #

d_surjective_944 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny -> T_Σ_14 Source #

d_'42''45'homo_948 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_950 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_950 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaHomomorphism_76 Source #

d_'42''45'isMagmaMonomorphism_952 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaMonomorphism_94 Source #

du_'42''45'isMagmaMonomorphism_952 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaMonomorphism_94 Source #

d_homo_954 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_956 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_958 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_958 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaMonomorphism_94 Source #

d_'43''45'isMonoidHomomorphism_960 :: T_IsNearSemiringIsomorphism_934 -> T_IsMonoidHomomorphism_266 Source #

d_'43''45'isMonoidMonomorphism_962 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMonoidMonomorphism_288 Source #

du_'43''45'isMonoidMonomorphism_962 :: T_IsNearSemiringIsomorphism_934 -> T_IsMonoidMonomorphism_288 Source #

d_ε'45'homo_964 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny Source #

d_injective_966 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isNearSemiringHomomorphism_968 :: T_IsNearSemiringIsomorphism_934 -> T_IsNearSemiringHomomorphism_864 Source #

d_isRelHomomorphism_970 :: T_IsNearSemiringIsomorphism_934 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_972 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_972 :: T_IsNearSemiringIsomorphism_934 -> T_IsRelMonomorphism_64 Source #

d_cong_974 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'43''45'isMonoidIsomorphism_976 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMonoidIsomorphism_320 Source #

du_'43''45'isMonoidIsomorphism_976 :: T_IsNearSemiringIsomorphism_934 -> T_IsMonoidIsomorphism_320 Source #

d_isMagmaIsomorphism_980 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_980 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaIsomorphism_118 Source #

d_isRelIsomorphism_982 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_982 :: T_IsNearSemiringIsomorphism_934 -> T_IsRelIsomorphism_94 Source #

d_'42''45'isMagmaIsomorphism_984 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawNearSemiring_1304 -> T_RawNearSemiring_1304 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaIsomorphism_118 Source #

du_'42''45'isMagmaIsomorphism_984 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaIsomorphism_118 Source #

d_1'35'_1020 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> AgdaAny Source #

du_1'35'_1020 :: T_RawSemiring_1672 -> AgdaAny Source #

d_Carrier_1022 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> () Source #

d_IsMonoidHomomorphism_1054 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMonoidIsomorphism_1056 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMonoidMonomorphism_1058 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_1062 :: T_IsMonoidHomomorphism_266 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1064 :: T_IsMonoidHomomorphism_266 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_1066 :: T_IsMonoidHomomorphism_266 -> T_IsRelHomomorphism_42 Source #

d_ε'45'homo_1068 :: T_IsMonoidHomomorphism_266 -> AgdaAny Source #

d_cong_1070 :: T_IsMonoidHomomorphism_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_1074 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_1076 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1078 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaIsomorphism_1080 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_1080 :: (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaIsomorphism_118 Source #

d_isMagmaMonomorphism_1082 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1082 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_1084 :: T_IsMonoidIsomorphism_320 -> T_IsMonoidHomomorphism_266 Source #

d_isMonoidMonomorphism_1086 :: T_IsMonoidIsomorphism_320 -> T_IsMonoidMonomorphism_288 Source #

d_isRelHomomorphism_1088 :: T_IsMonoidIsomorphism_320 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1090 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1090 :: T_IsMonoidIsomorphism_320 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_1092 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1092 :: T_IsMonoidIsomorphism_320 -> T_IsRelMonomorphism_64 Source #

d_surjective_1094 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> T_Σ_14 Source #

d_ε'45'homo_1096 :: T_IsMonoidIsomorphism_320 -> AgdaAny Source #

d_cong_1098 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_1102 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_1104 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1106 :: T_IsMonoidMonomorphism_288 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_1108 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1108 :: (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_1110 :: T_IsMonoidMonomorphism_288 -> T_IsMonoidHomomorphism_266 Source #

d_isRelHomomorphism_1112 :: T_IsMonoidMonomorphism_288 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1114 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1114 :: T_IsMonoidMonomorphism_288 -> T_IsRelMonomorphism_64 Source #

d_ε'45'homo_1116 :: T_IsMonoidMonomorphism_288 -> AgdaAny Source #

d_cong_1118 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_Homomorphic'8320'_1122 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Injective_1136 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_1144 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> () Source #

d_IsNearSemiringHomomorphism_1148 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsNearSemiringIsomorphism_1150 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsNearSemiringMonomorphism_1152 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_'42''45'homo_1156 :: T_IsNearSemiringHomomorphism_864 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1158 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringHomomorphism_864 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1158 :: (AgdaAny -> AgdaAny) -> T_IsNearSemiringHomomorphism_864 -> T_IsMagmaHomomorphism_76 Source #

d_homo_1160 :: T_IsNearSemiringHomomorphism_864 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1162 :: T_IsNearSemiringHomomorphism_864 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_1164 :: T_IsNearSemiringHomomorphism_864 -> T_IsMonoidHomomorphism_266 Source #

d_ε'45'homo_1166 :: T_IsNearSemiringHomomorphism_864 -> AgdaAny Source #

d_isRelHomomorphism_1168 :: T_IsNearSemiringHomomorphism_864 -> T_IsRelHomomorphism_42 Source #

d_cong_1170 :: T_IsNearSemiringHomomorphism_864 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'homo_1174 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1176 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1176 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaHomomorphism_76 Source #

d_'42''45'isMagmaIsomorphism_1178 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaIsomorphism_118 Source #

du_'42''45'isMagmaIsomorphism_1178 :: (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaIsomorphism_118 Source #

d_'42''45'isMagmaMonomorphism_1180 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaMonomorphism_94 Source #

du_'42''45'isMagmaMonomorphism_1180 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaMonomorphism_94 Source #

d_homo_1182 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1184 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaIsomorphism_1186 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_1186 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaIsomorphism_118 Source #

d_isMagmaMonomorphism_1188 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1188 :: T_IsNearSemiringIsomorphism_934 -> T_IsMagmaMonomorphism_94 Source #

d_'43''45'isMonoidHomomorphism_1190 :: T_IsNearSemiringIsomorphism_934 -> T_IsMonoidHomomorphism_266 Source #

d_'43''45'isMonoidIsomorphism_1192 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMonoidIsomorphism_320 Source #

du_'43''45'isMonoidIsomorphism_1192 :: (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMonoidIsomorphism_320 Source #

d_'43''45'isMonoidMonomorphism_1194 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsMonoidMonomorphism_288 Source #

du_'43''45'isMonoidMonomorphism_1194 :: T_IsNearSemiringIsomorphism_934 -> T_IsMonoidMonomorphism_288 Source #

d_ε'45'homo_1196 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny Source #

d_injective_1198 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isNearSemiringHomomorphism_1200 :: T_IsNearSemiringIsomorphism_934 -> T_IsNearSemiringHomomorphism_864 Source #

d_isNearSemiringMonomorphism_1202 :: T_IsNearSemiringIsomorphism_934 -> T_IsNearSemiringMonomorphism_892 Source #

d_isRelHomomorphism_1204 :: T_IsNearSemiringIsomorphism_934 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1206 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1206 :: T_IsNearSemiringIsomorphism_934 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_1208 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_934 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1208 :: T_IsNearSemiringIsomorphism_934 -> T_IsRelMonomorphism_64 Source #

d_surjective_1210 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny -> T_Σ_14 Source #

d_cong_1212 :: T_IsNearSemiringIsomorphism_934 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'homo_1216 :: T_IsNearSemiringMonomorphism_892 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1218 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1218 :: T_IsNearSemiringMonomorphism_892 -> T_IsMagmaHomomorphism_76 Source #

d_'42''45'isMagmaMonomorphism_1220 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsMagmaMonomorphism_94 Source #

du_'42''45'isMagmaMonomorphism_1220 :: (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsMagmaMonomorphism_94 Source #

d_homo_1222 :: T_IsNearSemiringMonomorphism_892 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1224 :: T_IsNearSemiringMonomorphism_892 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_1226 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1226 :: T_IsNearSemiringMonomorphism_892 -> T_IsMagmaMonomorphism_94 Source #

d_'43''45'isMonoidHomomorphism_1228 :: T_IsNearSemiringMonomorphism_892 -> T_IsMonoidHomomorphism_266 Source #

d_'43''45'isMonoidMonomorphism_1230 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsMonoidMonomorphism_288 Source #

du_'43''45'isMonoidMonomorphism_1230 :: (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsMonoidMonomorphism_288 Source #

d_ε'45'homo_1232 :: T_IsNearSemiringMonomorphism_892 -> AgdaAny Source #

d_injective_1234 :: T_IsNearSemiringMonomorphism_892 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isNearSemiringHomomorphism_1236 :: T_IsNearSemiringMonomorphism_892 -> T_IsNearSemiringHomomorphism_864 Source #

d_isRelHomomorphism_1238 :: T_IsNearSemiringMonomorphism_892 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1240 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_892 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1240 :: T_IsNearSemiringMonomorphism_892 -> T_IsRelMonomorphism_64 Source #

d_cong_1242 :: T_IsNearSemiringMonomorphism_892 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsSemiringHomomorphism_1246 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsSemiringHomomorphism_1246 Source #

Constructors

C_IsSemiringHomomorphism'46'constructor_18773 T_IsNearSemiringHomomorphism_864 AgdaAny

d_isNearSemiringHomomorphism_1254 :: T_IsSemiringHomomorphism_1246 -> T_IsNearSemiringHomomorphism_864 Source #

d_1'35''45'homo_1256 :: T_IsSemiringHomomorphism_1246 -> AgdaAny Source #

d_'42''45'homo_1260 :: T_IsSemiringHomomorphism_1246 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1262 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1246 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1262 :: T_IsSemiringHomomorphism_1246 -> T_IsMagmaHomomorphism_76 Source #

d_homo_1264 :: T_IsSemiringHomomorphism_1246 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1266 :: T_IsSemiringHomomorphism_1246 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_1268 :: T_IsSemiringHomomorphism_1246 -> T_IsMonoidHomomorphism_266 Source #

d_ε'45'homo_1270 :: T_IsSemiringHomomorphism_1246 -> AgdaAny Source #

d_isRelHomomorphism_1272 :: T_IsSemiringHomomorphism_1246 -> T_IsRelHomomorphism_42 Source #

d_cong_1274 :: T_IsSemiringHomomorphism_1246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMonoidHomomorphism_1276 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1246 -> T_IsMonoidHomomorphism_266 Source #

du_'42''45'isMonoidHomomorphism_1276 :: T_IsSemiringHomomorphism_1246 -> T_IsMonoidHomomorphism_266 Source #

d_IsSemiringMonomorphism_1280 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsSemiringMonomorphism_1280 Source #

Constructors

C_IsSemiringMonomorphism'46'constructor_19695 T_IsSemiringHomomorphism_1246 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isSemiringHomomorphism_1288 :: T_IsSemiringMonomorphism_1280 -> T_IsSemiringHomomorphism_1246 Source #

d_injective_1290 :: T_IsSemiringMonomorphism_1280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'homo_1294 :: T_IsSemiringMonomorphism_1280 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1296 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1296 :: T_IsSemiringMonomorphism_1280 -> T_IsMagmaHomomorphism_76 Source #

d_'42''45'isMonoidHomomorphism_1298 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMonoidHomomorphism_266 Source #

du_'42''45'isMonoidHomomorphism_1298 :: T_IsSemiringMonomorphism_1280 -> T_IsMonoidHomomorphism_266 Source #

d_homo_1300 :: T_IsSemiringMonomorphism_1280 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1302 :: T_IsSemiringMonomorphism_1280 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_1304 :: T_IsSemiringMonomorphism_1280 -> T_IsMonoidHomomorphism_266 Source #

d_ε'45'homo_1306 :: T_IsSemiringMonomorphism_1280 -> AgdaAny Source #

d_1'35''45'homo_1308 :: T_IsSemiringMonomorphism_1280 -> AgdaAny Source #

d_isNearSemiringHomomorphism_1310 :: T_IsSemiringMonomorphism_1280 -> T_IsNearSemiringHomomorphism_864 Source #

d_isRelHomomorphism_1312 :: T_IsSemiringMonomorphism_1280 -> T_IsRelHomomorphism_42 Source #

d_cong_1314 :: T_IsSemiringMonomorphism_1280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isNearSemiringMonomorphism_1316 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsNearSemiringMonomorphism_892 Source #

du_isNearSemiringMonomorphism_1316 :: T_IsSemiringMonomorphism_1280 -> T_IsNearSemiringMonomorphism_892 Source #

d_'42''45'isMagmaMonomorphism_1320 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMagmaMonomorphism_94 Source #

du_'42''45'isMagmaMonomorphism_1320 :: T_IsSemiringMonomorphism_1280 -> T_IsMagmaMonomorphism_94 Source #

d_'43''45'isMonoidMonomorphism_1322 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMonoidMonomorphism_288 Source #

du_'43''45'isMonoidMonomorphism_1322 :: T_IsSemiringMonomorphism_1280 -> T_IsMonoidMonomorphism_288 Source #

d_'42''45'isMonoidMonomorphism_1324 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMonoidMonomorphism_288 Source #

du_'42''45'isMonoidMonomorphism_1324 :: T_IsSemiringMonomorphism_1280 -> T_IsMonoidMonomorphism_288 Source #

d_IsSemiringIsomorphism_1328 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsSemiringIsomorphism_1328 Source #

Constructors

C_IsSemiringIsomorphism'46'constructor_21255 T_IsSemiringMonomorphism_1280 (AgdaAny -> T_Σ_14)

d_isSemiringMonomorphism_1336 :: T_IsSemiringIsomorphism_1328 -> T_IsSemiringMonomorphism_1280 Source #

d_surjective_1338 :: T_IsSemiringIsomorphism_1328 -> AgdaAny -> T_Σ_14 Source #

d_'42''45'homo_1342 :: T_IsSemiringIsomorphism_1328 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1344 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1344 :: T_IsSemiringIsomorphism_1328 -> T_IsMagmaHomomorphism_76 Source #

d_'42''45'isMagmaMonomorphism_1346 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMagmaMonomorphism_94 Source #

du_'42''45'isMagmaMonomorphism_1346 :: T_IsSemiringIsomorphism_1328 -> T_IsMagmaMonomorphism_94 Source #

d_'42''45'isMonoidHomomorphism_1348 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidHomomorphism_266 Source #

du_'42''45'isMonoidHomomorphism_1348 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidHomomorphism_266 Source #

d_'42''45'isMonoidMonomorphism_1350 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidMonomorphism_288 Source #

du_'42''45'isMonoidMonomorphism_1350 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidMonomorphism_288 Source #

d_homo_1352 :: T_IsSemiringIsomorphism_1328 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1354 :: T_IsSemiringIsomorphism_1328 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_1356 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidHomomorphism_266 Source #

d_'43''45'isMonoidMonomorphism_1358 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidMonomorphism_288 Source #

du_'43''45'isMonoidMonomorphism_1358 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidMonomorphism_288 Source #

d_ε'45'homo_1360 :: T_IsSemiringIsomorphism_1328 -> AgdaAny Source #

d_1'35''45'homo_1362 :: T_IsSemiringIsomorphism_1328 -> AgdaAny Source #

d_injective_1364 :: T_IsSemiringIsomorphism_1328 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isNearSemiringHomomorphism_1366 :: T_IsSemiringIsomorphism_1328 -> T_IsNearSemiringHomomorphism_864 Source #

d_isNearSemiringMonomorphism_1368 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsNearSemiringMonomorphism_892 Source #

du_isNearSemiringMonomorphism_1368 :: T_IsSemiringIsomorphism_1328 -> T_IsNearSemiringMonomorphism_892 Source #

d_isRelHomomorphism_1370 :: T_IsSemiringIsomorphism_1328 -> T_IsRelHomomorphism_42 Source #

d_isSemiringHomomorphism_1372 :: T_IsSemiringIsomorphism_1328 -> T_IsSemiringHomomorphism_1246 Source #

d_cong_1374 :: T_IsSemiringIsomorphism_1328 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isNearSemiringIsomorphism_1376 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsNearSemiringIsomorphism_934 Source #

du_isNearSemiringIsomorphism_1376 :: T_IsSemiringIsomorphism_1328 -> T_IsNearSemiringIsomorphism_934 Source #

d_'42''45'isMagmaIsomorphism_1380 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMagmaIsomorphism_118 Source #

du_'42''45'isMagmaIsomorphism_1380 :: T_IsSemiringIsomorphism_1328 -> T_IsMagmaIsomorphism_118 Source #

d_'43''45'isMonoidIsomorphism_1382 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidIsomorphism_320 Source #

du_'43''45'isMonoidIsomorphism_1382 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidIsomorphism_320 Source #

d_'42''45'isMonoidIsomorphism_1384 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> T_RawSemiring_1672 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidIsomorphism_320 Source #

du_'42''45'isMonoidIsomorphism_1384 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidIsomorphism_320 Source #

d_'45'__1420 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> AgdaAny -> AgdaAny Source #

du_'45'__1420 :: T_RawRing_2558 -> AgdaAny -> AgdaAny Source #

d_Carrier_1426 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> () Source #

d_IsGroupHomomorphism_1462 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsGroupIsomorphism_1464 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsGroupMonomorphism_1466 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_1470 :: T_IsGroupHomomorphism_554 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1472 :: T_IsGroupHomomorphism_554 -> T_IsMagmaHomomorphism_76 Source #

d_isMonoidHomomorphism_1474 :: T_IsGroupHomomorphism_554 -> T_IsMonoidHomomorphism_266 Source #

d_isRelHomomorphism_1476 :: T_IsGroupHomomorphism_554 -> T_IsRelHomomorphism_42 Source #

d_ε'45'homo_1478 :: T_IsGroupHomomorphism_554 -> AgdaAny Source #

d_'8315''185''45'homo_1480 :: T_IsGroupHomomorphism_554 -> AgdaAny -> AgdaAny Source #

d_cong_1482 :: T_IsGroupHomomorphism_554 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_1486 :: T_IsGroupIsomorphism_618 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isGroupHomomorphism_1488 :: T_IsGroupIsomorphism_618 -> T_IsGroupHomomorphism_554 Source #

d_isGroupMonomorphism_1490 :: T_IsGroupIsomorphism_618 -> T_IsGroupMonomorphism_580 Source #

d_isMagmaHomomorphism_1492 :: T_IsGroupIsomorphism_618 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaIsomorphism_1494 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_1494 :: T_IsGroupIsomorphism_618 -> T_IsMagmaIsomorphism_118 Source #

d_isMagmaMonomorphism_1496 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1496 :: T_IsGroupIsomorphism_618 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_1498 :: T_IsGroupIsomorphism_618 -> T_IsMonoidHomomorphism_266 Source #

d_isMonoidIsomorphism_1500 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsMonoidIsomorphism_320 Source #

du_isMonoidIsomorphism_1500 :: (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsMonoidIsomorphism_320 Source #

d_isMonoidMonomorphism_1502 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsMonoidMonomorphism_288 Source #

du_isMonoidMonomorphism_1502 :: T_IsGroupIsomorphism_618 -> T_IsMonoidMonomorphism_288 Source #

d_isRelHomomorphism_1504 :: T_IsGroupIsomorphism_618 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1506 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1506 :: T_IsGroupIsomorphism_618 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_1508 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_618 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1508 :: T_IsGroupIsomorphism_618 -> T_IsRelMonomorphism_64 Source #

d_surjective_1510 :: T_IsGroupIsomorphism_618 -> AgdaAny -> T_Σ_14 Source #

d_ε'45'homo_1512 :: T_IsGroupIsomorphism_618 -> AgdaAny Source #

d_'8315''185''45'homo_1514 :: T_IsGroupIsomorphism_618 -> AgdaAny -> AgdaAny Source #

d_homo_1516 :: T_IsGroupIsomorphism_618 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_1518 :: T_IsGroupIsomorphism_618 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_1522 :: T_IsGroupMonomorphism_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isGroupHomomorphism_1524 :: T_IsGroupMonomorphism_580 -> T_IsGroupHomomorphism_554 Source #

d_isMagmaHomomorphism_1526 :: T_IsGroupMonomorphism_580 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_1528 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_580 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1528 :: T_IsGroupMonomorphism_580 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_1530 :: T_IsGroupMonomorphism_580 -> T_IsMonoidHomomorphism_266 Source #

d_isMonoidMonomorphism_1532 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_580 -> T_IsMonoidMonomorphism_288 Source #

du_isMonoidMonomorphism_1532 :: (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_580 -> T_IsMonoidMonomorphism_288 Source #

d_isRelHomomorphism_1534 :: T_IsGroupMonomorphism_580 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1536 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_580 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1536 :: T_IsGroupMonomorphism_580 -> T_IsRelMonomorphism_64 Source #

d_ε'45'homo_1538 :: T_IsGroupMonomorphism_580 -> AgdaAny Source #

d_'8315''185''45'homo_1540 :: T_IsGroupMonomorphism_580 -> AgdaAny -> AgdaAny Source #

d_homo_1542 :: T_IsGroupMonomorphism_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_1544 :: T_IsGroupMonomorphism_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMonoidHomomorphism_1548 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMonoidIsomorphism_1550 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMonoidMonomorphism_1552 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_1556 :: T_IsMonoidHomomorphism_266 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1558 :: T_IsMonoidHomomorphism_266 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_1560 :: T_IsMonoidHomomorphism_266 -> T_IsRelHomomorphism_42 Source #

d_ε'45'homo_1562 :: T_IsMonoidHomomorphism_266 -> AgdaAny Source #

d_cong_1564 :: T_IsMonoidHomomorphism_266 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_1568 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_1570 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1572 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaIsomorphism_1574 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_1574 :: (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaIsomorphism_118 Source #

d_isMagmaMonomorphism_1576 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1576 :: T_IsMonoidIsomorphism_320 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_1578 :: T_IsMonoidIsomorphism_320 -> T_IsMonoidHomomorphism_266 Source #

d_isMonoidMonomorphism_1580 :: T_IsMonoidIsomorphism_320 -> T_IsMonoidMonomorphism_288 Source #

d_isRelHomomorphism_1582 :: T_IsMonoidIsomorphism_320 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_1584 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1584 :: T_IsMonoidIsomorphism_320 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_1586 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_320 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1586 :: T_IsMonoidIsomorphism_320 -> T_IsRelMonomorphism_64 Source #

d_surjective_1588 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> T_Σ_14 Source #

d_ε'45'homo_1590 :: T_IsMonoidIsomorphism_320 -> AgdaAny Source #

d_cong_1592 :: T_IsMonoidIsomorphism_320 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_1596 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_1598 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1600 :: T_IsMonoidMonomorphism_288 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_1602 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1602 :: (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidHomomorphism_1604 :: T_IsMonoidMonomorphism_288 -> T_IsMonoidHomomorphism_266 Source #

d_isRelHomomorphism_1606 :: T_IsMonoidMonomorphism_288 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_1608 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_288 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1608 :: T_IsMonoidMonomorphism_288 -> T_IsRelMonomorphism_64 Source #

d_ε'45'homo_1610 :: T_IsMonoidMonomorphism_288 -> AgdaAny Source #

d_cong_1612 :: T_IsMonoidMonomorphism_288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_Homomorphic'8321'_1618 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Injective_1630 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_1638 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> () Source #

d_IsSemiringHomomorphism_1642 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsSemiringIsomorphism_1644 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsSemiringMonomorphism_1646 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_'42''45'homo_1650 :: T_IsSemiringHomomorphism_1246 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1652 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1246 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1652 :: T_IsSemiringHomomorphism_1246 -> T_IsMagmaHomomorphism_76 Source #

d_'42''45'isMonoidHomomorphism_1654 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1246 -> T_IsMonoidHomomorphism_266 Source #

du_'42''45'isMonoidHomomorphism_1654 :: (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1246 -> T_IsMonoidHomomorphism_266 Source #

d_homo_1656 :: T_IsSemiringHomomorphism_1246 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1658 :: T_IsSemiringHomomorphism_1246 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_1660 :: T_IsSemiringHomomorphism_1246 -> T_IsMonoidHomomorphism_266 Source #

d_ε'45'homo_1662 :: T_IsSemiringHomomorphism_1246 -> AgdaAny Source #

d_1'35''45'homo_1664 :: T_IsSemiringHomomorphism_1246 -> AgdaAny Source #

d_isNearSemiringHomomorphism_1666 :: T_IsSemiringHomomorphism_1246 -> T_IsNearSemiringHomomorphism_864 Source #

d_isRelHomomorphism_1668 :: T_IsSemiringHomomorphism_1246 -> T_IsRelHomomorphism_42 Source #

d_cong_1670 :: T_IsSemiringHomomorphism_1246 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'homo_1674 :: T_IsSemiringIsomorphism_1328 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1676 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1676 :: T_IsSemiringIsomorphism_1328 -> T_IsMagmaHomomorphism_76 Source #

d_'42''45'isMagmaIsomorphism_1678 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMagmaIsomorphism_118 Source #

du_'42''45'isMagmaIsomorphism_1678 :: T_IsSemiringIsomorphism_1328 -> T_IsMagmaIsomorphism_118 Source #

d_'42''45'isMagmaMonomorphism_1680 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMagmaMonomorphism_94 Source #

du_'42''45'isMagmaMonomorphism_1680 :: T_IsSemiringIsomorphism_1328 -> T_IsMagmaMonomorphism_94 Source #

d_'42''45'isMonoidHomomorphism_1682 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidHomomorphism_266 Source #

du_'42''45'isMonoidHomomorphism_1682 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidHomomorphism_266 Source #

d_'42''45'isMonoidIsomorphism_1684 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidIsomorphism_320 Source #

du_'42''45'isMonoidIsomorphism_1684 :: (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidIsomorphism_320 Source #

d_'42''45'isMonoidMonomorphism_1686 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidMonomorphism_288 Source #

du_'42''45'isMonoidMonomorphism_1686 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidMonomorphism_288 Source #

d_homo_1688 :: T_IsSemiringIsomorphism_1328 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1690 :: T_IsSemiringIsomorphism_1328 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_1692 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidHomomorphism_266 Source #

d_'43''45'isMonoidIsomorphism_1694 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidIsomorphism_320 Source #

du_'43''45'isMonoidIsomorphism_1694 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidIsomorphism_320 Source #

d_'43''45'isMonoidMonomorphism_1696 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsMonoidMonomorphism_288 Source #

du_'43''45'isMonoidMonomorphism_1696 :: T_IsSemiringIsomorphism_1328 -> T_IsMonoidMonomorphism_288 Source #

d_ε'45'homo_1698 :: T_IsSemiringIsomorphism_1328 -> AgdaAny Source #

d_1'35''45'homo_1700 :: T_IsSemiringIsomorphism_1328 -> AgdaAny Source #

d_injective_1702 :: T_IsSemiringIsomorphism_1328 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isNearSemiringHomomorphism_1704 :: T_IsSemiringIsomorphism_1328 -> T_IsNearSemiringHomomorphism_864 Source #

d_isNearSemiringIsomorphism_1706 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsNearSemiringIsomorphism_934 Source #

du_isNearSemiringIsomorphism_1706 :: (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsNearSemiringIsomorphism_934 Source #

d_isNearSemiringMonomorphism_1708 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1328 -> T_IsNearSemiringMonomorphism_892 Source #

du_isNearSemiringMonomorphism_1708 :: T_IsSemiringIsomorphism_1328 -> T_IsNearSemiringMonomorphism_892 Source #

d_isRelHomomorphism_1710 :: T_IsSemiringIsomorphism_1328 -> T_IsRelHomomorphism_42 Source #

d_isSemiringHomomorphism_1712 :: T_IsSemiringIsomorphism_1328 -> T_IsSemiringHomomorphism_1246 Source #

d_isSemiringMonomorphism_1714 :: T_IsSemiringIsomorphism_1328 -> T_IsSemiringMonomorphism_1280 Source #

d_surjective_1716 :: T_IsSemiringIsomorphism_1328 -> AgdaAny -> T_Σ_14 Source #

d_cong_1718 :: T_IsSemiringIsomorphism_1328 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'homo_1722 :: T_IsSemiringMonomorphism_1280 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1724 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1724 :: T_IsSemiringMonomorphism_1280 -> T_IsMagmaHomomorphism_76 Source #

d_'42''45'isMagmaMonomorphism_1726 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMagmaMonomorphism_94 Source #

du_'42''45'isMagmaMonomorphism_1726 :: T_IsSemiringMonomorphism_1280 -> T_IsMagmaMonomorphism_94 Source #

d_'42''45'isMonoidHomomorphism_1728 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMonoidHomomorphism_266 Source #

du_'42''45'isMonoidHomomorphism_1728 :: T_IsSemiringMonomorphism_1280 -> T_IsMonoidHomomorphism_266 Source #

d_'42''45'isMonoidMonomorphism_1730 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMonoidMonomorphism_288 Source #

du_'42''45'isMonoidMonomorphism_1730 :: (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMonoidMonomorphism_288 Source #

d_homo_1732 :: T_IsSemiringMonomorphism_1280 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1734 :: T_IsSemiringMonomorphism_1280 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_1736 :: T_IsSemiringMonomorphism_1280 -> T_IsMonoidHomomorphism_266 Source #

d_'43''45'isMonoidMonomorphism_1738 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsMonoidMonomorphism_288 Source #

du_'43''45'isMonoidMonomorphism_1738 :: T_IsSemiringMonomorphism_1280 -> T_IsMonoidMonomorphism_288 Source #

d_ε'45'homo_1740 :: T_IsSemiringMonomorphism_1280 -> AgdaAny Source #

d_1'35''45'homo_1742 :: T_IsSemiringMonomorphism_1280 -> AgdaAny Source #

d_injective_1744 :: T_IsSemiringMonomorphism_1280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isNearSemiringHomomorphism_1746 :: T_IsSemiringMonomorphism_1280 -> T_IsNearSemiringHomomorphism_864 Source #

d_isNearSemiringMonomorphism_1748 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsNearSemiringMonomorphism_892 Source #

du_isNearSemiringMonomorphism_1748 :: (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1280 -> T_IsNearSemiringMonomorphism_892 Source #

d_isRelHomomorphism_1750 :: T_IsSemiringMonomorphism_1280 -> T_IsRelHomomorphism_42 Source #

d_isSemiringHomomorphism_1752 :: T_IsSemiringMonomorphism_1280 -> T_IsSemiringHomomorphism_1246 Source #

d_cong_1754 :: T_IsSemiringMonomorphism_1280 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsRingHomomorphism_1758 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsRingHomomorphism_1758 Source #

Constructors

C_IsRingHomomorphism'46'constructor_25779 T_IsSemiringHomomorphism_1246 (AgdaAny -> AgdaAny)

d_isSemiringHomomorphism_1766 :: T_IsRingHomomorphism_1758 -> T_IsSemiringHomomorphism_1246 Source #

d_'45''8255'homo_1768 :: T_IsRingHomomorphism_1758 -> AgdaAny -> AgdaAny Source #

d_'42''45'homo_1772 :: T_IsRingHomomorphism_1758 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1774 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingHomomorphism_1758 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1774 :: T_IsRingHomomorphism_1758 -> T_IsMagmaHomomorphism_76 Source #

d_'42''45'isMonoidHomomorphism_1776 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingHomomorphism_1758 -> T_IsMonoidHomomorphism_266 Source #

du_'42''45'isMonoidHomomorphism_1776 :: T_IsRingHomomorphism_1758 -> T_IsMonoidHomomorphism_266 Source #

d_homo_1778 :: T_IsRingHomomorphism_1758 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_1780 :: T_IsRingHomomorphism_1758 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_1782 :: T_IsRingHomomorphism_1758 -> T_IsMonoidHomomorphism_266 Source #

d_ε'45'homo_1784 :: T_IsRingHomomorphism_1758 -> AgdaAny Source #

d_1'35''45'homo_1786 :: T_IsRingHomomorphism_1758 -> AgdaAny Source #

d_isNearSemiringHomomorphism_1788 :: T_IsRingHomomorphism_1758 -> T_IsNearSemiringHomomorphism_864 Source #

d_isRelHomomorphism_1790 :: T_IsRingHomomorphism_1758 -> T_IsRelHomomorphism_42 Source #

d_cong_1792 :: T_IsRingHomomorphism_1758 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'43''45'isGroupHomomorphism_1794 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingHomomorphism_1758 -> T_IsGroupHomomorphism_554 Source #

du_'43''45'isGroupHomomorphism_1794 :: T_IsRingHomomorphism_1758 -> T_IsGroupHomomorphism_554 Source #

d_IsRingMonomorphism_1798 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsRingMonomorphism_1798 Source #

Constructors

C_IsRingMonomorphism'46'constructor_26877 T_IsRingHomomorphism_1758 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isRingHomomorphism_1806 :: T_IsRingMonomorphism_1798 -> T_IsRingHomomorphism_1758 Source #

d_injective_1808 :: T_IsRingMonomorphism_1798 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'homo_1812 :: T_IsRingMonomorphism_1798 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1814 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_1798 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1814 :: T_IsRingMonomorphism_1798 -> T_IsMagmaHomomorphism_76 Source #

d_'42''45'isMonoidHomomorphism_1816 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_1798 -> T_IsMonoidHomomorphism_266 Source #

du_'42''45'isMonoidHomomorphism_1816 :: T_IsRingMonomorphism_1798 -> T_IsMonoidHomomorphism_266 Source #

d_homo_1818 :: T_IsRingMonomorphism_1798 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'43''45'isGroupHomomorphism_1820 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_1798 -> T_IsGroupHomomorphism_554 Source #

du_'43''45'isGroupHomomorphism_1820 :: T_IsRingMonomorphism_1798 -> T_IsGroupHomomorphism_554 Source #

d_isMagmaHomomorphism_1822 :: T_IsRingMonomorphism_1798 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_1824 :: T_IsRingMonomorphism_1798 -> T_IsMonoidHomomorphism_266 Source #

d_'45''8255'homo_1826 :: T_IsRingMonomorphism_1798 -> AgdaAny -> AgdaAny Source #

d_ε'45'homo_1828 :: T_IsRingMonomorphism_1798 -> AgdaAny Source #

d_1'35''45'homo_1830 :: T_IsRingMonomorphism_1798 -> AgdaAny Source #

d_isNearSemiringHomomorphism_1832 :: T_IsRingMonomorphism_1798 -> T_IsNearSemiringHomomorphism_864 Source #

d_isRelHomomorphism_1834 :: T_IsRingMonomorphism_1798 -> T_IsRelHomomorphism_42 Source #

d_isSemiringHomomorphism_1836 :: T_IsRingMonomorphism_1798 -> T_IsSemiringHomomorphism_1246 Source #

d_cong_1838 :: T_IsRingMonomorphism_1798 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isSemiringMonomorphism_1840 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_1798 -> T_IsSemiringMonomorphism_1280 Source #

du_isSemiringMonomorphism_1840 :: T_IsRingMonomorphism_1798 -> T_IsSemiringMonomorphism_1280 Source #

d_'43''45'isGroupMonomorphism_1842 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_1798 -> T_IsGroupMonomorphism_580 Source #

du_'43''45'isGroupMonomorphism_1842 :: T_IsRingMonomorphism_1798 -> T_IsGroupMonomorphism_580 Source #

d_isMagmaMonomorphism_1846 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_1798 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1846 :: T_IsRingMonomorphism_1798 -> T_IsMagmaMonomorphism_94 Source #

d_isMonoidMonomorphism_1848 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_1798 -> T_IsMonoidMonomorphism_288 Source #

du_isMonoidMonomorphism_1848 :: T_IsRingMonomorphism_1798 -> T_IsMonoidMonomorphism_288 Source #

d_isRelMonomorphism_1850 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_1798 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_1850 :: T_IsRingMonomorphism_1798 -> T_IsRelMonomorphism_64 Source #

d_'42''45'isMonoidMonomorphism_1852 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_1798 -> T_IsMonoidMonomorphism_288 Source #

du_'42''45'isMonoidMonomorphism_1852 :: T_IsRingMonomorphism_1798 -> T_IsMonoidMonomorphism_288 Source #

d_isMagmaMonomorphism_1856 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_1798 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1856 :: T_IsRingMonomorphism_1798 -> T_IsMagmaMonomorphism_94 Source #

d_IsRingIsomorphism_1860 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsRingIsomorphism_1860 Source #

Constructors

C_IsRingIsomorphism'46'constructor_28989 T_IsRingMonomorphism_1798 (AgdaAny -> T_Σ_14)

d_isRingMonomorphism_1868 :: T_IsRingIsomorphism_1860 -> T_IsRingMonomorphism_1798 Source #

d_surjective_1870 :: T_IsRingIsomorphism_1860 -> AgdaAny -> T_Σ_14 Source #

d_'42''45'homo_1874 :: T_IsRingIsomorphism_1860 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'42''45'isMagmaHomomorphism_1876 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsMagmaHomomorphism_76 Source #

du_'42''45'isMagmaHomomorphism_1876 :: T_IsRingIsomorphism_1860 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_1878 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsMagmaMonomorphism_94 Source #

du_isMagmaMonomorphism_1878 :: T_IsRingIsomorphism_1860 -> T_IsMagmaMonomorphism_94 Source #

d_'42''45'isMonoidHomomorphism_1880 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsMonoidHomomorphism_266 Source #

du_'42''45'isMonoidHomomorphism_1880 :: T_IsRingIsomorphism_1860 -> T_IsMonoidHomomorphism_266 Source #

d_'42''45'isMonoidMonomorphism_1882 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsMonoidMonomorphism_288 Source #

du_'42''45'isMonoidMonomorphism_1882 :: T_IsRingIsomorphism_1860 -> T_IsMonoidMonomorphism_288 Source #

d_homo_1884 :: T_IsRingIsomorphism_1860 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'43''45'isGroupHomomorphism_1886 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsGroupHomomorphism_554 Source #

du_'43''45'isGroupHomomorphism_1886 :: T_IsRingIsomorphism_1860 -> T_IsGroupHomomorphism_554 Source #

d_'43''45'isGroupMonomorphism_1888 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsGroupMonomorphism_580 Source #

du_'43''45'isGroupMonomorphism_1888 :: T_IsRingIsomorphism_1860 -> T_IsGroupMonomorphism_580 Source #

d_isMagmaHomomorphism_1890 :: T_IsRingIsomorphism_1860 -> T_IsMagmaHomomorphism_76 Source #

d_'43''45'isMonoidHomomorphism_1892 :: T_IsRingIsomorphism_1860 -> T_IsMonoidHomomorphism_266 Source #

d_'45''8255'homo_1894 :: T_IsRingIsomorphism_1860 -> AgdaAny -> AgdaAny Source #

d_ε'45'homo_1896 :: T_IsRingIsomorphism_1860 -> AgdaAny Source #

d_1'35''45'homo_1898 :: T_IsRingIsomorphism_1860 -> AgdaAny Source #

d_injective_1900 :: T_IsRingIsomorphism_1860 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isNearSemiringHomomorphism_1902 :: T_IsRingIsomorphism_1860 -> T_IsNearSemiringHomomorphism_864 Source #

d_isRelHomomorphism_1904 :: T_IsRingIsomorphism_1860 -> T_IsRelHomomorphism_42 Source #

d_isRingHomomorphism_1906 :: T_IsRingIsomorphism_1860 -> T_IsRingHomomorphism_1758 Source #

d_isSemiringHomomorphism_1908 :: T_IsRingIsomorphism_1860 -> T_IsSemiringHomomorphism_1246 Source #

d_isSemiringMonomorphism_1910 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsSemiringMonomorphism_1280 Source #

du_isSemiringMonomorphism_1910 :: T_IsRingIsomorphism_1860 -> T_IsSemiringMonomorphism_1280 Source #

d_cong_1912 :: T_IsRingIsomorphism_1860 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isSemiringIsomorphism_1914 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsSemiringIsomorphism_1328 Source #

du_isSemiringIsomorphism_1914 :: T_IsRingIsomorphism_1860 -> T_IsSemiringIsomorphism_1328 Source #

d_'43''45'isGroupIsomorphism_1916 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsGroupIsomorphism_618 Source #

du_'43''45'isGroupIsomorphism_1916 :: T_IsRingIsomorphism_1860 -> T_IsGroupIsomorphism_618 Source #

d_isMagmaIsomorphism_1920 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_1920 :: T_IsRingIsomorphism_1860 -> T_IsMagmaIsomorphism_118 Source #

d_isMonoidIsomorphism_1922 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsMonoidIsomorphism_320 Source #

du_isMonoidIsomorphism_1922 :: T_IsRingIsomorphism_1860 -> T_IsMonoidIsomorphism_320 Source #

d_isRelIsomorphism_1924 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_1924 :: T_IsRingIsomorphism_1860 -> T_IsRelIsomorphism_94 Source #

d_'42''45'isMonoidIsomorphism_1926 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsMonoidIsomorphism_320 Source #

du_'42''45'isMonoidIsomorphism_1926 :: T_IsRingIsomorphism_1860 -> T_IsMonoidIsomorphism_320 Source #

d_isMagmaIsomorphism_1930 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_RawRing_2558 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_1860 -> T_IsMagmaIsomorphism_118 Source #

du_isMagmaIsomorphism_1930 :: T_IsRingIsomorphism_1860 -> T_IsMagmaIsomorphism_118 Source #

d__'47''47'__1948 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'47''47'__1948 :: T_RawQuasigroup_3042 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'92''92'__1950 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'92''92'__1950 :: T_RawQuasigroup_3042 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8729'__1952 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'8729'__1952 :: T_RawQuasigroup_3042 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__1954 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_1960 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> () Source #

d_IsMagmaHomomorphism_1988 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaIsomorphism_1990 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaMonomorphism_1992 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_1996 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_1998 :: T_IsMagmaHomomorphism_76 -> T_IsRelHomomorphism_42 Source #

d_cong_2000 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2004 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2006 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2008 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_2010 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaMonomorphism_94 Source #

d_isRelHomomorphism_2012 :: T_IsMagmaIsomorphism_118 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_2014 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_2014 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_2016 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2016 :: T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

d_surjective_2018 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> T_Σ_14 Source #

d_cong_2020 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2024 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2026 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2028 :: T_IsMagmaMonomorphism_94 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_2030 :: T_IsMagmaMonomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_2032 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2032 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_cong_2034 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMagmaHomomorphism_2038 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaIsomorphism_2040 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaMonomorphism_2042 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_2046 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_2048 :: T_IsMagmaHomomorphism_76 -> T_IsRelHomomorphism_42 Source #

d_cong_2050 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2054 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2056 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2058 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_2060 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaMonomorphism_94 Source #

d_isRelHomomorphism_2062 :: T_IsMagmaIsomorphism_118 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_2064 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_2064 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_2066 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2066 :: T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

d_surjective_2068 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> T_Σ_14 Source #

d_cong_2070 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2074 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2076 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2078 :: T_IsMagmaMonomorphism_94 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_2080 :: T_IsMagmaMonomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_2082 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2082 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_cong_2084 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMagmaHomomorphism_2088 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaIsomorphism_2090 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaMonomorphism_2092 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_2096 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_2098 :: T_IsMagmaHomomorphism_76 -> T_IsRelHomomorphism_42 Source #

d_cong_2100 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2104 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2106 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2108 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_2110 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaMonomorphism_94 Source #

d_isRelHomomorphism_2112 :: T_IsMagmaIsomorphism_118 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_2114 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_2114 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_2116 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2116 :: T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

d_surjective_2118 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> T_Σ_14 Source #

d_cong_2120 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2124 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2126 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2128 :: T_IsMagmaMonomorphism_94 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_2130 :: T_IsMagmaMonomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_2132 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2132 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_cong_2134 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_Homomorphic'8322'_2142 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Injective_2152 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_2160 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> () Source #

d_IsQuasigroupHomomorphism_2164 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsQuasigroupHomomorphism_2164 Source #

Constructors

C_IsQuasigroupHomomorphism'46'constructor_33287 T_IsRelHomomorphism_42 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny)

d_isRelHomomorphism_2176 :: T_IsQuasigroupHomomorphism_2164 -> T_IsRelHomomorphism_42 Source #

d_'8729''45'homo_2178 :: T_IsQuasigroupHomomorphism_2164 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'homo_2180 :: T_IsQuasigroupHomomorphism_2164 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'homo_2182 :: T_IsQuasigroupHomomorphism_2164 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_2186 :: T_IsQuasigroupHomomorphism_2164 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaHomomorphism_2188 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

du_'8729''45'isMagmaHomomorphism_2188 :: T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

d_'92''92''45'isMagmaHomomorphism_2190 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

du_'92''92''45'isMagmaHomomorphism_2190 :: T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

d_'47''47''45'isMagmaHomomorphism_2192 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

du_'47''47''45'isMagmaHomomorphism_2192 :: T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

d_IsQuasigroupMonomorphism_2196 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsQuasigroupMonomorphism_2196 Source #

Constructors

C_IsQuasigroupMonomorphism'46'constructor_34525 T_IsQuasigroupHomomorphism_2164 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isQuasigroupHomomorphism_2204 :: T_IsQuasigroupMonomorphism_2196 -> T_IsQuasigroupHomomorphism_2164 Source #

d_injective_2206 :: T_IsQuasigroupMonomorphism_2196 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'homo_2210 :: T_IsQuasigroupMonomorphism_2196 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'isMagmaHomomorphism_2212 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

du_'47''47''45'isMagmaHomomorphism_2212 :: T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

d_'92''92''45'homo_2214 :: T_IsQuasigroupMonomorphism_2196 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'isMagmaHomomorphism_2216 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

du_'92''92''45'isMagmaHomomorphism_2216 :: T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_2218 :: T_IsQuasigroupMonomorphism_2196 -> T_IsRelHomomorphism_42 Source #

d_'8729''45'homo_2220 :: T_IsQuasigroupMonomorphism_2196 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaHomomorphism_2222 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

du_'8729''45'isMagmaHomomorphism_2222 :: T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

d_cong_2224 :: T_IsQuasigroupMonomorphism_2196 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaMonomorphism_2226 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

du_'8729''45'isMagmaMonomorphism_2226 :: T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

d_'92''92''45'isMagmaMonomorphism_2228 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

du_'92''92''45'isMagmaMonomorphism_2228 :: T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

d_'47''47''45'isMagmaMonomorphism_2230 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

du_'47''47''45'isMagmaMonomorphism_2230 :: T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

d_isRelMonomorphism_2234 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2234 :: T_IsQuasigroupMonomorphism_2196 -> T_IsRelMonomorphism_64 Source #

d_IsQuasigroupIsomorphism_2238 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsQuasigroupIsomorphism_2238 Source #

Constructors

C_IsQuasigroupIsomorphism'46'constructor_36089 T_IsQuasigroupMonomorphism_2196 (AgdaAny -> T_Σ_14)

d_isQuasigroupMonomorphism_2246 :: T_IsQuasigroupIsomorphism_2238 -> T_IsQuasigroupMonomorphism_2196 Source #

d_surjective_2248 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> T_Σ_14 Source #

d_'47''47''45'homo_2252 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'isMagmaHomomorphism_2254 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

du_'47''47''45'isMagmaHomomorphism_2254 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

d_'47''47''45'isMagmaMonomorphism_2256 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

du_'47''47''45'isMagmaMonomorphism_2256 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

d_'92''92''45'homo_2258 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'isMagmaHomomorphism_2260 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

du_'92''92''45'isMagmaHomomorphism_2260 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

d_'92''92''45'isMagmaMonomorphism_2262 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

du_'92''92''45'isMagmaMonomorphism_2262 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

d_injective_2264 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isQuasigroupHomomorphism_2266 :: T_IsQuasigroupIsomorphism_2238 -> T_IsQuasigroupHomomorphism_2164 Source #

d_isRelHomomorphism_2268 :: T_IsQuasigroupIsomorphism_2238 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_2270 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2270 :: T_IsQuasigroupIsomorphism_2238 -> T_IsRelMonomorphism_64 Source #

d_'8729''45'homo_2272 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaHomomorphism_2274 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

du_'8729''45'isMagmaHomomorphism_2274 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

d_'8729''45'isMagmaMonomorphism_2276 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

du_'8729''45'isMagmaMonomorphism_2276 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

d_cong_2278 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaIsomorphism_2280 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

du_'8729''45'isMagmaIsomorphism_2280 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

d_'92''92''45'isMagmaIsomorphism_2282 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

du_'92''92''45'isMagmaIsomorphism_2282 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

d_'47''47''45'isMagmaIsomorphism_2284 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

du_'47''47''45'isMagmaIsomorphism_2284 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

d_isRelIsomorphism_2288 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawQuasigroup_3042 -> T_RawQuasigroup_3042 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_2288 :: T_IsQuasigroupIsomorphism_2238 -> T_IsRelIsomorphism_94 Source #

d_Carrier_2318 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> () Source #

d_ε_2324 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> AgdaAny Source #

du_ε_2324 :: T_RawLoop_3174 -> AgdaAny Source #

d_Homomorphic'8320'_2354 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Injective_2368 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_2376 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> () Source #

d_IsQuasigroupHomomorphism_2380 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsQuasigroupIsomorphism_2382 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsQuasigroupMonomorphism_2384 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaHomomorphism_2388 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaIsomorphism_2390 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaMonomorphism_2392 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_2396 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_2398 :: T_IsMagmaHomomorphism_76 -> T_IsRelHomomorphism_42 Source #

d_cong_2400 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2404 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2406 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2408 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_2410 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaMonomorphism_94 Source #

d_isRelHomomorphism_2412 :: T_IsMagmaIsomorphism_118 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_2414 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_2414 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_2416 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2416 :: T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

d_surjective_2418 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> T_Σ_14 Source #

d_cong_2420 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2424 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2426 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2428 :: T_IsMagmaMonomorphism_94 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_2430 :: T_IsMagmaMonomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_2432 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2432 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_cong_2434 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'homo_2438 :: T_IsQuasigroupHomomorphism_2164 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'isMagmaHomomorphism_2440 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

du_'47''47''45'isMagmaHomomorphism_2440 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

d_'92''92''45'homo_2442 :: T_IsQuasigroupHomomorphism_2164 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'isMagmaHomomorphism_2444 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

du_'92''92''45'isMagmaHomomorphism_2444 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_2446 :: T_IsQuasigroupHomomorphism_2164 -> T_IsRelHomomorphism_42 Source #

d_'8729''45'homo_2448 :: T_IsQuasigroupHomomorphism_2164 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaHomomorphism_2450 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

du_'8729''45'isMagmaHomomorphism_2450 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2164 -> T_IsMagmaHomomorphism_76 Source #

d_cong_2452 :: T_IsQuasigroupHomomorphism_2164 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'homo_2456 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'isMagmaHomomorphism_2458 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

du_'47''47''45'isMagmaHomomorphism_2458 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

d_'47''47''45'isMagmaIsomorphism_2460 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

du_'47''47''45'isMagmaIsomorphism_2460 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

d_'47''47''45'isMagmaMonomorphism_2462 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

du_'47''47''45'isMagmaMonomorphism_2462 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

d_'92''92''45'homo_2464 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'isMagmaHomomorphism_2466 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

du_'92''92''45'isMagmaHomomorphism_2466 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

d_'92''92''45'isMagmaIsomorphism_2468 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

du_'92''92''45'isMagmaIsomorphism_2468 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

d_'92''92''45'isMagmaMonomorphism_2470 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

du_'92''92''45'isMagmaMonomorphism_2470 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

d_injective_2472 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isQuasigroupHomomorphism_2474 :: T_IsQuasigroupIsomorphism_2238 -> T_IsQuasigroupHomomorphism_2164 Source #

d_isQuasigroupMonomorphism_2476 :: T_IsQuasigroupIsomorphism_2238 -> T_IsQuasigroupMonomorphism_2196 Source #

d_isRelHomomorphism_2478 :: T_IsQuasigroupIsomorphism_2238 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_2480 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_2480 :: T_IsQuasigroupIsomorphism_2238 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_2482 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2482 :: T_IsQuasigroupIsomorphism_2238 -> T_IsRelMonomorphism_64 Source #

d_surjective_2484 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> T_Σ_14 Source #

d_'8729''45'homo_2486 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaHomomorphism_2488 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

du_'8729''45'isMagmaHomomorphism_2488 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaHomomorphism_76 Source #

d_'8729''45'isMagmaIsomorphism_2490 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

du_'8729''45'isMagmaIsomorphism_2490 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaIsomorphism_118 Source #

d_'8729''45'isMagmaMonomorphism_2492 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

du_'8729''45'isMagmaMonomorphism_2492 :: T_IsQuasigroupIsomorphism_2238 -> T_IsMagmaMonomorphism_94 Source #

d_cong_2494 :: T_IsQuasigroupIsomorphism_2238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'homo_2498 :: T_IsQuasigroupMonomorphism_2196 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'isMagmaHomomorphism_2500 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

du_'47''47''45'isMagmaHomomorphism_2500 :: T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

d_'47''47''45'isMagmaMonomorphism_2502 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

du_'47''47''45'isMagmaMonomorphism_2502 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

d_'92''92''45'homo_2504 :: T_IsQuasigroupMonomorphism_2196 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'isMagmaHomomorphism_2506 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

du_'92''92''45'isMagmaHomomorphism_2506 :: T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

d_'92''92''45'isMagmaMonomorphism_2508 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

du_'92''92''45'isMagmaMonomorphism_2508 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

d_injective_2510 :: T_IsQuasigroupMonomorphism_2196 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isQuasigroupHomomorphism_2512 :: T_IsQuasigroupMonomorphism_2196 -> T_IsQuasigroupHomomorphism_2164 Source #

d_isRelHomomorphism_2514 :: T_IsQuasigroupMonomorphism_2196 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_2516 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2516 :: T_IsQuasigroupMonomorphism_2196 -> T_IsRelMonomorphism_64 Source #

d_'8729''45'homo_2518 :: T_IsQuasigroupMonomorphism_2196 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaHomomorphism_2520 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

du_'8729''45'isMagmaHomomorphism_2520 :: T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaHomomorphism_76 Source #

d_'8729''45'isMagmaMonomorphism_2522 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

du_'8729''45'isMagmaMonomorphism_2522 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2196 -> T_IsMagmaMonomorphism_94 Source #

d_cong_2524 :: T_IsQuasigroupMonomorphism_2196 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMagmaHomomorphism_2528 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaIsomorphism_2530 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaMonomorphism_2532 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_2536 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_2538 :: T_IsMagmaHomomorphism_76 -> T_IsRelHomomorphism_42 Source #

d_cong_2540 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2544 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2546 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2548 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_2550 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaMonomorphism_94 Source #

d_isRelHomomorphism_2552 :: T_IsMagmaIsomorphism_118 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_2554 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_2554 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_2556 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2556 :: T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

d_surjective_2558 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> T_Σ_14 Source #

d_cong_2560 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2564 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2566 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2568 :: T_IsMagmaMonomorphism_94 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_2570 :: T_IsMagmaMonomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_2572 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2572 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_cong_2574 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMagmaHomomorphism_2578 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaIsomorphism_2580 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsMagmaMonomorphism_2582 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_homo_2586 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_2588 :: T_IsMagmaHomomorphism_76 -> T_IsRelHomomorphism_42 Source #

d_cong_2590 :: T_IsMagmaHomomorphism_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2594 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2596 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2598 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaHomomorphism_76 Source #

d_isMagmaMonomorphism_2600 :: T_IsMagmaIsomorphism_118 -> T_IsMagmaMonomorphism_94 Source #

d_isRelHomomorphism_2602 :: T_IsMagmaIsomorphism_118 -> T_IsRelHomomorphism_42 Source #

d_isRelIsomorphism_2604 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_2604 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelIsomorphism_94 Source #

d_isRelMonomorphism_2606 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2606 :: T_IsMagmaIsomorphism_118 -> T_IsRelMonomorphism_64 Source #

d_surjective_2608 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> T_Σ_14 Source #

d_cong_2610 :: T_IsMagmaIsomorphism_118 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_homo_2614 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_2616 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMagmaHomomorphism_2618 :: T_IsMagmaMonomorphism_94 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_2620 :: T_IsMagmaMonomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_2622 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_2622 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_cong_2624 :: T_IsMagmaMonomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsLoopHomomorphism_2628 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsLoopHomomorphism_2628 Source #

Constructors

C_IsLoopHomomorphism'46'constructor_40203 T_IsQuasigroupHomomorphism_2164 AgdaAny

d_isQuasigroupHomomorphism_2636 :: T_IsLoopHomomorphism_2628 -> T_IsQuasigroupHomomorphism_2164 Source #

d_ε'45'homo_2638 :: T_IsLoopHomomorphism_2628 -> AgdaAny Source #

d_'47''47''45'homo_2642 :: T_IsLoopHomomorphism_2628 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'isMagmaHomomorphism_2644 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsLoopHomomorphism_2628 -> T_IsMagmaHomomorphism_76 Source #

du_'47''47''45'isMagmaHomomorphism_2644 :: T_IsLoopHomomorphism_2628 -> T_IsMagmaHomomorphism_76 Source #

d_'92''92''45'homo_2646 :: T_IsLoopHomomorphism_2628 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'isMagmaHomomorphism_2648 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsLoopHomomorphism_2628 -> T_IsMagmaHomomorphism_76 Source #

du_'92''92''45'isMagmaHomomorphism_2648 :: T_IsLoopHomomorphism_2628 -> T_IsMagmaHomomorphism_76 Source #

d_isRelHomomorphism_2650 :: T_IsLoopHomomorphism_2628 -> T_IsRelHomomorphism_42 Source #

d_'8729''45'homo_2652 :: T_IsLoopHomomorphism_2628 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaHomomorphism_2654 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsLoopHomomorphism_2628 -> T_IsMagmaHomomorphism_76 Source #

du_'8729''45'isMagmaHomomorphism_2654 :: T_IsLoopHomomorphism_2628 -> T_IsMagmaHomomorphism_76 Source #

d_cong_2656 :: T_IsLoopHomomorphism_2628 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsLoopMonomorphism_2660 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsLoopMonomorphism_2660 Source #

Constructors

C_IsLoopMonomorphism'46'constructor_40941 T_IsLoopHomomorphism_2628 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isLoopHomomorphism_2668 :: T_IsLoopMonomorphism_2660 -> T_IsLoopHomomorphism_2628 Source #

d_injective_2670 :: T_IsLoopMonomorphism_2660 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'homo_2674 :: T_IsLoopMonomorphism_2660 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'isMagmaHomomorphism_2676 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsLoopMonomorphism_2660 -> T_IsMagmaHomomorphism_76 Source #

du_'47''47''45'isMagmaHomomorphism_2676 :: T_IsLoopMonomorphism_2660 -> T_IsMagmaHomomorphism_76 Source #

d_'92''92''45'homo_2678 :: T_IsLoopMonomorphism_2660 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'isMagmaHomomorphism_2680 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsLoopMonomorphism_2660 -> T_IsMagmaHomomorphism_76 Source #

du_'92''92''45'isMagmaHomomorphism_2680 :: T_IsLoopMonomorphism_2660 -> T_IsMagmaHomomorphism_76 Source #

d_isQuasigroupHomomorphism_2682 :: T_IsLoopMonomorphism_2660 -> T_IsQuasigroupHomomorphism_2164 Source #

d_isRelHomomorphism_2684 :: T_IsLoopMonomorphism_2660 -> T_IsRelHomomorphism_42 Source #

d_ε'45'homo_2686 :: T_IsLoopMonomorphism_2660 -> AgdaAny Source #

d_'8729''45'homo_2688 :: T_IsLoopMonomorphism_2660 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaHomomorphism_2690 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsLoopMonomorphism_2660 -> T_IsMagmaHomomorphism_76 Source #

du_'8729''45'isMagmaHomomorphism_2690 :: T_IsLoopMonomorphism_2660 -> T_IsMagmaHomomorphism_76 Source #

d_cong_2692 :: T_IsLoopMonomorphism_2660 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsLoopIsomorphism_2696 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsLoopIsomorphism_2696 Source #

Constructors

C_IsLoopIsomorphism'46'constructor_41813 T_IsLoopMonomorphism_2660 (AgdaAny -> T_Σ_14)

d_isLoopMonomorphism_2704 :: T_IsLoopIsomorphism_2696 -> T_IsLoopMonomorphism_2660 Source #

d_surjective_2706 :: T_IsLoopIsomorphism_2696 -> AgdaAny -> T_Σ_14 Source #

d_'47''47''45'homo_2710 :: T_IsLoopIsomorphism_2696 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'47''47''45'isMagmaHomomorphism_2712 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsLoopIsomorphism_2696 -> T_IsMagmaHomomorphism_76 Source #

du_'47''47''45'isMagmaHomomorphism_2712 :: T_IsLoopIsomorphism_2696 -> T_IsMagmaHomomorphism_76 Source #

d_'92''92''45'homo_2714 :: T_IsLoopIsomorphism_2696 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'92''92''45'isMagmaHomomorphism_2716 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsLoopIsomorphism_2696 -> T_IsMagmaHomomorphism_76 Source #

du_'92''92''45'isMagmaHomomorphism_2716 :: T_IsLoopIsomorphism_2696 -> T_IsMagmaHomomorphism_76 Source #

d_injective_2718 :: T_IsLoopIsomorphism_2696 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isLoopHomomorphism_2720 :: T_IsLoopIsomorphism_2696 -> T_IsLoopHomomorphism_2628 Source #

d_isQuasigroupHomomorphism_2722 :: T_IsLoopIsomorphism_2696 -> T_IsQuasigroupHomomorphism_2164 Source #

d_isRelHomomorphism_2724 :: T_IsLoopIsomorphism_2696 -> T_IsRelHomomorphism_42 Source #

d_ε'45'homo_2726 :: T_IsLoopIsomorphism_2696 -> AgdaAny Source #

d_'8729''45'homo_2728 :: T_IsLoopIsomorphism_2696 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'isMagmaHomomorphism_2730 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawLoop_3174 -> T_RawLoop_3174 -> (AgdaAny -> AgdaAny) -> T_IsLoopIsomorphism_2696 -> T_IsMagmaHomomorphism_76 Source #

du_'8729''45'isMagmaHomomorphism_2730 :: T_IsLoopIsomorphism_2696 -> T_IsMagmaHomomorphism_76 Source #

d_cong_2732 :: T_IsLoopIsomorphism_2696 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #