Documentation

d_IsBand_72 ∷ p → p → p → p → () Source #

d_IsLattice_98 ∷ p → p → p → p → p → () Source #

d_IsMagma_100 ∷ p → p → p → p → () Source #

d_IsSemigroup_110 ∷ p → p → p → p → () Source #

d_IsSemilattice_112 ∷ p → p → p → p → () Source #

d_Idempotent_1524 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_'8743''45'idem_1588 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny Source #

du_'8743''45'idem_1588 ∷ T_Lattice_1144 → AgdaAny → AgdaAny Source #

d_'8743''45'isMagma_1592 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsMagma_86 Source #

du_'8743''45'isMagma_1592 ∷ T_Lattice_1144 → T_IsMagma_86 Source #

d_'8743''45'isSemigroup_1594 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsSemigroup_194 Source #

du_'8743''45'isSemigroup_1594 ∷ T_Lattice_1144 → T_IsSemigroup_194 Source #

d_'8743''45'isBand_1596 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsBand_230 Source #

du_'8743''45'isBand_1596 ∷ T_Lattice_1144 → T_IsBand_230 Source #

d_'8743''45'isSemilattice_1598 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsSemilattice_312 Source #

du_'8743''45'isSemilattice_1598 ∷ T_Lattice_1144 → T_IsSemilattice_312 Source #

d_'8743''45'semilattice_1600 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_Semilattice_402 Source #

du_'8743''45'semilattice_1600 ∷ T_Lattice_1144 → T_Semilattice_402 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_1604 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsJoinSemilattice_68 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_1604 ∷ T_Lattice_1144 → T_IsJoinSemilattice_68 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_1606 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsMeetSemilattice_438 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_1606 ∷ T_Lattice_1144 → T_IsMeetSemilattice_438 Source #

d_'8743''45'orderTheoreticJoinSemilattice_1608 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_JoinSemilattice_170 Source #

du_'8743''45'orderTheoreticJoinSemilattice_1608 ∷ T_Lattice_1144 → T_JoinSemilattice_170 Source #

d_'8743''45'orderTheoreticMeetSemilattice_1610 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_MeetSemilattice_540 Source #

du_'8743''45'orderTheoreticMeetSemilattice_1610 ∷ T_Lattice_1144 → T_MeetSemilattice_540 Source #

d_'8744''45'idem_1612 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny Source #

du_'8744''45'idem_1612 ∷ T_Lattice_1144 → AgdaAny → AgdaAny Source #

d_'8744''45'isMagma_1616 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsMagma_86 Source #

du_'8744''45'isMagma_1616 ∷ T_Lattice_1144 → T_IsMagma_86 Source #

d_'8744''45'isSemigroup_1618 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsSemigroup_194 Source #

du_'8744''45'isSemigroup_1618 ∷ T_Lattice_1144 → T_IsSemigroup_194 Source #

d_'8744''45'isBand_1620 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsBand_230 Source #

du_'8744''45'isBand_1620 ∷ T_Lattice_1144 → T_IsBand_230 Source #

d_'8744''45'isSemilattice_1622 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsSemilattice_312 Source #

du_'8744''45'isSemilattice_1622 ∷ T_Lattice_1144 → T_IsSemilattice_312 Source #

d_'8744''45'semilattice_1624 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_Semilattice_402 Source #

du_'8744''45'semilattice_1624 ∷ T_Lattice_1144 → T_Semilattice_402 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_1628 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsJoinSemilattice_68 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_1628 ∷ T_Lattice_1144 → T_IsJoinSemilattice_68 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_1630 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsMeetSemilattice_438 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_1630 ∷ T_Lattice_1144 → T_IsMeetSemilattice_438 Source #

d_'8743''45'orderTheoreticJoinSemilattice_1632 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_JoinSemilattice_170 Source #

du_'8743''45'orderTheoreticJoinSemilattice_1632 ∷ T_Lattice_1144 → T_JoinSemilattice_170 Source #

d_'8743''45'orderTheoreticMeetSemilattice_1634 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_MeetSemilattice_540 Source #

du_'8743''45'orderTheoreticMeetSemilattice_1634 ∷ T_Lattice_1144 → T_MeetSemilattice_540 Source #

d_'8743''45''8744''45'isLattice_1636 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsLattice_740 Source #

du_'8743''45''8744''45'isLattice_1636 ∷ T_Lattice_1144 → T_IsLattice_740 Source #

d_'8743''45''8744''45'lattice_1638 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_Lattice_1144 Source #

du_'8743''45''8744''45'lattice_1638 ∷ T_Lattice_1144 → T_Lattice_1144 Source #

d_poset_1642 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_Poset_282 Source #

du_poset_1642 ∷ T_Lattice_1144 → T_Poset_282 Source #

d__'8804'__1646 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → () Source #

d_'8744''45''8743''45'isOrderTheoreticLattice_1650 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsLattice_810 Source #

du_'8744''45''8743''45'isOrderTheoreticLattice_1650 ∷ T_Lattice_1144 → T_IsLattice_810 Source #

d__'8804'__1662 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → () Source #

d_sound_1674 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sound_1674 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_complete_1686 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_complete_1686 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_1694 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_supremum_1694 ∷ T_Lattice_1144 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_'8744''45''8743''45'orderTheoreticLattice_1706 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_Lattice_898 Source #

du_'8744''45''8743''45'orderTheoreticLattice_1706 ∷ T_Lattice_1144 → T_Lattice_898 Source #

d_'8743''45'idempotent_1708 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → AgdaAny → AgdaAny Source #

du_'8743''45'idempotent_1708 ∷ T_Lattice_1144 → AgdaAny → AgdaAny Source #

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

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

d_isOrderTheoreticLattice_1712 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_IsLattice_810 Source #

du_isOrderTheoreticLattice_1712 ∷ T_Lattice_1144 → T_IsLattice_810 Source #

d_orderTheoreticLattice_1714 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → T_Lattice_898 Source #

du_orderTheoreticLattice_1714 ∷ T_Lattice_1144 → T_Lattice_898 Source #

d_replace'45'equality_1722 ∷ T_Level_18 → T_Level_18 → T_Lattice_1144 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Equivalence_16) → T_Lattice_1144 Source #

du_replace'45'equality_1722 ∷ T_Lattice_1144 → (AgdaAny → AgdaAny → T_Equivalence_16) → T_Lattice_1144 Source #