Documentation

d_Semilattice_10 ∷ p → p → () Source #

data T_Semilattice_10 Source #

d_Carrier_24 ∷ T_Semilattice_10 → () Source #

d__'8776'__26 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → () Source #

d__'8729'__28 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny Source #

d_isSemilattice_30 ∷ T_Semilattice_10 → T_IsCommutativeBand_612 Source #

d_assoc_34 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_34 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_36 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_38 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny Source #

du_idem_38 ∷ T_Semilattice_10 → AgdaAny → AgdaAny Source #

d_isBand_40 ∷ T_Semilattice_10 → T_IsBand_526 Source #

d_isEquivalence_42 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsEquivalence_28 Source #

du_isEquivalence_42 ∷ T_Semilattice_10 → T_IsEquivalence_28 Source #

d_isMagma_44 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsMagma_178 Source #

du_isMagma_44 ∷ T_Semilattice_10 → T_IsMagma_178 Source #

d_isPartialEquivalence_46 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_46 ∷ T_Semilattice_10 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_48 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsSemigroup_488 Source #

du_isSemigroup_48 ∷ T_Semilattice_10 → T_IsSemigroup_488 Source #

d_refl_50 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny Source #

du_refl_50 ∷ T_Semilattice_10 → AgdaAny → AgdaAny Source #

d_reflexive_52 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_52 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_54 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_Setoid_46 Source #

du_setoid_54 ∷ T_Semilattice_10 → T_Setoid_46 Source #

d_sym_56 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_56 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_58 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_58 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_60 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_60 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_62 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_62 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_64 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_64 ∷ T_Semilattice_10 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_band_66 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_Band_620 Source #

du_band_66 ∷ T_Semilattice_10 → T_Band_620 Source #

d__'8777'__70 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → AgdaAny → AgdaAny → () Source #

d_isBand_72 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsBand_526 Source #

du_isBand_72 ∷ T_Semilattice_10 → T_IsBand_526 Source #

d_isMagma_74 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsMagma_178 Source #

du_isMagma_74 ∷ T_Semilattice_10 → T_IsMagma_178 Source #

d_isSemigroup_76 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_IsSemigroup_488 Source #

du_isSemigroup_76 ∷ T_Semilattice_10 → T_IsSemigroup_488 Source #

d_magma_78 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_Magma_74 Source #

du_magma_78 ∷ T_Semilattice_10 → T_Magma_74 Source #

d_rawMagma_80 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_RawMagma_44 Source #

du_rawMagma_80 ∷ T_Semilattice_10 → T_RawMagma_44 Source #

d_semigroup_82 ∷ T_Level_18 → T_Level_18 → T_Semilattice_10 → T_Semigroup_558 Source #

du_semigroup_82 ∷ T_Semilattice_10 → T_Semigroup_558 Source #

d_MeetSemilattice_90 ∷ p → p → () Source #

data T_MeetSemilattice_90 Source #

d_Carrier_104 ∷ T_MeetSemilattice_90 → () Source #

d__'8776'__106 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny → () Source #

d__'8743'__108 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMeetSemilattice_110 ∷ T_MeetSemilattice_90 → T_IsCommutativeBand_612 Source #

d_assoc_114 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_114 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_116 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_118 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → AgdaAny → AgdaAny Source #

du_idem_118 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny Source #

d_isBand_120 ∷ T_MeetSemilattice_90 → T_IsBand_526 Source #

d_isEquivalence_122 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → T_IsEquivalence_28 Source #

du_isEquivalence_122 ∷ T_MeetSemilattice_90 → T_IsEquivalence_28 Source #

d_isMagma_124 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → T_IsMagma_178 Source #

du_isMagma_124 ∷ T_MeetSemilattice_90 → T_IsMagma_178 Source #

d_isPartialEquivalence_126 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_126 ∷ T_MeetSemilattice_90 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_128 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → T_IsSemigroup_488 Source #

du_isSemigroup_128 ∷ T_MeetSemilattice_90 → T_IsSemigroup_488 Source #

d_refl_130 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → AgdaAny → AgdaAny Source #

du_refl_130 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny Source #

d_reflexive_132 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_132 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_134 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → T_Setoid_46 Source #

du_setoid_134 ∷ T_MeetSemilattice_90 → T_Setoid_46 Source #

d_sym_136 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_136 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_138 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_138 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_140 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_140 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_142 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_142 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_144 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_144 ∷ T_MeetSemilattice_90 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semilattice_146 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → T_Semilattice_10 Source #

du_semilattice_146 ∷ T_MeetSemilattice_90 → T_Semilattice_10 Source #

d_band_150 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → T_Band_620 Source #

du_band_150 ∷ T_MeetSemilattice_90 → T_Band_620 Source #

d_magma_152 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → T_Magma_74 Source #

du_magma_152 ∷ T_MeetSemilattice_90 → T_Magma_74 Source #

d_rawMagma_154 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → T_RawMagma_44 Source #

du_rawMagma_154 ∷ T_MeetSemilattice_90 → T_RawMagma_44 Source #

d_semigroup_156 ∷ T_Level_18 → T_Level_18 → T_MeetSemilattice_90 → T_Semigroup_558 Source #

du_semigroup_156 ∷ T_MeetSemilattice_90 → T_Semigroup_558 Source #

d_JoinSemilattice_164 ∷ p → p → () Source #

data T_JoinSemilattice_164 Source #

d_Carrier_178 ∷ T_JoinSemilattice_164 → () Source #

d__'8776'__180 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny → () Source #

d__'8744'__182 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny Source #

d_isJoinSemilattice_184 ∷ T_JoinSemilattice_164 → T_IsCommutativeBand_612 Source #

d_assoc_188 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_188 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_190 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_192 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → AgdaAny → AgdaAny Source #

du_idem_192 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny Source #

d_isBand_194 ∷ T_JoinSemilattice_164 → T_IsBand_526 Source #

d_isEquivalence_196 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → T_IsEquivalence_28 Source #

du_isEquivalence_196 ∷ T_JoinSemilattice_164 → T_IsEquivalence_28 Source #

d_isMagma_198 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → T_IsMagma_178 Source #

du_isMagma_198 ∷ T_JoinSemilattice_164 → T_IsMagma_178 Source #

d_isPartialEquivalence_200 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_200 ∷ T_JoinSemilattice_164 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_202 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → T_IsSemigroup_488 Source #

du_isSemigroup_202 ∷ T_JoinSemilattice_164 → T_IsSemigroup_488 Source #

d_refl_204 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → AgdaAny → AgdaAny Source #

du_refl_204 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny Source #

d_reflexive_206 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_206 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_208 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → T_Setoid_46 Source #

du_setoid_208 ∷ T_JoinSemilattice_164 → T_Setoid_46 Source #

d_sym_210 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_210 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_212 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_212 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_214 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_214 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_216 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_216 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_218 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_218 ∷ T_JoinSemilattice_164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semilattice_220 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → T_Semilattice_10 Source #

du_semilattice_220 ∷ T_JoinSemilattice_164 → T_Semilattice_10 Source #

d_band_224 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → T_Band_620 Source #

du_band_224 ∷ T_JoinSemilattice_164 → T_Band_620 Source #

d_magma_226 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → T_Magma_74 Source #

du_magma_226 ∷ T_JoinSemilattice_164 → T_Magma_74 Source #

d_rawMagma_228 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → T_RawMagma_44 Source #

du_rawMagma_228 ∷ T_JoinSemilattice_164 → T_RawMagma_44 Source #

d_semigroup_230 ∷ T_Level_18 → T_Level_18 → T_JoinSemilattice_164 → T_Semigroup_558 Source #

du_semigroup_230 ∷ T_JoinSemilattice_164 → T_Semigroup_558 Source #

d_BoundedSemilattice_238 ∷ p → p → () Source #

data T_BoundedSemilattice_238 Source #

d_Carrier_254 ∷ T_BoundedSemilattice_238 → () Source #

d__'8776'__256 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny → () Source #

d__'8729'__258 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny → AgdaAny Source #

d_ε_260 ∷ T_BoundedSemilattice_238 → AgdaAny Source #

d_isBoundedSemilattice_262 ∷ T_BoundedSemilattice_238 → T_IsIdempotentCommutativeMonoid_884 Source #

d_assoc_266 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_268 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_270 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny Source #

d_identity_272 ∷ T_BoundedSemilattice_238 → T_Σ_14 Source #

d_identity'691'_274 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → AgdaAny → AgdaAny Source #

du_identity'691'_274 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny Source #

d_identity'737'_276 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → AgdaAny → AgdaAny Source #

du_identity'737'_276 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny Source #

d_isBand_278 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_IsBand_526 Source #

du_isBand_278 ∷ T_BoundedSemilattice_238 → T_IsBand_526 Source #

d_isCommutativeMagma_280 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_280 ∷ T_BoundedSemilattice_238 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_282 ∷ T_BoundedSemilattice_238 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_284 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_284 ∷ T_BoundedSemilattice_238 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_286 ∷ T_BoundedSemilattice_238 → T_IsEquivalence_28 Source #

d_isIdempotentMonoid_288 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_IsIdempotentMonoid_826 Source #

du_isIdempotentMonoid_288 ∷ T_BoundedSemilattice_238 → T_IsIdempotentMonoid_826 Source #

d_isMagma_290 ∷ T_BoundedSemilattice_238 → T_IsMagma_178 Source #

d_isMonoid_292 ∷ T_BoundedSemilattice_238 → T_IsMonoid_712 Source #

d_isPartialEquivalence_294 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_294 ∷ T_BoundedSemilattice_238 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_296 ∷ T_BoundedSemilattice_238 → T_IsSemigroup_488 Source #

d_isCommutativeBand_298 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_IsCommutativeBand_612 Source #

du_isCommutativeBand_298 ∷ T_BoundedSemilattice_238 → T_IsCommutativeBand_612 Source #

d_isUnitalMagma_300 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_300 ∷ T_BoundedSemilattice_238 → T_IsUnitalMagma_666 Source #

d_refl_302 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny Source #

d_reflexive_304 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_304 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_306 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_Setoid_46 Source #

du_setoid_306 ∷ T_BoundedSemilattice_238 → T_Setoid_46 Source #

d_sym_308 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_310 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_312 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_314 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_314 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_316 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_316 ∷ T_BoundedSemilattice_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_semilattice_318 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_Semilattice_10 Source #

du_semilattice_318 ∷ T_BoundedSemilattice_238 → T_Semilattice_10 Source #

d_band_322 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_Band_620 Source #

du_band_322 ∷ T_BoundedSemilattice_238 → T_Band_620 Source #

d_magma_324 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_Magma_74 Source #

du_magma_324 ∷ T_BoundedSemilattice_238 → T_Magma_74 Source #

d_rawMagma_326 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_RawMagma_44 Source #

du_rawMagma_326 ∷ T_BoundedSemilattice_238 → T_RawMagma_44 Source #

d_semigroup_328 ∷ T_Level_18 → T_Level_18 → T_BoundedSemilattice_238 → T_Semigroup_558 Source #

du_semigroup_328 ∷ T_BoundedSemilattice_238 → T_Semigroup_558 Source #

d_BoundedMeetSemilattice_336 ∷ p → p → () Source #

data T_BoundedMeetSemilattice_336 Source #

d_Carrier_352 ∷ T_BoundedMeetSemilattice_336 → () Source #

d__'8776'__354 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → () Source #

d__'8743'__356 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8868'_358 ∷ T_BoundedMeetSemilattice_336 → AgdaAny Source #

d_isBoundedMeetSemilattice_360 ∷ T_BoundedMeetSemilattice_336 → T_IsIdempotentCommutativeMonoid_884 Source #

d_assoc_364 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_364 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_366 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny Source #

du_comm_366 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_368 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny Source #

du_idem_368 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny Source #

d_identity_370 ∷ T_BoundedMeetSemilattice_336 → T_Σ_14 Source #

d_identity'691'_372 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny Source #

du_identity'691'_372 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny Source #

d_identity'737'_374 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny Source #

du_identity'737'_374 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny Source #

d_isBand_376 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_IsBand_526 Source #

du_isBand_376 ∷ T_BoundedMeetSemilattice_336 → T_IsBand_526 Source #

d_isEquivalence_378 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_IsEquivalence_28 Source #

du_isEquivalence_378 ∷ T_BoundedMeetSemilattice_336 → T_IsEquivalence_28 Source #

d_isMagma_380 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_IsMagma_178 Source #

du_isMagma_380 ∷ T_BoundedMeetSemilattice_336 → T_IsMagma_178 Source #

d_isCommutativeBand_382 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_IsCommutativeBand_612 Source #

du_isCommutativeBand_382 ∷ T_BoundedMeetSemilattice_336 → T_IsCommutativeBand_612 Source #

d_isPartialEquivalence_384 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_384 ∷ T_BoundedMeetSemilattice_336 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_386 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_IsSemigroup_488 Source #

du_isSemigroup_386 ∷ T_BoundedMeetSemilattice_336 → T_IsSemigroup_488 Source #

d_refl_388 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny Source #

du_refl_388 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny Source #

d_reflexive_390 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_390 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_392 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_Setoid_46 Source #

du_setoid_392 ∷ T_BoundedMeetSemilattice_336 → T_Setoid_46 Source #

d_sym_394 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_394 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_396 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_396 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_398 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_398 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_400 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_400 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_402 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_402 ∷ T_BoundedMeetSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedSemilattice_404 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_BoundedSemilattice_238 Source #

du_boundedSemilattice_404 ∷ T_BoundedMeetSemilattice_336 → T_BoundedSemilattice_238 Source #

d_band_408 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_Band_620 Source #

du_band_408 ∷ T_BoundedMeetSemilattice_336 → T_Band_620 Source #

d_magma_410 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_Magma_74 Source #

du_magma_410 ∷ T_BoundedMeetSemilattice_336 → T_Magma_74 Source #

d_rawMagma_412 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_RawMagma_44 Source #

du_rawMagma_412 ∷ T_BoundedMeetSemilattice_336 → T_RawMagma_44 Source #

d_semigroup_414 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_Semigroup_558 Source #

du_semigroup_414 ∷ T_BoundedMeetSemilattice_336 → T_Semigroup_558 Source #

d_semilattice_416 ∷ T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_336 → T_Semilattice_10 Source #

du_semilattice_416 ∷ T_BoundedMeetSemilattice_336 → T_Semilattice_10 Source #

d_BoundedJoinSemilattice_424 ∷ p → p → () Source #

data T_BoundedJoinSemilattice_424 Source #

d_Carrier_440 ∷ T_BoundedJoinSemilattice_424 → () Source #

d__'8776'__442 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → () Source #

d__'8744'__444 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8869'_446 ∷ T_BoundedJoinSemilattice_424 → AgdaAny Source #

d_isBoundedJoinSemilattice_448 ∷ T_BoundedJoinSemilattice_424 → T_IsIdempotentCommutativeMonoid_884 Source #

d_assoc_452 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc_452 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_454 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny Source #

du_comm_454 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny Source #

d_idem_456 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny Source #

du_idem_456 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny Source #

d_identity_458 ∷ T_BoundedJoinSemilattice_424 → T_Σ_14 Source #

d_identity'691'_460 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny Source #

du_identity'691'_460 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny Source #

d_identity'737'_462 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny Source #

du_identity'737'_462 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny Source #

d_isBand_464 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_IsBand_526 Source #

du_isBand_464 ∷ T_BoundedJoinSemilattice_424 → T_IsBand_526 Source #

d_isEquivalence_466 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_IsEquivalence_28 Source #

du_isEquivalence_466 ∷ T_BoundedJoinSemilattice_424 → T_IsEquivalence_28 Source #

d_isCommutativeBand_468 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_IsCommutativeBand_612 Source #

du_isCommutativeBand_468 ∷ T_BoundedJoinSemilattice_424 → T_IsCommutativeBand_612 Source #

d_isMagma_470 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_IsMagma_178 Source #

du_isMagma_470 ∷ T_BoundedJoinSemilattice_424 → T_IsMagma_178 Source #

d_isPartialEquivalence_472 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_472 ∷ T_BoundedJoinSemilattice_424 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_474 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_IsSemigroup_488 Source #

du_isSemigroup_474 ∷ T_BoundedJoinSemilattice_424 → T_IsSemigroup_488 Source #

d_refl_476 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny Source #

du_refl_476 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny Source #

d_reflexive_478 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_478 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_480 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_Setoid_46 Source #

du_setoid_480 ∷ T_BoundedJoinSemilattice_424 → T_Setoid_46 Source #

d_sym_482 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_482 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_484 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_484 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_486 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong_486 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_488 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_488 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_490 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_490 ∷ T_BoundedJoinSemilattice_424 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedSemilattice_492 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_BoundedSemilattice_238 Source #

du_boundedSemilattice_492 ∷ T_BoundedJoinSemilattice_424 → T_BoundedSemilattice_238 Source #

d_band_496 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_Band_620 Source #

du_band_496 ∷ T_BoundedJoinSemilattice_424 → T_Band_620 Source #

d_magma_498 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_Magma_74 Source #

du_magma_498 ∷ T_BoundedJoinSemilattice_424 → T_Magma_74 Source #

d_rawMagma_500 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_RawMagma_44 Source #

du_rawMagma_500 ∷ T_BoundedJoinSemilattice_424 → T_RawMagma_44 Source #

d_semigroup_502 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_Semigroup_558 Source #

du_semigroup_502 ∷ T_BoundedJoinSemilattice_424 → T_Semigroup_558 Source #

d_semilattice_504 ∷ T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_424 → T_Semilattice_10 Source #

du_semilattice_504 ∷ T_BoundedJoinSemilattice_424 → T_Semilattice_10 Source #

d_Lattice_512 ∷ p → p → () Source #

data T_Lattice_512 Source #

d_Carrier_528 ∷ T_Lattice_512 → () Source #

d__'8776'__530 ∷ T_Lattice_512 → AgdaAny → AgdaAny → () Source #

d__'8744'__532 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__534 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny Source #

d_isLattice_536 ∷ T_Lattice_512 → T_IsLattice_3070 Source #

d_absorptive_540 ∷ T_Lattice_512 → T_Σ_14 Source #

d_isEquivalence_542 ∷ T_Lattice_512 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_544 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_544 ∷ T_Lattice_512 → T_IsPartialEquivalence_16 Source #

d_refl_546 ∷ T_Lattice_512 → AgdaAny → AgdaAny Source #

d_reflexive_548 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_548 ∷ T_Lattice_512 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_550 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_552 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_554 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_554 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_556 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_558 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_560 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_562 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_562 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_564 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_564 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_566 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_566 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_568 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_570 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_572 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_574 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_574 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_576 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_576 ∷ T_Lattice_512 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_rawLattice_578 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_RawLattice_12 Source #

du_rawLattice_578 ∷ T_Lattice_512 → T_RawLattice_12 Source #

d_'8743''45'rawMagma_582 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_RawMagma_44 Source #

du_'8743''45'rawMagma_582 ∷ T_Lattice_512 → T_RawMagma_44 Source #

d_'8744''45'rawMagma_584 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_RawMagma_44 Source #

du_'8744''45'rawMagma_584 ∷ T_Lattice_512 → T_RawMagma_44 Source #

d_setoid_586 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → T_Setoid_46 Source #

du_setoid_586 ∷ T_Lattice_512 → T_Setoid_46 Source #

d__'8777'__590 ∷ T_Level_18 → T_Level_18 → T_Lattice_512 → AgdaAny → AgdaAny → () Source #

d_DistributiveLattice_598 ∷ p → p → () Source #

data T_DistributiveLattice_598 Source #

d_Carrier_614 ∷ T_DistributiveLattice_598 → () Source #

d__'8776'__616 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → () Source #

d__'8744'__618 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__620 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny Source #

d_isDistributiveLattice_622 ∷ T_DistributiveLattice_598 → T_IsDistributiveLattice_3146 Source #

d_absorptive_626 ∷ T_DistributiveLattice_598 → T_Σ_14 Source #

d_isEquivalence_628 ∷ T_DistributiveLattice_598 → T_IsEquivalence_28 Source #

d_isLattice_630 ∷ T_DistributiveLattice_598 → T_IsLattice_3070 Source #

d_isPartialEquivalence_632 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_632 ∷ T_DistributiveLattice_598 → T_IsPartialEquivalence_16 Source #

d_refl_634 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny Source #

d_reflexive_636 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_636 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_638 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_640 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_642 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_642 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_644 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_646 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong_648 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_650 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_650 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_652 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_652 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8744'_654 ∷ T_DistributiveLattice_598 → T_Σ_14 Source #

d_'8743''45'distrib'691''45''8744'_656 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_656 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_658 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_658 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_660 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_660 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_662 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_664 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong_666 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_668 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_668 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_670 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_670 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'45''8743'_672 ∷ T_DistributiveLattice_598 → T_Σ_14 Source #

d_'8744''45'distrib'691''45''8743'_674 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_674 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_676 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_676 ∷ T_DistributiveLattice_598 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lattice_678 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_Lattice_512 Source #

du_lattice_678 ∷ T_DistributiveLattice_598 → T_Lattice_512 Source #

d__'8777'__682 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → AgdaAny → AgdaAny → () Source #

d_rawLattice_684 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_RawLattice_12 Source #

du_rawLattice_684 ∷ T_DistributiveLattice_598 → T_RawLattice_12 Source #

d_setoid_686 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_Setoid_46 Source #

du_setoid_686 ∷ T_DistributiveLattice_598 → T_Setoid_46 Source #

d_'8743''45'rawMagma_688 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_RawMagma_44 Source #

du_'8743''45'rawMagma_688 ∷ T_DistributiveLattice_598 → T_RawMagma_44 Source #

d_'8744''45'rawMagma_690 ∷ T_Level_18 → T_Level_18 → T_DistributiveLattice_598 → T_RawMagma_44 Source #

du_'8744''45'rawMagma_690 ∷ T_DistributiveLattice_598 → T_RawMagma_44 Source #

d_BooleanAlgebra_698 ∷ p → p → () Source #

data T_BooleanAlgebra_698 Source #

d_Carrier_720 ∷ T_BooleanAlgebra_698 → () Source #

d__'8776'__722 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → () Source #

d__'8744'__724 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__726 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172'__728 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8868'_730 ∷ T_BooleanAlgebra_698 → AgdaAny Source #

d_'8869'_732 ∷ T_BooleanAlgebra_698 → AgdaAny Source #

d_isBooleanAlgebra_734 ∷ T_BooleanAlgebra_698 → T_IsBooleanAlgebra_3224 Source #

d_absorptive_738 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_isDistributiveLattice_740 ∷ T_BooleanAlgebra_698 → T_IsDistributiveLattice_3146 Source #

d_isEquivalence_742 ∷ T_BooleanAlgebra_698 → T_IsEquivalence_28 Source #

d_isLattice_744 ∷ T_BooleanAlgebra_698 → T_IsLattice_3070 Source #

d_isPartialEquivalence_746 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_746 ∷ T_BooleanAlgebra_698 → T_IsPartialEquivalence_16 Source #

d_refl_748 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_reflexive_750 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_750 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_752 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_754 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'172''45'cong_756 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'absorbs'45''8744'_758 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'absorbs'45''8744'_758 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'assoc_760 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'comm_762 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'complement_764 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8743''45'complement'691'_766 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8743''45'complement'691'_766 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8743''45'complement'737'_768 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8743''45'complement'737'_768 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8743''45'cong_770 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'691'_772 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'691'_772 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'cong'737'_774 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'cong'737'_774 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'45''8744'_776 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8743''45'distrib'691''45''8744'_778 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'691''45''8744'_778 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'distrib'737''45''8744'_780 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'distrib'737''45''8744'_780 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'absorbs'45''8743'_782 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'absorbs'45''8743'_782 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'assoc_784 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'comm_786 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'complement_788 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8744''45'complement'691'_790 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8744''45'complement'691'_790 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8744''45'complement'737'_792 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

du_'8744''45'complement'737'_792 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny Source #

d_'8744''45'cong_794 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'691'_796 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'691'_796 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'cong'737'_798 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'cong'737'_798 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'45''8743'_800 ∷ T_BooleanAlgebra_698 → T_Σ_14 Source #

d_'8744''45'distrib'691''45''8743'_802 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'691''45''8743'_802 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'distrib'737''45''8743'_804 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'distrib'737''45''8743'_804 ∷ T_BooleanAlgebra_698 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distributiveLattice_806 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_DistributiveLattice_598 Source #

du_distributiveLattice_806 ∷ T_BooleanAlgebra_698 → T_DistributiveLattice_598 Source #

d__'8777'__810 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → AgdaAny → AgdaAny → () Source #

d_lattice_812 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Lattice_512 Source #

du_lattice_812 ∷ T_BooleanAlgebra_698 → T_Lattice_512 Source #

d_rawLattice_814 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_RawLattice_12 Source #

du_rawLattice_814 ∷ T_BooleanAlgebra_698 → T_RawLattice_12 Source #

d_setoid_816 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_Setoid_46 Source #

du_setoid_816 ∷ T_BooleanAlgebra_698 → T_Setoid_46 Source #

d_'8743''45'rawMagma_818 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_RawMagma_44 Source #

du_'8743''45'rawMagma_818 ∷ T_BooleanAlgebra_698 → T_RawMagma_44 Source #

d_'8744''45'rawMagma_820 ∷ T_Level_18 → T_Level_18 → T_BooleanAlgebra_698 → T_RawMagma_44 Source #

du_'8744''45'rawMagma_820 ∷ T_BooleanAlgebra_698 → T_RawMagma_44 Source #