Documentation

d_Idempotent_112 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_IsBand_210 :: p -> p -> p -> p -> () #

d_IsMagma_250 :: p -> p -> p -> p -> () #

d_IsSemigroup_278 :: p -> p -> p -> p -> () #

d_idem_392 :: T_IsBand_508 -> AgdaAny -> AgdaAny #

d_isSemigroup_400 :: T_IsBand_508 -> T_IsSemigroup_472 #

d_isEquivalence_1550 :: T_IsMagma_176 -> T_IsEquivalence_26 #

d_'8729''45'cong_1564 :: T_IsMagma_176 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_assoc_2404 :: T_IsSemigroup_472 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isMagma_2408 :: T_IsSemigroup_472 -> T_IsMagma_176 #

d_IsLattice_2732 :: p -> p -> p -> p -> p -> () #

d_IsSemilattice_2736 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_absorptive_3036 :: T_IsLattice_2962 -> T_Σ_14 #

d_isEquivalence_3038 :: T_IsLattice_2962 -> T_IsEquivalence_26 #

d_'8743''45'assoc_3052 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'comm_3054 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'cong_3056 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'assoc_3064 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'comm_3066 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'cong_3068 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'idem_3182 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny #

du_'8743''45'idem_3182 :: T_Lattice_500 -> AgdaAny -> AgdaAny #

d_'8743''45'isMagma_3186 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsMagma_176 #

du_'8743''45'isMagma_3186 :: T_Lattice_500 -> T_IsMagma_176 #

d_'8743''45'isSemigroup_3188 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsSemigroup_472 #

du_'8743''45'isSemigroup_3188 :: T_Lattice_500 -> T_IsSemigroup_472 #

d_'8743''45'isBand_3190 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsBand_508 #

du_'8743''45'isBand_3190 :: T_Lattice_500 -> T_IsBand_508 #

d_'8743''45'isSemilattice_3192 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsCommutativeBand_590 #

du_'8743''45'isSemilattice_3192 :: T_Lattice_500 -> T_IsCommutativeBand_590 #

d_'8743''45'semilattice_3194 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_Semilattice_10 #

du_'8743''45'semilattice_3194 :: T_Lattice_500 -> T_Semilattice_10 #

d_'8743''45'isOrderTheoreticJoinSemilattice_3198 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsJoinSemilattice_22 #

du_'8743''45'isOrderTheoreticJoinSemilattice_3198 :: T_Lattice_500 -> T_IsJoinSemilattice_22 #

d_'8743''45'isOrderTheoreticMeetSemilattice_3200 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsMeetSemilattice_180 #

du_'8743''45'isOrderTheoreticMeetSemilattice_3200 :: T_Lattice_500 -> T_IsMeetSemilattice_180 #

d_'8743''45'orderTheoreticJoinSemilattice_3202 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_JoinSemilattice_14 #

du_'8743''45'orderTheoreticJoinSemilattice_3202 :: T_Lattice_500 -> T_JoinSemilattice_14 #

d_'8743''45'orderTheoreticMeetSemilattice_3204 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_MeetSemilattice_200 #

du_'8743''45'orderTheoreticMeetSemilattice_3204 :: T_Lattice_500 -> T_MeetSemilattice_200 #

d_'8744''45'idem_3206 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny #

du_'8744''45'idem_3206 :: T_Lattice_500 -> AgdaAny -> AgdaAny #

d_'8744''45'isMagma_3210 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsMagma_176 #

du_'8744''45'isMagma_3210 :: T_Lattice_500 -> T_IsMagma_176 #

d_'8744''45'isSemigroup_3212 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsSemigroup_472 #

du_'8744''45'isSemigroup_3212 :: T_Lattice_500 -> T_IsSemigroup_472 #

d_'8744''45'isBand_3214 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsBand_508 #

du_'8744''45'isBand_3214 :: T_Lattice_500 -> T_IsBand_508 #

d_'8744''45'isSemilattice_3216 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsCommutativeBand_590 #

du_'8744''45'isSemilattice_3216 :: T_Lattice_500 -> T_IsCommutativeBand_590 #

d_'8744''45'semilattice_3218 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_Semilattice_10 #

du_'8744''45'semilattice_3218 :: T_Lattice_500 -> T_Semilattice_10 #

d_'8743''45'isOrderTheoreticJoinSemilattice_3222 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsJoinSemilattice_22 #

du_'8743''45'isOrderTheoreticJoinSemilattice_3222 :: T_Lattice_500 -> T_IsJoinSemilattice_22 #

d_'8743''45'isOrderTheoreticMeetSemilattice_3224 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsMeetSemilattice_180 #

du_'8743''45'isOrderTheoreticMeetSemilattice_3224 :: T_Lattice_500 -> T_IsMeetSemilattice_180 #

d_'8743''45'orderTheoreticJoinSemilattice_3226 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_JoinSemilattice_14 #

du_'8743''45'orderTheoreticJoinSemilattice_3226 :: T_Lattice_500 -> T_JoinSemilattice_14 #

d_'8743''45'orderTheoreticMeetSemilattice_3228 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_MeetSemilattice_200 #

du_'8743''45'orderTheoreticMeetSemilattice_3228 :: T_Lattice_500 -> T_MeetSemilattice_200 #

d_'8743''45''8744''45'isLattice_3230 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsLattice_2962 #

du_'8743''45''8744''45'isLattice_3230 :: T_Lattice_500 -> T_IsLattice_2962 #

d_'8743''45''8744''45'lattice_3232 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_Lattice_500 #

du_'8743''45''8744''45'lattice_3232 :: T_Lattice_500 -> T_Lattice_500 #

d_poset_3236 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_Poset_314 #

du_poset_3236 :: T_Lattice_500 -> T_Poset_314 #

d__'8804'__3240 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny -> () #

d_'8744''45''8743''45'isOrderTheoreticLattice_3244 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsLattice_340 #

du_'8744''45''8743''45'isOrderTheoreticLattice_3244 :: T_Lattice_500 -> T_IsLattice_340 #

d__'8804'__3256 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny -> () #

d_sound_3268 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sound_3268 :: T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_complete_3280 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_complete_3280 :: T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_supremum_3288 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Σ_14 #

du_supremum_3288 :: T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Σ_14 #

d_'8744''45''8743''45'orderTheoreticLattice_3300 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_Lattice_386 #

du_'8744''45''8743''45'orderTheoreticLattice_3300 :: T_Lattice_500 -> T_Lattice_386 #