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 -> () #

d_Homomorphic'8321'_34 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_Homomorphic'8322'_36 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Morphism_38 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> () #

d__'8729'__58 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny #

du__'8729'__58 :: T_Semigroup_536 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__60 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_Semigroup_536 -> AgdaAny -> AgdaAny -> () #

d_Homomorphic'8320'_138 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_Semigroup_536 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_Homomorphic'8321'_140 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_Semigroup_536 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_Homomorphic'8322'_142 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_Semigroup_536 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Morphism_144 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_Semigroup_536 -> () #

d_IsSemigroupMorphism_148 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsSemigroupMorphism_148 #

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 #

d_'8729''45'homo_158 :: T_IsSemigroupMorphism_148 -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsSemigroupMorphism'45'syntax_160 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Semigroup_536 -> T_Semigroup_536 -> (AgdaAny -> AgdaAny) -> () #

d_semigroup_218 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Monoid_882 -> T_Semigroup_536 #

du_semigroup_218 :: T_Monoid_882 -> T_Semigroup_536 #

d_ε_228 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Monoid_882 -> AgdaAny #

du_ε_228 :: T_Monoid_882 -> AgdaAny #

d_semigroup_276 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Monoid_882 -> T_Semigroup_536 #

du_semigroup_276 :: T_Monoid_882 -> T_Semigroup_536 #

d_Homomorphic'8320'_296 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Monoid_882 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_Homomorphic'8321'_298 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Monoid_882 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_Homomorphic'8322'_300 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Monoid_882 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Morphism_302 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Monoid_882 -> () #

d_IsMonoidMorphism_306 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsMonoidMorphism_306 #

Constructors

C_IsMonoidMorphism'46'constructor_2139 T_IsSemigroupMorphism_148 AgdaAny

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

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

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

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

d_IsMonoidMorphism'45'syntax_324 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Monoid_882 -> T_Monoid_882 -> (AgdaAny -> AgdaAny) -> () #

d_monoid_386 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_CommutativeMonoid_962 -> T_Monoid_882 #

du_monoid_386 :: T_CommutativeMonoid_962 -> T_Monoid_882 #

d_monoid_458 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_CommutativeMonoid_962 -> T_Monoid_882 #

du_monoid_458 :: T_CommutativeMonoid_962 -> T_Monoid_882 #

d_Homomorphic'8320'_488 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_CommutativeMonoid_962 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_Homomorphic'8321'_490 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_CommutativeMonoid_962 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_Homomorphic'8322'_492 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_CommutativeMonoid_962 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Morphism_494 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_CommutativeMonoid_962 -> () #

d_IsCommutativeMonoidMorphism_498 :: p -> p -> p -> p -> p -> p -> p -> () #

newtype T_IsCommutativeMonoidMorphism_498 #

Constructors

C_IsCommutativeMonoidMorphism'46'constructor_3705 T_IsMonoidMorphism_306

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

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

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

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

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

d_IsCommutativeMonoidMorphism'45'syntax_516 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_CommutativeMonoid_962 -> T_CommutativeMonoid_962 -> (AgdaAny -> AgdaAny) -> () #

d_commutativeMonoid_554 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962 #

du_commutativeMonoid_554 :: T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962 #

d_monoid_596 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentCommutativeMonoid_1148 -> T_Monoid_882 #

du_monoid_596 :: T_IdempotentCommutativeMonoid_1148 -> T_Monoid_882 #

d_commutativeMonoid_644 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962 #

du_commutativeMonoid_644 :: T_IdempotentCommutativeMonoid_1148 -> T_CommutativeMonoid_962 #

d_monoid_686 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentCommutativeMonoid_1148 -> T_Monoid_882 #

du_monoid_686 :: T_IdempotentCommutativeMonoid_1148 -> T_Monoid_882 #

d_Homomorphic'8320'_716 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentCommutativeMonoid_1148 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_Homomorphic'8321'_718 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentCommutativeMonoid_1148 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_Homomorphic'8322'_720 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentCommutativeMonoid_1148 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Morphism_722 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentCommutativeMonoid_1148 -> () #

d_IsIdempotentCommutativeMonoidMorphism_726 :: p -> p -> p -> p -> p -> p -> p -> () #

newtype T_IsIdempotentCommutativeMonoidMorphism_726 #

Constructors

C_IsIdempotentCommutativeMonoidMorphism'46'constructor_5361 T_IsMonoidMorphism_306

d_mn'45'homo_732 :: T_IsIdempotentCommutativeMonoidMorphism_726 -> T_IsMonoidMorphism_306 #

d_sm'45'homo_736 :: T_IsIdempotentCommutativeMonoidMorphism_726 -> T_IsSemigroupMorphism_148 #

d_ε'45'homo_738 :: T_IsIdempotentCommutativeMonoidMorphism_726 -> AgdaAny #

d_'8729''45'homo_740 :: T_IsIdempotentCommutativeMonoidMorphism_726 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'10214''10215''45'cong_742 :: T_IsIdempotentCommutativeMonoidMorphism_726 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCommutativeMonoidMorphism_744 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentCommutativeMonoid_1148 -> (AgdaAny -> AgdaAny) -> T_IsIdempotentCommutativeMonoidMorphism_726 -> T_IsCommutativeMonoidMorphism_498 #

du_isCommutativeMonoidMorphism_744 :: T_IsIdempotentCommutativeMonoidMorphism_726 -> T_IsCommutativeMonoidMorphism_498 #

d_IsIdempotentCommutativeMonoidMorphism'45'syntax_746 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_IdempotentCommutativeMonoid_1148 -> T_IdempotentCommutativeMonoid_1148 -> (AgdaAny -> AgdaAny) -> () #

d__'8315''185'_772 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Group_1520 -> AgdaAny -> AgdaAny #

du__'8315''185'_772 :: T_Group_1520 -> AgdaAny -> AgdaAny #

d_monoid_820 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Group_1520 -> T_Monoid_882 #

du_monoid_820 :: T_Group_1520 -> T_Monoid_882 #

d_monoid_912 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Group_1520 -> T_Monoid_882 #

du_monoid_912 :: T_Group_1520 -> T_Monoid_882 #

d_Homomorphic'8320'_950 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Group_1520 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_Homomorphic'8321'_952 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Group_1520 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_Homomorphic'8322'_954 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Group_1520 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Morphism_956 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Group_1520 -> () #

d_IsGroupMorphism_960 :: p -> p -> p -> p -> p -> p -> p -> () #

newtype T_IsGroupMorphism_960 #

Constructors

C_IsGroupMorphism'46'constructor_7465 T_IsMonoidMorphism_306

d_mn'45'homo_966 :: T_IsGroupMorphism_960 -> T_IsMonoidMorphism_306 #

d_sm'45'homo_970 :: T_IsGroupMorphism_960 -> T_IsSemigroupMorphism_148 #

d_ε'45'homo_972 :: T_IsGroupMorphism_960 -> AgdaAny #

d_'8729''45'homo_974 :: T_IsGroupMorphism_960 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'10214''10215''45'cong_976 :: T_IsGroupMorphism_960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8315''185''45'homo_978 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Group_1520 -> (AgdaAny -> AgdaAny) -> T_IsGroupMorphism_960 -> AgdaAny -> AgdaAny #

du_'8315''185''45'homo_978 :: T_Group_1520 -> T_Group_1520 -> (AgdaAny -> AgdaAny) -> T_IsGroupMorphism_960 -> AgdaAny -> AgdaAny #

d_IsGroupMorphism'45'syntax_1022 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Group_1520 -> T_Group_1520 -> (AgdaAny -> AgdaAny) -> () #

d_group_1064 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_AbelianGroup_1636 -> T_Group_1520 #

du_group_1064 :: T_AbelianGroup_1636 -> T_Group_1520 #

d_group_1168 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_AbelianGroup_1636 -> T_Group_1520 #

du_group_1168 :: T_AbelianGroup_1636 -> T_Group_1520 #

d_Homomorphic'8320'_1250 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_AbelianGroup_1636 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_Homomorphic'8321'_1252 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_AbelianGroup_1636 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_Homomorphic'8322'_1254 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_AbelianGroup_1636 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Morphism_1256 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_AbelianGroup_1636 -> () #

d_IsAbelianGroupMorphism_1260 :: p -> p -> p -> p -> p -> p -> p -> () #

newtype T_IsAbelianGroupMorphism_1260 #

Constructors

C_IsAbelianGroupMorphism'46'constructor_11939 T_IsGroupMorphism_960

d_gp'45'homo_1266 :: T_IsAbelianGroupMorphism_1260 -> T_IsGroupMorphism_960 #

d_mn'45'homo_1270 :: T_IsAbelianGroupMorphism_1260 -> T_IsMonoidMorphism_306 #

d_sm'45'homo_1272 :: T_IsAbelianGroupMorphism_1260 -> T_IsSemigroupMorphism_148 #

d_ε'45'homo_1274 :: T_IsAbelianGroupMorphism_1260 -> AgdaAny #

d_'8315''185''45'homo_1276 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_AbelianGroup_1636 -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroupMorphism_1260 -> AgdaAny -> AgdaAny #

du_'8315''185''45'homo_1276 :: T_AbelianGroup_1636 -> T_AbelianGroup_1636 -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroupMorphism_1260 -> AgdaAny -> AgdaAny #

d_'8729''45'homo_1278 :: T_IsAbelianGroupMorphism_1260 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'10214''10215''45'cong_1280 :: T_IsAbelianGroupMorphism_1260 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsAbelianGroupMorphism'45'syntax_1282 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_AbelianGroup_1636 -> T_AbelianGroup_1636 -> (AgdaAny -> AgdaAny) -> () #

d_'42''45'monoid_1334 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Ring_3800 -> T_Monoid_882 #

du_'42''45'monoid_1334 :: T_Ring_3800 -> T_Monoid_882 #

d_'43''45'abelianGroup_1342 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Ring_3800 -> T_AbelianGroup_1636 #

du_'43''45'abelianGroup_1342 :: T_Ring_3800 -> T_AbelianGroup_1636 #

d_'42''45'monoid_1516 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Ring_3800 -> T_Monoid_882 #

du_'42''45'monoid_1516 :: T_Ring_3800 -> T_Monoid_882 #

d_'43''45'abelianGroup_1524 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Ring_3800 -> T_AbelianGroup_1636 #

du_'43''45'abelianGroup_1524 :: T_Ring_3800 -> T_AbelianGroup_1636 #

d_Homomorphic'8320'_1666 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Ring_3800 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> () #

d_Homomorphic'8321'_1668 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Ring_3800 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_Homomorphic'8322'_1670 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Ring_3800 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Morphism_1672 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Ring_3800 -> () #

d_IsRingMorphism_1676 :: p -> p -> p -> p -> p -> p -> p -> () #

data T_IsRingMorphism_1676 #

Constructors

C_IsRingMorphism'46'constructor_13939 T_IsAbelianGroupMorphism_1260 T_IsMonoidMorphism_306

d_'43''45'abgp'45'homo_1684 :: T_IsRingMorphism_1676 -> T_IsAbelianGroupMorphism_1260 #

d_'42''45'mn'45'homo_1686 :: T_IsRingMorphism_1676 -> T_IsMonoidMorphism_306 #

d_IsRingMorphism'45'syntax_1688 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Ring_3800 -> T_Ring_3800 -> (AgdaAny -> AgdaAny) -> () #