Documentation

d__'8851'__100 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #

du__'8851'__100 ∷ T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDistributiveLattice_126 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsLattice_132 ∷ p → p → p → p → p → p → p → p → () Source #

d_isLattice_354 ∷ T_IsDistributiveLattice_3146 → T_IsLattice_3070 Source #

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

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

d_absorptive_438 ∷ T_IsLattice_3070 → T_Σ_14 Source #

d_isEquivalence_440 ∷ T_IsLattice_3070 → T_IsEquivalence_28 Source #

d_'8743''45'assoc_454 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_456 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_458 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_466 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_468 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_470 ∷ T_IsLattice_3070 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8851''45'isSemilattice_798 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsCommutativeBand_612 Source #

du_'8851''45'isSemilattice_798 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_IsCommutativeBand_612 Source #

d_'8851''45'semilattice_800 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Semilattice_10 Source #

du_'8851''45'semilattice_800 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_Semilattice_10 Source #

d_'8851''45'isSemilattice_804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsCommutativeBand_612 Source #

du_'8851''45'isSemilattice_804 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_IsCommutativeBand_612 Source #

d_'8851''45'semilattice_806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Semilattice_10 Source #

du_'8851''45'semilattice_806 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_Semilattice_10 Source #

d_'8852''45''8851''45'isLattice_808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsLattice_3070 Source #

du_'8852''45''8851''45'isLattice_808 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsLattice_3070 Source #

d_'8851''45''8852''45'isLattice_810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsLattice_3070 Source #

du_'8851''45''8852''45'isLattice_810 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsLattice_3070 Source #

d_'8851''45''8852''45'isDistributiveLattice_812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsDistributiveLattice_3146 Source #

du_'8851''45''8852''45'isDistributiveLattice_812 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsDistributiveLattice_3146 Source #

d_'8852''45''8851''45'isDistributiveLattice_814 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsDistributiveLattice_3146 Source #

du_'8852''45''8851''45'isDistributiveLattice_814 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_IsDistributiveLattice_3146 Source #

d_'8852''45''8851''45'lattice_816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Lattice_512 Source #

du_'8852''45''8851''45'lattice_816 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Lattice_512 Source #

d_'8851''45''8852''45'lattice_818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Lattice_512 Source #

du_'8851''45''8852''45'lattice_818 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_Lattice_512 Source #

d_'8852''45''8851''45'distributiveLattice_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_DistributiveLattice_598 Source #

du_'8852''45''8851''45'distributiveLattice_820 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_DistributiveLattice_598 Source #

d_'8851''45''8852''45'distributiveLattice_822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_DistributiveLattice_598 Source #

du_'8851''45''8852''45'distributiveLattice_822 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_MaxOperator_138 → T_DistributiveLattice_598 Source #