Documentation

d_IsDistributiveLattice_230 ∷ p → p → p → p → p → () Source #

d_isLattice_454 ∷ T_IsDistributiveLattice_3036 → T_IsLattice_2962 Source #

d_'8743''45'distrib'45''8744'_478 ∷ T_IsDistributiveLattice_3036 → T_Σ_14 Source #

d_'8744''45'distrib'45''8743'_496 ∷ T_IsDistributiveLattice_3036 → T_Σ_14 Source #

d_poset_686 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_Poset_314 Source #

du_poset_686 ∷ T_DistributiveLattice_584 → T_Poset_314 Source #

d_'8743''45'idem_688 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny Source #

du_'8743''45'idem_688 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny Source #

d_'8743''45'isBand_690 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsBand_508 Source #

du_'8743''45'isBand_690 ∷ T_DistributiveLattice_584 → T_IsBand_508 Source #

d_'8743''45'isMagma_692 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsMagma_176 Source #

du_'8743''45'isMagma_692 ∷ T_DistributiveLattice_584 → T_IsMagma_176 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_694 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_694 ∷ T_DistributiveLattice_584 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_696 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsMeetSemilattice_180 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_696 ∷ T_DistributiveLattice_584 → T_IsMeetSemilattice_180 Source #

d_'8743''45'isSemigroup_698 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsSemigroup_472 Source #

du_'8743''45'isSemigroup_698 ∷ T_DistributiveLattice_584 → T_IsSemigroup_472 Source #

d_'8743''45'isSemilattice_700 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsCommutativeBand_590 Source #

du_'8743''45'isSemilattice_700 ∷ T_DistributiveLattice_584 → T_IsCommutativeBand_590 Source #

d_'8743''45'orderTheoreticJoinSemilattice_702 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_702 ∷ T_DistributiveLattice_584 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_704 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_MeetSemilattice_200 Source #

du_'8743''45'orderTheoreticMeetSemilattice_704 ∷ T_DistributiveLattice_584 → T_MeetSemilattice_200 Source #

d_'8743''45'semilattice_706 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_Semilattice_10 Source #

du_'8743''45'semilattice_706 ∷ T_DistributiveLattice_584 → T_Semilattice_10 Source #

d_'8743''45''8744''45'isLattice_708 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsLattice_2962 Source #

du_'8743''45''8744''45'isLattice_708 ∷ T_DistributiveLattice_584 → T_IsLattice_2962 Source #

d_'8743''45''8744''45'lattice_710 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_Lattice_500 Source #

du_'8743''45''8744''45'lattice_710 ∷ T_DistributiveLattice_584 → T_Lattice_500 Source #

d_'8744''45'idem_712 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → AgdaAny → AgdaAny Source #

du_'8744''45'idem_712 ∷ T_DistributiveLattice_584 → AgdaAny → AgdaAny Source #

d_'8744''45'isBand_714 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsBand_508 Source #

du_'8744''45'isBand_714 ∷ T_DistributiveLattice_584 → T_IsBand_508 Source #

d_'8744''45'isMagma_716 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsMagma_176 Source #

du_'8744''45'isMagma_716 ∷ T_DistributiveLattice_584 → T_IsMagma_176 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_718 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_718 ∷ T_DistributiveLattice_584 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_720 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsMeetSemilattice_180 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_720 ∷ T_DistributiveLattice_584 → T_IsMeetSemilattice_180 Source #

d_'8744''45'isSemigroup_722 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsSemigroup_472 Source #

du_'8744''45'isSemigroup_722 ∷ T_DistributiveLattice_584 → T_IsSemigroup_472 Source #

d_'8744''45'isSemilattice_724 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsCommutativeBand_590 Source #

du_'8744''45'isSemilattice_724 ∷ T_DistributiveLattice_584 → T_IsCommutativeBand_590 Source #

d_'8743''45'orderTheoreticJoinSemilattice_726 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_726 ∷ T_DistributiveLattice_584 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_728 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_MeetSemilattice_200 Source #

du_'8743''45'orderTheoreticMeetSemilattice_728 ∷ T_DistributiveLattice_584 → T_MeetSemilattice_200 Source #

d_'8744''45'semilattice_730 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_Semilattice_10 Source #

du_'8744''45'semilattice_730 ∷ T_DistributiveLattice_584 → T_Semilattice_10 Source #

d_'8744''45''8743''45'isOrderTheoreticLattice_732 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsLattice_340 Source #

du_'8744''45''8743''45'isOrderTheoreticLattice_732 ∷ T_DistributiveLattice_584 → T_IsLattice_340 Source #

d_'8744''45''8743''45'orderTheoreticLattice_734 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_Lattice_386 Source #

du_'8744''45''8743''45'orderTheoreticLattice_734 ∷ T_DistributiveLattice_584 → T_Lattice_386 Source #

d_'8743''45''8744''45'isDistributiveLattice_736 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_IsDistributiveLattice_3036 Source #

du_'8743''45''8744''45'isDistributiveLattice_736 ∷ T_DistributiveLattice_584 → T_IsDistributiveLattice_3036 Source #

d_'8743''45''8744''45'distributiveLattice_738 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_584 → T_DistributiveLattice_584 Source #

du_'8743''45''8744''45'distributiveLattice_738 ∷ T_DistributiveLattice_584 → T_DistributiveLattice_584 Source #