Documentation

d__'8851'__92 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → AgdaAny → AgdaAny → AgdaAny Source #

du__'8851'__92 ∷ T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny Source #

d_IsDistributiveLattice_116 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsLattice_120 ∷ p → p → p → p → p → p → p → p → () Source #

d_isLattice_340 ∷ T_IsDistributiveLattice_3036 → T_IsLattice_2962 Source #

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

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

d_absorptive_424 ∷ T_IsLattice_2962 → T_Σ_14 Source #

d_isEquivalence_426 ∷ T_IsLattice_2962 → T_IsEquivalence_26 Source #

d_'8743''45'assoc_440 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_442 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_444 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_452 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_454 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_456 ∷ T_IsLattice_2962 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8851''45'isSemilattice_784 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsCommutativeBand_590 Source #

du_'8851''45'isSemilattice_784 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_IsCommutativeBand_590 Source #

d_'8851''45'semilattice_786 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Semilattice_10 Source #

du_'8851''45'semilattice_786 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_Semilattice_10 Source #

d_'8851''45'isSemilattice_790 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsCommutativeBand_590 Source #

du_'8851''45'isSemilattice_790 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → T_IsCommutativeBand_590 Source #

d_'8851''45'semilattice_792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Semilattice_10 Source #

du_'8851''45'semilattice_792 ∷ T_TotalPreorder_222 → T_MaxOperator_128 → T_Semilattice_10 Source #

d_'8852''45''8851''45'isLattice_794 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsLattice_2962 Source #

du_'8852''45''8851''45'isLattice_794 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsLattice_2962 Source #

d_'8851''45''8852''45'isLattice_796 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsLattice_2962 Source #

du_'8851''45''8852''45'isLattice_796 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsLattice_2962 Source #

d_'8851''45''8852''45'isDistributiveLattice_798 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsDistributiveLattice_3036 Source #

du_'8851''45''8852''45'isDistributiveLattice_798 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsDistributiveLattice_3036 Source #

d_'8852''45''8851''45'isDistributiveLattice_800 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsDistributiveLattice_3036 Source #

du_'8852''45''8851''45'isDistributiveLattice_800 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_IsDistributiveLattice_3036 Source #

d_'8852''45''8851''45'lattice_802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Lattice_500 Source #

du_'8852''45''8851''45'lattice_802 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Lattice_500 Source #

d_'8851''45''8852''45'lattice_804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Lattice_500 Source #

du_'8851''45''8852''45'lattice_804 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_Lattice_500 Source #

d_'8852''45''8851''45'distributiveLattice_806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_DistributiveLattice_584 Source #

du_'8852''45''8851''45'distributiveLattice_806 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_DistributiveLattice_584 Source #

d_'8851''45''8852''45'distributiveLattice_808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_DistributiveLattice_584 Source #

du_'8851''45''8852''45'distributiveLattice_808 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_MaxOperator_128 → T_DistributiveLattice_584 Source #