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_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_comm_238 ∷ T_IsAbelianGroup_1132 → 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 #

du_identity'691'_242 ∷ 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 #

du_identity'737'_244 ∷ 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 #

du_inverse'691'_248 ∷ 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 #

du_inverse'737'_250 ∷ 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 #

du_isCommutativeMagma_252 ∷ 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 #

du_isCommutativeSemigroup_256 ∷ T_IsAbelianGroup_1132 → T_IsCommutativeSemigroup_548 Source #

d_isGroup_260 ∷ T_IsAbelianGroup_1132 → T_IsGroup_1036 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 #

du_isInvertibleMagma_262 ∷ 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 #

du_isInvertibleUnitalMagma_264 ∷ 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 #

du_isPartialEquivalence_270 ∷ 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 #

du_isUnitalMagma_274 ∷ 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 #

du_reflexive_278 ∷ 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 #

du_setoid_280 ∷ 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_comm_528 ∷ T_IsCommutativeMonoid_736 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMonoid_544 ∷ T_IsCommutativeMonoid_736 → T_IsMonoid_686 Source #

d_'42''45'comm_728 ∷ T_IsCommutativeSemiring_1678 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSemiring_798 ∷ T_IsCommutativeSemiring_1678 → T_IsSemiring_1570 Source #

d_identity_1600 ∷ T_IsMonoid_686 → T_Σ_14 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 #

du_isPartialEquivalence_1610 ∷ T_IsMonoid_686 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1612 ∷ T_IsMonoid_686 → T_IsSemigroup_472 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 #

du_reflexive_1618 ∷ 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 #

du_setoid_1620 ∷ 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'assoc_1700 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'cong_1702 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isMonoid_1728 ∷ T_IsNearSemiring_1218 → T_IsMonoid_686 Source #

d_distrib'691'_1734 ∷ T_IsNearSemiring_1218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'737'_1750 ∷ T_IsNearSemiring_1218 → 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_'42''45'identity_2126 ∷ T_IsRing_2650 → T_Σ_14 Source #

d_'43''45'isAbelianGroup_2154 ∷ T_IsRing_2650 → T_IsAbelianGroup_1132 Source #

d_distrib_2184 ∷ T_IsRing_2650 → T_Σ_14 Source #

d_assoc_2344 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_2348 ∷ T_IsSemigroup_472 → T_IsMagma_176 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_'42''45'identity_2492 ∷ T_IsSemiringWithoutAnnihilatingZero_1468 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_2522 ∷ T_IsSemiringWithoutAnnihilatingZero_1468 → T_IsCommutativeMonoid_736 Source #

d_distrib_2534 ∷ T_IsSemiringWithoutAnnihilatingZero_1468 → T_Σ_14 Source #

d_'42''45'assoc_2560 ∷ T_IsSemiringWithoutOne_1298 → AgdaAny → AgdaAny → AgdaAny → AgdaAny 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_distrib_2584 ∷ T_IsSemiringWithoutOne_1298 → T_Σ_14 Source #

d_zero_2604 ∷ T_IsSemiringWithoutOne_1298 → T_Σ_14 Source #

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

data T_IsCommutativeMonoid'737'_2662 Source #

Constructors

C_IsCommutativeMonoid'737''46'constructor_34899 T_IsSemigroup_472 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny)

d_isSemigroup_2674 ∷ T_IsCommutativeMonoid'737'_2662 → T_IsSemigroup_472 Source #

d_identity'737'_2676 ∷ T_IsCommutativeMonoid'737'_2662 → AgdaAny → AgdaAny Source #

d_comm_2678 ∷ T_IsCommutativeMonoid'737'_2662 → AgdaAny → AgdaAny → AgdaAny 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 #

data T_IsCommutativeMonoid'691'_2716 Source #

Constructors

C_IsCommutativeMonoid'691''46'constructor_36341 T_IsSemigroup_472 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny)

d_isSemigroup_2728 ∷ T_IsCommutativeMonoid'691'_2716 → T_IsSemigroup_472 Source #

d_identity'691'_2730 ∷ T_IsCommutativeMonoid'691'_2716 → AgdaAny → AgdaAny Source #

d_comm_2732 ∷ T_IsCommutativeMonoid'691'_2716 → AgdaAny → AgdaAny → AgdaAny 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 #

data T_IsSemiringWithoutOne'42'_2772 Source #

Constructors

C_IsSemiringWithoutOne'42''46'constructor_37821 T_IsCommutativeMonoid_736 T_IsSemigroup_472 T_Σ_14 T_Σ_14

d_'43''45'isCommutativeMonoid_2788 ∷ T_IsSemiringWithoutOne'42'_2772 → T_IsCommutativeMonoid_736 Source #

d_'42''45'isSemigroup_2790 ∷ T_IsSemiringWithoutOne'42'_2772 → T_IsSemigroup_472 Source #

d_distrib_2792 ∷ T_IsSemiringWithoutOne'42'_2772 → T_Σ_14 Source #

d_zero_2794 ∷ T_IsSemiringWithoutOne'42'_2772 → T_Σ_14 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 #

data T_IsNearSemiring'42'_2834 Source #

Constructors

C_IsNearSemiring'42''46'constructor_39635 T_IsMonoid_686 T_IsSemigroup_472 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny)

d_'43''45'isMonoid_2850 ∷ T_IsNearSemiring'42'_2834 → T_IsMonoid_686 Source #

d_'42''45'isSemigroup_2852 ∷ T_IsNearSemiring'42'_2834 → T_IsSemigroup_472 Source #

d_distrib'691'_2854 ∷ T_IsNearSemiring'42'_2834 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'737'_2856 ∷ T_IsNearSemiring'42'_2834 → AgdaAny → AgdaAny 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 #

du_isNearSemiring_2858 ∷ T_IsNearSemiring'42'_2834 → T_IsNearSemiring_1218 Source #

d_IsSemiringWithoutAnnihilatingZero'42'_2898 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsSemiringWithoutAnnihilatingZero'42'_2898 Source #

Constructors

C_IsSemiringWithoutAnnihilatingZero'42''46'constructor_41443 T_IsCommutativeMonoid_736 T_IsMonoid_686 T_Σ_14

d_'43''45'isCommutativeMonoid_2914 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_2898 → T_IsCommutativeMonoid_736 Source #

d_'42''45'isMonoid_2916 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_2898 → T_IsMonoid_686 Source #

d_distrib_2918 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_2898 → T_Σ_14 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 #

du_identity'691'_2932 ∷ 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 #

du_identity'737'_2934 ∷ 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 #

du_isUnitalMagma_2944 ∷ 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 #

du_setoid_2950 ∷ 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 #

data T_IsCommutativeSemiring'737'_2970 Source #

Constructors

C_IsCommutativeSemiring'737''46'constructor_43731 T_IsCommutativeMonoid_736 T_IsCommutativeMonoid_736 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny)

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_zero'737'_2994 ∷ T_IsCommutativeSemiring'737'_2970 → 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 #

data T_IsCommutativeSemiring'691'_3098 Source #

Constructors

C_IsCommutativeSemiring'691''46'constructor_48791 T_IsCommutativeMonoid_736 T_IsCommutativeMonoid_736 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny)

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_zero'691'_3122 ∷ T_IsCommutativeSemiring'691'_3098 → 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 #

Constructors

C_IsRing'42''46'constructor_53915 T_IsAbelianGroup_1132 T_IsMonoid_686 T_Σ_14 T_Σ_14

d_'43''45'isAbelianGroup_3248 ∷ T_IsRing'42'_3228 → T_IsAbelianGroup_1132 Source #

d_'42''45'isMonoid_3250 ∷ T_IsRing'42'_3228 → T_IsMonoid_686 Source #

d_distrib_3252 ∷ T_IsRing'42'_3228 → T_Σ_14 Source #

d_zero_3254 ∷ T_IsRing'42'_3228 → T_Σ_14 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 #

du_isRing_3256 ∷ 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 #

du_identity'691'_3268 ∷ 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 #

du_identity'737'_3270 ∷ 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 #

du_isPartialEquivalence_3276 ∷ 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 #

du_isUnitalMagma_3280 ∷ 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 #

du_reflexive_3284 ∷ 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 #

du_setoid_3286 ∷ 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 #

data T_IsRingWithoutAnnihilatingZero_3308 Source #

Constructors

C_IsRingWithoutAnnihilatingZero'46'constructor_56523 T_IsAbelianGroup_1132 T_IsMonoid_686 T_Σ_14

d_'43''45'isAbelianGroup_3326 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsAbelianGroup_1132 Source #

d_'42''45'isMonoid_3328 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsMonoid_686 Source #

d_distrib_3330 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_Σ_14 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_comm_3338 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_3340 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_Σ_14 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 #

du_identity'691'_3342 ∷ 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 #

du_identity'737'_3344 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #

d_inverse_3346 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_Σ_14 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 #

du_inverse'691'_3348 ∷ 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 #

du_inverse'737'_3350 ∷ 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_isEquivalence_3358 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsEquivalence_26 Source #

d_isGroup_3360 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsGroup_1036 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 #

du_isInvertibleMagma_3362 ∷ 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_isMagma_3366 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsMagma_176 Source #

d_isMonoid_3368 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsMonoid_686 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_isSemigroup_3372 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsSemigroup_472 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 #

du_isUnitalMagma_3374 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsUnitalMagma_642 Source #

d_refl_3376 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny 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 #

du_setoid_3380 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_Setoid_44 Source #

d_sym_3382 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny 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_3402 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_Σ_14 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 #

du_identity'691'_3404 ∷ 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 #

du_identity'737'_3406 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny Source #

d_isEquivalence_3408 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsEquivalence_26 Source #

d_isMagma_3410 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsMagma_176 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_isSemigroup_3414 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsSemigroup_472 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 #

du_isUnitalMagma_3416 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsUnitalMagma_642 Source #

d_refl_3418 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny 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 #

du_setoid_3422 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_Setoid_44 Source #

d_sym_3424 ∷ T_IsRingWithoutAnnihilatingZero_3308 → AgdaAny → AgdaAny → AgdaAny → AgdaAny 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 #

du_isRing_3440 ∷ T_IsRingWithoutAnnihilatingZero_3308 → T_IsRing_2650 Source #