Documentation

d_Homomorphic'8320'_32 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_34 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_36 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_38 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → () Source #

d__'8729'__58 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Semigroup_558 → T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny Source #

du__'8729'__58 ∷ T_Semigroup_558 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__60 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Semigroup_558 → T_Semigroup_558 → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8320'_138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Semigroup_558 → T_Semigroup_558 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Semigroup_558 → T_Semigroup_558 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Semigroup_558 → T_Semigroup_558 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_144 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Semigroup_558 → T_Semigroup_558 → () Source #

d_IsSemigroupMorphism_148 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSemigroupMorphism_148 Source #

d_'10214''10215''45'cong_156 ∷ T_IsSemigroupMorphism_148 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'homo_158 ∷ T_IsSemigroupMorphism_148 → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSemigroupMorphism'45'syntax_162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Semigroup_558 → T_Semigroup_558 → (AgdaAny → AgdaAny) → () Source #

d_semigroup_220 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_914 → T_Monoid_914 → T_Semigroup_558 Source #

du_semigroup_220 ∷ T_Monoid_914 → T_Semigroup_558 Source #

d_ε_230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_914 → T_Monoid_914 → AgdaAny Source #

du_ε_230 ∷ T_Monoid_914 → AgdaAny Source #

d_semigroup_278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_914 → T_Monoid_914 → T_Semigroup_558 Source #

du_semigroup_278 ∷ T_Monoid_914 → T_Semigroup_558 Source #

d_Homomorphic'8320'_298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_914 → T_Monoid_914 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_914 → T_Monoid_914 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_914 → T_Monoid_914 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_914 → T_Monoid_914 → () Source #

d_IsMonoidMorphism_308 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMonoidMorphism_308 Source #

d_sm'45'homo_316 ∷ T_IsMonoidMorphism_308 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_318 ∷ T_IsMonoidMorphism_308 → AgdaAny Source #

d_'8729''45'homo_322 ∷ T_IsMonoidMorphism_308 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_324 ∷ T_IsMonoidMorphism_308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoidMorphism'45'syntax_328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_914 → T_Monoid_914 → (AgdaAny → AgdaAny) → () Source #

d_monoid_390 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_CommutativeMonoid_996 → T_Monoid_914 Source #

du_monoid_390 ∷ T_CommutativeMonoid_996 → T_Monoid_914 Source #

d_monoid_462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_CommutativeMonoid_996 → T_Monoid_914 Source #

du_monoid_462 ∷ T_CommutativeMonoid_996 → T_Monoid_914 Source #

d_Homomorphic'8320'_492 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_CommutativeMonoid_996 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_494 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_CommutativeMonoid_996 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_496 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_CommutativeMonoid_996 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_498 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_CommutativeMonoid_996 → () Source #

d_IsCommutativeMonoidMorphism_502 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsCommutativeMonoidMorphism_502 Source #

d_mn'45'homo_508 ∷ T_IsCommutativeMonoidMorphism_502 → T_IsMonoidMorphism_308 Source #

d_sm'45'homo_512 ∷ T_IsCommutativeMonoidMorphism_502 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_514 ∷ T_IsCommutativeMonoidMorphism_502 → AgdaAny Source #

d_'8729''45'homo_516 ∷ T_IsCommutativeMonoidMorphism_502 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_518 ∷ T_IsCommutativeMonoidMorphism_502 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsCommutativeMonoidMorphism'45'syntax_522 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_996 → T_CommutativeMonoid_996 → (AgdaAny → AgdaAny) → () Source #

d_commutativeMonoid_560 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentCommutativeMonoid_1186 → T_CommutativeMonoid_996 Source #

du_commutativeMonoid_560 ∷ T_IdempotentCommutativeMonoid_1186 → T_CommutativeMonoid_996 Source #

d_monoid_602 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentCommutativeMonoid_1186 → T_Monoid_914 Source #

du_monoid_602 ∷ T_IdempotentCommutativeMonoid_1186 → T_Monoid_914 Source #

d_commutativeMonoid_650 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentCommutativeMonoid_1186 → T_CommutativeMonoid_996 Source #

du_commutativeMonoid_650 ∷ T_IdempotentCommutativeMonoid_1186 → T_CommutativeMonoid_996 Source #

d_monoid_692 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentCommutativeMonoid_1186 → T_Monoid_914 Source #

du_monoid_692 ∷ T_IdempotentCommutativeMonoid_1186 → T_Monoid_914 Source #

d_Homomorphic'8320'_722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentCommutativeMonoid_1186 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_724 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentCommutativeMonoid_1186 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_726 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentCommutativeMonoid_1186 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentCommutativeMonoid_1186 → () Source #

d_IsIdempotentCommutativeMonoidMorphism_732 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsIdempotentCommutativeMonoidMorphism_732 Source #

d_mn'45'homo_738 ∷ T_IsIdempotentCommutativeMonoidMorphism_732 → T_IsMonoidMorphism_308 Source #

d_sm'45'homo_742 ∷ T_IsIdempotentCommutativeMonoidMorphism_732 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_744 ∷ T_IsIdempotentCommutativeMonoidMorphism_732 → AgdaAny Source #

d_'8729''45'homo_746 ∷ T_IsIdempotentCommutativeMonoidMorphism_732 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_748 ∷ T_IsIdempotentCommutativeMonoidMorphism_732 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMonoidMorphism_750 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentCommutativeMonoid_1186 → (AgdaAny → AgdaAny) → T_IsIdempotentCommutativeMonoidMorphism_732 → T_IsCommutativeMonoidMorphism_502 Source #

du_isCommutativeMonoidMorphism_750 ∷ T_IsIdempotentCommutativeMonoidMorphism_732 → T_IsCommutativeMonoidMorphism_502 Source #

d_IsIdempotentCommutativeMonoidMorphism'45'syntax_754 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1186 → T_IdempotentCommutativeMonoid_1186 → (AgdaAny → AgdaAny) → () Source #

d__'8315''185'_780 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1564 → T_Group_1564 → AgdaAny → AgdaAny Source #

du__'8315''185'_780 ∷ T_Group_1564 → AgdaAny → AgdaAny Source #

d_monoid_828 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1564 → T_Group_1564 → T_Monoid_914 Source #

du_monoid_828 ∷ T_Group_1564 → T_Monoid_914 Source #

d_monoid_920 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1564 → T_Group_1564 → T_Monoid_914 Source #

du_monoid_920 ∷ T_Group_1564 → T_Monoid_914 Source #

d_Homomorphic'8320'_958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1564 → T_Group_1564 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1564 → T_Group_1564 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1564 → T_Group_1564 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1564 → T_Group_1564 → () Source #

d_IsGroupMorphism_968 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsGroupMorphism_968 Source #

d_mn'45'homo_974 ∷ T_IsGroupMorphism_968 → T_IsMonoidMorphism_308 Source #

d_sm'45'homo_978 ∷ T_IsGroupMorphism_968 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_980 ∷ T_IsGroupMorphism_968 → AgdaAny Source #

d_'8729''45'homo_982 ∷ T_IsGroupMorphism_968 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_984 ∷ T_IsGroupMorphism_968 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'homo_986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1564 → T_Group_1564 → (AgdaAny → AgdaAny) → T_IsGroupMorphism_968 → AgdaAny → AgdaAny Source #

du_'8315''185''45'homo_986 ∷ T_Group_1564 → T_Group_1564 → (AgdaAny → AgdaAny) → T_IsGroupMorphism_968 → AgdaAny → AgdaAny Source #

d_IsGroupMorphism'45'syntax_1032 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1564 → T_Group_1564 → (AgdaAny → AgdaAny) → () Source #

d_group_1074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → T_AbelianGroup_1682 → T_Group_1564 Source #

du_group_1074 ∷ T_AbelianGroup_1682 → T_Group_1564 Source #

d_group_1178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → T_AbelianGroup_1682 → T_Group_1564 Source #

du_group_1178 ∷ T_AbelianGroup_1682 → T_Group_1564 Source #

d_Homomorphic'8320'_1260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → T_AbelianGroup_1682 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_1262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → T_AbelianGroup_1682 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_1264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → T_AbelianGroup_1682 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_1266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → T_AbelianGroup_1682 → () Source #

d_IsAbelianGroupMorphism_1270 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsAbelianGroupMorphism_1270 Source #

d_gp'45'homo_1276 ∷ T_IsAbelianGroupMorphism_1270 → T_IsGroupMorphism_968 Source #

d_mn'45'homo_1280 ∷ T_IsAbelianGroupMorphism_1270 → T_IsMonoidMorphism_308 Source #

d_sm'45'homo_1282 ∷ T_IsAbelianGroupMorphism_1270 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_1284 ∷ T_IsAbelianGroupMorphism_1270 → AgdaAny Source #

d_'8315''185''45'homo_1286 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → T_AbelianGroup_1682 → (AgdaAny → AgdaAny) → T_IsAbelianGroupMorphism_1270 → AgdaAny → AgdaAny Source #

du_'8315''185''45'homo_1286 ∷ T_AbelianGroup_1682 → T_AbelianGroup_1682 → (AgdaAny → AgdaAny) → T_IsAbelianGroupMorphism_1270 → AgdaAny → AgdaAny Source #

d_'8729''45'homo_1288 ∷ T_IsAbelianGroupMorphism_1270 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_1290 ∷ T_IsAbelianGroupMorphism_1270 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsAbelianGroupMorphism'45'syntax_1294 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1682 → T_AbelianGroup_1682 → (AgdaAny → AgdaAny) → () Source #

d_'42''45'monoid_1346 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_3908 → T_Ring_3908 → T_Monoid_914 Source #

du_'42''45'monoid_1346 ∷ T_Ring_3908 → T_Monoid_914 Source #

d_'43''45'abelianGroup_1354 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_3908 → T_Ring_3908 → T_AbelianGroup_1682 Source #

du_'43''45'abelianGroup_1354 ∷ T_Ring_3908 → T_AbelianGroup_1682 Source #

d_'42''45'monoid_1528 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_3908 → T_Ring_3908 → T_Monoid_914 Source #

du_'42''45'monoid_1528 ∷ T_Ring_3908 → T_Monoid_914 Source #

d_'43''45'abelianGroup_1536 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_3908 → T_Ring_3908 → T_AbelianGroup_1682 Source #

du_'43''45'abelianGroup_1536 ∷ T_Ring_3908 → T_AbelianGroup_1682 Source #

d_Homomorphic'8320'_1678 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_3908 → T_Ring_3908 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_1680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_3908 → T_Ring_3908 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_1682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_3908 → T_Ring_3908 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_1684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_3908 → T_Ring_3908 → () Source #

d_IsRingMorphism_1688 ∷ p → p → p → p → p → p → p → () Source #

data T_IsRingMorphism_1688 Source #

d_'43''45'abgp'45'homo_1696 ∷ T_IsRingMorphism_1688 → T_IsAbelianGroupMorphism_1270 Source #

d_'42''45'mn'45'homo_1698 ∷ T_IsRingMorphism_1688 → T_IsMonoidMorphism_308 Source #

d_IsRingMorphism'45'syntax_1702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_3908 → T_Ring_3908 → (AgdaAny → AgdaAny) → () Source #