| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp
Documentation
d__'8776'__24 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → () Source #
d__'8818'__26 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → () Source #
d__'8851'__90 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
d__Absorbs__106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver__108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver'691'__110 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver'737'__112 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Absorptive_118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_mono'45''8804''45'distrib'45''8851'_2948 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_mono'45''8804''45'distrib'45''8851'_2948 ∷ T_TotalPreorder_222 → T_MinOperator_98 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'x'8851'z'8804'y_2950 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'x'8851'z'8804'y_2950 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'z'8851'x'8804'y_2952 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'z'8851'x'8804'y_2952 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'y_2954 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'y_2954 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'z_2956 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'z_2956 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'x'8658'x'8804'y_2958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'x'8658'x'8804'y_2958 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'y'8658'y'8804'x_2960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'y'8658'y'8804'x_2960 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'x_2962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'x_2962 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'y_2964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'y_2964 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'assoc_2966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'assoc_2966 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'band_2968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Band_596 Source #
d_'8851''45'comm_2970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'comm_2970 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'commutativeSemigroup_2972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_CommutativeSemigroup_662 Source #
du_'8851''45'commutativeSemigroup_2972 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_CommutativeSemigroup_662 Source #
d_'8851''45'cong_2974 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong_2974 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'691'_2976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'691'_2976 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'737'_2978 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'737'_2978 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'glb_2980 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'glb_2980 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'idem_2982 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny Source #
d_'8851''45'identity_2984 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8851''45'identity_2984 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'identity'691'_2986 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'691'_2986 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity'737'_2988 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'737'_2988 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'isBand_2990 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsBand_508 Source #
d_'8851''45'isCommutativeSemigroup_2992 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsCommutativeSemigroup_548 Source #
du_'8851''45'isCommutativeSemigroup_2992 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_IsCommutativeSemigroup_548 Source #
d_'8851''45'isMagma_2994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsMagma_176 Source #
d_'8851''45'isMonoid_2996 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_686 Source #
du_'8851''45'isMonoid_2996 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_686 Source #
d_'8851''45'isSelectiveMagma_2998 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsSelectiveMagma_436 Source #
du_'8851''45'isSelectiveMagma_2998 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_IsSelectiveMagma_436 Source #
d_'8851''45'isSemigroup_3000 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsSemigroup_472 Source #
d_'8851''45'magma_3002 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Magma_68 Source #
d_'8851''45'mono'45''8804'_3004 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'45''8804'_3004 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'monoid_3006 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_882 Source #
du_'8851''45'monoid_3006 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_882 Source #
d_'8851''45'mono'691''45''8804'_3008 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'691''45''8804'_3008 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'737''45''8804'_3010 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'737''45''8804'_3010 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'rawMagma_3012 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_RawMagma_36 Source #
d_'8851''45'sel_3014 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_'8851''45'sel_3014 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_'8851''45'selectiveMagma_3016 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_SelectiveMagma_122 Source #
du_'8851''45'selectiveMagma_3016 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_SelectiveMagma_122 Source #
d_'8851''45'semigroup_3018 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Semigroup_536 Source #
d_'8851''45'triangulate_3020 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'triangulate_3020 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'zero_3022 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8851''45'zero_3022 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'zero'691'_3024 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'691'_3024 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero'737'_3026 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'737'_3026 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_mono'45''8804''45'distrib'45''8852'_3030 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_mono'45''8804''45'distrib'45''8852'_3030 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'x_3032 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'x_3032 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'x'8851'z'8804'y_3034 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'x'8851'z'8804'y_3034 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'z'8851'x'8804'y_3036 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'z'8851'x'8804'y_3036 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'y_3038 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'y_3038 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'x'8658'x'8804'y_3040 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'x'8658'x'8804'y_3040 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'y'8658'y'8804'x_3042 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'y'8658'y'8804'x_3042 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'y_3044 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'y_3044 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'z_3046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'z_3046 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'assoc_3048 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'assoc_3048 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'band_3050 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Band_596 Source #
d_'8851''45'comm_3052 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'comm_3052 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'commutativeSemigroup_3054 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_CommutativeSemigroup_662 Source #
du_'8851''45'commutativeSemigroup_3054 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → T_CommutativeSemigroup_662 Source #
d_'8851''45'cong_3056 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong_3056 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'691'_3058 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'691'_3058 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'737'_3060 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'737'_3060 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'idem_3062 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny Source #
d_'8851''45'identity_3064 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'identity'691'_3066 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'691'_3066 ∷ T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity'737'_3068 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'737'_3068 ∷ T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'isBand_3070 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsBand_508 Source #
d_'8851''45'isCommutativeSemigroup_3072 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsCommutativeSemigroup_548 Source #
du_'8851''45'isCommutativeSemigroup_3072 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → T_IsCommutativeSemigroup_548 Source #
d_'8851''45'isMagma_3074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsMagma_176 Source #
d_'8851''45'isMonoid_3076 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_686 Source #
du_'8851''45'isMonoid_3076 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_686 Source #
d_'8851''45'isSelectiveMagma_3078 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsSelectiveMagma_436 Source #
du_'8851''45'isSelectiveMagma_3078 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → T_IsSelectiveMagma_436 Source #
d_'8851''45'isSemigroup_3080 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsSemigroup_472 Source #
du_'8851''45'isSemigroup_3080 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → T_IsSemigroup_472 Source #
d_'8851''45'glb_3082 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'glb_3082 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'magma_3084 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Magma_68 Source #
d_'8851''45'mono'45''8804'_3086 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'45''8804'_3086 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'monoid_3088 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_882 Source #
du_'8851''45'monoid_3088 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_882 Source #
d_'8851''45'mono'691''45''8804'_3090 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'691''45''8804'_3090 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'737''45''8804'_3092 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'737''45''8804'_3092 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'sel_3094 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_'8851''45'sel_3094 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_'8851''45'selectiveMagma_3096 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_SelectiveMagma_122 Source #
du_'8851''45'selectiveMagma_3096 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → T_SelectiveMagma_122 Source #
d_'8851''45'semigroup_3098 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Semigroup_536 Source #
d_'8851''45'triangulate_3100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'triangulate_3100 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'zero_3102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8851''45'zero_3102 ∷ T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'zero'691'_3104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'691'_3104 ∷ T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero'737'_3106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'737'_3106 ∷ T_MaxOperator_128 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'distrib'737''45''8852'_3108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'distrib'737''45''8852'_3108 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'distrib'691''45''8852'_3136 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'distrib'691''45''8852'_3136 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'distrib'45''8852'_3138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Σ_14 Source #
du_'8851''45'distrib'45''8852'_3138 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Σ_14 Source #
d_'8852''45'distrib'737''45''8851'_3140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8852''45'distrib'737''45''8851'_3140 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45'distrib'691''45''8851'_3168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8852''45'distrib'691''45''8851'_3168 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45'distrib'45''8851'_3170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Σ_14 Source #
du_'8852''45'distrib'45''8851'_3170 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Σ_14 Source #
d_'8851''45'absorbs'45''8852'_3172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'absorbs'45''8852'_3172 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45'absorbs'45''8851'_3194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8852''45'absorbs'45''8851'_3194 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45''8851''45'absorptive_3216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Σ_14 Source #
du_'8852''45''8851''45'absorptive_3216 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Σ_14 Source #
d_'8851''45''8852''45'absorptive_3218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Σ_14 Source #
du_'8851''45''8852''45'absorptive_3218 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Σ_14 Source #
d__'8805'__3220 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → () Source #
d_antimono'45''8804''45'distrib'45''8851'_3228 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_antimono'45''8804''45'distrib'45''8851'_3228 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_antimono'45''8804''45'distrib'45''8852'_3274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_antimono'45''8804''45'distrib'45''8852'_3274 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #