Safe Haskell	None

MAlonzo.Code.Algebra.Structures.Biased

Documentation

d__DistributesOver__18 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d__DistributesOver'691'__20 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d__DistributesOver'737'__22 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Commutative_38 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftIdentity_70 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_LeftZero_74 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightIdentity_88 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_RightZero_92 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_Zero_96 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () Source #

d_IsAbelianGroup_100 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsCommutativeMonoid_108 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_IsCommutativeSemiring_114 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

d_IsMonoid_130 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_IsNearSemiring_132 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsRing_136 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

d_IsSemigroup_142 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

d_IsSemiringWithoutAnnihilatingZero_146 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

d_IsSemiringWithoutOne_148 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d__'45'__154 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'45'__154 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity'691'_162 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

du_identity'691'_162 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

d_identity'737'_164 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

du_identity'737'_164 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

d_inverse'691'_168 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_168 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_170 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_170 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_172 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_172 :: T_IsAbelianGroup_740 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeMonoid_174 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsCommutativeMonoid_420 Source #

du_isCommutativeMonoid_174 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_176 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_176 :: T_IsAbelianGroup_740 -> T_IsCommutativeSemigroup_282 Source #

d_isInvertibleMagma_182 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsInvertibleMagma_546 Source #

du_isInvertibleMagma_182 :: T_IsAbelianGroup_740 -> T_IsInvertibleMagma_546 Source #

d_isInvertibleUnitalMagma_184 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsInvertibleUnitalMagma_594 Source #

du_isInvertibleUnitalMagma_184 :: T_IsAbelianGroup_740 -> T_IsInvertibleUnitalMagma_594 Source #

d_isPartialEquivalence_190 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_190 :: T_IsAbelianGroup_740 -> T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_194 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_194 :: T_IsAbelianGroup_740 -> T_IsUnitalMagma_326 Source #

d_reflexive_198 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_198 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_200 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_Setoid_44 Source #

du_setoid_200 :: T_IsAbelianGroup_740 -> T_Setoid_44 Source #

d_unique'691''45''8315''185'_206 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'691''45''8315''185'_206 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'737''45''8315''185'_208 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'737''45''8315''185'_208 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_214 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_214 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_216 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_216 :: T_IsAbelianGroup_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity'691'_970 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny Source #

du_identity'691'_970 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny Source #

d_identity'737'_972 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny Source #

du_identity'737'_972 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_978 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_978 :: T_IsMonoid_370 -> T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_982 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_982 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> T_IsUnitalMagma_326 Source #

d_reflexive_986 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_986 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_988 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> T_Setoid_44 Source #

du_setoid_988 :: T_IsMonoid_370 -> T_Setoid_44 Source #

d_'8729''45'cong'691'_996 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_996 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_998 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_998 :: T_IsMonoid_370 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsCommutativeMonoid'737'_1578 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsCommutativeMonoid'737'_1578 Source #

Constructors

C_IsCommutativeMonoid'737''46'constructor_19675 T_IsSemigroup_206 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny)

d_isSemigroup_1590 :: T_IsCommutativeMonoid'737'_1578 -> T_IsSemigroup_206 Source #

d_identity'737'_1592 :: T_IsCommutativeMonoid'737'_1578 -> AgdaAny -> AgdaAny Source #

d_comm_1594 :: T_IsCommutativeMonoid'737'_1578 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMonoid_1596 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid'737'_1578 -> T_IsCommutativeMonoid_420 Source #

du_isCommutativeMonoid_1596 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid'737'_1578 -> T_IsCommutativeMonoid_420 Source #

d_IsCommutativeMonoid'691'_1632 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_IsCommutativeMonoid'691'_1632 Source #

Constructors

C_IsCommutativeMonoid'691''46'constructor_20965 T_IsSemigroup_206 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny)

d_isSemigroup_1644 :: T_IsCommutativeMonoid'691'_1632 -> T_IsSemigroup_206 Source #

d_identity'691'_1646 :: T_IsCommutativeMonoid'691'_1632 -> AgdaAny -> AgdaAny Source #

d_comm_1648 :: T_IsCommutativeMonoid'691'_1632 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isCommutativeMonoid_1650 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid'691'_1632 -> T_IsCommutativeMonoid_420 Source #

du_isCommutativeMonoid_1650 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid'691'_1632 -> T_IsCommutativeMonoid_420 Source #

d_IsSemiringWithoutOne'42'_1688 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsSemiringWithoutOne'42'_1688 Source #

Constructors

C_IsSemiringWithoutOne'42''46'constructor_22269 T_IsCommutativeMonoid_420 T_IsSemigroup_206 T_Σ_14 T_Σ_14

d_'43''45'isCommutativeMonoid_1704 :: T_IsSemiringWithoutOne'42'_1688 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isSemigroup_1706 :: T_IsSemiringWithoutOne'42'_1688 -> T_IsSemigroup_206 Source #

d_distrib_1708 :: T_IsSemiringWithoutOne'42'_1688 -> T_Σ_14 Source #

d_zero_1710 :: T_IsSemiringWithoutOne'42'_1688 -> T_Σ_14 Source #

d_isSemiringWithoutOne_1712 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne'42'_1688 -> T_IsSemiringWithoutOne_906 Source #

du_isSemiringWithoutOne_1712 :: T_IsSemiringWithoutOne'42'_1688 -> T_IsSemiringWithoutOne_906 Source #

d_IsNearSemiring'42'_1750 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_IsNearSemiring'42'_1750 Source #

Constructors

C_IsNearSemiring'42''46'constructor_23859 T_IsMonoid_370 T_IsSemigroup_206 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny)

d_'43''45'isMonoid_1766 :: T_IsNearSemiring'42'_1750 -> T_IsMonoid_370 Source #

d_'42''45'isSemigroup_1768 :: T_IsNearSemiring'42'_1750 -> T_IsSemigroup_206 Source #

d_distrib'691'_1770 :: T_IsNearSemiring'42'_1750 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero'737'_1772 :: T_IsNearSemiring'42'_1750 -> AgdaAny -> AgdaAny Source #

d_isNearSemiring_1774 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring'42'_1750 -> T_IsNearSemiring_826 Source #

du_isNearSemiring_1774 :: T_IsNearSemiring'42'_1750 -> T_IsNearSemiring_826 Source #

d_IsSemiringWithoutAnnihilatingZero'42'_1814 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

data T_IsSemiringWithoutAnnihilatingZero'42'_1814 Source #

Constructors

C_IsSemiringWithoutAnnihilatingZero'42''46'constructor_25457 T_IsCommutativeMonoid_420 T_IsMonoid_370 T_Σ_14

d_'43''45'isCommutativeMonoid_1830 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isMonoid_1832 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_IsMonoid_370 Source #

d_distrib_1834 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_Σ_14 Source #

d_isSemiringWithoutAnnihilatingZero_1836 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

du_isSemiringWithoutAnnihilatingZero_1836 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_IsSemiringWithoutAnnihilatingZero_1034 Source #

d_identity'691'_1848 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> AgdaAny -> AgdaAny Source #

du_identity'691'_1848 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> AgdaAny -> AgdaAny Source #

d_identity'737'_1850 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> AgdaAny -> AgdaAny Source #

du_identity'737'_1850 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_1856 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1856 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_1860 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_1860 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_IsUnitalMagma_326 Source #

d_reflexive_1864 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1864 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1866 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_Setoid_44 Source #

du_setoid_1866 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> T_Setoid_44 Source #

d_'8729''45'cong'691'_1874 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_1874 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_1876 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_1876 :: T_IsSemiringWithoutAnnihilatingZero'42'_1814 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsCommutativeSemiring'737'_1886 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

data T_IsCommutativeSemiring'737'_1886 Source #

Constructors

C_IsCommutativeSemiring'737''46'constructor_27497 T_IsCommutativeMonoid_420 T_IsCommutativeMonoid_420 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny)

d_'43''45'isCommutativeMonoid_1904 :: T_IsCommutativeSemiring'737'_1886 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isCommutativeMonoid_1906 :: T_IsCommutativeSemiring'737'_1886 -> T_IsCommutativeMonoid_420 Source #

d_distrib'691'_1908 :: T_IsCommutativeSemiring'737'_1886 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero'737'_1910 :: T_IsCommutativeSemiring'737'_1886 -> AgdaAny -> AgdaAny Source #

d_isCommutativeSemiring_1912 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring'737'_1886 -> T_IsCommutativeSemiring_1244 Source #

du_isCommutativeSemiring_1912 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiring'737'_1886 -> T_IsCommutativeSemiring_1244 Source #

d_IsCommutativeSemiring'691'_2014 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

data T_IsCommutativeSemiring'691'_2014 Source #

Constructors

C_IsCommutativeSemiring'691''46'constructor_32019 T_IsCommutativeMonoid_420 T_IsCommutativeMonoid_420 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny)

d_'43''45'isCommutativeMonoid_2032 :: T_IsCommutativeSemiring'691'_2014 -> T_IsCommutativeMonoid_420 Source #

d_'42''45'isCommutativeMonoid_2034 :: T_IsCommutativeSemiring'691'_2014 -> T_IsCommutativeMonoid_420 Source #

d_distrib'737'_2036 :: T_IsCommutativeSemiring'691'_2014 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero'691'_2038 :: T_IsCommutativeSemiring'691'_2014 -> AgdaAny -> AgdaAny Source #

d_isCommutativeSemiring_2040 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsCommutativeSemiring'691'_2014 -> T_IsCommutativeSemiring_1244 Source #

du_isCommutativeSemiring_2040 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiring'691'_2014 -> T_IsCommutativeSemiring_1244 Source #

d_IsRingWithoutAnnihilatingZero_2144 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_IsRingWithoutAnnihilatingZero_2144 Source #

Constructors

C_IsRingWithoutAnnihilatingZero'46'constructor_36567 T_IsAbelianGroup_740 T_IsMonoid_370 T_Σ_14

d_'43''45'isAbelianGroup_2162 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsAbelianGroup_740 Source #

d_'42''45'isMonoid_2164 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsMonoid_370 Source #

d_distrib_2166 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_Σ_14 Source #

d__'45'__2170 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'45'__2170 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_2172 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_comm_2174 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_2176 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_Σ_14 Source #

d_identity'691'_2178 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

du_identity'691'_2178 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

d_identity'737'_2180 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

du_identity'737'_2180 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

d_inverse_2182 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_Σ_14 Source #

d_inverse'691'_2184 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_2184 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

d_inverse'737'_2186 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_2186 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

d_isCommutativeMagma_2188 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsCommutativeMagma_134 Source #

du_isCommutativeMagma_2188 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsCommutativeMagma_134 Source #

d_isCommutativeMonoid_2190 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsCommutativeMonoid_420 Source #

du_isCommutativeMonoid_2190 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsCommutativeMonoid_420 Source #

d_isCommutativeSemigroup_2192 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsCommutativeSemigroup_282 Source #

du_isCommutativeSemigroup_2192 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsCommutativeSemigroup_282 Source #

d_isEquivalence_2194 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsEquivalence_26 Source #

d_isGroup_2196 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsGroup_652 Source #

d_isInvertibleMagma_2198 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsInvertibleMagma_546 Source #

du_isInvertibleMagma_2198 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsInvertibleMagma_546 Source #

d_isInvertibleUnitalMagma_2200 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsInvertibleUnitalMagma_594 Source #

du_isInvertibleUnitalMagma_2200 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsInvertibleUnitalMagma_594 Source #

d_isMagma_2202 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsMagma_98 Source #

d_isMonoid_2204 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsMonoid_370 Source #

d_isPartialEquivalence_2206 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2206 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_2208 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_2210 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_2210 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsUnitalMagma_326 Source #

d_refl_2212 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

d_reflexive_2214 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_2214 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_2216 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_Setoid_44 Source #

du_setoid_2216 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_Setoid_44 Source #

d_sym_2218 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_2220 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'691''45''8315''185'_2222 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'691''45''8315''185'_2222 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_unique'737''45''8315''185'_2224 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_unique'737''45''8315''185'_2224 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8315''185''45'cong_2226 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_2228 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_2230 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_2230 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_2232 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_2232 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_assoc_2236 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_identity_2238 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_Σ_14 Source #

d_identity'691'_2240 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

du_identity'691'_2240 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

d_identity'737'_2242 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

du_identity'737'_2242 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

d_isEquivalence_2244 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsEquivalence_26 Source #

d_isMagma_2246 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsMagma_98 Source #

d_isPartialEquivalence_2248 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2248 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsPartialEquivalence_16 Source #

d_isSemigroup_2250 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsSemigroup_206 Source #

d_isUnitalMagma_2252 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_2252 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_IsUnitalMagma_326 Source #

d_refl_2254 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

d_reflexive_2256 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_2256 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_2258 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_Setoid_44 Source #

du_setoid_2258 :: T_IsRingWithoutAnnihilatingZero_2144 -> T_Setoid_44 Source #

d_sym_2260 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_2262 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong_2264 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'691'_2266 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_2266 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_2268 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_2268 :: T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zero'737'_2270 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

du_zero'737'_2270 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

d_zero'691'_2272 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

du_zero'691'_2272 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> AgdaAny -> AgdaAny Source #

d_zero_2274 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_Σ_14 Source #

du_zero_2274 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_Σ_14 Source #

d_isRing_2276 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsRing_1610 Source #

du_isRing_2276 :: (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_IsRingWithoutAnnihilatingZero_2144 -> T_IsRing_1610 Source #

d_IsRing'42'_2288 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_IsRing'42'_2288 Source #

Constructors

C_IsRing'42''46'constructor_44031 T_IsAbelianGroup_740 T_IsMonoid_370 T_Σ_14 T_Σ_14

d_'43''45'isAbelianGroup_2308 :: T_IsRing'42'_2288 -> T_IsAbelianGroup_740 Source #

d_'42''45'isMonoid_2310 :: T_IsRing'42'_2288 -> T_IsMonoid_370 Source #

d_distrib_2312 :: T_IsRing'42'_2288 -> T_Σ_14 Source #

d_zero_2314 :: T_IsRing'42'_2288 -> T_Σ_14 Source #

d_isRing_2316 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing'42'_2288 -> T_IsRing_1610 Source #

du_isRing_2316 :: T_IsRing'42'_2288 -> T_IsRing_1610 Source #

d_identity'691'_2328 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing'42'_2288 -> AgdaAny -> AgdaAny Source #

du_identity'691'_2328 :: T_IsRing'42'_2288 -> AgdaAny -> AgdaAny Source #

d_identity'737'_2330 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing'42'_2288 -> AgdaAny -> AgdaAny Source #

du_identity'737'_2330 :: T_IsRing'42'_2288 -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_2336 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing'42'_2288 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2336 :: T_IsRing'42'_2288 -> T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_2340 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing'42'_2288 -> T_IsUnitalMagma_326 Source #

du_isUnitalMagma_2340 :: T_IsRing'42'_2288 -> T_IsUnitalMagma_326 Source #

d_reflexive_2344 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing'42'_2288 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_2344 :: T_IsRing'42'_2288 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_2346 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing'42'_2288 -> T_Setoid_44 Source #

du_setoid_2346 :: T_IsRing'42'_2288 -> T_Setoid_44 Source #

d_'8729''45'cong'691'_2354 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing'42'_2288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'691'_2354 :: T_IsRing'42'_2288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8729''45'cong'737'_2356 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_IsRing'42'_2288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8729''45'cong'737'_2356 :: T_IsRing'42'_2288 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #