Documentation

d_IsDistributiveLattice_232 ∷ p → p → p → p → p → () Source #

d_isLattice_460 ∷ T_IsDistributiveLattice_3146 → T_IsLattice_3070 Source #

d_'8743''45'distrib'45''8744'_484 ∷ T_IsDistributiveLattice_3146 → T_Σ_14 Source #

d_'8744''45'distrib'45''8743'_502 ∷ T_IsDistributiveLattice_3146 → T_Σ_14 Source #

d_poset_692 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_Poset_492 Source #

du_poset_692 ∷ T_DistributiveLattice_598 → T_Poset_492 Source #

d_'8743''45'idem_694 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny Source #

du_'8743''45'idem_694 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny Source #

d_'8743''45'isBand_696 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsBand_526 Source #

du_'8743''45'isBand_696 ∷ T_DistributiveLattice_598 → T_IsBand_526 Source #

d_'8743''45'isMagma_698 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsMagma_178 Source #

du_'8743''45'isMagma_698 ∷ T_DistributiveLattice_598 → T_IsMagma_178 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_700 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_700 ∷ T_DistributiveLattice_598 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_702 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsMeetSemilattice_184 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_702 ∷ T_DistributiveLattice_598 → T_IsMeetSemilattice_184 Source #

d_'8743''45'isSemigroup_704 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsSemigroup_488 Source #

du_'8743''45'isSemigroup_704 ∷ T_DistributiveLattice_598 → T_IsSemigroup_488 Source #

d_'8743''45'isSemilattice_706 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsCommutativeBand_612 Source #

du_'8743''45'isSemilattice_706 ∷ T_DistributiveLattice_598 → T_IsCommutativeBand_612 Source #

d_'8743''45'orderTheoreticJoinSemilattice_708 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_708 ∷ T_DistributiveLattice_598 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_710 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_MeetSemilattice_204 Source #

du_'8743''45'orderTheoreticMeetSemilattice_710 ∷ T_DistributiveLattice_598 → T_MeetSemilattice_204 Source #

d_'8743''45'semilattice_712 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_Semilattice_10 Source #

du_'8743''45'semilattice_712 ∷ T_DistributiveLattice_598 → T_Semilattice_10 Source #

d_'8743''45''8744''45'isLattice_714 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsLattice_3070 Source #

du_'8743''45''8744''45'isLattice_714 ∷ T_DistributiveLattice_598 → T_IsLattice_3070 Source #

d_'8743''45''8744''45'lattice_716 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_Lattice_512 Source #

du_'8743''45''8744''45'lattice_716 ∷ T_DistributiveLattice_598 → T_Lattice_512 Source #

d_'8744''45'idem_718 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny Source #

du_'8744''45'idem_718 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny Source #

d_'8744''45'isBand_720 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsBand_526 Source #

du_'8744''45'isBand_720 ∷ T_DistributiveLattice_598 → T_IsBand_526 Source #

d_'8744''45'isMagma_722 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsMagma_178 Source #

du_'8744''45'isMagma_722 ∷ T_DistributiveLattice_598 → T_IsMagma_178 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_724 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_724 ∷ T_DistributiveLattice_598 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_726 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsMeetSemilattice_184 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_726 ∷ T_DistributiveLattice_598 → T_IsMeetSemilattice_184 Source #

d_'8744''45'isSemigroup_728 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsSemigroup_488 Source #

du_'8744''45'isSemigroup_728 ∷ T_DistributiveLattice_598 → T_IsSemigroup_488 Source #

d_'8744''45'isSemilattice_730 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsCommutativeBand_612 Source #

du_'8744''45'isSemilattice_730 ∷ T_DistributiveLattice_598 → T_IsCommutativeBand_612 Source #

d_'8743''45'orderTheoreticJoinSemilattice_732 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_732 ∷ T_DistributiveLattice_598 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_734 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_MeetSemilattice_204 Source #

du_'8743''45'orderTheoreticMeetSemilattice_734 ∷ T_DistributiveLattice_598 → T_MeetSemilattice_204 Source #

d_'8744''45'semilattice_736 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_Semilattice_10 Source #

du_'8744''45'semilattice_736 ∷ T_DistributiveLattice_598 → T_Semilattice_10 Source #

d_'8744''45''8743''45'isOrderTheoreticLattice_738 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsLattice_348 Source #

du_'8744''45''8743''45'isOrderTheoreticLattice_738 ∷ T_DistributiveLattice_598 → T_IsLattice_348 Source #

d_'8744''45''8743''45'orderTheoreticLattice_740 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_Lattice_394 Source #

du_'8744''45''8743''45'orderTheoreticLattice_740 ∷ T_DistributiveLattice_598 → T_Lattice_394 Source #

d_'8743''45''8744''45'isDistributiveLattice_742 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsDistributiveLattice_3146 Source #

du_'8743''45''8744''45'isDistributiveLattice_742 ∷ T_DistributiveLattice_598 → T_IsDistributiveLattice_3146 Source #

d_'8743''45''8744''45'distributiveLattice_744 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_DistributiveLattice_598 Source #

du_'8743''45''8744''45'distributiveLattice_744 ∷ T_DistributiveLattice_598 → T_DistributiveLattice_598 Source #