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

d_IsCommutativeSemiring_182 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsMonoid_246 ∷ p → p → p → p → p → p → () Source #

d_IsNearSemiring_254 ∷ p → p → p → p → p → p → p → () Source #

d_IsRing_278 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_IsSemigroup_290 ∷ p → p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_302 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutOne_306 ∷ p → p → p → p → p → p → p → () Source #

d__'47''47'__320 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny Source #

du__'47''47'__320 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_324 ∷ T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity'691'_328 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny Source #

du_identity'691'_328 ∷ T_IsAbelianGroup_1172 → AgdaAny → AgdaAny Source #

d_identity'737'_330 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny Source #

du_identity'737'_330 ∷ T_IsAbelianGroup_1172 → AgdaAny → AgdaAny Source #

d_inverse'691'_334 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny Source #

du_inverse'691'_334 ∷ T_IsAbelianGroup_1172 → AgdaAny → AgdaAny Source #

d_inverse'737'_336 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny Source #

du_inverse'737'_336 ∷ T_IsAbelianGroup_1172 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_338 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_338 ∷ T_IsAbelianGroup_1172 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_340 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → T_IsCommutativeMonoid_764 Source #

du_isCommutativeMonoid_340 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_342 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_342 ∷ T_IsAbelianGroup_1172 → T_IsCommutativeSemigroup_568 Source #

d_isGroup_346 ∷ T_IsAbelianGroup_1172 → T_IsGroup_1074 Source #

d_isInvertibleMagma_348 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → T_IsInvertibleMagma_958 Source #

du_isInvertibleMagma_348 ∷ T_IsAbelianGroup_1172 → T_IsInvertibleMagma_958 Source #

d_isInvertibleUnitalMagma_350 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → T_IsInvertibleUnitalMagma_1012 Source #

du_isInvertibleUnitalMagma_350 ∷ T_IsAbelianGroup_1172 → T_IsInvertibleUnitalMagma_1012 Source #

d_isPartialEquivalence_356 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_356 ∷ T_IsAbelianGroup_1172 → T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_360 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_360 ∷ T_IsAbelianGroup_1172 → T_IsUnitalMagma_666 Source #

d_reflexive_364 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_364 ∷ T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_366 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → T_Setoid_46 Source #

du_setoid_366 ∷ T_IsAbelianGroup_1172 → T_Setoid_46 Source #

d_unique'691''45''8315''185'_372 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_372 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_374 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_374 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_380 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_380 ∷ T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_382 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_382 ∷ T_IsAbelianGroup_1172 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_614 ∷ T_IsCommutativeMonoid_764 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMonoid_630 ∷ T_IsCommutativeMonoid_764 → T_IsMonoid_712 Source #

d_'42''45'comm_814 ∷ T_IsCommutativeSemiring_1750 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSemiring_884 ∷ T_IsCommutativeSemiring_1750 → T_IsSemiring_1640 Source #

d_identity_1696 ∷ T_IsMonoid_712 → T_Σ_14 Source #

d_identity'691'_1698 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → AgdaAny → AgdaAny Source #

du_identity'691'_1698 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → AgdaAny → AgdaAny Source #

d_identity'737'_1700 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → AgdaAny → AgdaAny Source #

du_identity'737'_1700 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_1706 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1706 ∷ T_IsMonoid_712 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1708 ∷ T_IsMonoid_712 → T_IsSemigroup_488 Source #

d_isUnitalMagma_1710 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1710 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → T_IsUnitalMagma_666 Source #

d_reflexive_1714 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1714 ∷ T_IsMonoid_712 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1716 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → T_Setoid_46 Source #

du_setoid_1716 ∷ T_IsMonoid_712 → T_Setoid_46 Source #

d_'8729''45'cong'691'_1724 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_1724 ∷ T_IsMonoid_712 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_1726 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMonoid_712 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_1726 ∷ T_IsMonoid_712 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'assoc_1796 ∷ T_IsNearSemiring_1260 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'cong_1798 ∷ T_IsNearSemiring_1260 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isMonoid_1824 ∷ T_IsNearSemiring_1260 → T_IsMonoid_712 Source #

d_distrib'691'_1830 ∷ T_IsNearSemiring_1260 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'737'_1846 ∷ T_IsNearSemiring_1260 → AgdaAny → AgdaAny Source #

d_'42''45'assoc_2214 ∷ T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'cong_2216 ∷ T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'identity_2222 ∷ T_IsRing_2740 → T_Σ_14 Source #

d_'43''45'isAbelianGroup_2250 ∷ T_IsRing_2740 → T_IsAbelianGroup_1172 Source #

d_distrib_2280 ∷ T_IsRing_2740 → T_Σ_14 Source #

d_assoc_2442 ∷ T_IsSemigroup_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_2446 ∷ T_IsSemigroup_488 → T_IsMagma_178 Source #

d_'42''45'assoc_2582 ∷ T_IsSemiringWithoutAnnihilatingZero_1536 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'cong_2584 ∷ T_IsSemiringWithoutAnnihilatingZero_1536 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'identity_2590 ∷ T_IsSemiringWithoutAnnihilatingZero_1536 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_2620 ∷ T_IsSemiringWithoutAnnihilatingZero_1536 → T_IsCommutativeMonoid_764 Source #

d_distrib_2632 ∷ T_IsSemiringWithoutAnnihilatingZero_1536 → T_Σ_14 Source #

d_'42''45'assoc_2654 ∷ T_IsSemiringWithoutOne_1342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'42''45'cong_2656 ∷ T_IsSemiringWithoutOne_1342 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'43''45'isCommutativeMonoid_2684 ∷ T_IsSemiringWithoutOne_1342 → T_IsCommutativeMonoid_764 Source #

d_distrib_2690 ∷ T_IsSemiringWithoutOne_1342 → T_Σ_14 Source #

d_zero_2712 ∷ T_IsSemiringWithoutOne_1342 → T_Σ_14 Source #

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

data T_IsCommutativeMonoid'737'_2770 Source #

d_isSemigroup_2782 ∷ T_IsCommutativeMonoid'737'_2770 → T_IsSemigroup_488 Source #

d_identity'737'_2784 ∷ T_IsCommutativeMonoid'737'_2770 → AgdaAny → AgdaAny Source #

d_comm_2786 ∷ T_IsCommutativeMonoid'737'_2770 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMonoid_2788 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_2770 → T_IsCommutativeMonoid_764 Source #

du_isCommutativeMonoid_2788 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_2770 → T_IsCommutativeMonoid_764 Source #

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

data T_IsCommutativeMonoid'691'_2826 Source #

d_isSemigroup_2838 ∷ T_IsCommutativeMonoid'691'_2826 → T_IsSemigroup_488 Source #

d_identity'691'_2840 ∷ T_IsCommutativeMonoid'691'_2826 → AgdaAny → AgdaAny Source #

d_comm_2842 ∷ T_IsCommutativeMonoid'691'_2826 → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeMonoid_2844 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_2826 → T_IsCommutativeMonoid_764 Source #

du_isCommutativeMonoid_2844 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_2826 → T_IsCommutativeMonoid_764 Source #

d_IsSemiringWithoutOne'42'_2884 ∷ p → p → p → p → p → p → p → () Source #

data T_IsSemiringWithoutOne'42'_2884 Source #

d_'43''45'isCommutativeMonoid_2900 ∷ T_IsSemiringWithoutOne'42'_2884 → T_IsCommutativeMonoid_764 Source #

d_'42''45'isSemigroup_2902 ∷ T_IsSemiringWithoutOne'42'_2884 → T_IsSemigroup_488 Source #

d_distrib_2904 ∷ T_IsSemiringWithoutOne'42'_2884 → T_Σ_14 Source #

d_zero_2906 ∷ T_IsSemiringWithoutOne'42'_2884 → T_Σ_14 Source #

d_isSemiringWithoutOne_2908 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsSemiringWithoutOne'42'_2884 → T_IsSemiringWithoutOne_1342 Source #

du_isSemiringWithoutOne_2908 ∷ T_IsSemiringWithoutOne'42'_2884 → T_IsSemiringWithoutOne_1342 Source #

d_IsNearSemiring'42'_2948 ∷ p → p → p → p → p → p → p → () Source #

data T_IsNearSemiring'42'_2948 Source #

d_'43''45'isMonoid_2964 ∷ T_IsNearSemiring'42'_2948 → T_IsMonoid_712 Source #

d_'42''45'isSemigroup_2966 ∷ T_IsNearSemiring'42'_2948 → T_IsSemigroup_488 Source #

d_distrib'691'_2968 ∷ T_IsNearSemiring'42'_2948 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'737'_2970 ∷ T_IsNearSemiring'42'_2948 → AgdaAny → AgdaAny Source #

d_isNearSemiring_2972 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsNearSemiring'42'_2948 → T_IsNearSemiring_1260 Source #

du_isNearSemiring_2972 ∷ T_IsNearSemiring'42'_2948 → T_IsNearSemiring_1260 Source #

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

data T_IsSemiringWithoutAnnihilatingZero'42'_3014 Source #

d_'43''45'isCommutativeMonoid_3030 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_IsCommutativeMonoid_764 Source #

d_'42''45'isMonoid_3032 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_IsMonoid_712 Source #

d_distrib_3034 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_Σ_14 Source #

d_isSemiringWithoutAnnihilatingZero_3036 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

du_isSemiringWithoutAnnihilatingZero_3036 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

d_identity'691'_3048 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_3014 → AgdaAny → AgdaAny Source #

du_identity'691'_3048 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → AgdaAny → AgdaAny Source #

d_identity'737'_3050 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_3014 → AgdaAny → AgdaAny Source #

du_identity'737'_3050 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_3056 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3056 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_3060 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_3060 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_IsUnitalMagma_666 Source #

d_reflexive_3064 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_3014 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3064 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_3066 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_Setoid_46 Source #

du_setoid_3066 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → T_Setoid_46 Source #

d_'8729''45'cong'691'_3074 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_3014 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_3074 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_3076 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiringWithoutAnnihilatingZero'42'_3014 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_3076 ∷ T_IsSemiringWithoutAnnihilatingZero'42'_3014 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

data T_IsCommutativeSemiring'737'_3088 Source #

d_'43''45'isCommutativeMonoid_3106 ∷ T_IsCommutativeSemiring'737'_3088 → T_IsCommutativeMonoid_764 Source #

d_'42''45'isCommutativeMonoid_3108 ∷ T_IsCommutativeSemiring'737'_3088 → T_IsCommutativeMonoid_764 Source #

d_distrib'691'_3110 ∷ T_IsCommutativeSemiring'737'_3088 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'737'_3112 ∷ T_IsCommutativeSemiring'737'_3088 → AgdaAny → AgdaAny Source #

d_isCommutativeSemiring_3114 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_3088 → T_IsCommutativeSemiring_1750 Source #

du_isCommutativeSemiring_3114 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'737'_3088 → T_IsCommutativeSemiring_1750 Source #

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

data T_IsCommutativeSemiring'691'_3218 Source #

d_'43''45'isCommutativeMonoid_3236 ∷ T_IsCommutativeSemiring'691'_3218 → T_IsCommutativeMonoid_764 Source #

d_'42''45'isCommutativeMonoid_3238 ∷ T_IsCommutativeSemiring'691'_3218 → T_IsCommutativeMonoid_764 Source #

d_distrib'737'_3240 ∷ T_IsCommutativeSemiring'691'_3218 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'691'_3242 ∷ T_IsCommutativeSemiring'691'_3218 → AgdaAny → AgdaAny Source #

d_isCommutativeSemiring_3244 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_3218 → T_IsCommutativeSemiring_1750 Source #

du_isCommutativeSemiring_3244 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'691'_3218 → T_IsCommutativeSemiring_1750 Source #

d_IsRing'42'_3350 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsRing'42'_3350 Source #

d_'43''45'isAbelianGroup_3370 ∷ T_IsRing'42'_3350 → T_IsAbelianGroup_1172 Source #

d_'42''45'isMonoid_3372 ∷ T_IsRing'42'_3350 → T_IsMonoid_712 Source #

d_distrib_3374 ∷ T_IsRing'42'_3350 → T_Σ_14 Source #

d_zero_3376 ∷ T_IsRing'42'_3350 → T_Σ_14 Source #

d_isRing_3378 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3350 → T_IsRing_2740 Source #

du_isRing_3378 ∷ T_IsRing'42'_3350 → T_IsRing_2740 Source #

d_identity'691'_3390 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3350 → AgdaAny → AgdaAny Source #

du_identity'691'_3390 ∷ T_IsRing'42'_3350 → AgdaAny → AgdaAny Source #

d_identity'737'_3392 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3350 → AgdaAny → AgdaAny Source #

du_identity'737'_3392 ∷ T_IsRing'42'_3350 → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_3398 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3350 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3398 ∷ T_IsRing'42'_3350 → T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_3402 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3350 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_3402 ∷ T_IsRing'42'_3350 → T_IsUnitalMagma_666 Source #

d_reflexive_3406 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3350 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3406 ∷ T_IsRing'42'_3350 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_3408 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3350 → T_Setoid_46 Source #

du_setoid_3408 ∷ T_IsRing'42'_3350 → T_Setoid_46 Source #

d_'8729''45'cong'691'_3416 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3350 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_3416 ∷ T_IsRing'42'_3350 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_3418 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing'42'_3350 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_3418 ∷ T_IsRing'42'_3350 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsRingWithoutAnnihilatingZero_3432 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsRingWithoutAnnihilatingZero_3432 Source #

d_'43''45'isAbelianGroup_3450 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsAbelianGroup_1172 Source #

d_'42''45'isMonoid_3452 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsMonoid_712 Source #

d_distrib_3454 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_Σ_14 Source #

d__'47''47'__3458 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny Source #

du__'47''47'__3458 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_3460 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_3462 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_3464 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_Σ_14 Source #

d_identity'691'_3466 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

du_identity'691'_3466 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

d_identity'737'_3468 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

du_identity'737'_3468 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

d_inverse_3470 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_Σ_14 Source #

d_inverse'691'_3472 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

du_inverse'691'_3472 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

d_inverse'737'_3474 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

du_inverse'737'_3474 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

d_isCommutativeMagma_3476 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_3476 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_3478 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_IsCommutativeMonoid_764 Source #

du_isCommutativeMonoid_3478 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_3480 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_3480 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_3482 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsEquivalence_28 Source #

d_isGroup_3484 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsGroup_1074 Source #

d_isInvertibleMagma_3486 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_IsInvertibleMagma_958 Source #

du_isInvertibleMagma_3486 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsInvertibleMagma_958 Source #

d_isInvertibleUnitalMagma_3488 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_IsInvertibleUnitalMagma_1012 Source #

du_isInvertibleUnitalMagma_3488 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsInvertibleUnitalMagma_1012 Source #

d_isMagma_3490 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsMagma_178 Source #

d_isMonoid_3492 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsMonoid_712 Source #

d_isPartialEquivalence_3494 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3494 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_3496 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsSemigroup_488 Source #

d_isUnitalMagma_3498 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_3498 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsUnitalMagma_666 Source #

d_refl_3500 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

d_reflexive_3502 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3502 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_3504 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_Setoid_46 Source #

du_setoid_3504 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_Setoid_46 Source #

d_sym_3506 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3508 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'691''45''8315''185'_3510 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'691''45''8315''185'_3510 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_unique'737''45''8315''185'_3512 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_unique'737''45''8315''185'_3512 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8315''185''45'cong_3514 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_3516 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_3518 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_3518 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_3520 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_3520 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_3524 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_3526 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_Σ_14 Source #

d_identity'691'_3528 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

du_identity'691'_3528 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

d_identity'737'_3530 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

du_identity'737'_3530 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

d_isEquivalence_3532 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsEquivalence_28 Source #

d_isMagma_3534 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsMagma_178 Source #

d_isPartialEquivalence_3536 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_3536 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_3538 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsSemigroup_488 Source #

d_isUnitalMagma_3540 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_3540 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsUnitalMagma_666 Source #

d_refl_3542 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

d_reflexive_3544 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_3544 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_3546 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_Setoid_46 Source #

du_setoid_3546 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_Setoid_46 Source #

d_sym_3548 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3550 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_3552 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_3554 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_3554 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_3556 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_3556 ∷ T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero'737'_3558 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

du_zero'737'_3558 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

d_zero'691'_3560 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

du_zero'691'_3560 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → AgdaAny → AgdaAny Source #

d_zero_3562 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_Σ_14 Source #

du_zero_3562 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_Σ_14 Source #

d_isRing_3564 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_3432 → T_IsRing_2740 Source #

du_isRing_3564 ∷ T_IsRingWithoutAnnihilatingZero_3432 → T_IsRing_2740 Source #