Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Algebra.Morphism.Structures

Documentation

d__'8776'__30 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSuccessorSet_10 -> T_RawSuccessorSet_10 -> AgdaAny -> AgdaAny -> () #

d_Carrier_32 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSuccessorSet_10 -> T_RawSuccessorSet_10 -> () #

d_suc'35'_34 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSuccessorSet_10 -> T_RawSuccessorSet_10 -> AgdaAny -> AgdaAny #

du_suc'35'_34 :: T_RawSuccessorSet_10 -> AgdaAny -> AgdaAny #

d_zero'35'_36 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSuccessorSet_10 -> T_RawSuccessorSet_10 -> AgdaAny #

du_zero'35'_36 :: T_RawSuccessorSet_10 -> AgdaAny #

d_Homomorphic'8320'_50 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSuccessorSet_10 -> T_RawSuccessorSet_10 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_Homomorphic'8321'_52 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSuccessorSet_10 -> T_RawSuccessorSet_10 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_IsSuccessorSetHomomorphism_60 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsSuccessorSetHomomorphism_60 #

Constructors

C_IsSuccessorSetHomomorphism'46'constructor_777 T_IsRelHomomorphism_42 (AgdaAny -> AgdaAny) AgdaAny

d_isRelHomomorphism_70 :: T_IsSuccessorSetHomomorphism_60 -> T_IsRelHomomorphism_42 #

d_suc'35''45'homo_72 :: T_IsSuccessorSetHomomorphism_60 -> AgdaAny -> AgdaAny #

d_zero'35''45'homo_74 :: T_IsSuccessorSetHomomorphism_60 -> AgdaAny #

d_IsSuccessorSetMonomorphism_78 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsSuccessorSetMonomorphism_78 #

Constructors

C_IsSuccessorSetMonomorphism'46'constructor_1407 T_IsSuccessorSetHomomorphism_60 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isSuccessorSetHomomorphism_86 :: T_IsSuccessorSetMonomorphism_78 -> T_IsSuccessorSetHomomorphism_60 #

d_injective_88 :: T_IsSuccessorSetMonomorphism_78 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_92 :: T_IsSuccessorSetMonomorphism_78 -> T_IsRelHomomorphism_42 #

d_suc'35''45'homo_94 :: T_IsSuccessorSetMonomorphism_78 -> AgdaAny -> AgdaAny #

d_zero'35''45'homo_96 :: T_IsSuccessorSetMonomorphism_78 -> AgdaAny #

d_isRelMonomorphism_98 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSuccessorSet_10 -> T_RawSuccessorSet_10 -> (AgdaAny -> AgdaAny) -> T_IsSuccessorSetMonomorphism_78 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_98 :: T_IsSuccessorSetMonomorphism_78 -> T_IsRelMonomorphism_64 #

d_IsSuccessorSetIsomorphism_102 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsSuccessorSetIsomorphism_102 #

Constructors

C_IsSuccessorSetIsomorphism'46'constructor_2827 T_IsSuccessorSetMonomorphism_78 (AgdaAny -> T_Σ_14)

d_isSuccessorSetMonomorphism_110 :: T_IsSuccessorSetIsomorphism_102 -> T_IsSuccessorSetMonomorphism_78 #

d_surjective_112 :: T_IsSuccessorSetIsomorphism_102 -> AgdaAny -> T_Σ_14 #

d_injective_116 :: T_IsSuccessorSetIsomorphism_102 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_118 :: T_IsSuccessorSetIsomorphism_102 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_120 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSuccessorSet_10 -> T_RawSuccessorSet_10 -> (AgdaAny -> AgdaAny) -> T_IsSuccessorSetIsomorphism_102 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_120 :: T_IsSuccessorSetIsomorphism_102 -> T_IsRelMonomorphism_64 #

d_isSuccessorSetHomomorphism_122 :: T_IsSuccessorSetIsomorphism_102 -> T_IsSuccessorSetHomomorphism_60 #

d_suc'35''45'homo_124 :: T_IsSuccessorSetIsomorphism_102 -> AgdaAny -> AgdaAny #

d_zero'35''45'homo_126 :: T_IsSuccessorSetIsomorphism_102 -> AgdaAny #

d_isRelIsomorphism_128 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSuccessorSet_10 -> T_RawSuccessorSet_10 -> (AgdaAny -> AgdaAny) -> T_IsSuccessorSetIsomorphism_102 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_128 :: T_IsSuccessorSetIsomorphism_102 -> T_IsRelIsomorphism_94 #

d__'8729'__146 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMagma_36 -> T_RawMagma_36 -> AgdaAny -> AgdaAny -> AgdaAny #

du__'8729'__146 :: T_RawMagma_36 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__148 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMagma_36 -> T_RawMagma_36 -> AgdaAny -> AgdaAny -> () #

d_Carrier_152 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMagma_36 -> T_RawMagma_36 -> () #

d_Homomorphic'8322'_170 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMagma_36 -> T_RawMagma_36 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_IsMagmaHomomorphism_176 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsMagmaHomomorphism_176 #

Constructors

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

d_isRelHomomorphism_184 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_homo_186 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_190 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMagmaMonomorphism_194 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsMagmaMonomorphism_194 #

Constructors

C_IsMagmaMonomorphism'46'constructor_5763 T_IsMagmaHomomorphism_176 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isMagmaHomomorphism_202 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_injective_204 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_208 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_210 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_cong_212 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelMonomorphism_214 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMagma_36 -> T_RawMagma_36 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_214 :: T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_IsMagmaIsomorphism_218 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsMagmaIsomorphism_218 #

Constructors

C_IsMagmaIsomorphism'46'constructor_7199 T_IsMagmaMonomorphism_194 (AgdaAny -> T_Σ_14)

d_isMagmaMonomorphism_226 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_surjective_228 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_homo_232 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_234 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_236 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_238 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_240 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMagma_36 -> T_RawMagma_36 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_240 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_cong_242 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelIsomorphism_244 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMagma_36 -> T_RawMagma_36 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_244 :: T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d__'8776'__264 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> AgdaAny -> AgdaAny -> () #

d_Carrier_268 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> () #

d_ε_272 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> AgdaAny #

du_ε_272 :: T_RawMonoid_64 -> AgdaAny #

d_Homomorphic'8320'_290 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_IsMagmaHomomorphism_300 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaIsomorphism_302 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaMonomorphism_304 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_308 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_310 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_cong_312 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_316 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_318 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_320 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_322 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_isRelHomomorphism_324 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_326 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_326 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_328 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_328 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_surjective_330 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_cong_332 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_336 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_338 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_340 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_342 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_344 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_344 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_cong_346 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMonoidHomomorphism_350 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsMonoidHomomorphism_350 #

Constructors

C_IsMonoidHomomorphism'46'constructor_9411 T_IsMagmaHomomorphism_176 AgdaAny

d_isMagmaHomomorphism_358 :: T_IsMonoidHomomorphism_350 -> T_IsMagmaHomomorphism_176 #

d_ε'45'homo_360 :: T_IsMonoidHomomorphism_350 -> AgdaAny #

d_homo_364 :: T_IsMonoidHomomorphism_350 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_366 :: T_IsMonoidHomomorphism_350 -> T_IsRelHomomorphism_42 #

d_cong_368 :: T_IsMonoidHomomorphism_350 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMonoidMonomorphism_372 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsMonoidMonomorphism_372 #

Constructors

C_IsMonoidMonomorphism'46'constructor_10237 T_IsMonoidHomomorphism_350 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isMonoidHomomorphism_380 :: T_IsMonoidMonomorphism_372 -> T_IsMonoidHomomorphism_350 #

d_injective_382 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_386 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_388 :: T_IsMonoidMonomorphism_372 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_390 :: T_IsMonoidMonomorphism_372 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_392 :: T_IsMonoidMonomorphism_372 -> AgdaAny #

d_cong_394 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaMonomorphism_396 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_396 :: T_IsMonoidMonomorphism_372 -> T_IsMagmaMonomorphism_194 #

d_isRelMonomorphism_400 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_400 :: T_IsMonoidMonomorphism_372 -> T_IsRelMonomorphism_64 #

d_IsMonoidIsomorphism_404 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsMonoidIsomorphism_404 #

Constructors

C_IsMonoidIsomorphism'46'constructor_11597 T_IsMonoidMonomorphism_372 (AgdaAny -> T_Σ_14)

d_isMonoidMonomorphism_412 :: T_IsMonoidIsomorphism_404 -> T_IsMonoidMonomorphism_372 #

d_surjective_414 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> T_Σ_14 #

d_homo_418 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_420 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_422 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_424 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_424 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_426 :: T_IsMonoidIsomorphism_404 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_428 :: T_IsMonoidIsomorphism_404 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_430 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_430 :: T_IsMonoidIsomorphism_404 -> T_IsRelMonomorphism_64 #

d_ε'45'homo_432 :: T_IsMonoidIsomorphism_404 -> AgdaAny #

d_cong_434 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaIsomorphism_436 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_436 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaIsomorphism_218 #

d_isRelIsomorphism_440 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawMonoid_64 -> T_RawMonoid_64 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_440 :: T_IsMonoidIsomorphism_404 -> T_IsRelIsomorphism_94 #

d__'8315''185'_458 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> AgdaAny -> AgdaAny #

du__'8315''185'_458 :: T_RawGroup_96 -> AgdaAny -> AgdaAny #

d__'8776'__462 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> AgdaAny -> AgdaAny -> () #

d_Carrier_466 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> () #

d_Homomorphic'8321'_496 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_IsMagmaHomomorphism_504 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaIsomorphism_506 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaMonomorphism_508 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_512 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_514 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_cong_516 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_520 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_522 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_524 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_526 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_isRelHomomorphism_528 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_530 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_530 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_532 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_532 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_surjective_534 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_cong_536 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_540 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_542 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_544 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_546 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_548 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_548 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_cong_550 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMonoidHomomorphism_554 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMonoidIsomorphism_556 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMonoidMonomorphism_558 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_562 :: T_IsMonoidHomomorphism_350 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_564 :: T_IsMonoidHomomorphism_350 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_566 :: T_IsMonoidHomomorphism_350 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_568 :: T_IsMonoidHomomorphism_350 -> AgdaAny #

d_cong_570 :: T_IsMonoidHomomorphism_350 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_574 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_576 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_578 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaHomomorphism_176 #

d_isMagmaIsomorphism_580 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_580 :: (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaIsomorphism_218 #

d_isMagmaMonomorphism_582 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_582 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_584 :: T_IsMonoidIsomorphism_404 -> T_IsMonoidHomomorphism_350 #

d_isMonoidMonomorphism_586 :: T_IsMonoidIsomorphism_404 -> T_IsMonoidMonomorphism_372 #

d_isRelHomomorphism_588 :: T_IsMonoidIsomorphism_404 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_590 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_590 :: T_IsMonoidIsomorphism_404 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_592 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_592 :: T_IsMonoidIsomorphism_404 -> T_IsRelMonomorphism_64 #

d_surjective_594 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> T_Σ_14 #

d_ε'45'homo_596 :: T_IsMonoidIsomorphism_404 -> AgdaAny #

d_cong_598 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_602 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_604 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_606 :: T_IsMonoidMonomorphism_372 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_608 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_608 :: (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_610 :: T_IsMonoidMonomorphism_372 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_612 :: T_IsMonoidMonomorphism_372 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_614 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_614 :: T_IsMonoidMonomorphism_372 -> T_IsRelMonomorphism_64 #

d_ε'45'homo_616 :: T_IsMonoidMonomorphism_372 -> AgdaAny #

d_cong_618 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsGroupHomomorphism_622 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsGroupHomomorphism_622 #

Constructors

C_IsGroupHomomorphism'46'constructor_14585 T_IsMonoidHomomorphism_350 (AgdaAny -> AgdaAny)

d_isMonoidHomomorphism_630 :: T_IsGroupHomomorphism_622 -> T_IsMonoidHomomorphism_350 #

d_'8315''185''45'homo_632 :: T_IsGroupHomomorphism_622 -> AgdaAny -> AgdaAny #

d_homo_636 :: T_IsGroupHomomorphism_622 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_638 :: T_IsGroupHomomorphism_622 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_640 :: T_IsGroupHomomorphism_622 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_642 :: T_IsGroupHomomorphism_622 -> AgdaAny #

d_cong_644 :: T_IsGroupHomomorphism_622 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsGroupMonomorphism_648 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsGroupMonomorphism_648 #

Constructors

C_IsGroupMonomorphism'46'constructor_15537 T_IsGroupHomomorphism_622 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isGroupHomomorphism_656 :: T_IsGroupMonomorphism_648 -> T_IsGroupHomomorphism_622 #

d_injective_658 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_662 :: T_IsGroupMonomorphism_648 -> T_IsMagmaHomomorphism_176 #

d_isMonoidHomomorphism_664 :: T_IsGroupMonomorphism_648 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_666 :: T_IsGroupMonomorphism_648 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_668 :: T_IsGroupMonomorphism_648 -> AgdaAny #

d_'8315''185''45'homo_670 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny #

d_homo_672 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_674 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMonoidMonomorphism_676 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsMonoidMonomorphism_372 #

du_isMonoidMonomorphism_676 :: T_IsGroupMonomorphism_648 -> T_IsMonoidMonomorphism_372 #

d_isMagmaMonomorphism_680 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_680 :: T_IsGroupMonomorphism_648 -> T_IsMagmaMonomorphism_194 #

d_isRelMonomorphism_682 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_682 :: T_IsGroupMonomorphism_648 -> T_IsRelMonomorphism_64 #

d_IsGroupIsomorphism_686 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsGroupIsomorphism_686 #

Constructors

C_IsGroupIsomorphism'46'constructor_17073 T_IsGroupMonomorphism_648 (AgdaAny -> T_Σ_14)

d_isGroupMonomorphism_694 :: T_IsGroupIsomorphism_686 -> T_IsGroupMonomorphism_648 #

d_surjective_696 :: T_IsGroupIsomorphism_686 -> AgdaAny -> T_Σ_14 #

d_injective_700 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isGroupHomomorphism_702 :: T_IsGroupIsomorphism_686 -> T_IsGroupHomomorphism_622 #

d_isMagmaHomomorphism_704 :: T_IsGroupIsomorphism_686 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_706 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_706 :: T_IsGroupIsomorphism_686 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_708 :: T_IsGroupIsomorphism_686 -> T_IsMonoidHomomorphism_350 #

d_isMonoidMonomorphism_710 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMonoidMonomorphism_372 #

du_isMonoidMonomorphism_710 :: T_IsGroupIsomorphism_686 -> T_IsMonoidMonomorphism_372 #

d_isRelHomomorphism_712 :: T_IsGroupIsomorphism_686 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_714 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_714 :: T_IsGroupIsomorphism_686 -> T_IsRelMonomorphism_64 #

d_ε'45'homo_716 :: T_IsGroupIsomorphism_686 -> AgdaAny #

d_'8315''185''45'homo_718 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny #

d_homo_720 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_722 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMonoidIsomorphism_724 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMonoidIsomorphism_404 #

du_isMonoidIsomorphism_724 :: T_IsGroupIsomorphism_686 -> T_IsMonoidIsomorphism_404 #

d_isMagmaIsomorphism_728 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_728 :: T_IsGroupIsomorphism_686 -> T_IsMagmaIsomorphism_218 #

d_isRelIsomorphism_730 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawGroup_96 -> T_RawGroup_96 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_730 :: T_IsGroupIsomorphism_686 -> T_IsRelIsomorphism_94 #

d__'42'__748 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> AgdaAny #

du__'42'__748 :: T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__752 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> AgdaAny -> AgdaAny -> () #

d_Carrier_764 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> () #

d_IsMonoidHomomorphism_788 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMonoidIsomorphism_790 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMonoidMonomorphism_792 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_796 :: T_IsMonoidHomomorphism_350 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_798 :: T_IsMonoidHomomorphism_350 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_800 :: T_IsMonoidHomomorphism_350 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_802 :: T_IsMonoidHomomorphism_350 -> AgdaAny #

d_cong_804 :: T_IsMonoidHomomorphism_350 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_808 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_810 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_812 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaHomomorphism_176 #

d_isMagmaIsomorphism_814 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_814 :: (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaIsomorphism_218 #

d_isMagmaMonomorphism_816 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_816 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_818 :: T_IsMonoidIsomorphism_404 -> T_IsMonoidHomomorphism_350 #

d_isMonoidMonomorphism_820 :: T_IsMonoidIsomorphism_404 -> T_IsMonoidMonomorphism_372 #

d_isRelHomomorphism_822 :: T_IsMonoidIsomorphism_404 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_824 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_824 :: T_IsMonoidIsomorphism_404 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_826 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_826 :: T_IsMonoidIsomorphism_404 -> T_IsRelMonomorphism_64 #

d_surjective_828 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> T_Σ_14 #

d_ε'45'homo_830 :: T_IsMonoidIsomorphism_404 -> AgdaAny #

d_cong_832 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_836 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_838 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_840 :: T_IsMonoidMonomorphism_372 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_842 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_842 :: (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_844 :: T_IsMonoidMonomorphism_372 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_846 :: T_IsMonoidMonomorphism_372 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_848 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_848 :: T_IsMonoidMonomorphism_372 -> T_IsRelMonomorphism_64 #

d_ε'45'homo_850 :: T_IsMonoidMonomorphism_372 -> AgdaAny #

d_cong_852 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMagmaHomomorphism_856 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaIsomorphism_858 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaMonomorphism_860 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_864 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_866 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_cong_868 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_872 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_874 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_876 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_878 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_isRelHomomorphism_880 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_882 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_882 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_884 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_884 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_surjective_886 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_cong_888 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_892 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_894 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_896 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_898 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_900 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_900 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_cong_902 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_Homomorphic'8322'_910 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_IsNearSemiringHomomorphism_916 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsNearSemiringHomomorphism_916 #

Constructors

C_IsNearSemiringHomomorphism'46'constructor_19989 T_IsMonoidHomomorphism_350 (AgdaAny -> AgdaAny -> AgdaAny)

d_'43''45'isMonoidHomomorphism_924 :: T_IsNearSemiringHomomorphism_916 -> T_IsMonoidHomomorphism_350 #

d_'42''45'homo_926 :: T_IsNearSemiringHomomorphism_916 -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_930 :: T_IsNearSemiringHomomorphism_916 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_932 :: T_IsNearSemiringHomomorphism_916 -> T_IsMagmaHomomorphism_176 #

d_ε'45'homo_934 :: T_IsNearSemiringHomomorphism_916 -> AgdaAny #

d_isRelHomomorphism_936 :: T_IsNearSemiringHomomorphism_916 -> T_IsRelHomomorphism_42 #

d_cong_938 :: T_IsNearSemiringHomomorphism_916 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_940 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringHomomorphism_916 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_940 :: T_IsNearSemiringHomomorphism_916 -> T_IsMagmaHomomorphism_176 #

d_IsNearSemiringMonomorphism_944 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsNearSemiringMonomorphism_944 #

Constructors

C_IsNearSemiringMonomorphism'46'constructor_21119 T_IsNearSemiringHomomorphism_916 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isNearSemiringHomomorphism_952 :: T_IsNearSemiringMonomorphism_944 -> T_IsNearSemiringHomomorphism_916 #

d_injective_954 :: T_IsNearSemiringMonomorphism_944 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_958 :: T_IsNearSemiringMonomorphism_944 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_960 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_960 :: T_IsNearSemiringMonomorphism_944 -> T_IsMagmaHomomorphism_176 #

d_homo_962 :: T_IsNearSemiringMonomorphism_944 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_964 :: T_IsNearSemiringMonomorphism_944 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_966 :: T_IsNearSemiringMonomorphism_944 -> T_IsMonoidHomomorphism_350 #

d_ε'45'homo_968 :: T_IsNearSemiringMonomorphism_944 -> AgdaAny #

d_isRelHomomorphism_970 :: T_IsNearSemiringMonomorphism_944 -> T_IsRelHomomorphism_42 #

d_cong_972 :: T_IsNearSemiringMonomorphism_944 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'43''45'isMonoidMonomorphism_974 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsMonoidMonomorphism_372 #

du_'43''45'isMonoidMonomorphism_974 :: T_IsNearSemiringMonomorphism_944 -> T_IsMonoidMonomorphism_372 #

d_isMagmaMonomorphism_978 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_978 :: T_IsNearSemiringMonomorphism_944 -> T_IsMagmaMonomorphism_194 #

d_isRelMonomorphism_980 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_980 :: T_IsNearSemiringMonomorphism_944 -> T_IsRelMonomorphism_64 #

d_'42''45'isMagmaMonomorphism_982 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_982 :: T_IsNearSemiringMonomorphism_944 -> T_IsMagmaMonomorphism_194 #

d_IsNearSemiringIsomorphism_986 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsNearSemiringIsomorphism_986 #

Constructors

C_IsNearSemiringIsomorphism'46'constructor_23007 T_IsNearSemiringMonomorphism_944 (AgdaAny -> T_Σ_14)

d_isNearSemiringMonomorphism_994 :: T_IsNearSemiringIsomorphism_986 -> T_IsNearSemiringMonomorphism_944 #

d_surjective_996 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny -> T_Σ_14 #

d_'42''45'homo_1000 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_1002 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_1002 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMagmaMonomorphism_1004 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_1004 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaMonomorphism_194 #

d_homo_1006 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1008 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_1010 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1010 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaMonomorphism_194 #

d_'43''45'isMonoidHomomorphism_1012 :: T_IsNearSemiringIsomorphism_986 -> T_IsMonoidHomomorphism_350 #

d_'43''45'isMonoidMonomorphism_1014 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMonoidMonomorphism_372 #

du_'43''45'isMonoidMonomorphism_1014 :: T_IsNearSemiringIsomorphism_986 -> T_IsMonoidMonomorphism_372 #

d_ε'45'homo_1016 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny #

d_injective_1018 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringHomomorphism_1020 :: T_IsNearSemiringIsomorphism_986 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_1022 :: T_IsNearSemiringIsomorphism_986 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_1024 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1024 :: T_IsNearSemiringIsomorphism_986 -> T_IsRelMonomorphism_64 #

d_cong_1026 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'43''45'isMonoidIsomorphism_1028 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMonoidIsomorphism_404 #

du_'43''45'isMonoidIsomorphism_1028 :: T_IsNearSemiringIsomorphism_986 -> T_IsMonoidIsomorphism_404 #

d_isMagmaIsomorphism_1032 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_1032 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaIsomorphism_218 #

d_isRelIsomorphism_1034 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_1034 :: T_IsNearSemiringIsomorphism_986 -> T_IsRelIsomorphism_94 #

d_'42''45'isMagmaIsomorphism_1036 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawNearSemiring_134 -> T_RawNearSemiring_134 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaIsomorphism_218 #

du_'42''45'isMagmaIsomorphism_1036 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaIsomorphism_218 #

d__'8776'__1058 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> AgdaAny -> AgdaAny -> () #

d_1'35'_1072 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> AgdaAny #

du_1'35'_1072 :: T_RawSemiring_174 -> AgdaAny #

d_Carrier_1074 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> () #

d_IsMonoidHomomorphism_1106 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMonoidIsomorphism_1108 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMonoidMonomorphism_1110 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_1114 :: T_IsMonoidHomomorphism_350 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1116 :: T_IsMonoidHomomorphism_350 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_1118 :: T_IsMonoidHomomorphism_350 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_1120 :: T_IsMonoidHomomorphism_350 -> AgdaAny #

d_cong_1122 :: T_IsMonoidHomomorphism_350 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_1126 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_1128 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1130 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaHomomorphism_176 #

d_isMagmaIsomorphism_1132 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_1132 :: (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaIsomorphism_218 #

d_isMagmaMonomorphism_1134 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1134 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_1136 :: T_IsMonoidIsomorphism_404 -> T_IsMonoidHomomorphism_350 #

d_isMonoidMonomorphism_1138 :: T_IsMonoidIsomorphism_404 -> T_IsMonoidMonomorphism_372 #

d_isRelHomomorphism_1140 :: T_IsMonoidIsomorphism_404 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_1142 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_1142 :: T_IsMonoidIsomorphism_404 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_1144 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1144 :: T_IsMonoidIsomorphism_404 -> T_IsRelMonomorphism_64 #

d_surjective_1146 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> T_Σ_14 #

d_ε'45'homo_1148 :: T_IsMonoidIsomorphism_404 -> AgdaAny #

d_cong_1150 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_1154 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_1156 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1158 :: T_IsMonoidMonomorphism_372 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_1160 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1160 :: (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_1162 :: T_IsMonoidMonomorphism_372 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_1164 :: T_IsMonoidMonomorphism_372 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_1166 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1166 :: T_IsMonoidMonomorphism_372 -> T_IsRelMonomorphism_64 #

d_ε'45'homo_1168 :: T_IsMonoidMonomorphism_372 -> AgdaAny #

d_cong_1170 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_Homomorphic'8320'_1174 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_IsNearSemiringHomomorphism_1184 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsNearSemiringIsomorphism_1186 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsNearSemiringMonomorphism_1188 :: p -> p -> p -> p -> p -> p -> p -> () #

d_'42''45'homo_1192 :: T_IsNearSemiringHomomorphism_916 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_1194 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringHomomorphism_916 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_1194 :: (AgdaAny -> AgdaAny) -> T_IsNearSemiringHomomorphism_916 -> T_IsMagmaHomomorphism_176 #

d_homo_1196 :: T_IsNearSemiringHomomorphism_916 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1198 :: T_IsNearSemiringHomomorphism_916 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_1200 :: T_IsNearSemiringHomomorphism_916 -> T_IsMonoidHomomorphism_350 #

d_ε'45'homo_1202 :: T_IsNearSemiringHomomorphism_916 -> AgdaAny #

d_isRelHomomorphism_1204 :: T_IsNearSemiringHomomorphism_916 -> T_IsRelHomomorphism_42 #

d_cong_1206 :: T_IsNearSemiringHomomorphism_916 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_1210 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_1212 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_1212 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMagmaIsomorphism_1214 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaIsomorphism_218 #

du_'42''45'isMagmaIsomorphism_1214 :: (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaIsomorphism_218 #

d_'42''45'isMagmaMonomorphism_1216 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_1216 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaMonomorphism_194 #

d_homo_1218 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1220 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaHomomorphism_176 #

d_isMagmaIsomorphism_1222 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_1222 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaIsomorphism_218 #

d_isMagmaMonomorphism_1224 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1224 :: T_IsNearSemiringIsomorphism_986 -> T_IsMagmaMonomorphism_194 #

d_'43''45'isMonoidHomomorphism_1226 :: T_IsNearSemiringIsomorphism_986 -> T_IsMonoidHomomorphism_350 #

d_'43''45'isMonoidIsomorphism_1228 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMonoidIsomorphism_404 #

du_'43''45'isMonoidIsomorphism_1228 :: (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMonoidIsomorphism_404 #

d_'43''45'isMonoidMonomorphism_1230 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsMonoidMonomorphism_372 #

du_'43''45'isMonoidMonomorphism_1230 :: T_IsNearSemiringIsomorphism_986 -> T_IsMonoidMonomorphism_372 #

d_ε'45'homo_1232 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny #

d_injective_1234 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringHomomorphism_1236 :: T_IsNearSemiringIsomorphism_986 -> T_IsNearSemiringHomomorphism_916 #

d_isNearSemiringMonomorphism_1238 :: T_IsNearSemiringIsomorphism_986 -> T_IsNearSemiringMonomorphism_944 #

d_isRelHomomorphism_1240 :: T_IsNearSemiringIsomorphism_986 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_1242 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_1242 :: T_IsNearSemiringIsomorphism_986 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_1244 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringIsomorphism_986 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1244 :: T_IsNearSemiringIsomorphism_986 -> T_IsRelMonomorphism_64 #

d_surjective_1246 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny -> T_Σ_14 #

d_cong_1248 :: T_IsNearSemiringIsomorphism_986 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_1252 :: T_IsNearSemiringMonomorphism_944 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_1254 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_1254 :: T_IsNearSemiringMonomorphism_944 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMagmaMonomorphism_1256 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_1256 :: (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsMagmaMonomorphism_194 #

d_homo_1258 :: T_IsNearSemiringMonomorphism_944 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1260 :: T_IsNearSemiringMonomorphism_944 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_1262 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1262 :: T_IsNearSemiringMonomorphism_944 -> T_IsMagmaMonomorphism_194 #

d_'43''45'isMonoidHomomorphism_1264 :: T_IsNearSemiringMonomorphism_944 -> T_IsMonoidHomomorphism_350 #

d_'43''45'isMonoidMonomorphism_1266 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsMonoidMonomorphism_372 #

du_'43''45'isMonoidMonomorphism_1266 :: (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsMonoidMonomorphism_372 #

d_ε'45'homo_1268 :: T_IsNearSemiringMonomorphism_944 -> AgdaAny #

d_injective_1270 :: T_IsNearSemiringMonomorphism_944 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringHomomorphism_1272 :: T_IsNearSemiringMonomorphism_944 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_1274 :: T_IsNearSemiringMonomorphism_944 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_1276 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsNearSemiringMonomorphism_944 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1276 :: T_IsNearSemiringMonomorphism_944 -> T_IsRelMonomorphism_64 #

d_cong_1278 :: T_IsNearSemiringMonomorphism_944 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsSemiringHomomorphism_1282 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsSemiringHomomorphism_1282 #

Constructors

C_IsSemiringHomomorphism'46'constructor_26561 T_IsNearSemiringHomomorphism_916 AgdaAny

d_isNearSemiringHomomorphism_1290 :: T_IsSemiringHomomorphism_1282 -> T_IsNearSemiringHomomorphism_916 #

d_1'35''45'homo_1292 :: T_IsSemiringHomomorphism_1282 -> AgdaAny #

d_'42''45'homo_1296 :: T_IsSemiringHomomorphism_1282 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_1298 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1282 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_1298 :: T_IsSemiringHomomorphism_1282 -> T_IsMagmaHomomorphism_176 #

d_homo_1300 :: T_IsSemiringHomomorphism_1282 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1302 :: T_IsSemiringHomomorphism_1282 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_1304 :: T_IsSemiringHomomorphism_1282 -> T_IsMonoidHomomorphism_350 #

d_ε'45'homo_1306 :: T_IsSemiringHomomorphism_1282 -> AgdaAny #

d_isRelHomomorphism_1308 :: T_IsSemiringHomomorphism_1282 -> T_IsRelHomomorphism_42 #

d_cong_1310 :: T_IsSemiringHomomorphism_1282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMonoidHomomorphism_1312 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1282 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_1312 :: T_IsSemiringHomomorphism_1282 -> T_IsMonoidHomomorphism_350 #

d_IsSemiringMonomorphism_1316 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsSemiringMonomorphism_1316 #

Constructors

C_IsSemiringMonomorphism'46'constructor_27871 T_IsSemiringHomomorphism_1282 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isSemiringHomomorphism_1324 :: T_IsSemiringMonomorphism_1316 -> T_IsSemiringHomomorphism_1282 #

d_injective_1326 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_1330 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_1332 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_1332 :: T_IsSemiringMonomorphism_1316 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMonoidHomomorphism_1334 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_1334 :: T_IsSemiringMonomorphism_1316 -> T_IsMonoidHomomorphism_350 #

d_homo_1336 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1338 :: T_IsSemiringMonomorphism_1316 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_1340 :: T_IsSemiringMonomorphism_1316 -> T_IsMonoidHomomorphism_350 #

d_ε'45'homo_1342 :: T_IsSemiringMonomorphism_1316 -> AgdaAny #

d_1'35''45'homo_1344 :: T_IsSemiringMonomorphism_1316 -> AgdaAny #

d_isNearSemiringHomomorphism_1346 :: T_IsSemiringMonomorphism_1316 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_1348 :: T_IsSemiringMonomorphism_1316 -> T_IsRelHomomorphism_42 #

d_cong_1350 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringMonomorphism_1352 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsNearSemiringMonomorphism_944 #

du_isNearSemiringMonomorphism_1352 :: T_IsSemiringMonomorphism_1316 -> T_IsNearSemiringMonomorphism_944 #

d_'42''45'isMagmaMonomorphism_1356 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_1356 :: T_IsSemiringMonomorphism_1316 -> T_IsMagmaMonomorphism_194 #

d_'43''45'isMonoidMonomorphism_1358 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

du_'43''45'isMonoidMonomorphism_1358 :: T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

d_'42''45'isMonoidMonomorphism_1360 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

du_'42''45'isMonoidMonomorphism_1360 :: T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

d_IsSemiringIsomorphism_1364 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsSemiringIsomorphism_1364 #

Constructors

C_IsSemiringIsomorphism'46'constructor_29931 T_IsSemiringMonomorphism_1316 (AgdaAny -> T_Σ_14)

d_isSemiringMonomorphism_1372 :: T_IsSemiringIsomorphism_1364 -> T_IsSemiringMonomorphism_1316 #

d_surjective_1374 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> T_Σ_14 #

d_'42''45'homo_1378 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_1380 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_1380 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMagmaMonomorphism_1382 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_1382 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaMonomorphism_194 #

d_'42''45'isMonoidHomomorphism_1384 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_1384 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidHomomorphism_350 #

d_'42''45'isMonoidMonomorphism_1386 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

du_'42''45'isMonoidMonomorphism_1386 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

d_homo_1388 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1390 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_1392 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidHomomorphism_350 #

d_'43''45'isMonoidMonomorphism_1394 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

du_'43''45'isMonoidMonomorphism_1394 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

d_ε'45'homo_1396 :: T_IsSemiringIsomorphism_1364 -> AgdaAny #

d_1'35''45'homo_1398 :: T_IsSemiringIsomorphism_1364 -> AgdaAny #

d_injective_1400 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringHomomorphism_1402 :: T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringHomomorphism_916 #

d_isNearSemiringMonomorphism_1404 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringMonomorphism_944 #

du_isNearSemiringMonomorphism_1404 :: T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringMonomorphism_944 #

d_isRelHomomorphism_1406 :: T_IsSemiringIsomorphism_1364 -> T_IsRelHomomorphism_42 #

d_isSemiringHomomorphism_1408 :: T_IsSemiringIsomorphism_1364 -> T_IsSemiringHomomorphism_1282 #

d_cong_1410 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringIsomorphism_1412 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringIsomorphism_986 #

du_isNearSemiringIsomorphism_1412 :: T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringIsomorphism_986 #

d_'42''45'isMagmaIsomorphism_1416 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMagmaIsomorphism_218 #

du_'42''45'isMagmaIsomorphism_1416 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaIsomorphism_218 #

d_'43''45'isMonoidIsomorphism_1418 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

du_'43''45'isMonoidIsomorphism_1418 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

d_'42''45'isMonoidIsomorphism_1420 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawSemiring_174 -> T_RawSemiring_174 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

du_'42''45'isMonoidIsomorphism_1420 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

d__'42'__1438 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> AgdaAny #

du__'42'__1438 :: T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__1442 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1458 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> () #

d_IsGroupHomomorphism_1486 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsGroupIsomorphism_1488 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsGroupMonomorphism_1490 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_1494 :: T_IsGroupHomomorphism_622 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1496 :: T_IsGroupHomomorphism_622 -> T_IsMagmaHomomorphism_176 #

d_isMonoidHomomorphism_1498 :: T_IsGroupHomomorphism_622 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_1500 :: T_IsGroupHomomorphism_622 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_1502 :: T_IsGroupHomomorphism_622 -> AgdaAny #

d_'8315''185''45'homo_1504 :: T_IsGroupHomomorphism_622 -> AgdaAny -> AgdaAny #

d_cong_1506 :: T_IsGroupHomomorphism_622 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_1510 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isGroupHomomorphism_1512 :: T_IsGroupIsomorphism_686 -> T_IsGroupHomomorphism_622 #

d_isGroupMonomorphism_1514 :: T_IsGroupIsomorphism_686 -> T_IsGroupMonomorphism_648 #

d_isMagmaHomomorphism_1516 :: T_IsGroupIsomorphism_686 -> T_IsMagmaHomomorphism_176 #

d_isMagmaIsomorphism_1518 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_1518 :: T_IsGroupIsomorphism_686 -> T_IsMagmaIsomorphism_218 #

d_isMagmaMonomorphism_1520 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1520 :: T_IsGroupIsomorphism_686 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_1522 :: T_IsGroupIsomorphism_686 -> T_IsMonoidHomomorphism_350 #

d_isMonoidIsomorphism_1524 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMonoidIsomorphism_404 #

du_isMonoidIsomorphism_1524 :: (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMonoidIsomorphism_404 #

d_isMonoidMonomorphism_1526 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMonoidMonomorphism_372 #

du_isMonoidMonomorphism_1526 :: T_IsGroupIsomorphism_686 -> T_IsMonoidMonomorphism_372 #

d_isRelHomomorphism_1528 :: T_IsGroupIsomorphism_686 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_1530 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_1530 :: T_IsGroupIsomorphism_686 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_1532 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1532 :: T_IsGroupIsomorphism_686 -> T_IsRelMonomorphism_64 #

d_surjective_1534 :: T_IsGroupIsomorphism_686 -> AgdaAny -> T_Σ_14 #

d_ε'45'homo_1536 :: T_IsGroupIsomorphism_686 -> AgdaAny #

d_'8315''185''45'homo_1538 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny #

d_homo_1540 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_1542 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_1546 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isGroupHomomorphism_1548 :: T_IsGroupMonomorphism_648 -> T_IsGroupHomomorphism_622 #

d_isMagmaHomomorphism_1550 :: T_IsGroupMonomorphism_648 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_1552 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1552 :: T_IsGroupMonomorphism_648 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_1554 :: T_IsGroupMonomorphism_648 -> T_IsMonoidHomomorphism_350 #

d_isMonoidMonomorphism_1556 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsMonoidMonomorphism_372 #

du_isMonoidMonomorphism_1556 :: (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsMonoidMonomorphism_372 #

d_isRelHomomorphism_1558 :: T_IsGroupMonomorphism_648 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_1560 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1560 :: T_IsGroupMonomorphism_648 -> T_IsRelMonomorphism_64 #

d_ε'45'homo_1562 :: T_IsGroupMonomorphism_648 -> AgdaAny #

d_'8315''185''45'homo_1564 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny #

d_homo_1566 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_1568 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMagmaHomomorphism_1572 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaIsomorphism_1574 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaMonomorphism_1576 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_1580 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_1582 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_cong_1584 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_1588 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_1590 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1592 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_1594 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_isRelHomomorphism_1596 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_1598 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_1598 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_1600 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1600 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_surjective_1602 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_cong_1604 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_1608 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_1610 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1612 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_1614 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_1616 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1616 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_cong_1618 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_Homomorphic'8322'_1626 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_IsRingWithoutOneHomomorphism_1632 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsRingWithoutOneHomomorphism_1632 #

Constructors

C_IsRingWithoutOneHomomorphism'46'constructor_33433 T_IsGroupHomomorphism_622 (AgdaAny -> AgdaAny -> AgdaAny)

d_'43''45'isGroupHomomorphism_1640 :: T_IsRingWithoutOneHomomorphism_1632 -> T_IsGroupHomomorphism_622 #

d_'42''45'homo_1642 :: T_IsRingWithoutOneHomomorphism_1632 -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_1646 :: T_IsRingWithoutOneHomomorphism_1632 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1648 :: T_IsRingWithoutOneHomomorphism_1632 -> T_IsMagmaHomomorphism_176 #

d_ε'45'homo_1650 :: T_IsRingWithoutOneHomomorphism_1632 -> AgdaAny #

d_isMonoidHomomorphism_1652 :: T_IsRingWithoutOneHomomorphism_1632 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_1654 :: T_IsRingWithoutOneHomomorphism_1632 -> T_IsRelHomomorphism_42 #

d_'8315''185''45'homo_1656 :: T_IsRingWithoutOneHomomorphism_1632 -> AgdaAny -> AgdaAny #

d_cong_1658 :: T_IsRingWithoutOneHomomorphism_1632 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_1660 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneHomomorphism_1632 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_1660 :: T_IsRingWithoutOneHomomorphism_1632 -> T_IsMagmaHomomorphism_176 #

d_IsRingWithoutOneMonomorphism_1664 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsRingWithoutOneMonomorphism_1664 #

Constructors

C_IsRingWithoutOneMonomorphism'46'constructor_34691 T_IsRingWithoutOneHomomorphism_1632 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isRingWithoutOneHomomorphism_1672 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsRingWithoutOneHomomorphism_1632 #

d_injective_1674 :: T_IsRingWithoutOneMonomorphism_1664 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_1678 :: T_IsRingWithoutOneMonomorphism_1664 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_1680 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneMonomorphism_1664 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_1680 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsMagmaHomomorphism_176 #

d_homo_1682 :: T_IsRingWithoutOneMonomorphism_1664 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'43''45'isGroupHomomorphism_1684 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsGroupHomomorphism_622 #

d_isMagmaHomomorphism_1686 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsMagmaHomomorphism_176 #

d_ε'45'homo_1688 :: T_IsRingWithoutOneMonomorphism_1664 -> AgdaAny #

d_isMonoidHomomorphism_1690 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_1692 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsRelHomomorphism_42 #

d_'8315''185''45'homo_1694 :: T_IsRingWithoutOneMonomorphism_1664 -> AgdaAny -> AgdaAny #

d_cong_1696 :: T_IsRingWithoutOneMonomorphism_1664 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'43''45'isGroupMonomorphism_1698 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneMonomorphism_1664 -> T_IsGroupMonomorphism_648 #

du_'43''45'isGroupMonomorphism_1698 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsGroupMonomorphism_648 #

d_isMagmaMonomorphism_1702 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneMonomorphism_1664 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1702 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsMagmaMonomorphism_194 #

d_isMonoidMonomorphism_1704 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneMonomorphism_1664 -> T_IsMonoidMonomorphism_372 #

du_isMonoidMonomorphism_1704 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsMonoidMonomorphism_372 #

d_isRelMonomorphism_1706 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneMonomorphism_1664 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1706 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsRelMonomorphism_64 #

d_'42''45'isMagmaMonomorphism_1708 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneMonomorphism_1664 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_1708 :: T_IsRingWithoutOneMonomorphism_1664 -> T_IsMagmaMonomorphism_194 #

d_IsRingWithoutOneIsoMorphism_1712 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsRingWithoutOneIsoMorphism_1712 #

Constructors

C_IsRingWithoutOneIsoMorphism'46'constructor_36755 T_IsRingWithoutOneMonomorphism_1664 (AgdaAny -> T_Σ_14)

d_isRingWithoutOneMonomorphism_1720 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsRingWithoutOneMonomorphism_1664 #

d_surjective_1722 :: T_IsRingWithoutOneIsoMorphism_1712 -> AgdaAny -> T_Σ_14 #

d_'42''45'homo_1726 :: T_IsRingWithoutOneIsoMorphism_1712 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_1728 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_1728 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMagmaMonomorphism_1730 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_1730 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaMonomorphism_194 #

d_homo_1732 :: T_IsRingWithoutOneIsoMorphism_1712 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'43''45'isGroupHomomorphism_1734 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsGroupHomomorphism_622 #

d_'43''45'isGroupMonomorphism_1736 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsGroupMonomorphism_648 #

du_'43''45'isGroupMonomorphism_1736 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsGroupMonomorphism_648 #

d_isMagmaHomomorphism_1738 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_1740 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1740 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaMonomorphism_194 #

d_isMonoidMonomorphism_1742 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMonoidMonomorphism_372 #

du_isMonoidMonomorphism_1742 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMonoidMonomorphism_372 #

d_ε'45'homo_1744 :: T_IsRingWithoutOneIsoMorphism_1712 -> AgdaAny #

d_injective_1746 :: T_IsRingWithoutOneIsoMorphism_1712 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMonoidHomomorphism_1748 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_1750 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_1752 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1752 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsRelMonomorphism_64 #

d_isRingWithoutOneHomomorphism_1754 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsRingWithoutOneHomomorphism_1632 #

d_'8315''185''45'homo_1756 :: T_IsRingWithoutOneIsoMorphism_1712 -> AgdaAny -> AgdaAny #

d_cong_1758 :: T_IsRingWithoutOneIsoMorphism_1712 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'43''45'isGroupIsomorphism_1760 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsGroupIsomorphism_686 #

du_'43''45'isGroupIsomorphism_1760 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsGroupIsomorphism_686 #

d_isMagmaIsomorphism_1764 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_1764 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaIsomorphism_218 #

d_isMonoidIsomorphism_1766 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMonoidIsomorphism_404 #

du_isMonoidIsomorphism_1766 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMonoidIsomorphism_404 #

d_isRelIsomorphism_1768 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_1768 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsRelIsomorphism_94 #

d_'42''45'isMagmaIsomorphism_1770 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRingWithoutOne_222 -> T_RawRingWithoutOne_222 -> (AgdaAny -> AgdaAny) -> T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaIsomorphism_218 #

du_'42''45'isMagmaIsomorphism_1770 :: T_IsRingWithoutOneIsoMorphism_1712 -> T_IsMagmaIsomorphism_218 #

d__'8776'__1792 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> AgdaAny -> AgdaAny -> () #

d_'45'__1806 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> AgdaAny -> AgdaAny #

du_'45'__1806 :: T_RawRing_268 -> AgdaAny -> AgdaAny #

d_Carrier_1812 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> () #

d_IsGroupHomomorphism_1852 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsGroupIsomorphism_1854 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsGroupMonomorphism_1856 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_1860 :: T_IsGroupHomomorphism_622 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1862 :: T_IsGroupHomomorphism_622 -> T_IsMagmaHomomorphism_176 #

d_isMonoidHomomorphism_1864 :: T_IsGroupHomomorphism_622 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_1866 :: T_IsGroupHomomorphism_622 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_1868 :: T_IsGroupHomomorphism_622 -> AgdaAny #

d_'8315''185''45'homo_1870 :: T_IsGroupHomomorphism_622 -> AgdaAny -> AgdaAny #

d_cong_1872 :: T_IsGroupHomomorphism_622 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_1876 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isGroupHomomorphism_1878 :: T_IsGroupIsomorphism_686 -> T_IsGroupHomomorphism_622 #

d_isGroupMonomorphism_1880 :: T_IsGroupIsomorphism_686 -> T_IsGroupMonomorphism_648 #

d_isMagmaHomomorphism_1882 :: T_IsGroupIsomorphism_686 -> T_IsMagmaHomomorphism_176 #

d_isMagmaIsomorphism_1884 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_1884 :: T_IsGroupIsomorphism_686 -> T_IsMagmaIsomorphism_218 #

d_isMagmaMonomorphism_1886 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1886 :: T_IsGroupIsomorphism_686 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_1888 :: T_IsGroupIsomorphism_686 -> T_IsMonoidHomomorphism_350 #

d_isMonoidIsomorphism_1890 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMonoidIsomorphism_404 #

du_isMonoidIsomorphism_1890 :: (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMonoidIsomorphism_404 #

d_isMonoidMonomorphism_1892 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsMonoidMonomorphism_372 #

du_isMonoidMonomorphism_1892 :: T_IsGroupIsomorphism_686 -> T_IsMonoidMonomorphism_372 #

d_isRelHomomorphism_1894 :: T_IsGroupIsomorphism_686 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_1896 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_1896 :: T_IsGroupIsomorphism_686 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_1898 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsGroupIsomorphism_686 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1898 :: T_IsGroupIsomorphism_686 -> T_IsRelMonomorphism_64 #

d_surjective_1900 :: T_IsGroupIsomorphism_686 -> AgdaAny -> T_Σ_14 #

d_ε'45'homo_1902 :: T_IsGroupIsomorphism_686 -> AgdaAny #

d_'8315''185''45'homo_1904 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny #

d_homo_1906 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_1908 :: T_IsGroupIsomorphism_686 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_1912 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isGroupHomomorphism_1914 :: T_IsGroupMonomorphism_648 -> T_IsGroupHomomorphism_622 #

d_isMagmaHomomorphism_1916 :: T_IsGroupMonomorphism_648 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_1918 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1918 :: T_IsGroupMonomorphism_648 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_1920 :: T_IsGroupMonomorphism_648 -> T_IsMonoidHomomorphism_350 #

d_isMonoidMonomorphism_1922 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsMonoidMonomorphism_372 #

du_isMonoidMonomorphism_1922 :: (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsMonoidMonomorphism_372 #

d_isRelHomomorphism_1924 :: T_IsGroupMonomorphism_648 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_1926 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsGroupMonomorphism_648 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1926 :: T_IsGroupMonomorphism_648 -> T_IsRelMonomorphism_64 #

d_ε'45'homo_1928 :: T_IsGroupMonomorphism_648 -> AgdaAny #

d_'8315''185''45'homo_1930 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny #

d_homo_1932 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_1934 :: T_IsGroupMonomorphism_648 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMonoidHomomorphism_1938 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMonoidIsomorphism_1940 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMonoidMonomorphism_1942 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_1946 :: T_IsMonoidHomomorphism_350 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1948 :: T_IsMonoidHomomorphism_350 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_1950 :: T_IsMonoidHomomorphism_350 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_1952 :: T_IsMonoidHomomorphism_350 -> AgdaAny #

d_cong_1954 :: T_IsMonoidHomomorphism_350 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_1958 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_1960 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1962 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaHomomorphism_176 #

d_isMagmaIsomorphism_1964 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_1964 :: (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaIsomorphism_218 #

d_isMagmaMonomorphism_1966 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1966 :: T_IsMonoidIsomorphism_404 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_1968 :: T_IsMonoidIsomorphism_404 -> T_IsMonoidHomomorphism_350 #

d_isMonoidMonomorphism_1970 :: T_IsMonoidIsomorphism_404 -> T_IsMonoidMonomorphism_372 #

d_isRelHomomorphism_1972 :: T_IsMonoidIsomorphism_404 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_1974 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_1974 :: T_IsMonoidIsomorphism_404 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_1976 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsMonoidIsomorphism_404 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1976 :: T_IsMonoidIsomorphism_404 -> T_IsRelMonomorphism_64 #

d_surjective_1978 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> T_Σ_14 #

d_ε'45'homo_1980 :: T_IsMonoidIsomorphism_404 -> AgdaAny #

d_cong_1982 :: T_IsMonoidIsomorphism_404 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_1986 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_1988 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_1990 :: T_IsMonoidMonomorphism_372 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_1992 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_1992 :: (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsMagmaMonomorphism_194 #

d_isMonoidHomomorphism_1994 :: T_IsMonoidMonomorphism_372 -> T_IsMonoidHomomorphism_350 #

d_isRelHomomorphism_1996 :: T_IsMonoidMonomorphism_372 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_1998 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsMonoidMonomorphism_372 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_1998 :: T_IsMonoidMonomorphism_372 -> T_IsRelMonomorphism_64 #

d_ε'45'homo_2000 :: T_IsMonoidMonomorphism_372 -> AgdaAny #

d_cong_2002 :: T_IsMonoidMonomorphism_372 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_Homomorphic'8321'_2008 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_IsSemiringHomomorphism_2016 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsSemiringIsomorphism_2018 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsSemiringMonomorphism_2020 :: p -> p -> p -> p -> p -> p -> p -> () #

d_'42''45'homo_2024 :: T_IsSemiringHomomorphism_1282 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_2026 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1282 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_2026 :: T_IsSemiringHomomorphism_1282 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMonoidHomomorphism_2028 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1282 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_2028 :: (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1282 -> T_IsMonoidHomomorphism_350 #

d_homo_2030 :: T_IsSemiringHomomorphism_1282 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2032 :: T_IsSemiringHomomorphism_1282 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_2034 :: T_IsSemiringHomomorphism_1282 -> T_IsMonoidHomomorphism_350 #

d_ε'45'homo_2036 :: T_IsSemiringHomomorphism_1282 -> AgdaAny #

d_1'35''45'homo_2038 :: T_IsSemiringHomomorphism_1282 -> AgdaAny #

d_isNearSemiringHomomorphism_2040 :: T_IsSemiringHomomorphism_1282 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_2042 :: T_IsSemiringHomomorphism_1282 -> T_IsRelHomomorphism_42 #

d_cong_2044 :: T_IsSemiringHomomorphism_1282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_2048 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_2050 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_2050 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMagmaIsomorphism_2052 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMagmaIsomorphism_218 #

du_'42''45'isMagmaIsomorphism_2052 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaIsomorphism_218 #

d_'42''45'isMagmaMonomorphism_2054 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_2054 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaMonomorphism_194 #

d_'42''45'isMonoidHomomorphism_2056 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_2056 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidHomomorphism_350 #

d_'42''45'isMonoidIsomorphism_2058 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

du_'42''45'isMonoidIsomorphism_2058 :: (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

d_'42''45'isMonoidMonomorphism_2060 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

du_'42''45'isMonoidMonomorphism_2060 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

d_homo_2062 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2064 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_2066 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidHomomorphism_350 #

d_'43''45'isMonoidIsomorphism_2068 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

du_'43''45'isMonoidIsomorphism_2068 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

d_'43''45'isMonoidMonomorphism_2070 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

du_'43''45'isMonoidMonomorphism_2070 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

d_ε'45'homo_2072 :: T_IsSemiringIsomorphism_1364 -> AgdaAny #

d_1'35''45'homo_2074 :: T_IsSemiringIsomorphism_1364 -> AgdaAny #

d_injective_2076 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringHomomorphism_2078 :: T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringHomomorphism_916 #

d_isNearSemiringIsomorphism_2080 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringIsomorphism_986 #

du_isNearSemiringIsomorphism_2080 :: (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringIsomorphism_986 #

d_isNearSemiringMonomorphism_2082 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringMonomorphism_944 #

du_isNearSemiringMonomorphism_2082 :: T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringMonomorphism_944 #

d_isRelHomomorphism_2084 :: T_IsSemiringIsomorphism_1364 -> T_IsRelHomomorphism_42 #

d_isSemiringHomomorphism_2086 :: T_IsSemiringIsomorphism_1364 -> T_IsSemiringHomomorphism_1282 #

d_isSemiringMonomorphism_2088 :: T_IsSemiringIsomorphism_1364 -> T_IsSemiringMonomorphism_1316 #

d_surjective_2090 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> T_Σ_14 #

d_cong_2092 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_2096 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_2098 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_2098 :: T_IsSemiringMonomorphism_1316 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMagmaMonomorphism_2100 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_2100 :: T_IsSemiringMonomorphism_1316 -> T_IsMagmaMonomorphism_194 #

d_'42''45'isMonoidHomomorphism_2102 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_2102 :: T_IsSemiringMonomorphism_1316 -> T_IsMonoidHomomorphism_350 #

d_'42''45'isMonoidMonomorphism_2104 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

du_'42''45'isMonoidMonomorphism_2104 :: (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

d_homo_2106 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2108 :: T_IsSemiringMonomorphism_1316 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_2110 :: T_IsSemiringMonomorphism_1316 -> T_IsMonoidHomomorphism_350 #

d_'43''45'isMonoidMonomorphism_2112 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

du_'43''45'isMonoidMonomorphism_2112 :: T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

d_ε'45'homo_2114 :: T_IsSemiringMonomorphism_1316 -> AgdaAny #

d_1'35''45'homo_2116 :: T_IsSemiringMonomorphism_1316 -> AgdaAny #

d_injective_2118 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringHomomorphism_2120 :: T_IsSemiringMonomorphism_1316 -> T_IsNearSemiringHomomorphism_916 #

d_isNearSemiringMonomorphism_2122 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsNearSemiringMonomorphism_944 #

du_isNearSemiringMonomorphism_2122 :: (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsNearSemiringMonomorphism_944 #

d_isRelHomomorphism_2124 :: T_IsSemiringMonomorphism_1316 -> T_IsRelHomomorphism_42 #

d_isSemiringHomomorphism_2126 :: T_IsSemiringMonomorphism_1316 -> T_IsSemiringHomomorphism_1282 #

d_cong_2128 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsRingHomomorphism_2132 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsRingHomomorphism_2132 #

Constructors

C_IsRingHomomorphism'46'constructor_41447 T_IsSemiringHomomorphism_1282 (AgdaAny -> AgdaAny)

d_isSemiringHomomorphism_2140 :: T_IsRingHomomorphism_2132 -> T_IsSemiringHomomorphism_1282 #

d_'45''8255'homo_2142 :: T_IsRingHomomorphism_2132 -> AgdaAny -> AgdaAny #

d_'42''45'homo_2146 :: T_IsRingHomomorphism_2132 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_2148 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingHomomorphism_2132 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_2148 :: T_IsRingHomomorphism_2132 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMonoidHomomorphism_2150 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingHomomorphism_2132 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_2150 :: T_IsRingHomomorphism_2132 -> T_IsMonoidHomomorphism_350 #

d_homo_2152 :: T_IsRingHomomorphism_2132 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2154 :: T_IsRingHomomorphism_2132 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_2156 :: T_IsRingHomomorphism_2132 -> T_IsMonoidHomomorphism_350 #

d_ε'45'homo_2158 :: T_IsRingHomomorphism_2132 -> AgdaAny #

d_1'35''45'homo_2160 :: T_IsRingHomomorphism_2132 -> AgdaAny #

d_isNearSemiringHomomorphism_2162 :: T_IsRingHomomorphism_2132 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_2164 :: T_IsRingHomomorphism_2132 -> T_IsRelHomomorphism_42 #

d_cong_2166 :: T_IsRingHomomorphism_2132 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'43''45'isGroupHomomorphism_2168 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingHomomorphism_2132 -> T_IsGroupHomomorphism_622 #

du_'43''45'isGroupHomomorphism_2168 :: T_IsRingHomomorphism_2132 -> T_IsGroupHomomorphism_622 #

d_IsRingMonomorphism_2172 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsRingMonomorphism_2172 #

Constructors

C_IsRingMonomorphism'46'constructor_42933 T_IsRingHomomorphism_2132 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isRingHomomorphism_2180 :: T_IsRingMonomorphism_2172 -> T_IsRingHomomorphism_2132 #

d_injective_2182 :: T_IsRingMonomorphism_2172 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_2186 :: T_IsRingMonomorphism_2172 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_2188 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_2172 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_2188 :: T_IsRingMonomorphism_2172 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMonoidHomomorphism_2190 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_2172 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_2190 :: T_IsRingMonomorphism_2172 -> T_IsMonoidHomomorphism_350 #

d_homo_2192 :: T_IsRingMonomorphism_2172 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'43''45'isGroupHomomorphism_2194 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_2172 -> T_IsGroupHomomorphism_622 #

du_'43''45'isGroupHomomorphism_2194 :: T_IsRingMonomorphism_2172 -> T_IsGroupHomomorphism_622 #

d_isMagmaHomomorphism_2196 :: T_IsRingMonomorphism_2172 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_2198 :: T_IsRingMonomorphism_2172 -> T_IsMonoidHomomorphism_350 #

d_'45''8255'homo_2200 :: T_IsRingMonomorphism_2172 -> AgdaAny -> AgdaAny #

d_ε'45'homo_2202 :: T_IsRingMonomorphism_2172 -> AgdaAny #

d_1'35''45'homo_2204 :: T_IsRingMonomorphism_2172 -> AgdaAny #

d_isNearSemiringHomomorphism_2206 :: T_IsRingMonomorphism_2172 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_2208 :: T_IsRingMonomorphism_2172 -> T_IsRelHomomorphism_42 #

d_isSemiringHomomorphism_2210 :: T_IsRingMonomorphism_2172 -> T_IsSemiringHomomorphism_1282 #

d_cong_2212 :: T_IsRingMonomorphism_2172 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isSemiringMonomorphism_2214 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_2172 -> T_IsSemiringMonomorphism_1316 #

du_isSemiringMonomorphism_2214 :: T_IsRingMonomorphism_2172 -> T_IsSemiringMonomorphism_1316 #

d_'43''45'isGroupMonomorphism_2216 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_2172 -> T_IsGroupMonomorphism_648 #

du_'43''45'isGroupMonomorphism_2216 :: T_IsRingMonomorphism_2172 -> T_IsGroupMonomorphism_648 #

d_isMagmaMonomorphism_2220 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_2172 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_2220 :: T_IsRingMonomorphism_2172 -> T_IsMagmaMonomorphism_194 #

d_isMonoidMonomorphism_2222 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_2172 -> T_IsMonoidMonomorphism_372 #

du_isMonoidMonomorphism_2222 :: T_IsRingMonomorphism_2172 -> T_IsMonoidMonomorphism_372 #

d_isRelMonomorphism_2224 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_2172 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2224 :: T_IsRingMonomorphism_2172 -> T_IsRelMonomorphism_64 #

d_'42''45'isMonoidMonomorphism_2226 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_2172 -> T_IsMonoidMonomorphism_372 #

du_'42''45'isMonoidMonomorphism_2226 :: T_IsRingMonomorphism_2172 -> T_IsMonoidMonomorphism_372 #

d_isMagmaMonomorphism_2230 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingMonomorphism_2172 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_2230 :: T_IsRingMonomorphism_2172 -> T_IsMagmaMonomorphism_194 #

d_IsRingIsomorphism_2234 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsRingIsomorphism_2234 #

Constructors

C_IsRingIsomorphism'46'constructor_45617 T_IsRingMonomorphism_2172 (AgdaAny -> T_Σ_14)

d_isRingMonomorphism_2242 :: T_IsRingIsomorphism_2234 -> T_IsRingMonomorphism_2172 #

d_surjective_2244 :: T_IsRingIsomorphism_2234 -> AgdaAny -> T_Σ_14 #

d_'42''45'homo_2248 :: T_IsRingIsomorphism_2234 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_2250 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_2250 :: T_IsRingIsomorphism_2234 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_2252 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsMagmaMonomorphism_194 #

du_isMagmaMonomorphism_2252 :: T_IsRingIsomorphism_2234 -> T_IsMagmaMonomorphism_194 #

d_'42''45'isMonoidHomomorphism_2254 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_2254 :: T_IsRingIsomorphism_2234 -> T_IsMonoidHomomorphism_350 #

d_'42''45'isMonoidMonomorphism_2256 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsMonoidMonomorphism_372 #

du_'42''45'isMonoidMonomorphism_2256 :: T_IsRingIsomorphism_2234 -> T_IsMonoidMonomorphism_372 #

d_homo_2258 :: T_IsRingIsomorphism_2234 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'43''45'isGroupHomomorphism_2260 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsGroupHomomorphism_622 #

du_'43''45'isGroupHomomorphism_2260 :: T_IsRingIsomorphism_2234 -> T_IsGroupHomomorphism_622 #

d_'43''45'isGroupMonomorphism_2262 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsGroupMonomorphism_648 #

du_'43''45'isGroupMonomorphism_2262 :: T_IsRingIsomorphism_2234 -> T_IsGroupMonomorphism_648 #

d_isMagmaHomomorphism_2264 :: T_IsRingIsomorphism_2234 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_2266 :: T_IsRingIsomorphism_2234 -> T_IsMonoidHomomorphism_350 #

d_'45''8255'homo_2268 :: T_IsRingIsomorphism_2234 -> AgdaAny -> AgdaAny #

d_ε'45'homo_2270 :: T_IsRingIsomorphism_2234 -> AgdaAny #

d_1'35''45'homo_2272 :: T_IsRingIsomorphism_2234 -> AgdaAny #

d_injective_2274 :: T_IsRingIsomorphism_2234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringHomomorphism_2276 :: T_IsRingIsomorphism_2234 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_2278 :: T_IsRingIsomorphism_2234 -> T_IsRelHomomorphism_42 #

d_isRingHomomorphism_2280 :: T_IsRingIsomorphism_2234 -> T_IsRingHomomorphism_2132 #

d_isSemiringHomomorphism_2282 :: T_IsRingIsomorphism_2234 -> T_IsSemiringHomomorphism_1282 #

d_isSemiringMonomorphism_2284 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsSemiringMonomorphism_1316 #

du_isSemiringMonomorphism_2284 :: T_IsRingIsomorphism_2234 -> T_IsSemiringMonomorphism_1316 #

d_cong_2286 :: T_IsRingIsomorphism_2234 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isSemiringIsomorphism_2288 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsSemiringIsomorphism_1364 #

du_isSemiringIsomorphism_2288 :: T_IsRingIsomorphism_2234 -> T_IsSemiringIsomorphism_1364 #

d_'43''45'isGroupIsomorphism_2290 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsGroupIsomorphism_686 #

du_'43''45'isGroupIsomorphism_2290 :: T_IsRingIsomorphism_2234 -> T_IsGroupIsomorphism_686 #

d_isMagmaIsomorphism_2294 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_2294 :: T_IsRingIsomorphism_2234 -> T_IsMagmaIsomorphism_218 #

d_isMonoidIsomorphism_2296 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsMonoidIsomorphism_404 #

du_isMonoidIsomorphism_2296 :: T_IsRingIsomorphism_2234 -> T_IsMonoidIsomorphism_404 #

d_isRelIsomorphism_2298 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_2298 :: T_IsRingIsomorphism_2234 -> T_IsRelIsomorphism_94 #

d_'42''45'isMonoidIsomorphism_2300 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsMonoidIsomorphism_404 #

du_'42''45'isMonoidIsomorphism_2300 :: T_IsRingIsomorphism_2234 -> T_IsMonoidIsomorphism_404 #

d_isMagmaIsomorphism_2304 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawRing_268 -> T_RawRing_268 -> (AgdaAny -> AgdaAny) -> T_IsRingIsomorphism_2234 -> T_IsMagmaIsomorphism_218 #

du_isMagmaIsomorphism_2304 :: T_IsRingIsomorphism_2234 -> T_IsMagmaIsomorphism_218 #

d__'47''47'__2322 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny #

du__'47''47'__2322 :: T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'92''92'__2324 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny #

du__'92''92'__2324 :: T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8729'__2326 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny #

du__'8729'__2326 :: T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__2328 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> AgdaAny -> AgdaAny -> () #

d_Carrier_2334 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> () #

d_IsMagmaHomomorphism_2362 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaIsomorphism_2364 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaMonomorphism_2366 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_2370 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_2372 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_cong_2374 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2378 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2380 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2382 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_2384 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_isRelHomomorphism_2386 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_2388 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_2388 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_2390 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2390 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_surjective_2392 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_cong_2394 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2398 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2400 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2402 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_2404 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_2406 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2406 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_cong_2408 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMagmaHomomorphism_2412 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaIsomorphism_2414 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaMonomorphism_2416 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_2420 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_2422 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_cong_2424 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2428 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2430 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2432 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_2434 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_isRelHomomorphism_2436 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_2438 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_2438 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_2440 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2440 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_surjective_2442 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_cong_2444 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2448 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2450 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2452 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_2454 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_2456 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2456 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_cong_2458 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMagmaHomomorphism_2462 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaIsomorphism_2464 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaMonomorphism_2466 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_2470 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_2472 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_cong_2474 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2478 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2480 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2482 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_2484 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_isRelHomomorphism_2486 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_2488 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_2488 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_2490 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2490 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_surjective_2492 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_cong_2494 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2498 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2500 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2502 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_2504 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_2506 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2506 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_cong_2508 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_Homomorphic'8322'_2516 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_IsQuasigroupHomomorphism_2522 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsQuasigroupHomomorphism_2522 #

Constructors

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

d_isRelHomomorphism_2534 :: T_IsQuasigroupHomomorphism_2522 -> T_IsRelHomomorphism_42 #

d_'8729''45'homo_2536 :: T_IsQuasigroupHomomorphism_2522 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'92''92''45'homo_2538 :: T_IsQuasigroupHomomorphism_2522 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'homo_2540 :: T_IsQuasigroupHomomorphism_2522 -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_2544 :: T_IsQuasigroupHomomorphism_2522 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaHomomorphism_2546 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

du_'8729''45'isMagmaHomomorphism_2546 :: T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

d_'92''92''45'isMagmaHomomorphism_2548 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

du_'92''92''45'isMagmaHomomorphism_2548 :: T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

d_'47''47''45'isMagmaHomomorphism_2550 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

du_'47''47''45'isMagmaHomomorphism_2550 :: T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

d_IsQuasigroupMonomorphism_2554 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsQuasigroupMonomorphism_2554 #

Constructors

C_IsQuasigroupMonomorphism'46'constructor_51967 T_IsQuasigroupHomomorphism_2522 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isQuasigroupHomomorphism_2562 :: T_IsQuasigroupMonomorphism_2554 -> T_IsQuasigroupHomomorphism_2522 #

d_injective_2564 :: T_IsQuasigroupMonomorphism_2554 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'homo_2568 :: T_IsQuasigroupMonomorphism_2554 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'isMagmaHomomorphism_2570 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

du_'47''47''45'isMagmaHomomorphism_2570 :: T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

d_'92''92''45'homo_2572 :: T_IsQuasigroupMonomorphism_2554 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'92''92''45'isMagmaHomomorphism_2574 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

du_'92''92''45'isMagmaHomomorphism_2574 :: T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_2576 :: T_IsQuasigroupMonomorphism_2554 -> T_IsRelHomomorphism_42 #

d_'8729''45'homo_2578 :: T_IsQuasigroupMonomorphism_2554 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaHomomorphism_2580 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

du_'8729''45'isMagmaHomomorphism_2580 :: T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

d_cong_2582 :: T_IsQuasigroupMonomorphism_2554 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaMonomorphism_2584 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

du_'8729''45'isMagmaMonomorphism_2584 :: T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

d_'92''92''45'isMagmaMonomorphism_2586 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

du_'92''92''45'isMagmaMonomorphism_2586 :: T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

d_'47''47''45'isMagmaMonomorphism_2588 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

du_'47''47''45'isMagmaMonomorphism_2588 :: T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

d_isRelMonomorphism_2592 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2592 :: T_IsQuasigroupMonomorphism_2554 -> T_IsRelMonomorphism_64 #

d_IsQuasigroupIsomorphism_2596 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsQuasigroupIsomorphism_2596 #

Constructors

C_IsQuasigroupIsomorphism'46'constructor_54087 T_IsQuasigroupMonomorphism_2554 (AgdaAny -> T_Σ_14)

d_isQuasigroupMonomorphism_2604 :: T_IsQuasigroupIsomorphism_2596 -> T_IsQuasigroupMonomorphism_2554 #

d_surjective_2606 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> T_Σ_14 #

d_'47''47''45'homo_2610 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'isMagmaHomomorphism_2612 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

du_'47''47''45'isMagmaHomomorphism_2612 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

d_'47''47''45'isMagmaMonomorphism_2614 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

du_'47''47''45'isMagmaMonomorphism_2614 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

d_'92''92''45'homo_2616 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'92''92''45'isMagmaHomomorphism_2618 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

du_'92''92''45'isMagmaHomomorphism_2618 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

d_'92''92''45'isMagmaMonomorphism_2620 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

du_'92''92''45'isMagmaMonomorphism_2620 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

d_injective_2622 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isQuasigroupHomomorphism_2624 :: T_IsQuasigroupIsomorphism_2596 -> T_IsQuasigroupHomomorphism_2522 #

d_isRelHomomorphism_2626 :: T_IsQuasigroupIsomorphism_2596 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_2628 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2628 :: T_IsQuasigroupIsomorphism_2596 -> T_IsRelMonomorphism_64 #

d_'8729''45'homo_2630 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaHomomorphism_2632 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

du_'8729''45'isMagmaHomomorphism_2632 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

d_'8729''45'isMagmaMonomorphism_2634 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

du_'8729''45'isMagmaMonomorphism_2634 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

d_cong_2636 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaIsomorphism_2638 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

du_'8729''45'isMagmaIsomorphism_2638 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

d_'92''92''45'isMagmaIsomorphism_2640 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

du_'92''92''45'isMagmaIsomorphism_2640 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

d_'47''47''45'isMagmaIsomorphism_2642 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

du_'47''47''45'isMagmaIsomorphism_2642 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

d_isRelIsomorphism_2646 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawQuasigroup_326 -> T_RawQuasigroup_326 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_2646 :: T_IsQuasigroupIsomorphism_2596 -> T_IsRelIsomorphism_94 #

d__'8776'__2670 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> AgdaAny -> AgdaAny -> () #

d_Carrier_2676 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> () #

d_ε_2682 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> AgdaAny #

du_ε_2682 :: T_RawLoop_366 -> AgdaAny #

d_Homomorphic'8320'_2712 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_IsQuasigroupHomomorphism_2722 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsQuasigroupIsomorphism_2724 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsQuasigroupMonomorphism_2726 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaHomomorphism_2730 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaIsomorphism_2732 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaMonomorphism_2734 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_2738 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_2740 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_cong_2742 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2746 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2748 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2750 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_2752 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_isRelHomomorphism_2754 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_2756 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_2756 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_2758 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2758 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_surjective_2760 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_cong_2762 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2766 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2768 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2770 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_2772 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_2774 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2774 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_cong_2776 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'homo_2780 :: T_IsQuasigroupHomomorphism_2522 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'isMagmaHomomorphism_2782 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

du_'47''47''45'isMagmaHomomorphism_2782 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

d_'92''92''45'homo_2784 :: T_IsQuasigroupHomomorphism_2522 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'92''92''45'isMagmaHomomorphism_2786 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

du_'92''92''45'isMagmaHomomorphism_2786 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_2788 :: T_IsQuasigroupHomomorphism_2522 -> T_IsRelHomomorphism_42 #

d_'8729''45'homo_2790 :: T_IsQuasigroupHomomorphism_2522 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaHomomorphism_2792 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

du_'8729''45'isMagmaHomomorphism_2792 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupHomomorphism_2522 -> T_IsMagmaHomomorphism_176 #

d_cong_2794 :: T_IsQuasigroupHomomorphism_2522 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'homo_2798 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'isMagmaHomomorphism_2800 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

du_'47''47''45'isMagmaHomomorphism_2800 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

d_'47''47''45'isMagmaIsomorphism_2802 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

du_'47''47''45'isMagmaIsomorphism_2802 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

d_'47''47''45'isMagmaMonomorphism_2804 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

du_'47''47''45'isMagmaMonomorphism_2804 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

d_'92''92''45'homo_2806 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'92''92''45'isMagmaHomomorphism_2808 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

du_'92''92''45'isMagmaHomomorphism_2808 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

d_'92''92''45'isMagmaIsomorphism_2810 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

du_'92''92''45'isMagmaIsomorphism_2810 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

d_'92''92''45'isMagmaMonomorphism_2812 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

du_'92''92''45'isMagmaMonomorphism_2812 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

d_injective_2814 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isQuasigroupHomomorphism_2816 :: T_IsQuasigroupIsomorphism_2596 -> T_IsQuasigroupHomomorphism_2522 #

d_isQuasigroupMonomorphism_2818 :: T_IsQuasigroupIsomorphism_2596 -> T_IsQuasigroupMonomorphism_2554 #

d_isRelHomomorphism_2820 :: T_IsQuasigroupIsomorphism_2596 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_2822 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_2822 :: T_IsQuasigroupIsomorphism_2596 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_2824 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2824 :: T_IsQuasigroupIsomorphism_2596 -> T_IsRelMonomorphism_64 #

d_surjective_2826 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> T_Σ_14 #

d_'8729''45'homo_2828 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaHomomorphism_2830 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

du_'8729''45'isMagmaHomomorphism_2830 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaHomomorphism_176 #

d_'8729''45'isMagmaIsomorphism_2832 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

du_'8729''45'isMagmaIsomorphism_2832 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaIsomorphism_218 #

d_'8729''45'isMagmaMonomorphism_2834 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

du_'8729''45'isMagmaMonomorphism_2834 :: T_IsQuasigroupIsomorphism_2596 -> T_IsMagmaMonomorphism_194 #

d_cong_2836 :: T_IsQuasigroupIsomorphism_2596 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'homo_2840 :: T_IsQuasigroupMonomorphism_2554 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'isMagmaHomomorphism_2842 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

du_'47''47''45'isMagmaHomomorphism_2842 :: T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

d_'47''47''45'isMagmaMonomorphism_2844 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

du_'47''47''45'isMagmaMonomorphism_2844 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

d_'92''92''45'homo_2846 :: T_IsQuasigroupMonomorphism_2554 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'92''92''45'isMagmaHomomorphism_2848 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

du_'92''92''45'isMagmaHomomorphism_2848 :: T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

d_'92''92''45'isMagmaMonomorphism_2850 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

du_'92''92''45'isMagmaMonomorphism_2850 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

d_injective_2852 :: T_IsQuasigroupMonomorphism_2554 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isQuasigroupHomomorphism_2854 :: T_IsQuasigroupMonomorphism_2554 -> T_IsQuasigroupHomomorphism_2522 #

d_isRelHomomorphism_2856 :: T_IsQuasigroupMonomorphism_2554 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_2858 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2858 :: T_IsQuasigroupMonomorphism_2554 -> T_IsRelMonomorphism_64 #

d_'8729''45'homo_2860 :: T_IsQuasigroupMonomorphism_2554 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaHomomorphism_2862 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

du_'8729''45'isMagmaHomomorphism_2862 :: T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaHomomorphism_176 #

d_'8729''45'isMagmaMonomorphism_2864 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

du_'8729''45'isMagmaMonomorphism_2864 :: (AgdaAny -> AgdaAny) -> T_IsQuasigroupMonomorphism_2554 -> T_IsMagmaMonomorphism_194 #

d_cong_2866 :: T_IsQuasigroupMonomorphism_2554 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMagmaHomomorphism_2870 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaIsomorphism_2872 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaMonomorphism_2874 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_2878 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_2880 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_cong_2882 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2886 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2888 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2890 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_2892 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_isRelHomomorphism_2894 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_2896 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_2896 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_2898 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2898 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_surjective_2900 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_cong_2902 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2906 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2908 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2910 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_2912 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_2914 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2914 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_cong_2916 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsMagmaHomomorphism_2920 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaIsomorphism_2922 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsMagmaMonomorphism_2924 :: p -> p -> p -> p -> p -> p -> p -> () #

d_homo_2928 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRelHomomorphism_2930 :: T_IsMagmaHomomorphism_176 -> T_IsRelHomomorphism_42 #

d_cong_2932 :: T_IsMagmaHomomorphism_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2936 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2938 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2940 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaHomomorphism_176 #

d_isMagmaMonomorphism_2942 :: T_IsMagmaIsomorphism_218 -> T_IsMagmaMonomorphism_194 #

d_isRelHomomorphism_2944 :: T_IsMagmaIsomorphism_218 -> T_IsRelHomomorphism_42 #

d_isRelIsomorphism_2946 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_2946 :: (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelIsomorphism_94 #

d_isRelMonomorphism_2948 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2948 :: T_IsMagmaIsomorphism_218 -> T_IsRelMonomorphism_64 #

d_surjective_2950 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> T_Σ_14 #

d_cong_2952 :: T_IsMagmaIsomorphism_218 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_homo_2956 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_2958 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_2960 :: T_IsMagmaMonomorphism_194 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_2962 :: T_IsMagmaMonomorphism_194 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_2964 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_2964 :: (AgdaAny -> AgdaAny) -> T_IsMagmaMonomorphism_194 -> T_IsRelMonomorphism_64 #

d_cong_2966 :: T_IsMagmaMonomorphism_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsLoopHomomorphism_2970 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsLoopHomomorphism_2970 #

Constructors

C_IsLoopHomomorphism'46'constructor_58349 T_IsQuasigroupHomomorphism_2522 AgdaAny

d_isQuasigroupHomomorphism_2978 :: T_IsLoopHomomorphism_2970 -> T_IsQuasigroupHomomorphism_2522 #

d_ε'45'homo_2980 :: T_IsLoopHomomorphism_2970 -> AgdaAny #

d_'47''47''45'homo_2984 :: T_IsLoopHomomorphism_2970 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'isMagmaHomomorphism_2986 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsLoopHomomorphism_2970 -> T_IsMagmaHomomorphism_176 #

du_'47''47''45'isMagmaHomomorphism_2986 :: T_IsLoopHomomorphism_2970 -> T_IsMagmaHomomorphism_176 #

d_'92''92''45'homo_2988 :: T_IsLoopHomomorphism_2970 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'92''92''45'isMagmaHomomorphism_2990 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsLoopHomomorphism_2970 -> T_IsMagmaHomomorphism_176 #

du_'92''92''45'isMagmaHomomorphism_2990 :: T_IsLoopHomomorphism_2970 -> T_IsMagmaHomomorphism_176 #

d_isRelHomomorphism_2992 :: T_IsLoopHomomorphism_2970 -> T_IsRelHomomorphism_42 #

d_'8729''45'homo_2994 :: T_IsLoopHomomorphism_2970 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaHomomorphism_2996 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsLoopHomomorphism_2970 -> T_IsMagmaHomomorphism_176 #

du_'8729''45'isMagmaHomomorphism_2996 :: T_IsLoopHomomorphism_2970 -> T_IsMagmaHomomorphism_176 #

d_cong_2998 :: T_IsLoopHomomorphism_2970 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsLoopMonomorphism_3002 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsLoopMonomorphism_3002 #

Constructors

C_IsLoopMonomorphism'46'constructor_59459 T_IsLoopHomomorphism_2970 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isLoopHomomorphism_3010 :: T_IsLoopMonomorphism_3002 -> T_IsLoopHomomorphism_2970 #

d_injective_3012 :: T_IsLoopMonomorphism_3002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'homo_3016 :: T_IsLoopMonomorphism_3002 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'isMagmaHomomorphism_3018 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsLoopMonomorphism_3002 -> T_IsMagmaHomomorphism_176 #

du_'47''47''45'isMagmaHomomorphism_3018 :: T_IsLoopMonomorphism_3002 -> T_IsMagmaHomomorphism_176 #

d_'92''92''45'homo_3020 :: T_IsLoopMonomorphism_3002 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'92''92''45'isMagmaHomomorphism_3022 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsLoopMonomorphism_3002 -> T_IsMagmaHomomorphism_176 #

du_'92''92''45'isMagmaHomomorphism_3022 :: T_IsLoopMonomorphism_3002 -> T_IsMagmaHomomorphism_176 #

d_isQuasigroupHomomorphism_3024 :: T_IsLoopMonomorphism_3002 -> T_IsQuasigroupHomomorphism_2522 #

d_isRelHomomorphism_3026 :: T_IsLoopMonomorphism_3002 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_3028 :: T_IsLoopMonomorphism_3002 -> AgdaAny #

d_'8729''45'homo_3030 :: T_IsLoopMonomorphism_3002 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaHomomorphism_3032 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsLoopMonomorphism_3002 -> T_IsMagmaHomomorphism_176 #

du_'8729''45'isMagmaHomomorphism_3032 :: T_IsLoopMonomorphism_3002 -> T_IsMagmaHomomorphism_176 #

d_cong_3034 :: T_IsLoopMonomorphism_3002 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsLoopIsomorphism_3038 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsLoopIsomorphism_3038 #

Constructors

C_IsLoopIsomorphism'46'constructor_60703 T_IsLoopMonomorphism_3002 (AgdaAny -> T_Σ_14)

d_isLoopMonomorphism_3046 :: T_IsLoopIsomorphism_3038 -> T_IsLoopMonomorphism_3002 #

d_surjective_3048 :: T_IsLoopIsomorphism_3038 -> AgdaAny -> T_Σ_14 #

d_'47''47''45'homo_3052 :: T_IsLoopIsomorphism_3038 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'47''47''45'isMagmaHomomorphism_3054 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsLoopIsomorphism_3038 -> T_IsMagmaHomomorphism_176 #

du_'47''47''45'isMagmaHomomorphism_3054 :: T_IsLoopIsomorphism_3038 -> T_IsMagmaHomomorphism_176 #

d_'92''92''45'homo_3056 :: T_IsLoopIsomorphism_3038 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'92''92''45'isMagmaHomomorphism_3058 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsLoopIsomorphism_3038 -> T_IsMagmaHomomorphism_176 #

du_'92''92''45'isMagmaHomomorphism_3058 :: T_IsLoopIsomorphism_3038 -> T_IsMagmaHomomorphism_176 #

d_injective_3060 :: T_IsLoopIsomorphism_3038 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isLoopHomomorphism_3062 :: T_IsLoopIsomorphism_3038 -> T_IsLoopHomomorphism_2970 #

d_isQuasigroupHomomorphism_3064 :: T_IsLoopIsomorphism_3038 -> T_IsQuasigroupHomomorphism_2522 #

d_isRelHomomorphism_3066 :: T_IsLoopIsomorphism_3038 -> T_IsRelHomomorphism_42 #

d_ε'45'homo_3068 :: T_IsLoopIsomorphism_3038 -> AgdaAny #

d_'8729''45'homo_3070 :: T_IsLoopIsomorphism_3038 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8729''45'isMagmaHomomorphism_3072 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawLoop_366 -> T_RawLoop_366 -> (AgdaAny -> AgdaAny) -> T_IsLoopIsomorphism_3038 -> T_IsMagmaHomomorphism_176 #

du_'8729''45'isMagmaHomomorphism_3072 :: T_IsLoopIsomorphism_3038 -> T_IsMagmaHomomorphism_176 #

d_cong_3074 :: T_IsLoopIsomorphism_3038 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__3096 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny -> () #

d__'8902'_3100 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny #

du__'8902'_3100 :: T_RawKleeneAlgebra_412 -> AgdaAny -> AgdaAny #

d_Carrier_3114 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> () #

d_Homomorphic'8321'_3150 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_IsSemiringHomomorphism_3158 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsSemiringIsomorphism_3160 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsSemiringMonomorphism_3162 :: p -> p -> p -> p -> p -> p -> p -> () #

d_'42''45'homo_3166 :: T_IsSemiringHomomorphism_1282 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_3168 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1282 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_3168 :: T_IsSemiringHomomorphism_1282 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMonoidHomomorphism_3170 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1282 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_3170 :: (AgdaAny -> AgdaAny) -> T_IsSemiringHomomorphism_1282 -> T_IsMonoidHomomorphism_350 #

d_homo_3172 :: T_IsSemiringHomomorphism_1282 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_3174 :: T_IsSemiringHomomorphism_1282 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_3176 :: T_IsSemiringHomomorphism_1282 -> T_IsMonoidHomomorphism_350 #

d_ε'45'homo_3178 :: T_IsSemiringHomomorphism_1282 -> AgdaAny #

d_1'35''45'homo_3180 :: T_IsSemiringHomomorphism_1282 -> AgdaAny #

d_isNearSemiringHomomorphism_3182 :: T_IsSemiringHomomorphism_1282 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_3184 :: T_IsSemiringHomomorphism_1282 -> T_IsRelHomomorphism_42 #

d_cong_3186 :: T_IsSemiringHomomorphism_1282 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_3190 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_3192 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_3192 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMagmaIsomorphism_3194 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMagmaIsomorphism_218 #

du_'42''45'isMagmaIsomorphism_3194 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaIsomorphism_218 #

d_'42''45'isMagmaMonomorphism_3196 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_3196 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaMonomorphism_194 #

d_'42''45'isMonoidHomomorphism_3198 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_3198 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidHomomorphism_350 #

d_'42''45'isMonoidIsomorphism_3200 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

du_'42''45'isMonoidIsomorphism_3200 :: (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

d_'42''45'isMonoidMonomorphism_3202 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

du_'42''45'isMonoidMonomorphism_3202 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

d_homo_3204 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_3206 :: T_IsSemiringIsomorphism_1364 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_3208 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidHomomorphism_350 #

d_'43''45'isMonoidIsomorphism_3210 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

du_'43''45'isMonoidIsomorphism_3210 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidIsomorphism_404 #

d_'43''45'isMonoidMonomorphism_3212 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

du_'43''45'isMonoidMonomorphism_3212 :: T_IsSemiringIsomorphism_1364 -> T_IsMonoidMonomorphism_372 #

d_ε'45'homo_3214 :: T_IsSemiringIsomorphism_1364 -> AgdaAny #

d_1'35''45'homo_3216 :: T_IsSemiringIsomorphism_1364 -> AgdaAny #

d_injective_3218 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringHomomorphism_3220 :: T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringHomomorphism_916 #

d_isNearSemiringIsomorphism_3222 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringIsomorphism_986 #

du_isNearSemiringIsomorphism_3222 :: (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringIsomorphism_986 #

d_isNearSemiringMonomorphism_3224 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringMonomorphism_944 #

du_isNearSemiringMonomorphism_3224 :: T_IsSemiringIsomorphism_1364 -> T_IsNearSemiringMonomorphism_944 #

d_isRelHomomorphism_3226 :: T_IsSemiringIsomorphism_1364 -> T_IsRelHomomorphism_42 #

d_isSemiringHomomorphism_3228 :: T_IsSemiringIsomorphism_1364 -> T_IsSemiringHomomorphism_1282 #

d_isSemiringMonomorphism_3230 :: T_IsSemiringIsomorphism_1364 -> T_IsSemiringMonomorphism_1316 #

d_surjective_3232 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> T_Σ_14 #

d_cong_3234 :: T_IsSemiringIsomorphism_1364 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_3238 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_3240 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_3240 :: T_IsSemiringMonomorphism_1316 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMagmaMonomorphism_3242 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMagmaMonomorphism_194 #

du_'42''45'isMagmaMonomorphism_3242 :: T_IsSemiringMonomorphism_1316 -> T_IsMagmaMonomorphism_194 #

d_'42''45'isMonoidHomomorphism_3244 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_3244 :: T_IsSemiringMonomorphism_1316 -> T_IsMonoidHomomorphism_350 #

d_'42''45'isMonoidMonomorphism_3246 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

du_'42''45'isMonoidMonomorphism_3246 :: (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

d_homo_3248 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_3250 :: T_IsSemiringMonomorphism_1316 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_3252 :: T_IsSemiringMonomorphism_1316 -> T_IsMonoidHomomorphism_350 #

d_'43''45'isMonoidMonomorphism_3254 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

du_'43''45'isMonoidMonomorphism_3254 :: T_IsSemiringMonomorphism_1316 -> T_IsMonoidMonomorphism_372 #

d_ε'45'homo_3256 :: T_IsSemiringMonomorphism_1316 -> AgdaAny #

d_1'35''45'homo_3258 :: T_IsSemiringMonomorphism_1316 -> AgdaAny #

d_injective_3260 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isNearSemiringHomomorphism_3262 :: T_IsSemiringMonomorphism_1316 -> T_IsNearSemiringHomomorphism_916 #

d_isNearSemiringMonomorphism_3264 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsNearSemiringMonomorphism_944 #

du_isNearSemiringMonomorphism_3264 :: (AgdaAny -> AgdaAny) -> T_IsSemiringMonomorphism_1316 -> T_IsNearSemiringMonomorphism_944 #

d_isRelHomomorphism_3266 :: T_IsSemiringMonomorphism_1316 -> T_IsRelHomomorphism_42 #

d_isSemiringHomomorphism_3268 :: T_IsSemiringMonomorphism_1316 -> T_IsSemiringHomomorphism_1282 #

d_cong_3270 :: T_IsSemiringMonomorphism_1316 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsKleeneAlgebraHomomorphism_3274 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsKleeneAlgebraHomomorphism_3274 #

Constructors

C_IsKleeneAlgebraHomomorphism'46'constructor_63187 T_IsSemiringHomomorphism_1282 (AgdaAny -> AgdaAny)

d_isSemiringHomomorphism_3282 :: T_IsKleeneAlgebraHomomorphism_3274 -> T_IsSemiringHomomorphism_1282 #

d_'8902''45'homo_3284 :: T_IsKleeneAlgebraHomomorphism_3274 -> AgdaAny -> AgdaAny #

d_'42''45'homo_3288 :: T_IsKleeneAlgebraHomomorphism_3274 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_3290 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsKleeneAlgebraHomomorphism_3274 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_3290 :: T_IsKleeneAlgebraHomomorphism_3274 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMonoidHomomorphism_3292 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsKleeneAlgebraHomomorphism_3274 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_3292 :: T_IsKleeneAlgebraHomomorphism_3274 -> T_IsMonoidHomomorphism_350 #

d_homo_3294 :: T_IsKleeneAlgebraHomomorphism_3274 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_3296 :: T_IsKleeneAlgebraHomomorphism_3274 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_3298 :: T_IsKleeneAlgebraHomomorphism_3274 -> T_IsMonoidHomomorphism_350 #

d_ε'45'homo_3300 :: T_IsKleeneAlgebraHomomorphism_3274 -> AgdaAny #

d_1'35''45'homo_3302 :: T_IsKleeneAlgebraHomomorphism_3274 -> AgdaAny #

d_isNearSemiringHomomorphism_3304 :: T_IsKleeneAlgebraHomomorphism_3274 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_3306 :: T_IsKleeneAlgebraHomomorphism_3274 -> T_IsRelHomomorphism_42 #

d_cong_3308 :: T_IsKleeneAlgebraHomomorphism_3274 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsKleeneAlgebraMonomorphism_3312 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsKleeneAlgebraMonomorphism_3312 #

Constructors

C_IsKleeneAlgebraMonomorphism'46'constructor_64491 T_IsKleeneAlgebraHomomorphism_3274 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isKleeneAlgebraHomomorphism_3320 :: T_IsKleeneAlgebraMonomorphism_3312 -> T_IsKleeneAlgebraHomomorphism_3274 #

d_injective_3322 :: T_IsKleeneAlgebraMonomorphism_3312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'homo_3326 :: T_IsKleeneAlgebraMonomorphism_3312 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_3328 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsKleeneAlgebraMonomorphism_3312 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_3328 :: T_IsKleeneAlgebraMonomorphism_3312 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMonoidHomomorphism_3330 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsKleeneAlgebraMonomorphism_3312 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_3330 :: T_IsKleeneAlgebraMonomorphism_3312 -> T_IsMonoidHomomorphism_350 #

d_homo_3332 :: T_IsKleeneAlgebraMonomorphism_3312 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_3334 :: T_IsKleeneAlgebraMonomorphism_3312 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_3336 :: T_IsKleeneAlgebraMonomorphism_3312 -> T_IsMonoidHomomorphism_350 #

d_ε'45'homo_3338 :: T_IsKleeneAlgebraMonomorphism_3312 -> AgdaAny #

d_1'35''45'homo_3340 :: T_IsKleeneAlgebraMonomorphism_3312 -> AgdaAny #

d_isNearSemiringHomomorphism_3342 :: T_IsKleeneAlgebraMonomorphism_3312 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_3344 :: T_IsKleeneAlgebraMonomorphism_3312 -> T_IsRelHomomorphism_42 #

d_isSemiringHomomorphism_3346 :: T_IsKleeneAlgebraMonomorphism_3312 -> T_IsSemiringHomomorphism_1282 #

d_'8902''45'homo_3348 :: T_IsKleeneAlgebraMonomorphism_3312 -> AgdaAny -> AgdaAny #

d_cong_3350 :: T_IsKleeneAlgebraMonomorphism_3312 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsKleeneAlgebraIsomorphism_3354 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsKleeneAlgebraIsomorphism_3354 #

Constructors

C_IsKleeneAlgebraIsomorphism'46'constructor_65931 T_IsKleeneAlgebraMonomorphism_3312 (AgdaAny -> T_Σ_14)

d_isKleeneAlgebraMonomorphism_3362 :: T_IsKleeneAlgebraIsomorphism_3354 -> T_IsKleeneAlgebraMonomorphism_3312 #

d_surjective_3364 :: T_IsKleeneAlgebraIsomorphism_3354 -> AgdaAny -> T_Σ_14 #

d_'42''45'homo_3368 :: T_IsKleeneAlgebraIsomorphism_3354 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'42''45'isMagmaHomomorphism_3370 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsKleeneAlgebraIsomorphism_3354 -> T_IsMagmaHomomorphism_176 #

du_'42''45'isMagmaHomomorphism_3370 :: T_IsKleeneAlgebraIsomorphism_3354 -> T_IsMagmaHomomorphism_176 #

d_'42''45'isMonoidHomomorphism_3372 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_RawKleeneAlgebra_412 -> T_RawKleeneAlgebra_412 -> (AgdaAny -> AgdaAny) -> T_IsKleeneAlgebraIsomorphism_3354 -> T_IsMonoidHomomorphism_350 #

du_'42''45'isMonoidHomomorphism_3372 :: T_IsKleeneAlgebraIsomorphism_3354 -> T_IsMonoidHomomorphism_350 #

d_homo_3374 :: T_IsKleeneAlgebraIsomorphism_3354 -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagmaHomomorphism_3376 :: T_IsKleeneAlgebraIsomorphism_3354 -> T_IsMagmaHomomorphism_176 #

d_'43''45'isMonoidHomomorphism_3378 :: T_IsKleeneAlgebraIsomorphism_3354 -> T_IsMonoidHomomorphism_350 #

d_ε'45'homo_3380 :: T_IsKleeneAlgebraIsomorphism_3354 -> AgdaAny #

d_1'35''45'homo_3382 :: T_IsKleeneAlgebraIsomorphism_3354 -> AgdaAny #

d_injective_3384 :: T_IsKleeneAlgebraIsomorphism_3354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isKleeneAlgebraHomomorphism_3386 :: T_IsKleeneAlgebraIsomorphism_3354 -> T_IsKleeneAlgebraHomomorphism_3274 #

d_isNearSemiringHomomorphism_3388 :: T_IsKleeneAlgebraIsomorphism_3354 -> T_IsNearSemiringHomomorphism_916 #

d_isRelHomomorphism_3390 :: T_IsKleeneAlgebraIsomorphism_3354 -> T_IsRelHomomorphism_42 #

d_isSemiringHomomorphism_3392 :: T_IsKleeneAlgebraIsomorphism_3354 -> T_IsSemiringHomomorphism_1282 #

d_'8902''45'homo_3394 :: T_IsKleeneAlgebraIsomorphism_3354 -> AgdaAny -> AgdaAny #

d_cong_3396 :: T_IsKleeneAlgebraIsomorphism_3354 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #