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_536 → T_Semigroup_536 → AgdaAny → AgdaAny → AgdaAny Source #

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

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

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

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

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

d_Morphism_144 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Semigroup_536 → T_Semigroup_536 → () 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_536 → T_Semigroup_536 → (AgdaAny → AgdaAny) → () Source #

d_semigroup_218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_882 → T_Monoid_882 → T_Semigroup_536 Source #

du_semigroup_218 ∷ T_Monoid_882 → T_Semigroup_536 Source #

d_ε_228 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_882 → T_Monoid_882 → AgdaAny Source #

du_ε_228 ∷ T_Monoid_882 → AgdaAny Source #

d_semigroup_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_882 → T_Monoid_882 → T_Semigroup_536 Source #

du_semigroup_276 ∷ T_Monoid_882 → T_Semigroup_536 Source #

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

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

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

d_Morphism_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_882 → T_Monoid_882 → () Source #

d_IsMonoidMorphism_306 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMonoidMorphism_306 Source #

Constructors

C_IsMonoidMorphism'46'constructor_2139 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Monoid_882 → T_Monoid_882 → (AgdaAny → AgdaAny) → () Source #

d_monoid_386 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_CommutativeMonoid_962 → T_Monoid_882 Source #

du_monoid_386 ∷ T_CommutativeMonoid_962 → T_Monoid_882 Source #

d_monoid_458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_CommutativeMonoid_962 → T_Monoid_882 Source #

du_monoid_458 ∷ T_CommutativeMonoid_962 → T_Monoid_882 Source #

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

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

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

d_Morphism_494 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_CommutativeMonoid_962 → () Source #

d_IsCommutativeMonoidMorphism_498 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsCommutativeMonoidMorphism_498 Source #

Constructors

C_IsCommutativeMonoidMorphism'46'constructor_3705 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_CommutativeMonoid_962 → T_CommutativeMonoid_962 → (AgdaAny → AgdaAny) → () Source #

d_commutativeMonoid_554 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IdempotentCommutativeMonoid_1148 → T_CommutativeMonoid_962 Source #

du_commutativeMonoid_554 ∷ T_IdempotentCommutativeMonoid_1148 → T_CommutativeMonoid_962 Source #

d_monoid_596 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IdempotentCommutativeMonoid_1148 → T_Monoid_882 Source #

du_monoid_596 ∷ T_IdempotentCommutativeMonoid_1148 → T_Monoid_882 Source #

d_commutativeMonoid_644 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IdempotentCommutativeMonoid_1148 → T_CommutativeMonoid_962 Source #

du_commutativeMonoid_644 ∷ T_IdempotentCommutativeMonoid_1148 → T_CommutativeMonoid_962 Source #

d_monoid_686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IdempotentCommutativeMonoid_1148 → T_Monoid_882 Source #

du_monoid_686 ∷ T_IdempotentCommutativeMonoid_1148 → T_Monoid_882 Source #

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

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

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

d_Morphism_722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_IdempotentCommutativeMonoid_1148 → T_IdempotentCommutativeMonoid_1148 → () Source #

d_IsIdempotentCommutativeMonoidMorphism_726 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsIdempotentCommutativeMonoidMorphism_726 Source #

Constructors

C_IsIdempotentCommutativeMonoidMorphism'46'constructor_5361 T_IsMonoidMorphism_306

d_mn'45'homo_732 ∷ T_IsIdempotentCommutativeMonoidMorphism_726 → T_IsMonoidMorphism_306 Source #

d_sm'45'homo_736 ∷ T_IsIdempotentCommutativeMonoidMorphism_726 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_738 ∷ T_IsIdempotentCommutativeMonoidMorphism_726 → AgdaAny Source #

d_'8729''45'homo_740 ∷ T_IsIdempotentCommutativeMonoidMorphism_726 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_742 ∷ T_IsIdempotentCommutativeMonoidMorphism_726 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 Source #

du_isCommutativeMonoidMorphism_744 ∷ T_IsIdempotentCommutativeMonoidMorphism_726 → T_IsCommutativeMonoidMorphism_498 Source #

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

d__'8315''185'_772 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1520 → T_Group_1520 → AgdaAny → AgdaAny Source #

du__'8315''185'_772 ∷ T_Group_1520 → AgdaAny → AgdaAny Source #

d_monoid_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1520 → T_Group_1520 → T_Monoid_882 Source #

du_monoid_820 ∷ T_Group_1520 → T_Monoid_882 Source #

d_monoid_912 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1520 → T_Group_1520 → T_Monoid_882 Source #

du_monoid_912 ∷ T_Group_1520 → T_Monoid_882 Source #

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

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

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

d_Morphism_956 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Group_1520 → T_Group_1520 → () Source #

d_IsGroupMorphism_960 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsGroupMorphism_960 Source #

Constructors

C_IsGroupMorphism'46'constructor_7465 T_IsMonoidMorphism_306

d_mn'45'homo_966 ∷ T_IsGroupMorphism_960 → T_IsMonoidMorphism_306 Source #

d_sm'45'homo_970 ∷ T_IsGroupMorphism_960 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_972 ∷ T_IsGroupMorphism_960 → AgdaAny Source #

d_'8729''45'homo_974 ∷ T_IsGroupMorphism_960 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_976 ∷ T_IsGroupMorphism_960 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 Source #

du_'8315''185''45'homo_978 ∷ T_Group_1520 → T_Group_1520 → (AgdaAny → AgdaAny) → T_IsGroupMorphism_960 → AgdaAny → AgdaAny Source #

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

d_group_1064 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1636 → T_AbelianGroup_1636 → T_Group_1520 Source #

du_group_1064 ∷ T_AbelianGroup_1636 → T_Group_1520 Source #

d_group_1168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1636 → T_AbelianGroup_1636 → T_Group_1520 Source #

du_group_1168 ∷ T_AbelianGroup_1636 → T_Group_1520 Source #

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

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

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

d_Morphism_1256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_AbelianGroup_1636 → T_AbelianGroup_1636 → () Source #

d_IsAbelianGroupMorphism_1260 ∷ p → p → p → p → p → p → p → () Source #

newtype T_IsAbelianGroupMorphism_1260 Source #

Constructors

C_IsAbelianGroupMorphism'46'constructor_11939 T_IsGroupMorphism_960

d_gp'45'homo_1266 ∷ T_IsAbelianGroupMorphism_1260 → T_IsGroupMorphism_960 Source #

d_mn'45'homo_1270 ∷ T_IsAbelianGroupMorphism_1260 → T_IsMonoidMorphism_306 Source #

d_sm'45'homo_1272 ∷ T_IsAbelianGroupMorphism_1260 → T_IsSemigroupMorphism_148 Source #

d_ε'45'homo_1274 ∷ T_IsAbelianGroupMorphism_1260 → AgdaAny Source #

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 Source #

du_'8315''185''45'homo_1276 ∷ T_AbelianGroup_1636 → T_AbelianGroup_1636 → (AgdaAny → AgdaAny) → T_IsAbelianGroupMorphism_1260 → AgdaAny → AgdaAny Source #

d_'8729''45'homo_1278 ∷ T_IsAbelianGroupMorphism_1260 → AgdaAny → AgdaAny → AgdaAny Source #

d_'10214''10215''45'cong_1280 ∷ T_IsAbelianGroupMorphism_1260 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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 Source #

du_'42''45'monoid_1334 ∷ T_Ring_3800 → T_Monoid_882 Source #

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 Source #

du_'43''45'abelianGroup_1342 ∷ T_Ring_3800 → T_AbelianGroup_1636 Source #

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 Source #

du_'42''45'monoid_1516 ∷ T_Ring_3800 → T_Monoid_882 Source #

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 Source #

du_'43''45'abelianGroup_1524 ∷ T_Ring_3800 → T_AbelianGroup_1636 Source #

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

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

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

d_Morphism_1672 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Ring_3800 → T_Ring_3800 → () Source #

d_IsRingMorphism_1676 ∷ p → p → p → p → p → p → p → () Source #

data T_IsRingMorphism_1676 Source #

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 Source #

d_'42''45'mn'45'homo_1686 ∷ T_IsRingMorphism_1676 → T_IsMonoidMorphism_306 Source #

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