Documentation

d_Idempotent_78 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsBand_82 ∷ p → p → p → p → () Source #

d_IsMagma_86 ∷ p → p → p → p → () Source #

d_IsSemigroup_90 ∷ p → p → p → p → () Source #

d_idem_98 ∷ T_IsBand_526 → AgdaAny → AgdaAny Source #

d_isSemigroup_106 ∷ T_IsBand_526 → T_IsSemigroup_488 Source #

d_isEquivalence_126 ∷ T_IsMagma_178 → T_IsEquivalence_28 Source #

d_'8729''45'cong_140 ∷ T_IsMagma_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_148 ∷ T_IsSemigroup_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isMagma_152 ∷ T_IsSemigroup_488 → T_IsMagma_178 Source #

d_IsLattice_174 ∷ p → p → p → p → p → () Source #

d_IsSemilattice_178 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_absorptive_182 ∷ T_IsLattice_3070 → T_Σ_14 Source #

d_isEquivalence_184 ∷ T_IsLattice_3070 → T_IsEquivalence_28 Source #

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

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

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

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

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

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

d_'8743''45'idem_294 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny Source #

du_'8743''45'idem_294 ∷ T_Lattice_512 → AgdaAny → AgdaAny Source #

d_'8743''45'isMagma_298 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsMagma_178 Source #

du_'8743''45'isMagma_298 ∷ T_Lattice_512 → T_IsMagma_178 Source #

d_'8743''45'isSemigroup_300 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsSemigroup_488 Source #

du_'8743''45'isSemigroup_300 ∷ T_Lattice_512 → T_IsSemigroup_488 Source #

d_'8743''45'isBand_302 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsBand_526 Source #

du_'8743''45'isBand_302 ∷ T_Lattice_512 → T_IsBand_526 Source #

d_'8743''45'isSemilattice_304 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsCommutativeBand_612 Source #

du_'8743''45'isSemilattice_304 ∷ T_Lattice_512 → T_IsCommutativeBand_612 Source #

d_'8743''45'semilattice_306 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_Semilattice_10 Source #

du_'8743''45'semilattice_306 ∷ T_Lattice_512 → T_Semilattice_10 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_310 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_310 ∷ T_Lattice_512 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_312 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsMeetSemilattice_184 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_312 ∷ T_Lattice_512 → T_IsMeetSemilattice_184 Source #

d_'8743''45'orderTheoreticJoinSemilattice_314 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_314 ∷ T_Lattice_512 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_316 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_MeetSemilattice_204 Source #

du_'8743''45'orderTheoreticMeetSemilattice_316 ∷ T_Lattice_512 → T_MeetSemilattice_204 Source #

d_'8744''45'idem_318 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny Source #

du_'8744''45'idem_318 ∷ T_Lattice_512 → AgdaAny → AgdaAny Source #

d_'8744''45'isMagma_322 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsMagma_178 Source #

du_'8744''45'isMagma_322 ∷ T_Lattice_512 → T_IsMagma_178 Source #

d_'8744''45'isSemigroup_324 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsSemigroup_488 Source #

du_'8744''45'isSemigroup_324 ∷ T_Lattice_512 → T_IsSemigroup_488 Source #

d_'8744''45'isBand_326 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsBand_526 Source #

du_'8744''45'isBand_326 ∷ T_Lattice_512 → T_IsBand_526 Source #

d_'8744''45'isSemilattice_328 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsCommutativeBand_612 Source #

du_'8744''45'isSemilattice_328 ∷ T_Lattice_512 → T_IsCommutativeBand_612 Source #

d_'8744''45'semilattice_330 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_Semilattice_10 Source #

du_'8744''45'semilattice_330 ∷ T_Lattice_512 → T_Semilattice_10 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_334 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsJoinSemilattice_22 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_334 ∷ T_Lattice_512 → T_IsJoinSemilattice_22 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_336 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsMeetSemilattice_184 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_336 ∷ T_Lattice_512 → T_IsMeetSemilattice_184 Source #

d_'8743''45'orderTheoreticJoinSemilattice_338 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_JoinSemilattice_14 Source #

du_'8743''45'orderTheoreticJoinSemilattice_338 ∷ T_Lattice_512 → T_JoinSemilattice_14 Source #

d_'8743''45'orderTheoreticMeetSemilattice_340 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_MeetSemilattice_204 Source #

du_'8743''45'orderTheoreticMeetSemilattice_340 ∷ T_Lattice_512 → T_MeetSemilattice_204 Source #

d_'8743''45''8744''45'isLattice_342 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsLattice_3070 Source #

du_'8743''45''8744''45'isLattice_342 ∷ T_Lattice_512 → T_IsLattice_3070 Source #

d_'8743''45''8744''45'lattice_344 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_Lattice_512 Source #

du_'8743''45''8744''45'lattice_344 ∷ T_Lattice_512 → T_Lattice_512 Source #

d_poset_348 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_Poset_492 Source #

du_poset_348 ∷ T_Lattice_512 → T_Poset_492 Source #

d__'8804'__352 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → () Source #

d_'8744''45''8743''45'isOrderTheoreticLattice_356 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsLattice_348 Source #

du_'8744''45''8743''45'isOrderTheoreticLattice_356 ∷ T_Lattice_512 → T_IsLattice_348 Source #

d__'8804'__368 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → () Source #

d_sound_380 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sound_380 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_complete_392 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_complete_392 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_400 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_supremum_400 ∷ T_Lattice_512 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_'8744''45''8743''45'orderTheoreticLattice_412 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_Lattice_394 Source #

du_'8744''45''8743''45'orderTheoreticLattice_412 ∷ T_Lattice_512 → T_Lattice_394 Source #