Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Algebra.Structures.Biased

Documentation

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

d__DistributesOver'691'__20 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'737'__22 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

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

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

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

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

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

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

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

d_IsAbelianGroup_88 ∷ p → p → p → p → p → p → p → () Source #

d_IsCommutativeMonoid_100 ∷ p → p → p → p → p → p → () Source #

d_IsCommutativeSemiring_106 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsMonoid_120 ∷ p → p → p → p → p → p → () Source #

d_IsRing_124 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_IsSemigroup_128 ∷ p → p → p → p → p → () Source #

d_IsCommutativeMonoid'737'_1514 ∷ p → p → p → p → p → p → () Source #

data T_IsCommutativeMonoid'737'_1514 Source #

Constructors

C_IsCommutativeMonoid'737''46'constructor_18101 T_IsSemigroup_194 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny)

d_isSemigroup_1526 ∷ T_IsCommutativeMonoid'737'_1514 → T_IsSemigroup_194 Source #

d_identity'737'_1528 ∷ T_IsCommutativeMonoid'737'_1514 → AgdaAny → AgdaAny Source #

d_comm_1530 ∷ T_IsCommutativeMonoid'737'_1514 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity'691'_1558 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → AgdaAny → AgdaAny Source #

du_identity'691'_1558 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → AgdaAny → AgdaAny Source #

d_identity_1560 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → T_Σ_14 Source #

du_identity_1560 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → T_Σ_14 Source #

d_isCommutativeMonoid_1562 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → T_IsCommutativeMonoid_406 Source #

du_isCommutativeMonoid_1562 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → T_IsCommutativeMonoid_406 Source #

d_IsCommutativeMonoid'691'_1568 ∷ p → p → p → p → p → p → () Source #

data T_IsCommutativeMonoid'691'_1568 Source #

Constructors

C_IsCommutativeMonoid'691''46'constructor_19839 T_IsSemigroup_194 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny)

d_isSemigroup_1580 ∷ T_IsCommutativeMonoid'691'_1568 → T_IsSemigroup_194 Source #

d_identity'691'_1582 ∷ T_IsCommutativeMonoid'691'_1568 → AgdaAny → AgdaAny Source #

d_comm_1584 ∷ T_IsCommutativeMonoid'691'_1568 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity'737'_1612 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → AgdaAny → AgdaAny Source #

du_identity'737'_1612 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → AgdaAny → AgdaAny Source #

d_identity_1614 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → T_Σ_14 Source #

du_identity_1614 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → T_Σ_14 Source #

d_isCommutativeMonoid_1616 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → T_IsCommutativeMonoid_406 Source #

du_isCommutativeMonoid_1616 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → T_IsCommutativeMonoid_406 Source #

d_IsCommutativeSemiring'737'_1626 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsCommutativeSemiring'737'_1626 Source #

Constructors

C_IsCommutativeSemiring'737''46'constructor_21625 T_IsCommutativeMonoid_406 T_IsCommutativeMonoid_406 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny)

d_'43''45'isCommutativeMonoid_1644 ∷ T_IsCommutativeSemiring'737'_1626 → T_IsCommutativeMonoid_406 Source #

d_'42''45'isCommutativeMonoid_1646 ∷ T_IsCommutativeSemiring'737'_1626 → T_IsCommutativeMonoid_406 Source #

d_distrib'691'_1648 ∷ T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'737'_1650 ∷ T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny Source #

d_comm_1698 ∷ T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'737'_1736 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'737'_1736 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib_1738 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_1626 → T_Σ_14 Source #

du_distrib_1738 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemiring'737'_1626 → T_Σ_14 Source #

d_zero'691'_1740 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny Source #

du_zero'691'_1740 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny Source #

d_zero_1742 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_1626 → T_Σ_14 Source #

du_zero_1742 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'737'_1626 → T_Σ_14 Source #

d_isCommutativeSemiring_1744 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_1626 → T_IsCommutativeSemiring_1344 Source #

du_isCommutativeSemiring_1744 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'737'_1626 → T_IsCommutativeSemiring_1344 Source #

d_IsCommutativeSemiring'691'_1754 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsCommutativeSemiring'691'_1754 Source #

Constructors

C_IsCommutativeSemiring'691''46'constructor_26987 T_IsCommutativeMonoid_406 T_IsCommutativeMonoid_406 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny)

d_'43''45'isCommutativeMonoid_1772 ∷ T_IsCommutativeSemiring'691'_1754 → T_IsCommutativeMonoid_406 Source #

d_'42''45'isCommutativeMonoid_1774 ∷ T_IsCommutativeSemiring'691'_1754 → T_IsCommutativeMonoid_406 Source #

d_distrib'737'_1776 ∷ T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'691'_1778 ∷ T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny Source #

d_comm_1826 ∷ T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'691'_1864 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_distrib'691'_1864 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib_1866 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_1754 → T_Σ_14 Source #

du_distrib_1866 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemiring'691'_1754 → T_Σ_14 Source #

d_zero'737'_1868 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny Source #

du_zero'737'_1868 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny Source #

d_zero_1870 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_1754 → T_Σ_14 Source #

du_zero_1870 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'691'_1754 → T_Σ_14 Source #

d_isCommutativeSemiring_1872 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_1754 → T_IsCommutativeSemiring_1344 Source #

du_isCommutativeSemiring_1872 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'691'_1754 → T_IsCommutativeSemiring_1344 Source #

d_IsRingWithoutAnnihilatingZero_1884 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsRingWithoutAnnihilatingZero_1884 Source #

Constructors

C_IsRingWithoutAnnihilatingZero'46'constructor_32383 T_IsAbelianGroup_662 T_IsMonoid_358 T_Σ_14

d_'43''45'isAbelianGroup_1902 ∷ T_IsRingWithoutAnnihilatingZero_1884 → T_IsAbelianGroup_662 Source #

d_'42''45'isMonoid_1904 ∷ T_IsRingWithoutAnnihilatingZero_1884 → T_IsMonoid_358 Source #

d_distrib_1906 ∷ T_IsRingWithoutAnnihilatingZero_1884 → T_Σ_14 Source #

d_zero'737'_2002 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → AgdaAny → AgdaAny Source #

du_zero'737'_2002 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → AgdaAny → AgdaAny Source #

d_zero'691'_2004 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → AgdaAny → AgdaAny Source #

du_zero'691'_2004 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → AgdaAny → AgdaAny Source #

d_zero_2006 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → T_Σ_14 Source #

du_zero_2006 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → T_Σ_14 Source #

d_isRing_2008 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → T_IsRing_1584 Source #

du_isRing_2008 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → T_IsRing_1584 Source #