| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp
Documentation
d__'8776'__24 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → () Source #
d__'8818'__28 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → () Source #
d__'8851'__98 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
d__Absorbs__114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver__116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver'691'__118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver'737'__120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Absorptive_126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_mono'45''8804''45'distrib'45''8851'_3070 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_mono'45''8804''45'distrib'45''8851'_3070 ∷ T_TotalPreorder_240 → T_MinOperator_106 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'x'8851'z'8804'y_3072 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'x'8851'z'8804'y_3072 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'z'8851'x'8804'y_3074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'z'8851'x'8804'y_3074 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'y_3076 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'y_3076 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'z_3078 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'z_3078 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'x'8658'x'8804'y_3080 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'x'8658'x'8804'y_3080 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'y'8658'y'8804'x_3082 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'y'8658'y'8804'x_3082 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'x_3084 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'x_3084 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'y_3086 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'y_3086 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'assoc_3088 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'assoc_3088 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'band_3090 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Band_620 Source #
d_'8851''45'comm_3092 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'comm_3092 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'commutativeSemigroup_3094 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_CommutativeSemigroup_688 Source #
du_'8851''45'commutativeSemigroup_3094 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_CommutativeSemigroup_688 Source #
d_'8851''45'cong_3096 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong_3096 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'691'_3098 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'691'_3098 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'737'_3100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'737'_3100 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'glb_3102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'glb_3102 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'idem_3104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny Source #
d_'8851''45'identity_3106 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'identity'691'_3108 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'691'_3108 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity'737'_3110 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'737'_3110 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'isBand_3112 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsBand_526 Source #
d_'8851''45'isCommutativeSemigroup_3114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsCommutativeSemigroup_568 Source #
du_'8851''45'isCommutativeSemigroup_3114 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_IsCommutativeSemigroup_568 Source #
d_'8851''45'isMagma_3116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsMagma_178 Source #
d_'8851''45'isMonoid_3118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_712 Source #
du_'8851''45'isMonoid_3118 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_712 Source #
d_'8851''45'isSelectiveMagma_3120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsSelectiveMagma_450 Source #
du_'8851''45'isSelectiveMagma_3120 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_IsSelectiveMagma_450 Source #
d_'8851''45'isSemigroup_3122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsSemigroup_488 Source #
du_'8851''45'isSemigroup_3122 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_IsSemigroup_488 Source #
d_'8851''45'magma_3124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Magma_74 Source #
d_'8851''45'mono'45''8804'_3126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'45''8804'_3126 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'monoid_3128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_914 Source #
du_'8851''45'monoid_3128 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_914 Source #
d_'8851''45'mono'691''45''8804'_3130 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'691''45''8804'_3130 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'737''45''8804'_3132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'737''45''8804'_3132 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'rawMagma_3134 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_RawMagma_44 Source #
d_'8851''45'sel_3136 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_'8851''45'sel_3136 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_'8851''45'selectiveMagma_3138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_SelectiveMagma_130 Source #
du_'8851''45'selectiveMagma_3138 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_SelectiveMagma_130 Source #
d_'8851''45'semigroup_3140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Semigroup_558 Source #
d_'8851''45'triangulate_3142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'triangulate_3142 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'zero_3144 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8851''45'zero_3144 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'zero'691'_3146 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'691'_3146 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero'737'_3148 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'737'_3148 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_mono'45''8804''45'distrib'45''8852'_3152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_mono'45''8804''45'distrib'45''8852'_3152 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'x_3154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'x_3154 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'x'8851'z'8804'y_3156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'x'8851'z'8804'y_3156 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'z'8851'x'8804'y_3158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'z'8851'x'8804'y_3158 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'y_3160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'y_3160 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'x'8658'x'8804'y_3162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'x'8658'x'8804'y_3162 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'y'8658'y'8804'x_3164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'y'8658'y'8804'x_3164 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'y_3166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'y_3166 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'z_3168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'z_3168 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'assoc_3170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'assoc_3170 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'band_3172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Band_620 Source #
d_'8851''45'comm_3174 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'comm_3174 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'commutativeSemigroup_3176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_CommutativeSemigroup_688 Source #
du_'8851''45'commutativeSemigroup_3176 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_CommutativeSemigroup_688 Source #
d_'8851''45'cong_3178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong_3178 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'691'_3180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'691'_3180 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'737'_3182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'737'_3182 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'idem_3184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny Source #
d_'8851''45'identity_3186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'identity'691'_3188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'691'_3188 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity'737'_3190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'737'_3190 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'isBand_3192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsBand_526 Source #
d_'8851''45'isCommutativeSemigroup_3194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsCommutativeSemigroup_568 Source #
du_'8851''45'isCommutativeSemigroup_3194 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_IsCommutativeSemigroup_568 Source #
d_'8851''45'isMagma_3196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsMagma_178 Source #
d_'8851''45'isMonoid_3198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_712 Source #
du_'8851''45'isMonoid_3198 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_712 Source #
d_'8851''45'isSelectiveMagma_3200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsSelectiveMagma_450 Source #
du_'8851''45'isSelectiveMagma_3200 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_IsSelectiveMagma_450 Source #
d_'8851''45'isSemigroup_3202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsSemigroup_488 Source #
du_'8851''45'isSemigroup_3202 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_IsSemigroup_488 Source #
d_'8851''45'glb_3204 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'glb_3204 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'magma_3206 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Magma_74 Source #
d_'8851''45'mono'45''8804'_3208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'45''8804'_3208 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'monoid_3210 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_914 Source #
du_'8851''45'monoid_3210 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_914 Source #
d_'8851''45'mono'691''45''8804'_3212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'691''45''8804'_3212 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'737''45''8804'_3214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'737''45''8804'_3214 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'sel_3216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_'8851''45'sel_3216 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_'8851''45'selectiveMagma_3218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_SelectiveMagma_130 Source #
du_'8851''45'selectiveMagma_3218 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_SelectiveMagma_130 Source #
d_'8851''45'semigroup_3220 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Semigroup_558 Source #
d_'8851''45'triangulate_3222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'triangulate_3222 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'zero_3224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8851''45'zero_3224 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'zero'691'_3226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'691'_3226 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero'737'_3228 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'737'_3228 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'distrib'737''45''8852'_3230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'distrib'737''45''8852'_3230 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'distrib'691''45''8852'_3258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'distrib'691''45''8852'_3258 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'distrib'45''8852'_3260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Σ_14 Source #
du_'8851''45'distrib'45''8852'_3260 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Σ_14 Source #
d_'8852''45'distrib'737''45''8851'_3262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8852''45'distrib'737''45''8851'_3262 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45'distrib'691''45''8851'_3290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8852''45'distrib'691''45''8851'_3290 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45'distrib'45''8851'_3292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Σ_14 Source #
du_'8852''45'distrib'45''8851'_3292 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Σ_14 Source #
d_'8851''45'absorbs'45''8852'_3294 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'absorbs'45''8852'_3294 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45'absorbs'45''8851'_3316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8852''45'absorbs'45''8851'_3316 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45''8851''45'absorptive_3338 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Σ_14 Source #
du_'8852''45''8851''45'absorptive_3338 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Σ_14 Source #
d_'8851''45''8852''45'absorptive_3340 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Σ_14 Source #
du_'8851''45''8852''45'absorptive_3340 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Σ_14 Source #
d__'8805'__3342 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → () Source #
d_antimono'45''8804''45'distrib'45''8851'_3350 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_antimono'45''8804''45'distrib'45''8851'_3350 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_antimono'45''8804''45'distrib'45''8852'_3396 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_antimono'45''8804''45'distrib'45''8852'_3396 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #