Safe HaskellNone

MAlonzo.Code.Algebra.Morphism

Documentation

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

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

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

d_Morphism_38 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> () Source #

d__'8729'__58 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> T_Semigroup_206 -> AgdaAny -> AgdaAny -> () Source #

d_Homomorphic'8320'_138 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> T_Semigroup_206 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Homomorphic'8321'_140 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> T_Semigroup_206 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Homomorphic'8322'_142 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> T_Semigroup_206 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Morphism_144 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> T_Semigroup_206 -> () Source #

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

data T_IsSemigroupMorphism_148 Source #

Constructors

C_IsSemigroupMorphism'46'constructor_771 (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Semigroup_206 -> T_Semigroup_206 -> (AgdaAny -> AgdaAny) -> () Source #

d_semigroup_218 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Monoid_502 -> T_Semigroup_206 Source #

du_semigroup_218 :: T_Monoid_502 -> T_Semigroup_206 Source #

d_ε_228 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Monoid_502 -> AgdaAny Source #

du_ε_228 :: T_Monoid_502 -> AgdaAny Source #

d_semigroup_276 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Monoid_502 -> T_Semigroup_206 Source #

du_semigroup_276 :: T_Monoid_502 -> T_Semigroup_206 Source #

d_Homomorphic'8320'_296 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Monoid_502 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Homomorphic'8321'_298 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Monoid_502 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Homomorphic'8322'_300 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Monoid_502 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Morphism_302 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Monoid_502 -> () Source #

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

data T_IsMonoidMorphism_306 Source #

Constructors

C_IsMonoidMorphism'46'constructor_1593 T_IsSemigroupMorphism_148 AgdaAny 

d_sm'45'homo_314 :: T_IsMonoidMorphism_306 -> T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_316 :: T_IsMonoidMorphism_306 -> AgdaAny Source #

d_'8729''45'homo_320 :: T_IsMonoidMorphism_306 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'10214''10215''45'cong_322 :: T_IsMonoidMorphism_306 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsMonoidMorphism'45'syntax_324 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Monoid_502 -> T_Monoid_502 -> (AgdaAny -> AgdaAny) -> () Source #

d_monoid_386 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_CommutativeMonoid_582 -> T_Monoid_502 Source #

du_monoid_386 :: T_CommutativeMonoid_582 -> T_Monoid_502 Source #

d_monoid_458 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_CommutativeMonoid_582 -> T_Monoid_502 Source #

du_monoid_458 :: T_CommutativeMonoid_582 -> T_Monoid_502 Source #

d_Homomorphic'8320'_488 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_CommutativeMonoid_582 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Homomorphic'8321'_490 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_CommutativeMonoid_582 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Homomorphic'8322'_492 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_CommutativeMonoid_582 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Morphism_494 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_CommutativeMonoid_582 -> () Source #

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

newtype T_IsCommutativeMonoidMorphism_498 Source #

Constructors

C_IsCommutativeMonoidMorphism'46'constructor_2821 T_IsMonoidMorphism_306 

d_mn'45'homo_504 :: T_IsCommutativeMonoidMorphism_498 -> T_IsMonoidMorphism_306 Source #

d_sm'45'homo_508 :: T_IsCommutativeMonoidMorphism_498 -> T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_510 :: T_IsCommutativeMonoidMorphism_498 -> AgdaAny Source #

d_'8729''45'homo_512 :: T_IsCommutativeMonoidMorphism_498 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'10214''10215''45'cong_514 :: T_IsCommutativeMonoidMorphism_498 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsCommutativeMonoidMorphism'45'syntax_516 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_CommutativeMonoid_582 -> T_CommutativeMonoid_582 -> (AgdaAny -> AgdaAny) -> () Source #

d_commutativeMonoid_550 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IdempotentCommutativeMonoid_678 -> T_CommutativeMonoid_582 Source #

du_commutativeMonoid_550 :: T_IdempotentCommutativeMonoid_678 -> T_CommutativeMonoid_582 Source #

d_monoid_586 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IdempotentCommutativeMonoid_678 -> T_Monoid_502 Source #

du_monoid_586 :: T_IdempotentCommutativeMonoid_678 -> T_Monoid_502 Source #

d_commutativeMonoid_630 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IdempotentCommutativeMonoid_678 -> T_CommutativeMonoid_582 Source #

du_commutativeMonoid_630 :: T_IdempotentCommutativeMonoid_678 -> T_CommutativeMonoid_582 Source #

d_monoid_666 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IdempotentCommutativeMonoid_678 -> T_Monoid_502 Source #

du_monoid_666 :: T_IdempotentCommutativeMonoid_678 -> T_Monoid_502 Source #

d_Homomorphic'8320'_696 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IdempotentCommutativeMonoid_678 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Homomorphic'8321'_698 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IdempotentCommutativeMonoid_678 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Homomorphic'8322'_700 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IdempotentCommutativeMonoid_678 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Morphism_702 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IdempotentCommutativeMonoid_678 -> () Source #

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

newtype T_IsIdempotentCommutativeMonoidMorphism_706 Source #

Constructors

C_IsIdempotentCommutativeMonoidMorphism'46'constructor_4141 T_IsMonoidMorphism_306 

d_mn'45'homo_712 :: T_IsIdempotentCommutativeMonoidMorphism_706 -> T_IsMonoidMorphism_306 Source #

d_sm'45'homo_716 :: T_IsIdempotentCommutativeMonoidMorphism_706 -> T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_718 :: T_IsIdempotentCommutativeMonoidMorphism_706 -> AgdaAny Source #

d_'8729''45'homo_720 :: T_IsIdempotentCommutativeMonoidMorphism_706 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'10214''10215''45'cong_722 :: T_IsIdempotentCommutativeMonoidMorphism_706 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMonoidMorphism_724 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IdempotentCommutativeMonoid_678 -> (AgdaAny -> AgdaAny) -> T_IsIdempotentCommutativeMonoidMorphism_706 -> T_IsCommutativeMonoidMorphism_498 Source #

du_isCommutativeMonoidMorphism_724 :: T_IsIdempotentCommutativeMonoidMorphism_706 -> T_IsCommutativeMonoidMorphism_498 Source #

d_IsIdempotentCommutativeMonoidMorphism'45'syntax_726 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IdempotentCommutativeMonoid_678 -> T_IdempotentCommutativeMonoid_678 -> (AgdaAny -> AgdaAny) -> () Source #

d__'8315''185'_748 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Group_1062 -> AgdaAny -> AgdaAny Source #

du__'8315''185'_748 :: T_Group_1062 -> AgdaAny -> AgdaAny Source #

d_monoid_796 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Group_1062 -> T_Monoid_502 Source #

du_monoid_796 :: T_Group_1062 -> T_Monoid_502 Source #

d_monoid_884 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Group_1062 -> T_Monoid_502 Source #

du_monoid_884 :: T_Group_1062 -> T_Monoid_502 Source #

d_Homomorphic'8320'_922 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Group_1062 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Homomorphic'8321'_924 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Group_1062 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Homomorphic'8322'_926 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Group_1062 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Morphism_928 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Group_1062 -> () Source #

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

newtype T_IsGroupMorphism_932 Source #

Constructors

C_IsGroupMorphism'46'constructor_5835 T_IsMonoidMorphism_306 

d_mn'45'homo_938 :: T_IsGroupMorphism_932 -> T_IsMonoidMorphism_306 Source #

d_sm'45'homo_942 :: T_IsGroupMorphism_932 -> T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_944 :: T_IsGroupMorphism_932 -> AgdaAny Source #

d_'8729''45'homo_946 :: T_IsGroupMorphism_932 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'10214''10215''45'cong_948 :: T_IsGroupMorphism_932 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8315''185''45'homo_950 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Group_1062 -> (AgdaAny -> AgdaAny) -> T_IsGroupMorphism_932 -> AgdaAny -> AgdaAny Source #

du_'8315''185''45'homo_950 :: T_Group_1062 -> T_Group_1062 -> (AgdaAny -> AgdaAny) -> T_IsGroupMorphism_932 -> AgdaAny -> AgdaAny Source #

d_IsGroupMorphism'45'syntax_978 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Group_1062 -> T_Group_1062 -> (AgdaAny -> AgdaAny) -> () Source #

d_group_1020 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_AbelianGroup_1174 -> T_Group_1062 Source #

du_group_1020 :: T_AbelianGroup_1174 -> T_Group_1062 Source #

d_group_1124 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_AbelianGroup_1174 -> T_Group_1062 Source #

du_group_1124 :: T_AbelianGroup_1174 -> T_Group_1062 Source #

d_Homomorphic'8320'_1206 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_AbelianGroup_1174 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Homomorphic'8321'_1208 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_AbelianGroup_1174 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Homomorphic'8322'_1210 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_AbelianGroup_1174 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Morphism_1212 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_AbelianGroup_1174 -> () Source #

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

newtype T_IsAbelianGroupMorphism_1216 Source #

Constructors

C_IsAbelianGroupMorphism'46'constructor_8913 T_IsGroupMorphism_932 

d_gp'45'homo_1222 :: T_IsAbelianGroupMorphism_1216 -> T_IsGroupMorphism_932 Source #

d_mn'45'homo_1226 :: T_IsAbelianGroupMorphism_1216 -> T_IsMonoidMorphism_306 Source #

d_sm'45'homo_1228 :: T_IsAbelianGroupMorphism_1216 -> T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_1230 :: T_IsAbelianGroupMorphism_1216 -> AgdaAny Source #

d_'8315''185''45'homo_1232 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_AbelianGroup_1174 -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroupMorphism_1216 -> AgdaAny -> AgdaAny Source #

du_'8315''185''45'homo_1232 :: T_AbelianGroup_1174 -> T_AbelianGroup_1174 -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroupMorphism_1216 -> AgdaAny -> AgdaAny Source #

d_'8729''45'homo_1234 :: T_IsAbelianGroupMorphism_1216 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'10214''10215''45'cong_1236 :: T_IsAbelianGroupMorphism_1216 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsAbelianGroupMorphism'45'syntax_1238 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_AbelianGroup_1174 -> T_AbelianGroup_1174 -> (AgdaAny -> AgdaAny) -> () Source #

d_'42''45'monoid_1290 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Ring_2612 -> T_Ring_2612 -> T_Monoid_502 Source #

du_'42''45'monoid_1290 :: T_Ring_2612 -> T_Monoid_502 Source #

d_'43''45'abelianGroup_1298 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Ring_2612 -> T_Ring_2612 -> T_AbelianGroup_1174 Source #

du_'43''45'abelianGroup_1298 :: T_Ring_2612 -> T_AbelianGroup_1174 Source #

d_'42''45'monoid_1462 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Ring_2612 -> T_Ring_2612 -> T_Monoid_502 Source #

du_'42''45'monoid_1462 :: T_Ring_2612 -> T_Monoid_502 Source #

d_'43''45'abelianGroup_1470 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Ring_2612 -> T_Ring_2612 -> T_AbelianGroup_1174 Source #

du_'43''45'abelianGroup_1470 :: T_Ring_2612 -> T_AbelianGroup_1174 Source #

d_Homomorphic'8320'_1602 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Ring_2612 -> T_Ring_2612 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_Homomorphic'8321'_1604 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Ring_2612 -> T_Ring_2612 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Homomorphic'8322'_1606 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Ring_2612 -> T_Ring_2612 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Morphism_1608 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Ring_2612 -> T_Ring_2612 -> () Source #

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

data T_IsRingMorphism_1612 Source #

Constructors

C_IsRingMorphism'46'constructor_10653 T_IsAbelianGroupMorphism_1216 T_IsMonoidMorphism_306 

d_'43''45'abgp'45'homo_1620 :: T_IsRingMorphism_1612 -> T_IsAbelianGroupMorphism_1216 Source #

d_'42''45'mn'45'homo_1622 :: T_IsRingMorphism_1612 -> T_IsMonoidMorphism_306 Source #

d_IsRingMorphism'45'syntax_1624 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Ring_2612 -> T_Ring_2612 -> (AgdaAny -> AgdaAny) -> () Source #