Documentation

d__DistributesOver__80 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'691'__82 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'737'__84 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_isOrderTheoreticLattice_174 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsLattice_810 Source #

du_isOrderTheoreticLattice_174 ∷ T_DistributiveLattice_1228 → T_IsLattice_810 Source #

d_orderTheoreticLattice_176 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Lattice_898 Source #

du_orderTheoreticLattice_176 ∷ T_DistributiveLattice_1228 → T_Lattice_898 Source #

d_poset_178 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Poset_282 Source #

du_poset_178 ∷ T_DistributiveLattice_1228 → T_Poset_282 Source #

d_'8743''45'idem_180 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny Source #

du_'8743''45'idem_180 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny Source #

d_'8743''45'idempotent_182 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny Source #

du_'8743''45'idempotent_182 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny Source #

d_'8743''45'isBand_184 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsBand_230 Source #

du_'8743''45'isBand_184 ∷ T_DistributiveLattice_1228 → T_IsBand_230 Source #

d_'8743''45'isMagma_186 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsMagma_86 Source #

du_'8743''45'isMagma_186 ∷ T_DistributiveLattice_1228 → T_IsMagma_86 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_188 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsJoinSemilattice_68 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_188 ∷ T_DistributiveLattice_1228 → T_IsJoinSemilattice_68 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_190 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsMeetSemilattice_438 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_190 ∷ T_DistributiveLattice_1228 → T_IsMeetSemilattice_438 Source #

d_'8743''45'isSemigroup_192 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsSemigroup_194 Source #

du_'8743''45'isSemigroup_192 ∷ T_DistributiveLattice_1228 → T_IsSemigroup_194 Source #

d_'8743''45'isSemilattice_194 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsSemilattice_312 Source #

du_'8743''45'isSemilattice_194 ∷ T_DistributiveLattice_1228 → T_IsSemilattice_312 Source #

d_'8743''45'orderTheoreticJoinSemilattice_196 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_JoinSemilattice_170 Source #

du_'8743''45'orderTheoreticJoinSemilattice_196 ∷ T_DistributiveLattice_1228 → T_JoinSemilattice_170 Source #

d_'8743''45'orderTheoreticMeetSemilattice_198 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_MeetSemilattice_540 Source #

du_'8743''45'orderTheoreticMeetSemilattice_198 ∷ T_DistributiveLattice_1228 → T_MeetSemilattice_540 Source #

d_'8743''45'semilattice_200 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Semilattice_402 Source #

du_'8743''45'semilattice_200 ∷ T_DistributiveLattice_1228 → T_Semilattice_402 Source #

d_'8743''45''8744''45'isLattice_202 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsLattice_740 Source #

du_'8743''45''8744''45'isLattice_202 ∷ T_DistributiveLattice_1228 → T_IsLattice_740 Source #

d_'8743''45''8744''45'lattice_204 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Lattice_1144 Source #

du_'8743''45''8744''45'lattice_204 ∷ T_DistributiveLattice_1228 → T_Lattice_1144 Source #

d_'8744''45'idem_206 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny Source #

du_'8744''45'idem_206 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny Source #

d_'8744''45'idempotent_208 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny Source #

du_'8744''45'idempotent_208 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny Source #

d_'8744''45'isBand_210 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsBand_230 Source #

du_'8744''45'isBand_210 ∷ T_DistributiveLattice_1228 → T_IsBand_230 Source #

d_'8744''45'isMagma_212 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsMagma_86 Source #

du_'8744''45'isMagma_212 ∷ T_DistributiveLattice_1228 → T_IsMagma_86 Source #

d_'8743''45'isOrderTheoreticJoinSemilattice_214 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsJoinSemilattice_68 Source #

du_'8743''45'isOrderTheoreticJoinSemilattice_214 ∷ T_DistributiveLattice_1228 → T_IsJoinSemilattice_68 Source #

d_'8743''45'isOrderTheoreticMeetSemilattice_216 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsMeetSemilattice_438 Source #

du_'8743''45'isOrderTheoreticMeetSemilattice_216 ∷ T_DistributiveLattice_1228 → T_IsMeetSemilattice_438 Source #

d_'8744''45'isSemigroup_218 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsSemigroup_194 Source #

du_'8744''45'isSemigroup_218 ∷ T_DistributiveLattice_1228 → T_IsSemigroup_194 Source #

d_'8744''45'isSemilattice_220 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsSemilattice_312 Source #

du_'8744''45'isSemilattice_220 ∷ T_DistributiveLattice_1228 → T_IsSemilattice_312 Source #

d_'8743''45'orderTheoreticJoinSemilattice_222 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_JoinSemilattice_170 Source #

du_'8743''45'orderTheoreticJoinSemilattice_222 ∷ T_DistributiveLattice_1228 → T_JoinSemilattice_170 Source #

d_'8743''45'orderTheoreticMeetSemilattice_224 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_MeetSemilattice_540 Source #

du_'8743''45'orderTheoreticMeetSemilattice_224 ∷ T_DistributiveLattice_1228 → T_MeetSemilattice_540 Source #

d_'8744''45'semilattice_226 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Semilattice_402 Source #

du_'8744''45'semilattice_226 ∷ T_DistributiveLattice_1228 → T_Semilattice_402 Source #

d_'8744''45''8743''45'isOrderTheoreticLattice_228 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsLattice_810 Source #

du_'8744''45''8743''45'isOrderTheoreticLattice_228 ∷ T_DistributiveLattice_1228 → T_IsLattice_810 Source #

d_'8744''45''8743''45'orderTheoreticLattice_230 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Lattice_898 Source #

du_'8744''45''8743''45'orderTheoreticLattice_230 ∷ T_DistributiveLattice_1228 → T_Lattice_898 Source #

d_'8744''45'distrib'737''45''8743'_232 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_232 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'45''8743'_240 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Σ_14 Source #

du_'8744''45'distrib'45''8743'_240 ∷ T_DistributiveLattice_1228 → T_Σ_14 Source #

d_'8743''45'distrib'737''45''8744'_242 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_242 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'691''45''8744'_250 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_250 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8744'_258 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Σ_14 Source #

du_'8743''45'distrib'45''8744'_258 ∷ T_DistributiveLattice_1228 → T_Σ_14 Source #

d_'8743''45''8744''45'isDistributiveLattice_260 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_IsDistributiveLattice_814 Source #

du_'8743''45''8744''45'isDistributiveLattice_260 ∷ T_DistributiveLattice_1228 → T_IsDistributiveLattice_814 Source #

d_'8743''45''8744''45'distributiveLattice_262 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_DistributiveLattice_1228 Source #

du_'8743''45''8744''45'distributiveLattice_262 ∷ T_DistributiveLattice_1228 → T_DistributiveLattice_1228 Source #

d_'8744''45''8743''45'distrib'737'_264 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45''8743''45'distrib'737'_264 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45''8743''45'distrib_266 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Σ_14 Source #

du_'8744''45''8743''45'distrib_266 ∷ T_DistributiveLattice_1228 → T_Σ_14 Source #

d_'8743''45''8744''45'distrib'737'_268 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45''8744''45'distrib'737'_268 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45''8744''45'distrib'691'_270 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45''8744''45'distrib'691'_270 ∷ T_DistributiveLattice_1228 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45''8744''45'distrib_272 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → T_Σ_14 Source #

du_'8743''45''8744''45'distrib_272 ∷ T_DistributiveLattice_1228 → T_Σ_14 Source #

d_replace'45'equality_280 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_1228 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Equivalence_16) → T_DistributiveLattice_1228 Source #

du_replace'45'equality_280 ∷ T_DistributiveLattice_1228 → (AgdaAny → AgdaAny → T_Equivalence_16) → T_DistributiveLattice_1228 Source #