Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Algebra.Morphism

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_206 → T_Semigroup_206 → AgdaAny → AgdaAny → AgdaAny Source #

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

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

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

d_Homomorphic'8321'_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Semigroup_206 → T_Semigroup_206 → (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_206 → T_Semigroup_206 → (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_206 → T_Semigroup_206 → () Source #

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

data T_IsSemigroupMorphism_148 Source #

Constructors

C_IsSemigroupMorphism'46'constructor_1081 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny)

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_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Semigroup_206 → T_Semigroup_206 → (AgdaAny → AgdaAny) → () Source #

d_semigroup_216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_506 → T_Monoid_506 → T_Semigroup_206 Source #

du_semigroup_216 ∷ T_Monoid_506 → T_Semigroup_206 Source #

d_ε_224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_506 → T_Monoid_506 → AgdaAny Source #

du_ε_224 ∷ T_Monoid_506 → AgdaAny Source #

d_semigroup_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_506 → T_Monoid_506 → T_Semigroup_206 Source #

du_semigroup_270 ∷ T_Monoid_506 → T_Semigroup_206 Source #

d_Homomorphic'8320'_288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_506 → T_Monoid_506 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_506 → T_Monoid_506 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_506 → T_Monoid_506 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_294 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_506 → T_Monoid_506 → () Source #

d_IsMonoidMorphism_298 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMonoidMorphism_298 Source #

Constructors

C_IsMonoidMorphism'46'constructor_2137 T_IsSemigroupMorphism_148 AgdaAny

d_sm'45'homo_306 ∷ T_IsMonoidMorphism_298 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_308 ∷ T_IsMonoidMorphism_298 → AgdaAny Source #

d_'8729''45'homo_312 ∷ T_IsMonoidMorphism_298 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_314 ∷ T_IsMonoidMorphism_298 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsMonoidMorphism'45'syntax_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_506 → T_Monoid_506 → (AgdaAny → AgdaAny) → () Source #

d_monoid_376 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_CommutativeMonoid_582 → T_Monoid_506 Source #

du_monoid_376 ∷ T_CommutativeMonoid_582 → T_Monoid_506 Source #

d_monoid_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_CommutativeMonoid_582 → T_Monoid_506 Source #

du_monoid_444 ∷ T_CommutativeMonoid_582 → T_Monoid_506 Source #

d_Homomorphic'8320'_472 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_CommutativeMonoid_582 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_CommutativeMonoid_582 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_476 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_CommutativeMonoid_582 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_478 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_CommutativeMonoid_582 → () Source #

d_IsCommutativeMonoidMorphism_482 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsCommutativeMonoidMorphism_482 Source #

Constructors

C_IsCommutativeMonoidMorphism'46'constructor_3701 T_IsMonoidMorphism_298

d_mn'45'homo_488 ∷ T_IsCommutativeMonoidMorphism_482 → T_IsMonoidMorphism_298 Source #

d_sm'45'homo_492 ∷ T_IsCommutativeMonoidMorphism_482 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_494 ∷ T_IsCommutativeMonoidMorphism_482 → AgdaAny Source #

d_'8729''45'homo_496 ∷ T_IsCommutativeMonoidMorphism_482 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_498 ∷ T_IsCommutativeMonoidMorphism_482 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsCommutativeMonoidMorphism'45'syntax_500 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_582 → T_CommutativeMonoid_582 → (AgdaAny → AgdaAny) → () Source #

d_commutativeMonoid_534 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IdempotentCommutativeMonoid_674 → T_CommutativeMonoid_582 Source #

du_commutativeMonoid_534 ∷ T_IdempotentCommutativeMonoid_674 → T_CommutativeMonoid_582 Source #

d_monoid_566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IdempotentCommutativeMonoid_674 → T_Monoid_506 Source #

du_monoid_566 ∷ T_IdempotentCommutativeMonoid_674 → T_Monoid_506 Source #

d_commutativeMonoid_608 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IdempotentCommutativeMonoid_674 → T_CommutativeMonoid_582 Source #

du_commutativeMonoid_608 ∷ T_IdempotentCommutativeMonoid_674 → T_CommutativeMonoid_582 Source #

d_monoid_640 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IdempotentCommutativeMonoid_674 → T_Monoid_506 Source #

du_monoid_640 ∷ T_IdempotentCommutativeMonoid_674 → T_Monoid_506 Source #

d_Homomorphic'8320'_668 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IdempotentCommutativeMonoid_674 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_670 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IdempotentCommutativeMonoid_674 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_672 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IdempotentCommutativeMonoid_674 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_674 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IdempotentCommutativeMonoid_674 → () Source #

d_IsIdempotentCommutativeMonoidMorphism_678 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsIdempotentCommutativeMonoidMorphism_678 Source #

Constructors

C_IsIdempotentCommutativeMonoidMorphism'46'constructor_5357 T_IsMonoidMorphism_298

d_mn'45'homo_684 ∷ T_IsIdempotentCommutativeMonoidMorphism_678 → T_IsMonoidMorphism_298 Source #

d_sm'45'homo_688 ∷ T_IsIdempotentCommutativeMonoidMorphism_678 → T_IsSemigroupMorphism_148 Source #

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

d_'8729''45'homo_692 ∷ T_IsIdempotentCommutativeMonoidMorphism_678 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_694 ∷ T_IsIdempotentCommutativeMonoidMorphism_678 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMonoidMorphism_696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IdempotentCommutativeMonoid_674 → (AgdaAny → AgdaAny) → T_IsIdempotentCommutativeMonoidMorphism_678 → T_IsCommutativeMonoidMorphism_482 Source #

du_isCommutativeMonoidMorphism_696 ∷ T_IsIdempotentCommutativeMonoidMorphism_678 → T_IsCommutativeMonoidMorphism_482 Source #

d_IsIdempotentCommutativeMonoidMorphism'45'syntax_698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_674 → T_IdempotentCommutativeMonoid_674 → (AgdaAny → AgdaAny) → () Source #

d__'8315''185'_720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_890 → T_Group_890 → AgdaAny → AgdaAny Source #

du__'8315''185'_720 ∷ T_Group_890 → AgdaAny → AgdaAny Source #

d_monoid_758 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_890 → T_Group_890 → T_Monoid_506 Source #

du_monoid_758 ∷ T_Group_890 → T_Monoid_506 Source #

d_monoid_834 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_890 → T_Group_890 → T_Monoid_506 Source #

du_monoid_834 ∷ T_Group_890 → T_Monoid_506 Source #

d_Homomorphic'8320'_870 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_890 → T_Group_890 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_872 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_890 → T_Group_890 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_874 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_890 → T_Group_890 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_876 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_890 → T_Group_890 → () Source #

d_IsGroupMorphism_880 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsGroupMorphism_880 Source #

Constructors

C_IsGroupMorphism'46'constructor_7461 T_IsMonoidMorphism_298

d_mn'45'homo_886 ∷ T_IsGroupMorphism_880 → T_IsMonoidMorphism_298 Source #

d_sm'45'homo_890 ∷ T_IsGroupMorphism_880 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_892 ∷ T_IsGroupMorphism_880 → AgdaAny Source #

d_'8729''45'homo_894 ∷ T_IsGroupMorphism_880 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_896 ∷ T_IsGroupMorphism_880 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'homo_898 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_890 → T_Group_890 → (AgdaAny → AgdaAny) → T_IsGroupMorphism_880 → AgdaAny → AgdaAny Source #

du_'8315''185''45'homo_898 ∷ T_Group_890 → T_Group_890 → (AgdaAny → AgdaAny) → T_IsGroupMorphism_880 → AgdaAny → AgdaAny Source #

d_IsGroupMorphism'45'syntax_926 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_890 → T_Group_890 → (AgdaAny → AgdaAny) → () Source #

d_group_968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_AbelianGroup_990 → T_Group_890 Source #

du_group_968 ∷ T_AbelianGroup_990 → T_Group_890 Source #

d_group_1062 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_AbelianGroup_990 → T_Group_890 Source #

du_group_1062 ∷ T_AbelianGroup_990 → T_Group_890 Source #

d_Homomorphic'8320'_1134 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_AbelianGroup_990 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_1136 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_AbelianGroup_990 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_1138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_AbelianGroup_990 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_1140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_AbelianGroup_990 → () Source #

d_IsAbelianGroupMorphism_1144 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsAbelianGroupMorphism_1144 Source #

Constructors

C_IsAbelianGroupMorphism'46'constructor_11199 T_IsGroupMorphism_880

d_gp'45'homo_1150 ∷ T_IsAbelianGroupMorphism_1144 → T_IsGroupMorphism_880 Source #

d_mn'45'homo_1154 ∷ T_IsAbelianGroupMorphism_1144 → T_IsMonoidMorphism_298 Source #

d_sm'45'homo_1156 ∷ T_IsAbelianGroupMorphism_1144 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_1158 ∷ T_IsAbelianGroupMorphism_1144 → AgdaAny Source #

d_'8315''185''45'homo_1160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_AbelianGroup_990 → (AgdaAny → AgdaAny) → T_IsAbelianGroupMorphism_1144 → AgdaAny → AgdaAny Source #

du_'8315''185''45'homo_1160 ∷ T_AbelianGroup_990 → T_AbelianGroup_990 → (AgdaAny → AgdaAny) → T_IsAbelianGroupMorphism_1144 → AgdaAny → AgdaAny Source #

d_'8729''45'homo_1162 ∷ T_IsAbelianGroupMorphism_1144 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_1164 ∷ T_IsAbelianGroupMorphism_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsAbelianGroupMorphism'45'syntax_1166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_990 → T_AbelianGroup_990 → (AgdaAny → AgdaAny) → () Source #

d_'42''45'monoid_1218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_2514 → T_Ring_2514 → T_Monoid_506 Source #

du_'42''45'monoid_1218 ∷ T_Ring_2514 → T_Monoid_506 Source #

d_'43''45'abelianGroup_1226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_2514 → T_Ring_2514 → T_AbelianGroup_990 Source #

du_'43''45'abelianGroup_1226 ∷ T_Ring_2514 → T_AbelianGroup_990 Source #

d_'42''45'monoid_1378 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_2514 → T_Ring_2514 → T_Monoid_506 Source #

du_'42''45'monoid_1378 ∷ T_Ring_2514 → T_Monoid_506 Source #

d_'43''45'abelianGroup_1386 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_2514 → T_Ring_2514 → T_AbelianGroup_990 Source #

du_'43''45'abelianGroup_1386 ∷ T_Ring_2514 → T_AbelianGroup_990 Source #

d_Homomorphic'8320'_1506 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_2514 → T_Ring_2514 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #

d_Homomorphic'8321'_1508 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_2514 → T_Ring_2514 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Homomorphic'8322'_1510 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_2514 → T_Ring_2514 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Morphism_1512 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_2514 → T_Ring_2514 → () Source #

d_IsRingMorphism_1516 ∷ p → p → p → p → p → p → p → () Source #

data T_IsRingMorphism_1516 Source #

Constructors

C_IsRingMorphism'46'constructor_13379 T_IsAbelianGroupMorphism_1144 T_IsMonoidMorphism_298

d_'43''45'abgp'45'homo_1524 ∷ T_IsRingMorphism_1516 → T_IsAbelianGroupMorphism_1144 Source #

d_'42''45'mn'45'homo_1526 ∷ T_IsRingMorphism_1516 → T_IsMonoidMorphism_298 Source #

d_IsRingMorphism'45'syntax_1528 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_2514 → T_Ring_2514 → (AgdaAny → AgdaAny) → () Source #