plutus-metatheory-1.61.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_178 ∷ p → p → p → p → p → () Source #

d_IsCommutativeMagma_214 ∷ p → p → p → p → p → () Source #

d_IsIdempotentMagma_252 ∷ p → p → p → p → p → () Source #

d_IsAlternativeMagma_290 ∷ p → p → p → p → p → () Source #

d_IsFlexibleMagma_332 ∷ p → p → p → p → p → () Source #

d_IsMedialMagma_370 ∷ p → p → p → p → p → () Source #

d_IsSemimedialMagma_408 ∷ p → p → p → p → p → () Source #

d_IsSelectiveMagma_450 ∷ p → p → p → p → p → () Source #

d_IsSemigroup_488 ∷ p → p → p → p → p → () Source #

d_IsBand_526 ∷ p → p → p → p → p → () Source #

d_setoid_552T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → T_IsBand_526T_Setoid_46 Source #

d_IsCommutativeSemigroup_568 ∷ p → p → p → p → p → () Source #

d_IsCommutativeBand_612 ∷ p → p → p → p → p → () Source #

d_IsUnitalMagma_666 ∷ p → p → p → p → p → p → () Source #

d_IsMonoid_712 ∷ p → p → p → p → p → p → () Source #

d_IsCommutativeMonoid_764 ∷ p → p → p → p → p → p → () Source #

d_IsIdempotentMonoid_826 ∷ p → p → p → p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_884 ∷ p → p → p → p → p → p → () Source #

d_IsInvertibleMagma_958 ∷ p → p → p → p → p → p → p → () Source #

d_IsInvertibleUnitalMagma_1012 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroup_1074 ∷ p → p → p → p → p → p → p → () Source #

d_setoid_1118T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1074T_Setoid_46 Source #

d__'92''92'__1130T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1074AgdaAnyAgdaAnyAgdaAny Source #

d__'47''47'__1136T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1074AgdaAnyAgdaAnyAgdaAny Source #

d__'45'__1142T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1074AgdaAnyAgdaAnyAgdaAny Source #

d_inverse'737'_1144T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1074AgdaAnyAgdaAny Source #

d_inverse'691'_1146T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_1074AgdaAnyAgdaAny Source #

d_IsAbelianGroup_1172 ∷ p → p → p → p → p → p → p → () Source #

d_IsNearSemiring_1260 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutOne_1342 ∷ p → p → p → p → p → p → p → () Source #

d_IsCommutativeSemiringWithoutOne_1438 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_1536 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSemiring_1640 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_1724T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsSemiring_1640T_Setoid_46 Source #

d_zero'691'_1736T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsSemiring_1640AgdaAnyAgdaAny Source #

d_zero'737'_1738T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsSemiring_1640AgdaAnyAgdaAny Source #

d_IsCommutativeSemiring_1750 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsCancellativeCommutativeSemiring_1872 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsIdempotentSemiring_1998 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsKleeneAlgebra_2122 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_zero'691'_2238T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsKleeneAlgebra_2122AgdaAnyAgdaAny Source #

d_zero'737'_2240T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsKleeneAlgebra_2122AgdaAnyAgdaAny Source #

d_IsQuasiring_2260 ∷ p → p → p → p → p → p → p → p → () Source #

d_zero'737'_2334T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsQuasiring_2260AgdaAnyAgdaAny Source #

d_zero'691'_2336T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsQuasiring_2260AgdaAnyAgdaAny Source #

d_IsRingWithoutOne_2368 ∷ p → p → p → p → p → p → p → p → () Source #

d_zero_2468T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyT_IsRingWithoutOne_2368T_Σ_14 Source #

d_IsNonAssociativeRing_2494 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_IsNearring_2626 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_identity'691'_2662T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAny Source #

d_identity'737'_2664T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAny Source #

d_identity'691'_2682T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAny Source #

d_identity'737'_2684T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAny Source #

d_distrib'691'_2696T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_distrib'737'_2698T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_identity'691'_2700T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAny Source #

d_identity'737'_2702T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAny Source #

d_reflexive_2710T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_setoid_2712T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626T_Setoid_46 Source #

d_zero'691'_2720T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAny Source #

d_zero'737'_2722T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAny → (AgdaAnyAgdaAny) → T_IsNearring_2626AgdaAnyAgdaAny Source #

d_IsRing_2740 ∷ p → p → p → p → p → p → p → p → p → () Source #

d__'47''47'__2776T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'691'_2778T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'737'_2780T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_assoc_2786T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_comm_2788T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong_2790T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'691'_2792T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'737'_2794T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_identity_2796T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740T_Σ_14 Source #

d_identity'691'_2798T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAny Source #

d_identity'737'_2800T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAny Source #

d_isGroup_2808T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740T_IsGroup_1074 Source #

d_isMagma_2814T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740T_IsMagma_178 Source #

d_isMonoid_2816T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740T_IsMonoid_712 Source #

d_'8315''185''45'cong_2822T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_inverse_2824T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740T_Σ_14 Source #

d_inverse'691'_2826T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAny Source #

d_inverse'737'_2828T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAny Source #

d_distrib'691'_2830T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_distrib'737'_2832T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_refl_2840T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAny Source #

d_reflexive_2842T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_setoid_2844T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740T_Setoid_46 Source #

d_sym_2846T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_trans_2848T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_zero_2854T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740T_Σ_14 Source #

d_zero'691'_2856T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAny Source #

d_zero'737'_2858T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAny Source #

d_identity'691'_2864T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAny Source #

d_identity'737'_2866T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_2740AgdaAnyAgdaAny Source #

d_IsCommutativeRing_2888 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_assoc_2932T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2888AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_comm_2934T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2888AgdaAnyAgdaAnyAgdaAny Source #

d_inverse_2972T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2888T_Σ_14 Source #

d_refl_2998T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2888AgdaAnyAgdaAny Source #

d_sym_3004T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2888AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_trans_3006T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2888AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_zero_3012T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_2888T_Σ_14 Source #

d_IsQuasigroup_3038 ∷ p → p → p → p → p → p → p → () Source #

d_setoid_3076T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → T_IsQuasigroup_3038T_Setoid_46 Source #

d_IsLoop_3122 ∷ p → p → p → p → p → p → p → p → () Source #

d_leftDivides'691'_3162T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3122AgdaAnyAgdaAnyAgdaAny Source #

d_leftDivides'737'_3164T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3122AgdaAnyAgdaAnyAgdaAny Source #

d_reflexive_3168T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3122AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_rightDivides'691'_3172T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3122AgdaAnyAgdaAnyAgdaAny Source #

d_rightDivides'737'_3174T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3122AgdaAnyAgdaAnyAgdaAny Source #

d_setoid_3176T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3122T_Setoid_46 Source #

d_'8729''45'cong'691'_3184T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3122AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'737'_3186T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3122AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_identity'737'_3188T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3122AgdaAnyAgdaAny Source #

d_identity'691'_3190T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLoop_3122AgdaAnyAgdaAny Source #

d_IsLeftBolLoop_3202 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_3264T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsLeftBolLoop_3202T_Setoid_46 Source #

d_IsRightBolLoop_3286 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_3348T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsRightBolLoop_3286T_Setoid_46 Source #

d_IsMoufangLoop_3370 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_3440T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyT_IsMoufangLoop_3370T_Setoid_46 Source #

d_IsMiddleBolLoop_3462 ∷ p → p → p → p → p → p → p → p → () Source #