Documentation

d_IsAbelianGroup_92 ∷ p → p → p → p → p → p → () Source #

d_IsBooleanAlgebra_96 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsCommutativeMonoid_104 ∷ p → p → p → p → p → () Source #

d_IsCommutativeRing_106 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsCommutativeSemiring_110 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroup_116 ∷ p → p → p → p → p → p → () Source #

d_IsMagma_122 ∷ p → p → p → p → () Source #

d_IsMonoid_124 ∷ p → p → p → p → p → () Source #

d_IsRing_128 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSemigroup_132 ∷ p → p → p → p → () Source #

d_IsSemiring_136 ∷ p → p → p → p → p → p → p → () Source #

d__DistributesOver__1518 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'691'__1520 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'737'__1522 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Associative_1534 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Commutative_1538 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Congruent'8322'_1542 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Identity_1550 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Inverse_1554 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Involutive_1556 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny) → () Source #

d_LeftIdentity_1564 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftInverse_1566 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftZero_1568 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightIdentity_1576 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightInverse_1578 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightZero_1580 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Zero_1584 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_isOrderTheoreticLattice_1656 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsLattice_810 Source #

du_isOrderTheoreticLattice_1656 ∷ T_BooleanAlgebra_2920 → T_IsLattice_810 Source #

d_orderTheoreticLattice_1658 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Lattice_898 Source #

du_orderTheoreticLattice_1658 ∷ T_BooleanAlgebra_2920 → T_Lattice_898 Source #

d_poset_1660 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Poset_282 Source #

du_poset_1660 ∷ T_BooleanAlgebra_2920 → T_Poset_282 Source #

d_'8743''45'distrib'45''8744'_1662 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8743''45'distrib'45''8744'_1662 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8743''45'distrib'691''45''8744'_1664 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_1664 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_1666 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_1666 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'idem_1668 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8743''45'idem_1668 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8743''45'idempotent_1670 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8743''45'idempotent_1670 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8743''45'isBand_1672 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsBand_230 Source #

du_'8743''45'isBand_1672 ∷ T_BooleanAlgebra_2920 → T_IsBand_230 Source #

d_'8743''45'isMagma_1674 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsMagma_86 Source #

du_'8743''45'isMagma_1674 ∷ T_BooleanAlgebra_2920 → T_IsMagma_86 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_1676 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsJoinSemilattice_68 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_1676 ∷ T_BooleanAlgebra_2920 → T_IsJoinSemilattice_68 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_1678 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsMeetSemilattice_438 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_1678 ∷ T_BooleanAlgebra_2920 → T_IsMeetSemilattice_438 Source #

d_'8743''45'isSemigroup_1680 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsSemigroup_194 Source #

du_'8743''45'isSemigroup_1680 ∷ T_BooleanAlgebra_2920 → T_IsSemigroup_194 Source #

d_'8743''45'isSemilattice_1682 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsSemilattice_312 Source #

du_'8743''45'isSemilattice_1682 ∷ T_BooleanAlgebra_2920 → T_IsSemilattice_312 Source #

d_'8743''45'orderTheoreticJoinSemilattice_1684 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_JoinSemilattice_170 Source #

du_'8743''45'orderTheoreticJoinSemilattice_1684 ∷ T_BooleanAlgebra_2920 → T_JoinSemilattice_170 Source #

d_'8743''45'orderTheoreticMeetSemilattice_1686 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_MeetSemilattice_540 Source #

du_'8743''45'orderTheoreticMeetSemilattice_1686 ∷ T_BooleanAlgebra_2920 → T_MeetSemilattice_540 Source #

d_'8743''45'semilattice_1688 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Semilattice_402 Source #

du_'8743''45'semilattice_1688 ∷ T_BooleanAlgebra_2920 → T_Semilattice_402 Source #

d_'8743''45''8744''45'distrib_1690 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8743''45''8744''45'distrib_1690 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8743''45''8744''45'distributiveLattice_1692 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_DistributiveLattice_1228 Source #

du_'8743''45''8744''45'distributiveLattice_1692 ∷ T_BooleanAlgebra_2920 → T_DistributiveLattice_1228 Source #

d_'8743''45''8744''45'distrib'691'_1694 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45''8744''45'distrib'691'_1694 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45''8744''45'distrib'737'_1696 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45''8744''45'distrib'737'_1696 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45''8744''45'isDistributiveLattice_1698 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsDistributiveLattice_814 Source #

du_'8743''45''8744''45'isDistributiveLattice_1698 ∷ T_BooleanAlgebra_2920 → T_IsDistributiveLattice_814 Source #

d_'8743''45''8744''45'isLattice_1700 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsLattice_740 Source #

du_'8743''45''8744''45'isLattice_1700 ∷ T_BooleanAlgebra_2920 → T_IsLattice_740 Source #

d_'8743''45''8744''45'lattice_1702 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Lattice_1144 Source #

du_'8743''45''8744''45'lattice_1702 ∷ T_BooleanAlgebra_2920 → T_Lattice_1144 Source #

d_'8744''45'distrib'45''8743'_1704 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8744''45'distrib'45''8743'_1704 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8744''45'distrib'737''45''8743'_1706 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_1706 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'idem_1708 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8744''45'idem_1708 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8744''45'idempotent_1710 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8744''45'idempotent_1710 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8744''45'isBand_1712 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsBand_230 Source #

du_'8744''45'isBand_1712 ∷ T_BooleanAlgebra_2920 → T_IsBand_230 Source #

d_'8744''45'isMagma_1714 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsMagma_86 Source #

du_'8744''45'isMagma_1714 ∷ T_BooleanAlgebra_2920 → T_IsMagma_86 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_1716 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsJoinSemilattice_68 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_1716 ∷ T_BooleanAlgebra_2920 → T_IsJoinSemilattice_68 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_1718 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsMeetSemilattice_438 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_1718 ∷ T_BooleanAlgebra_2920 → T_IsMeetSemilattice_438 Source #

d_'8744''45'isSemigroup_1720 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsSemigroup_194 Source #

du_'8744''45'isSemigroup_1720 ∷ T_BooleanAlgebra_2920 → T_IsSemigroup_194 Source #

d_'8744''45'isSemilattice_1722 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsSemilattice_312 Source #

du_'8744''45'isSemilattice_1722 ∷ T_BooleanAlgebra_2920 → T_IsSemilattice_312 Source #

d_'8743''45'orderTheoreticJoinSemilattice_1724 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_JoinSemilattice_170 Source #

du_'8743''45'orderTheoreticJoinSemilattice_1724 ∷ T_BooleanAlgebra_2920 → T_JoinSemilattice_170 Source #

d_'8743''45'orderTheoreticMeetSemilattice_1726 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_MeetSemilattice_540 Source #

du_'8743''45'orderTheoreticMeetSemilattice_1726 ∷ T_BooleanAlgebra_2920 → T_MeetSemilattice_540 Source #

d_'8744''45'semilattice_1728 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Semilattice_402 Source #

du_'8744''45'semilattice_1728 ∷ T_BooleanAlgebra_2920 → T_Semilattice_402 Source #

d_'8744''45''8743''45'distrib_1730 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8744''45''8743''45'distrib_1730 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8744''45''8743''45'distrib'737'_1732 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45''8743''45'distrib'737'_1732 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45''8743''45'isOrderTheoreticLattice_1734 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsLattice_810 Source #

du_'8744''45''8743''45'isOrderTheoreticLattice_1734 ∷ T_BooleanAlgebra_2920 → T_IsLattice_810 Source #

d_'8744''45''8743''45'orderTheoreticLattice_1736 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Lattice_898 Source #

du_'8744''45''8743''45'orderTheoreticLattice_1736 ∷ T_BooleanAlgebra_2920 → T_Lattice_898 Source #

d_'8744''45'complement'737'_1738 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8744''45'complement'737'_1738 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8744''45'complement_1740 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8744''45'complement_1740 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8743''45'complement'737'_1742 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8743''45'complement'737'_1742 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8743''45'complement_1744 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8743''45'complement_1744 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8743''45''8744''45'isBooleanAlgebra_1746 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsBooleanAlgebra_1864 Source #

du_'8743''45''8744''45'isBooleanAlgebra_1746 ∷ T_BooleanAlgebra_2920 → T_IsBooleanAlgebra_1864 Source #

d_'8743''45''8744''45'booleanAlgebra_1748 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_BooleanAlgebra_2920 Source #

du_'8743''45''8744''45'booleanAlgebra_1748 ∷ T_BooleanAlgebra_2920 → T_BooleanAlgebra_2920 Source #

d_'8743''45'identity'691'_1750 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8743''45'identity'691'_1750 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8743''45'identity'737'_1754 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8743''45'identity'737'_1754 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8743''45'identity_1756 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8743''45'identity_1756 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8744''45'identity'691'_1758 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8744''45'identity'691'_1758 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8744''45'identity'737'_1762 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8744''45'identity'737'_1762 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8744''45'identity_1764 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8744''45'identity_1764 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8743''45'zero'691'_1766 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8743''45'zero'691'_1766 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8743''45'zero'737'_1770 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8743''45'zero'737'_1770 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8743''45'zero_1772 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8743''45'zero_1772 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8744''45'zero'691'_1776 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8744''45'zero'691'_1776 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8744''45'zero'737'_1780 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8744''45'zero'737'_1780 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8744''45'zero_1782 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8744''45'zero_1782 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8744''45''8869''45'isMonoid_1784 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsMonoid_358 Source #

du_'8744''45''8869''45'isMonoid_1784 ∷ T_BooleanAlgebra_2920 → T_IsMonoid_358 Source #

d_'8743''45''8868''45'isMonoid_1786 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsMonoid_358 Source #

du_'8743''45''8868''45'isMonoid_1786 ∷ T_BooleanAlgebra_2920 → T_IsMonoid_358 Source #

d_'8744''45''8869''45'isCommutativeMonoid_1788 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsCommutativeMonoid_406 Source #

du_'8744''45''8869''45'isCommutativeMonoid_1788 ∷ T_BooleanAlgebra_2920 → T_IsCommutativeMonoid_406 Source #

d_'8743''45''8868''45'isCommutativeMonoid_1790 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsCommutativeMonoid_406 Source #

du_'8743''45''8868''45'isCommutativeMonoid_1790 ∷ T_BooleanAlgebra_2920 → T_IsCommutativeMonoid_406 Source #

d_'8744''45''8743''45'isSemiring_1792 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsSemiring_1238 Source #

du_'8744''45''8743''45'isSemiring_1792 ∷ T_BooleanAlgebra_2920 → T_IsSemiring_1238 Source #

d_'8743''45''8744''45'isSemiring_1794 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsSemiring_1238 Source #

du_'8743''45''8744''45'isSemiring_1794 ∷ T_BooleanAlgebra_2920 → T_IsSemiring_1238 Source #

d_'8744''45''8743''45'isCommutativeSemiring_1796 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsCommutativeSemiring_1344 Source #

du_'8744''45''8743''45'isCommutativeSemiring_1796 ∷ T_BooleanAlgebra_2920 → T_IsCommutativeSemiring_1344 Source #

d_'8743''45''8744''45'isCommutativeSemiring_1798 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsCommutativeSemiring_1344 Source #

du_'8743''45''8744''45'isCommutativeSemiring_1798 ∷ T_BooleanAlgebra_2920 → T_IsCommutativeSemiring_1344 Source #

d_'8744''45''8743''45'commutativeSemiring_1800 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_CommutativeSemiring_2094 Source #

du_'8744''45''8743''45'commutativeSemiring_1800 ∷ T_BooleanAlgebra_2920 → T_CommutativeSemiring_2094 Source #

d_'8743''45''8744''45'commutativeSemiring_1802 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_CommutativeSemiring_2094 Source #

du_'8743''45''8744''45'commutativeSemiring_1802 ∷ T_BooleanAlgebra_2920 → T_CommutativeSemiring_2094 Source #

d_lemma_1808 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lemma_1808 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8869''8777''8868'_1818 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny Source #

du_'8869''8777''8868'_1818 ∷ T_BooleanAlgebra_2920 → AgdaAny Source #

d_'8868''8777''8869'_1820 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny Source #

du_'8868''8777''8869'_1820 ∷ T_BooleanAlgebra_2920 → AgdaAny Source #

d_'172''45'involutive_1822 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'172''45'involutive_1822 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_deMorgan'8321'_1830 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_deMorgan'8321'_1830 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8321'_1840 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8321'_1840 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8323'_1842 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8323'_1842 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322'_1844 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322'_1844 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_deMorgan'8322'_1850 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_deMorgan'8322'_1850 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8853'__1866 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du__'8853'__1866 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_helper_1876 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_helper_1876 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'cong_1882 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'cong_1882 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'comm_1896 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'comm_1896 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'737''45''8853'_1906 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'737''45''8853'_1906 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_lem_1920 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem_1920 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'691''45''8853'_1930 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'691''45''8853'_1930 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'annihilates'45''172'_1940 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'annihilates'45''172'_1940 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'identity'737'_1946 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'identity'737'_1946 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'identity'691'_1950 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'identity'691'_1950 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'identity_1952 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

du_'8853''45'identity_1952 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

d_'8853''45'inverse'737'_1954 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'737'_1954 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'inverse'691'_1958 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'691'_1958 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_'8853''45'inverse_1960 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

du_'8853''45'inverse_1960 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

d_'8743''45'distrib'737''45''8853'_1962 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8853'_1962 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322'_1974 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322'_1974 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8321'_1976 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8321'_1976 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8323'_1978 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8323'_1978 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'691''45''8853'_1980 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8853'_1980 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8853'_1982 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

du_'8743''45'distrib'45''8853'_1982 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

d_lemma'8322'_1992 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lemma'8322'_1992 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'assoc_2002 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'assoc_2002 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8321'_2014 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8321'_2014 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322''8242'_2016 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322''8242'_2016 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8322'_2018 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8322'_2018 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8323'_2020 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8323'_2020 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8324''8242'_2022 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8324''8242'_2022 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8324'_2024 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8324'_2024 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lem'8325'_2026 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_lem'8325'_2026 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'isMagma_2028 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 Source #

du_'8853''45'isMagma_2028 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_86 Source #

d_'8853''45'isSemigroup_2030 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 Source #

du_'8853''45'isSemigroup_2030 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 Source #

d_'8853''45''8869''45'isMonoid_2032 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMonoid_358 Source #

du_'8853''45''8869''45'isMonoid_2032 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMonoid_358 Source #

d_'8853''45''8869''45'isGroup_2034 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsGroup_580 Source #

du_'8853''45''8869''45'isGroup_2034 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsGroup_580 Source #

d_'8853''45''8869''45'isAbelianGroup_2036 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAbelianGroup_662 Source #

du_'8853''45''8869''45'isAbelianGroup_2036 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsAbelianGroup_662 Source #

d_'8853''45''8743''45'isRing_2038 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsRing_1584 Source #

du_'8853''45''8743''45'isRing_2038 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsRing_1584 Source #

d_'8853''45''8743''45'isCommutativeRing_2040 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeRing_1720 Source #

du_'8853''45''8743''45'isCommutativeRing_2040 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeRing_1720 Source #

d_'8853''45''8743''45'commutativeRing_2042 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_CommutativeRing_2704 Source #

du_'8853''45''8743''45'commutativeRing_2042 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_CommutativeRing_2704 Source #

d_'8853''45''172''45'distrib'737'_2044 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45''172''45'distrib'737'_2044 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45''172''45'distrib'691'_2046 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45''172''45'distrib'691'_2046 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_isCommutativeRing_2048 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeRing_1720 Source #

du_isCommutativeRing_2048 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeRing_1720 Source #

d_commutativeRing_2050 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_CommutativeRing_2704 Source #

du_commutativeRing_2050 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_CommutativeRing_2704 Source #

d__'8853'__2052 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_commutativeRing_2064 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_CommutativeRing_2704 Source #

du_commutativeRing_2064 ∷ T_BooleanAlgebra_2920 → T_CommutativeRing_2704 Source #

d_isCommutativeRing_2066 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsCommutativeRing_1720 Source #

du_isCommutativeRing_2066 ∷ T_BooleanAlgebra_2920 → T_IsCommutativeRing_1720 Source #

d_'172''45'distrib'691''45''8853'_2068 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'691''45''8853'_2068 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'distrib'737''45''8853'_2070 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_'172''45'distrib'737''45''8853'_2070 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8853'_2072 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8743''45'distrib'45''8853'_2072 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8743''45'distrib'691''45''8853'_2074 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8853'_2074 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8853'_2076 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8853'_2076 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'annihilates'45''172'_2078 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'annihilates'45''172'_2078 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'assoc_2080 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'assoc_2080 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'comm_2082 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'comm_2082 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'cong_2084 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45'cong_2084 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45'identity_2086 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8853''45'identity_2086 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8853''45'identity'691'_2088 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8853''45'identity'691'_2088 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8853''45'identity'737'_2090 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8853''45'identity'737'_2090 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8853''45'inverse_2092 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_Σ_14 Source #

du_'8853''45'inverse_2092 ∷ T_BooleanAlgebra_2920 → T_Σ_14 Source #

d_'8853''45'inverse'691'_2094 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'691'_2094 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8853''45'inverse'737'_2096 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

du_'8853''45'inverse'737'_2096 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny Source #

d_'8853''45'isMagma_2098 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsMagma_86 Source #

du_'8853''45'isMagma_2098 ∷ T_BooleanAlgebra_2920 → T_IsMagma_86 Source #

d_'8853''45'isSemigroup_2100 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsSemigroup_194 Source #

du_'8853''45'isSemigroup_2100 ∷ T_BooleanAlgebra_2920 → T_IsSemigroup_194 Source #

d_'8853''45''172''45'distrib'691'_2102 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45''172''45'distrib'691'_2102 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45''172''45'distrib'737'_2104 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8853''45''172''45'distrib'737'_2104 ∷ T_BooleanAlgebra_2920 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8853''45''8743''45'commutativeRing_2106 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_CommutativeRing_2704 Source #

du_'8853''45''8743''45'commutativeRing_2106 ∷ T_BooleanAlgebra_2920 → T_CommutativeRing_2704 Source #

d_'8853''45''8743''45'isCommutativeRing_2108 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsCommutativeRing_1720 Source #

du_'8853''45''8743''45'isCommutativeRing_2108 ∷ T_BooleanAlgebra_2920 → T_IsCommutativeRing_1720 Source #

d_'8853''45''8743''45'isRing_2110 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsRing_1584 Source #

du_'8853''45''8743''45'isRing_2110 ∷ T_BooleanAlgebra_2920 → T_IsRing_1584 Source #

d_'8853''45''8869''45'isAbelianGroup_2112 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsAbelianGroup_662 Source #

du_'8853''45''8869''45'isAbelianGroup_2112 ∷ T_BooleanAlgebra_2920 → T_IsAbelianGroup_662 Source #

d_'8853''45''8869''45'isGroup_2114 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsGroup_580 Source #

du_'8853''45''8869''45'isGroup_2114 ∷ T_BooleanAlgebra_2920 → T_IsGroup_580 Source #

d_'8853''45''8869''45'isMonoid_2116 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → T_IsMonoid_358 Source #

du_'8853''45''8869''45'isMonoid_2116 ∷ T_BooleanAlgebra_2920 → T_IsMonoid_358 Source #

d_'172''8869''61''8868'_2118 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny Source #

du_'172''8869''61''8868'_2118 ∷ T_BooleanAlgebra_2920 → AgdaAny Source #

d_'172''8868''61''8869'_2120 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → AgdaAny Source #

du_'172''8868''61''8869'_2120 ∷ T_BooleanAlgebra_2920 → AgdaAny Source #

d_replace'45'equality_2128 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Equivalence_16) → T_BooleanAlgebra_2920 Source #

du_replace'45'equality_2128 ∷ T_BooleanAlgebra_2920 → (AgdaAny → AgdaAny → T_Equivalence_16) → T_BooleanAlgebra_2920 Source #