Documentation

d_Idempotent_112 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsBand_210 ∷ p → p → p → p → () Source #

d_IsMagma_250 ∷ p → p → p → p → () Source #

d_IsSemigroup_278 ∷ p → p → p → p → () Source #

d_idem_392 ∷ T_IsBand_508 → AgdaAny → AgdaAny Source #

d_isSemigroup_400 ∷ T_IsBand_508 → T_IsSemigroup_472 Source #

d_isEquivalence_1550 ∷ T_IsMagma_176 → T_IsEquivalence_26 Source #

d_'8729''45'cong_1564 ∷ T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_2404 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_2408 ∷ T_IsSemigroup_472 → T_IsMagma_176 Source #

d_IsLattice_2732 ∷ p → p → p → p → p → () Source #

d_IsSemilattice_2736 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_absorptive_3036 ∷ T_IsLattice_2962 → T_Σ_14 Source #

d_isEquivalence_3038 ∷ T_IsLattice_2962 → T_IsEquivalence_26 Source #

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

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

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

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

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

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

d_'8743''45'idem_3182 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny Source #

du_'8743''45'idem_3182 ∷ T_Lattice_500 → AgdaAny → AgdaAny Source #

d_'8743''45'isMagma_3186 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsMagma_176 Source #

du_'8743''45'isMagma_3186 ∷ T_Lattice_500 → T_IsMagma_176 Source #

d_'8743''45'isSemigroup_3188 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsSemigroup_472 Source #

du_'8743''45'isSemigroup_3188 ∷ T_Lattice_500 → T_IsSemigroup_472 Source #

d_'8743''45'isBand_3190 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsBand_508 Source #

du_'8743''45'isBand_3190 ∷ T_Lattice_500 → T_IsBand_508 Source #

d_'8743''45'isSemilattice_3192 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsCommutativeBand_590 Source #

du_'8743''45'isSemilattice_3192 ∷ T_Lattice_500 → T_IsCommutativeBand_590 Source #

d_'8743''45'semilattice_3194 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_Semilattice_10 Source #

du_'8743''45'semilattice_3194 ∷ T_Lattice_500 → T_Semilattice_10 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_3198 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_3198 ∷ T_Lattice_500 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_3200 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsMeetSemilattice_180 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_3200 ∷ T_Lattice_500 → T_IsMeetSemilattice_180 Source #

d_'8743''45'orderTheoreticJoinSemilattice_3202 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_3202 ∷ T_Lattice_500 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_3204 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_MeetSemilattice_200 Source #

du_'8743''45'orderTheoreticMeetSemilattice_3204 ∷ T_Lattice_500 → T_MeetSemilattice_200 Source #

d_'8744''45'idem_3206 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny Source #

du_'8744''45'idem_3206 ∷ T_Lattice_500 → AgdaAny → AgdaAny Source #

d_'8744''45'isMagma_3210 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsMagma_176 Source #

du_'8744''45'isMagma_3210 ∷ T_Lattice_500 → T_IsMagma_176 Source #

d_'8744''45'isSemigroup_3212 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsSemigroup_472 Source #

du_'8744''45'isSemigroup_3212 ∷ T_Lattice_500 → T_IsSemigroup_472 Source #

d_'8744''45'isBand_3214 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsBand_508 Source #

du_'8744''45'isBand_3214 ∷ T_Lattice_500 → T_IsBand_508 Source #

d_'8744''45'isSemilattice_3216 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsCommutativeBand_590 Source #

du_'8744''45'isSemilattice_3216 ∷ T_Lattice_500 → T_IsCommutativeBand_590 Source #

d_'8744''45'semilattice_3218 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_Semilattice_10 Source #

du_'8744''45'semilattice_3218 ∷ T_Lattice_500 → T_Semilattice_10 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_3222 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_3222 ∷ T_Lattice_500 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_3224 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsMeetSemilattice_180 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_3224 ∷ T_Lattice_500 → T_IsMeetSemilattice_180 Source #

d_'8743''45'orderTheoreticJoinSemilattice_3226 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_3226 ∷ T_Lattice_500 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_3228 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_MeetSemilattice_200 Source #

du_'8743''45'orderTheoreticMeetSemilattice_3228 ∷ T_Lattice_500 → T_MeetSemilattice_200 Source #

d_'8743''45''8744''45'isLattice_3230 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsLattice_2962 Source #

du_'8743''45''8744''45'isLattice_3230 ∷ T_Lattice_500 → T_IsLattice_2962 Source #

d_'8743''45''8744''45'lattice_3232 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_Lattice_500 Source #

du_'8743''45''8744''45'lattice_3232 ∷ T_Lattice_500 → T_Lattice_500 Source #

d_poset_3236 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_Poset_314 Source #

du_poset_3236 ∷ T_Lattice_500 → T_Poset_314 Source #

d__'8804'__3240 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → () Source #

d_'8744''45''8743''45'isOrderTheoreticLattice_3244 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_IsLattice_340 Source #

du_'8744''45''8743''45'isOrderTheoreticLattice_3244 ∷ T_Lattice_500 → T_IsLattice_340 Source #

d__'8804'__3256 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → () Source #

d_sound_3268 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sound_3268 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_complete_3280 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_complete_3280 ∷ T_Lattice_500 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_3288 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_supremum_3288 ∷ T_Lattice_500 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_'8744''45''8743''45'orderTheoreticLattice_3300 ∷ T_Level_18 → T_Level_18 → T_Lattice_500 → T_Lattice_386 Source #

du_'8744''45''8743''45'orderTheoreticLattice_3300 ∷ T_Lattice_500 → T_Lattice_386 Source #