Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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_42 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftIdentity_84 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftZero_92 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightIdentity_114 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightZero_122 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Zero_142 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_IsAbelianGroup_146 ∷ p → p → p → p → p → p → p → () Source #
d_IsCommutativeMonoid_158 ∷ p → p → p → p → p → p → () Source #
d_IsCommutativeSemiring_164 ∷ p → p → p → p → p → p → p → p → () Source #
d_IsMonoid_196 ∷ p → p → p → p → p → p → () Source #
d_IsNearSemiring_200 ∷ p → p → p → p → p → p → p → () Source #
d_IsRing_212 ∷ p → p → p → p → p → p → p → p → p → () Source #
d_IsSemigroup_218 ∷ p → p → p → p → p → () Source #
d_IsSemiringWithoutAnnihilatingZero_224 ∷ p → p → p → p → p → p → p → p → () Source #
d_IsSemiringWithoutOne_226 ∷ p → p → p → p → p → p → p → () Source #
d__'47''47'__234 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny Source #
du__'47''47'__234 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_identity'691'_242 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #
d_identity'737'_244 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #
d_inverse'691'_248 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #
d_inverse'737'_250 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny Source #
d_isCommutativeMagma_252 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsCommutativeMagma_212 Source #
d_isCommutativeMonoid_254 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsCommutativeMonoid_736 Source #
du_isCommutativeMonoid_254 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsCommutativeMonoid_736 Source #
d_isCommutativeSemigroup_256 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsCommutativeSemigroup_548 Source #
d_isInvertibleMagma_262 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsInvertibleMagma_924 Source #
d_isInvertibleUnitalMagma_264 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsInvertibleUnitalMagma_976 Source #
d_isPartialEquivalence_270 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsPartialEquivalence_16 Source #
d_isUnitalMagma_274 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_IsUnitalMagma_642 Source #
d_reflexive_278 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_setoid_280 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → T_Setoid_44 Source #
d_unique'691''45''8315''185'_286 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_unique'691''45''8315''185'_286 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_unique'737''45''8315''185'_288 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_unique'737''45''8315''185'_288 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong'691'_294 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'691'_294 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong'737'_296 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'737'_296 ∷ T_IsAbelianGroup_1132 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_identity'691'_1602 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny Source #
du_identity'691'_1602 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny Source #
d_identity'737'_1604 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny Source #
du_identity'737'_1604 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_1610 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → T_IsPartialEquivalence_16 Source #
d_isUnitalMagma_1614 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → T_IsUnitalMagma_642 Source #
du_isUnitalMagma_1614 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → T_IsUnitalMagma_642 Source #
d_reflexive_1618 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_setoid_1620 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → T_Setoid_44 Source #
d_'8729''45'cong'691'_1628 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'691'_1628 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong'737'_1630 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'737'_1630 ∷ T_IsMonoid_686 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'42''45'cong_1702 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'42''45'assoc_2118 ∷ T_IsRing_2650 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'42''45'cong_2120 ∷ T_IsRing_2650 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc_2344 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'42''45'assoc_2484 ∷ T_IsSemiringWithoutAnnihilatingZero_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'42''45'cong_2486 ∷ T_IsSemiringWithoutAnnihilatingZero_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'43''45'isCommutativeMonoid_2522 ∷ T_IsSemiringWithoutAnnihilatingZero_1468 → T_IsCommutativeMonoid_736 Source #
d_'42''45'cong_2562 ∷ T_IsSemiringWithoutOne_1298 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'43''45'isCommutativeMonoid_2576 ∷ T_IsSemiringWithoutOne_1298 → T_IsCommutativeMonoid_736 Source #
d_IsCommutativeMonoid'737'_2662 ∷ p → p → p → p → p → p → () Source #
d_isCommutativeMonoid_2680 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_2662 → T_IsCommutativeMonoid_736 Source #
du_isCommutativeMonoid_2680 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_2662 → T_IsCommutativeMonoid_736 Source #
d_IsCommutativeMonoid'691'_2716 ∷ p → p → p → p → p → p → () Source #
d_isCommutativeMonoid_2734 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_2716 → T_IsCommutativeMonoid_736 Source #
du_isCommutativeMonoid_2734 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_2716 → T_IsCommutativeMonoid_736 Source #
d_IsSemiringWithoutOne'42'_2772 ∷ p → p → p → p → p → p → p → () Source #
d_'43''45'isCommutativeMonoid_2788 ∷ T_IsSemiringWithoutOne'42'_2772 → T_IsCommutativeMonoid_736 Source #
d_isSemiringWithoutOne_2796 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne'42'_2772 → T_IsSemiringWithoutOne_1298 Source #
du_isSemiringWithoutOne_2796 ∷ T_IsSemiringWithoutOne'42'_2772 → T_IsSemiringWithoutOne_1298 Source #
d_IsNearSemiring'42'_2834 ∷ p → p → p → p → p → p → p → () Source #
d_isNearSemiring_2858 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring'42'_2834 → T_IsNearSemiring_1218 Source #
d_IsSemiringWithoutAnnihilatingZero'42'_2898 ∷ p → p → p → p → p → p → p → p → () Source #
d_'43''45'isCommutativeMonoid_2914 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_2898 → T_IsCommutativeMonoid_736 Source #
d_isSemiringWithoutAnnihilatingZero_2920 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_2898 → T_IsSemiringWithoutAnnihilatingZero_1468 Source #
du_isSemiringWithoutAnnihilatingZero_2920 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_2898 → T_IsSemiringWithoutAnnihilatingZero_1468 Source #
d_identity'691'_2932 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_2898 → AgdaAny → AgdaAny Source #
d_identity'737'_2934 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_2898 → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_2940 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_2898 → T_IsPartialEquivalence_16 Source #
du_isPartialEquivalence_2940 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_2898 → T_IsPartialEquivalence_16 Source #
d_isUnitalMagma_2944 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_2898 → T_IsUnitalMagma_642 Source #
d_reflexive_2948 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_2898 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
du_reflexive_2948 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_2898 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_setoid_2950 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_2898 → T_Setoid_44 Source #
d_'8729''45'cong'691'_2958 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_2898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'691'_2958 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_2898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong'737'_2960 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_2898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'737'_2960 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_2898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_IsCommutativeSemiring'737'_2970 ∷ p → p → p → p → p → p → p → p → () Source #
d_'43''45'isCommutativeMonoid_2988 ∷ T_IsCommutativeSemiring'737'_2970 → T_IsCommutativeMonoid_736 Source #
d_'42''45'isCommutativeMonoid_2990 ∷ T_IsCommutativeSemiring'737'_2970 → T_IsCommutativeMonoid_736 Source #
d_distrib'691'_2992 ∷ T_IsCommutativeSemiring'737'_2970 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isCommutativeSemiring_2996 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_2970 → T_IsCommutativeSemiring_1678 Source #
du_isCommutativeSemiring_2996 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'737'_2970 → T_IsCommutativeSemiring_1678 Source #
d_IsCommutativeSemiring'691'_3098 ∷ p → p → p → p → p → p → p → p → () Source #
d_'43''45'isCommutativeMonoid_3116 ∷ T_IsCommutativeSemiring'691'_3098 → T_IsCommutativeMonoid_736 Source #
d_'42''45'isCommutativeMonoid_3118 ∷ T_IsCommutativeSemiring'691'_3098 → T_IsCommutativeMonoid_736 Source #
d_distrib'737'_3120 ∷ T_IsCommutativeSemiring'691'_3098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isCommutativeSemiring_3124 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_3098 → T_IsCommutativeSemiring_1678 Source #
du_isCommutativeSemiring_3124 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'691'_3098 → T_IsCommutativeSemiring_1678 Source #
d_IsRing'42'_3228 ∷ p → p → p → p → p → p → p → p → p → () Source #
data T_IsRing'42'_3228 Source #
d_isRing_3256 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3228 → T_IsRing_2650 Source #
d_identity'691'_3268 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3228 → AgdaAny → AgdaAny Source #
d_identity'737'_3270 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3228 → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_3276 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3228 → T_IsPartialEquivalence_16 Source #
d_isUnitalMagma_3280 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3228 → T_IsUnitalMagma_642 Source #
d_reflexive_3284 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3228 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_setoid_3286 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3228 → T_Setoid_44 Source #
d_'8729''45'cong'691'_3294 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'691'_3294 ∷ T_IsRing'42'_3228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong'737'_3296 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'737'_3296 ∷ T_IsRing'42'_3228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_IsRingWithoutAnnihilatingZero_3308 ∷ p → p → p → p → p → p → p → p → p → () Source #
d_'43''45'isAbelianGroup_3326 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsAbelianGroup_1132 Source #
d__'47''47'__3334 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny Source #
du__'47''47'__3334 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc_3336 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_identity'691'_3342 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #
d_identity'737'_3344 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #
d_inverse'691'_3348 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #
d_inverse'737'_3350 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #
d_isCommutativeMagma_3352 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_IsCommutativeMagma_212 Source #
du_isCommutativeMagma_3352 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsCommutativeMagma_212 Source #
d_isCommutativeMonoid_3354 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_IsCommutativeMonoid_736 Source #
du_isCommutativeMonoid_3354 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsCommutativeMonoid_736 Source #
d_isCommutativeSemigroup_3356 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_IsCommutativeSemigroup_548 Source #
du_isCommutativeSemigroup_3356 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsCommutativeSemigroup_548 Source #
d_isInvertibleMagma_3362 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_IsInvertibleMagma_924 Source #
d_isInvertibleUnitalMagma_3364 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_IsInvertibleUnitalMagma_976 Source #
du_isInvertibleUnitalMagma_3364 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsInvertibleUnitalMagma_976 Source #
d_isPartialEquivalence_3370 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_IsPartialEquivalence_16 Source #
du_isPartialEquivalence_3370 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsPartialEquivalence_16 Source #
d_isUnitalMagma_3374 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_IsUnitalMagma_642 Source #
d_reflexive_3378 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
du_reflexive_3378 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_setoid_3380 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_Setoid_44 Source #
d_trans_3384 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_unique'691''45''8315''185'_3386 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_unique'691''45''8315''185'_3386 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_unique'737''45''8315''185'_3388 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_unique'737''45''8315''185'_3388 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8315''185''45'cong_3390 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong_3392 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong'691'_3394 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'691'_3394 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong'737'_3396 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'737'_3396 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc_3400 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_identity'691'_3404 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #
d_identity'737'_3406 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_3412 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_IsPartialEquivalence_16 Source #
du_isPartialEquivalence_3412 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsPartialEquivalence_16 Source #
d_isUnitalMagma_3416 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_IsUnitalMagma_642 Source #
d_reflexive_3420 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
du_reflexive_3420 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_setoid_3422 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_Setoid_44 Source #
d_trans_3426 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong_3428 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong'691'_3430 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'691'_3430 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'cong'737'_3432 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'cong'737'_3432 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_zero'737'_3434 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #
du_zero'737'_3434 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #
d_zero'691'_3436 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #
du_zero'691'_3436 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #
d_zero_3438 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_Σ_14 Source #
du_zero_3438 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_Σ_14 Source #
d_isRing_3440 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3308 → T_IsRing_2650 Source #