plutus-metatheory-0.1.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

MAlonzo.Code.Algebra.Structures

Documentation

d__DistributesOver__16T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d__DistributesOver'691'__18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d__DistributesOver'737'__20T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_AlmostLeftCancellative_30T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_AlmostRightCancellative_32T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Alternative_34T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Associative_36T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Commutative_40T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Congruent'8321'_42T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny) → () Source #

d_Congruent'8322'_44T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Flexible_48T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Idempotent_50T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Identical_54T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Identity_56T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Inverse_60T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftAlternative_66T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftBol_68T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftCongruent_72T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftDivides_76T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftDivides'691'_78T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftDivides'737'_80T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftIdentity_82T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftInverse_84T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftSemimedial_88T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftZero_90T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Medial_92T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_MiddleBol_94T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightAlternative_96T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightBol_98T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightCongruent_102T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightDivides_106T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightDivides'691'_108T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightDivides'737'_110T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightIdentity_112T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightInverse_114T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightSemimedial_118T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightZero_120T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Selective_122T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Semimedial_126T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_StarDestructive_128T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → () Source #

d_StarExpansive_130T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → () Source #

d_StarLeftDestructive_132T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → () Source #

d_StarLeftExpansive_134T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → () Source #

d_StarRightDestructive_136T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → () Source #

d_StarRightExpansive_138T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → () Source #

d_Zero_140T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_IsSuccessorSet_146 ∷ p → p → p → p → p → p → () Source #

d_IsMagma_176 ∷ p → p → p → p → p → () Source #

d_IsCommutativeMagma_212 ∷ p → p → p → p → p → () Source #

d_IsIdempotentMagma_248 ∷ p → p → p → p → p → () Source #

d_IsAlternativeMagma_284 ∷ p → p → p → p → p → () Source #

d_IsFlexibleMagma_324 ∷ p → p → p → p → p → () Source #

d_IsMedialMagma_360 ∷ p → p → p → p → p → () Source #

d_IsSemimedialMagma_396 ∷ p → p → p → p → p → () Source #

d_IsSelectiveMagma_436 ∷ p → p → p → p → p → () Source #

d_IsSemigroup_472 ∷ p → p → p → p → p → () Source #

d_IsBand_508 ∷ p → p → p → p → p → () Source #

d_setoid_534T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → T_IsBand_508T_Setoid_44 Source #

d_IsCommutativeSemigroup_548 ∷ p → p → p → p → p → () Source #

d_IsCommutativeBand_590 ∷ p → p → p → p → p → () Source #

d_IsUnitalMagma_642 ∷ p → p → p → p → p → p → () Source #

d_IsMonoid_686 ∷ p → p → p → p → p → p → () Source #

d_IsCommutativeMonoid_736 ∷ p → p → p → p → p → p → () Source #

d_IsIdempotentMonoid_796 ∷ p → p → p → p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_852 ∷ p → p → p → p → p → p → () Source #

d_IsInvertibleMagma_924 ∷ p → p → p → p → p → p → p → () Source #

d_IsInvertibleUnitalMagma_976 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroup_1036 ∷ p → p → p → p → p → p → p → () Source #

d_setoid_1080T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1036T_Setoid_44 Source #

d__'92''92'__1092T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1036AgdaAnyAgdaAnyAgdaAny Source #

d__'47''47'__1098T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1036AgdaAnyAgdaAnyAgdaAny Source #

d__'45'__1104T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1036AgdaAnyAgdaAnyAgdaAny Source #

d_inverse'737'_1106T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1036AgdaAnyAgdaAny Source #

d_inverse'691'_1108T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1036AgdaAnyAgdaAny Source #

d_IsAbelianGroup_1132 ∷ p → p → p → p → p → p → p → () Source #

d_IsNearSemiring_1218 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutOne_1298 ∷ p → p → p → p → p → p → p → () Source #

d__'8776'__1340T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsSemiringWithoutOne_1298AgdaAnyAgdaAny → () Source #

d__'8777'__1342T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsSemiringWithoutOne_1298AgdaAnyAgdaAny → () Source #

d_Carrier_1344T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsSemiringWithoutOne_1298 → () Source #

d_IsCommutativeSemiringWithoutOne_1382 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_1468 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSemiring_1570 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_1654T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsSemiring_1570T_Setoid_44 Source #

d_zero'691'_1666T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsSemiring_1570AgdaAnyAgdaAny Source #

d_zero'737'_1668T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsSemiring_1570AgdaAnyAgdaAny Source #

d_IsCommutativeSemiring_1678 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsCancellativeCommutativeSemiring_1798 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsIdempotentSemiring_1922 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsKleeneAlgebra_2044 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_zero'691'_2160T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsKleeneAlgebra_2044AgdaAnyAgdaAny Source #

d_zero'737'_2162T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsKleeneAlgebra_2044AgdaAnyAgdaAny Source #

d_IsQuasiring_2180 ∷ p → p → p → p → p → p → p → p → () Source #

d_zero'737'_2254T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsQuasiring_2180AgdaAnyAgdaAny Source #

d_zero'691'_2256T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsQuasiring_2180AgdaAnyAgdaAny Source #

d_IsRingWithoutOne_2286 ∷ p → p → p → p → p → p → p → p → () Source #

d_zero_2386T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyT_IsRingWithoutOne_2286T_Σ_14 Source #

d_IsNonAssociativeRing_2408 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_IsNearring_2538 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_identity'691'_2574T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAny Source #

d_identity'737'_2576T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAny Source #

d_identity'691'_2594T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAny Source #

d_identity'737'_2596T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAny Source #

d_distrib'691'_2608T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_distrib'737'_2610T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_identity'691'_2612T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAny Source #

d_identity'737'_2614T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAny Source #

d_reflexive_2622T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_setoid_2624T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538T_Setoid_44 Source #

d_zero'691'_2632T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAny Source #

d_zero'737'_2634T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2538AgdaAnyAgdaAny Source #

d_IsRing_2650 ∷ p → p → p → p → p → p → p → p → p → () Source #

d__'47''47'__2686T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'691'_2688T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'737'_2690T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_assoc_2696T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_comm_2698T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong_2700T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'691'_2702T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'737'_2704T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_identity_2706T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650T_Σ_14 Source #

d_identity'691'_2708T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAny Source #

d_identity'737'_2710T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAny Source #

d_isGroup_2718T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650T_IsGroup_1036 Source #

d_isMagma_2724T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650T_IsMagma_176 Source #

d_isMonoid_2726T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650T_IsMonoid_686 Source #

d_'8315''185''45'cong_2732T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_inverse_2734T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650T_Σ_14 Source #

d_inverse'691'_2736T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAny Source #

d_inverse'737'_2738T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAny Source #

d_distrib'691'_2740T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_distrib'737'_2742T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_refl_2748T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAny Source #

d_reflexive_2750T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_setoid_2752T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650T_Setoid_44 Source #

d_sym_2754T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_trans_2756T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_zero_2762T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650T_Σ_14 Source #

d_zero'691'_2764T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAny Source #

d_zero'737'_2766T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAny Source #

d_identity'691'_2772T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAny Source #

d_identity'737'_2774T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2650AgdaAnyAgdaAny Source #

d_IsCommutativeRing_2796 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_assoc_2840T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2796AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_comm_2842T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2796AgdaAnyAgdaAnyAgdaAny Source #

d_inverse_2880T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2796T_Σ_14 Source #

d_refl_2906T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2796AgdaAnyAgdaAny Source #

d_sym_2912T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2796AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_trans_2914T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2796AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_zero_2920T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2796T_Σ_14 Source #

d_IsQuasigroup_2944 ∷ p → p → p → p → p → p → p → () Source #

d_setoid_2982T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsQuasigroup_2944T_Setoid_44 Source #

d_IsLoop_3026 ∷ p → p → p → p → p → p → p → p → () Source #

d_leftDivides'691'_3066T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3026AgdaAnyAgdaAnyAgdaAny Source #

d_leftDivides'737'_3068T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3026AgdaAnyAgdaAnyAgdaAny Source #

d_reflexive_3072T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3026AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_rightDivides'691'_3076T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3026AgdaAnyAgdaAnyAgdaAny Source #

d_rightDivides'737'_3078T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3026AgdaAnyAgdaAnyAgdaAny Source #

d_setoid_3080T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3026T_Setoid_44 Source #

d_'8729''45'cong'691'_3088T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3026AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'737'_3090T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3026AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_identity'737'_3092T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3026AgdaAnyAgdaAny Source #

d_identity'691'_3094T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3026AgdaAnyAgdaAny Source #

d_IsLeftBolLoop_3104 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_3166T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLeftBolLoop_3104T_Setoid_44 Source #

d_IsRightBolLoop_3186 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_3248T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsRightBolLoop_3186T_Setoid_44 Source #

d_IsMoufangLoop_3268 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_3338T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsMoufangLoop_3268T_Setoid_44 Source #

d_IsMiddleBolLoop_3358 ∷ p → p → p → p → p → p → p → p → () Source #