| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp
Documentation
d__'8776'__22 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → () Source #
d__'8818'__24 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → () Source #
d__'8851'__76 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
d__Absorbs__92 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver__94 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver'691'__96 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver'737'__98 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Absorptive_102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_IsDistributiveLattice_186 ∷ p → p → p → p → p → p → p → p → () Source #
d_IsLattice_192 ∷ p → p → p → p → p → p → p → p → () Source #
d_mono'45''8804''45'distrib'45''8851'_1678 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_mono'45''8804''45'distrib'45''8851'_1678 ∷ T_TotalPreorder_204 → T_MinOperator_84 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'x'8851'z'8804'y_1680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'x'8851'z'8804'y_1680 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'z'8851'x'8804'y_1682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'z'8851'x'8804'y_1682 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'y_1684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'y_1684 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'z_1686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'z_1686 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'x'8658'x'8804'y_1688 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'x'8658'x'8804'y_1688 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'y'8658'y'8804'x_1690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'y'8658'y'8804'x_1690 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'x_1692 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'x_1692 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'y_1694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'y_1694 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'assoc_1696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'assoc_1696 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'band_1698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Band_266 Source #
d_'8851''45'comm_1700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'comm_1700 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'commutativeSemigroup_1702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_CommutativeSemigroup_332 Source #
du_'8851''45'commutativeSemigroup_1702 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_CommutativeSemigroup_332 Source #
d_'8851''45'cong_1704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong_1704 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'691'_1706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'691'_1706 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'737'_1708 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'737'_1708 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'glb_1710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'glb_1710 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'idem_1712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny Source #
d_'8851''45'identity_1714 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8851''45'identity_1714 ∷ T_MinOperator_84 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'identity'691'_1716 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'691'_1716 ∷ T_MinOperator_84 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity'737'_1718 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'737'_1718 ∷ T_MinOperator_84 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'isBand_1720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsBand_230 Source #
d_'8851''45'isCommutativeSemigroup_1722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsCommutativeSemigroup_270 Source #
du_'8851''45'isCommutativeSemigroup_1722 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_IsCommutativeSemigroup_270 Source #
d_'8851''45'isMagma_1724 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsMagma_86 Source #
d_'8851''45'isMonoid_1726 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_358 Source #
du_'8851''45'isMonoid_1726 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_358 Source #
d_'8851''45'isSelectiveMagma_1728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsSelectiveMagma_158 Source #
du_'8851''45'isSelectiveMagma_1728 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_IsSelectiveMagma_158 Source #
d_'8851''45'isSemigroup_1730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsSemigroup_194 Source #
d_'8851''45'isSemilattice_1732 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsSemilattice_312 Source #
du_'8851''45'isSemilattice_1732 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_IsSemilattice_312 Source #
d_'8851''45'magma_1734 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Magma_36 Source #
d_'8851''45'mono'45''8804'_1736 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'45''8804'_1736 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'monoid_1738 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_506 Source #
du_'8851''45'monoid_1738 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_506 Source #
d_'8851''45'mono'691''45''8804'_1740 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'691''45''8804'_1740 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'737''45''8804'_1742 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'737''45''8804'_1742 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'rawMagma_1744 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_RawMagma_8 Source #
d_'8851''45'sel_1746 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_'8851''45'sel_1746 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_'8851''45'selectiveMagma_1748 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_SelectiveMagma_90 Source #
du_'8851''45'selectiveMagma_1748 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_SelectiveMagma_90 Source #
d_'8851''45'semigroup_1750 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Semigroup_206 Source #
d_'8851''45'semilattice_1752 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Semilattice_402 Source #
d_'8851''45'triangulate_1754 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'triangulate_1754 ∷ T_TotalPreorder_204 → T_MinOperator_84 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'zero_1756 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8851''45'zero_1756 ∷ T_MinOperator_84 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'zero'691'_1758 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'691'_1758 ∷ T_MinOperator_84 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero'737'_1760 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'737'_1760 ∷ T_MinOperator_84 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_mono'45''8804''45'distrib'45''8852'_1764 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_mono'45''8804''45'distrib'45''8852'_1764 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'x_1766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'x_1766 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'x'8851'z'8804'y_1768 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'x'8851'z'8804'y_1768 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'z'8851'x'8804'y_1770 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'z'8851'x'8804'y_1770 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'y_1772 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'y_1772 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'x'8658'x'8804'y_1774 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'x'8658'x'8804'y_1774 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'y'8658'y'8804'x_1776 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'y'8658'y'8804'x_1776 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'y_1778 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'y_1778 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'z_1780 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'z_1780 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'assoc_1782 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'assoc_1782 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'band_1784 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Band_266 Source #
d_'8851''45'comm_1786 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'comm_1786 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'commutativeSemigroup_1788 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_CommutativeSemigroup_332 Source #
du_'8851''45'commutativeSemigroup_1788 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → T_CommutativeSemigroup_332 Source #
d_'8851''45'cong_1790 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong_1790 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'691'_1792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'691'_1792 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'737'_1794 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'737'_1794 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'idem_1796 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny Source #
d_'8851''45'identity_1798 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'identity'691'_1800 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'691'_1800 ∷ T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity'737'_1802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'737'_1802 ∷ T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'isBand_1804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsBand_230 Source #
d_'8851''45'isCommutativeSemigroup_1806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsCommutativeSemigroup_270 Source #
du_'8851''45'isCommutativeSemigroup_1806 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → T_IsCommutativeSemigroup_270 Source #
d_'8851''45'isMagma_1808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsMagma_86 Source #
d_'8851''45'isMonoid_1810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_358 Source #
du_'8851''45'isMonoid_1810 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_358 Source #
d_'8851''45'isSelectiveMagma_1812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsSelectiveMagma_158 Source #
du_'8851''45'isSelectiveMagma_1812 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → T_IsSelectiveMagma_158 Source #
d_'8851''45'isSemigroup_1814 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsSemigroup_194 Source #
du_'8851''45'isSemigroup_1814 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → T_IsSemigroup_194 Source #
d_'8851''45'isSemilattice_1816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsSemilattice_312 Source #
du_'8851''45'isSemilattice_1816 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → T_IsSemilattice_312 Source #
d_'8851''45'glb_1818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'glb_1818 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'magma_1820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Magma_36 Source #
d_'8851''45'mono'45''8804'_1822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'45''8804'_1822 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'monoid_1824 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_506 Source #
du_'8851''45'monoid_1824 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_506 Source #
d_'8851''45'mono'691''45''8804'_1826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'691''45''8804'_1826 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'737''45''8804'_1828 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'737''45''8804'_1828 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'sel_1830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_'8851''45'sel_1830 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_'8851''45'selectiveMagma_1832 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_SelectiveMagma_90 Source #
du_'8851''45'selectiveMagma_1832 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → T_SelectiveMagma_90 Source #
d_'8851''45'semigroup_1834 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Semigroup_206 Source #
d_'8851''45'semilattice_1836 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Semilattice_402 Source #
du_'8851''45'semilattice_1836 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → T_Semilattice_402 Source #
d_'8851''45'triangulate_1838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'triangulate_1838 ∷ T_TotalPreorder_204 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'zero_1840 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8851''45'zero_1840 ∷ T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'zero'691'_1842 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'691'_1842 ∷ T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero'737'_1844 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'737'_1844 ∷ T_MaxOperator_114 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'distrib'737''45''8852'_1846 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'distrib'737''45''8852'_1846 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'distrib'691''45''8852'_1874 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'distrib'691''45''8852'_1874 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'distrib'45''8852'_1876 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Σ_14 Source #
du_'8851''45'distrib'45''8852'_1876 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Σ_14 Source #
d_'8852''45'distrib'737''45''8851'_1878 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8852''45'distrib'737''45''8851'_1878 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45'distrib'691''45''8851'_1906 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8852''45'distrib'691''45''8851'_1906 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45'distrib'45''8851'_1908 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Σ_14 Source #
du_'8852''45'distrib'45''8851'_1908 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Σ_14 Source #
d_'8851''45'absorbs'45''8852'_1910 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'absorbs'45''8852'_1910 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45'absorbs'45''8851'_1932 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8852''45'absorbs'45''8851'_1932 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8852''45''8851''45'absorptive_1954 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Σ_14 Source #
du_'8852''45''8851''45'absorptive_1954 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Σ_14 Source #
d_'8851''45''8852''45'absorptive_1956 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Σ_14 Source #
du_'8851''45''8852''45'absorptive_1956 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Σ_14 Source #
d_'8852''45''8851''45'isLattice_1958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsLattice_740 Source #
du_'8852''45''8851''45'isLattice_1958 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsLattice_740 Source #
d_'8851''45''8852''45'isLattice_1960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsLattice_740 Source #
du_'8851''45''8852''45'isLattice_1960 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsLattice_740 Source #
d_'8851''45''8852''45'isDistributiveLattice_1962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsDistributiveLattice_814 Source #
du_'8851''45''8852''45'isDistributiveLattice_1962 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsDistributiveLattice_814 Source #
d_'8852''45''8851''45'isDistributiveLattice_1964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsDistributiveLattice_814 Source #
du_'8852''45''8851''45'isDistributiveLattice_1964 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_IsDistributiveLattice_814 Source #
d_'8852''45''8851''45'lattice_1966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Lattice_1144 Source #
du_'8852''45''8851''45'lattice_1966 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Lattice_1144 Source #
d_'8851''45''8852''45'lattice_1968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Lattice_1144 Source #
du_'8851''45''8852''45'lattice_1968 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_Lattice_1144 Source #
d_'8852''45''8851''45'distributiveLattice_1970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_DistributiveLattice_1228 Source #
du_'8852''45''8851''45'distributiveLattice_1970 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_DistributiveLattice_1228 Source #
d_'8851''45''8852''45'distributiveLattice_1972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_DistributiveLattice_1228 Source #
du_'8851''45''8852''45'distributiveLattice_1972 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → T_DistributiveLattice_1228 Source #
d__'8805'__1974 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → AgdaAny → AgdaAny → () Source #
d_antimono'45''8804''45'distrib'45''8851'_1982 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_antimono'45''8804''45'distrib'45''8851'_1982 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_antimono'45''8804''45'distrib'45''8852'_2028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_antimono'45''8804''45'distrib'45''8852'_2028 ∷ T_TotalPreorder_204 → T_MinOperator_84 → T_MaxOperator_114 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #