Documentation

d_JoinSemilattice_14 ∷ p → p → p → () Source #

data T_JoinSemilattice_14 Source #

d_Carrier_32 ∷ T_JoinSemilattice_14 → () Source #

d__'8776'__34 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → () Source #

d__'8804'__36 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → () Source #

d__'8744'__38 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny Source #

d_isJoinSemilattice_40 ∷ T_JoinSemilattice_14 → T_IsJoinSemilattice_22 Source #

d_antisym_44 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_46 ∷ T_JoinSemilattice_14 → T_IsEquivalence_28 Source #

d_isPartialOrder_48 ∷ T_JoinSemilattice_14 → T_IsPartialOrder_248 Source #

d_isPreorder_50 ∷ T_JoinSemilattice_14 → T_IsPreorder_76 Source #

d_refl_52 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → AgdaAny → AgdaAny Source #

du_refl_52 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny Source #

d_reflexive_54 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_56 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_58 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_60 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_60 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_62 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_62 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_64 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_64 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_66 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_66 ∷ T_JoinSemilattice_14 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_68 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_68 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_70 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_70 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_72 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_72 ∷ T_JoinSemilattice_14 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_74 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_74 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_76 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_76 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_80 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_80 ∷ T_JoinSemilattice_14 → T_IsPartialEquivalence_16 Source #

d_refl_82 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny Source #

d_reflexive_84 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_84 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_86 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_88 ∷ T_JoinSemilattice_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_poset_90 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → T_Poset_492 Source #

du_poset_90 ∷ T_JoinSemilattice_14 → T_Poset_492 Source #

d_preorder_94 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → T_Preorder_142 Source #

du_preorder_94 ∷ T_JoinSemilattice_14 → T_Preorder_142 Source #

d_BoundedJoinSemilattice_104 ∷ p → p → p → () Source #

data T_BoundedJoinSemilattice_104 Source #

d_Carrier_124 ∷ T_BoundedJoinSemilattice_104 → () Source #

d__'8776'__126 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → () Source #

d__'8804'__128 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → () Source #

d__'8744'__130 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8869'_132 ∷ T_BoundedJoinSemilattice_104 → AgdaAny Source #

d_isBoundedJoinSemilattice_134 ∷ T_BoundedJoinSemilattice_104 → T_IsBoundedJoinSemilattice_118 Source #

d_antisym_138 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_140 ∷ T_BoundedJoinSemilattice_104 → T_IsEquivalence_28 Source #

d_isJoinSemilattice_142 ∷ T_BoundedJoinSemilattice_104 → T_IsJoinSemilattice_22 Source #

d_isPartialOrder_144 ∷ T_BoundedJoinSemilattice_104 → T_IsPartialOrder_248 Source #

d_isPreorder_146 ∷ T_BoundedJoinSemilattice_104 → T_IsPreorder_76 Source #

d_minimum_148 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny Source #

d_refl_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny Source #

du_refl_150 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny Source #

d_reflexive_152 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_154 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_156 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_158 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_160 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_162 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_164 ∷ T_BoundedJoinSemilattice_104 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_166 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_168 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_170 ∷ T_BoundedJoinSemilattice_104 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_172 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_174 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_174 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_178 ∷ T_BoundedJoinSemilattice_104 → T_IsPartialEquivalence_16 Source #

d_refl_180 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny Source #

d_reflexive_182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_182 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_184 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_186 ∷ T_BoundedJoinSemilattice_104 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_joinSemilattice_188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → T_JoinSemilattice_14 Source #

du_joinSemilattice_188 ∷ T_BoundedJoinSemilattice_104 → T_JoinSemilattice_14 Source #

d_poset_192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → T_Poset_492 Source #

du_poset_192 ∷ T_BoundedJoinSemilattice_104 → T_Poset_492 Source #

d_preorder_194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_104 → T_Preorder_142 Source #

du_preorder_194 ∷ T_BoundedJoinSemilattice_104 → T_Preorder_142 Source #

d_MeetSemilattice_204 ∷ p → p → p → () Source #

data T_MeetSemilattice_204 Source #

d_Carrier_222 ∷ T_MeetSemilattice_204 → () Source #

d__'8776'__224 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → () Source #

d__'8804'__226 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → () Source #

d__'8743'__228 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMeetSemilattice_230 ∷ T_MeetSemilattice_204 → T_IsMeetSemilattice_184 Source #

d_antisym_234 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_236 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_238 ∷ T_MeetSemilattice_204 → T_IsEquivalence_28 Source #

d_isPartialOrder_240 ∷ T_MeetSemilattice_204 → T_IsPartialOrder_248 Source #

d_isPreorder_242 ∷ T_MeetSemilattice_204 → T_IsPreorder_76 Source #

d_refl_244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → AgdaAny → AgdaAny Source #

du_refl_244 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny Source #

d_reflexive_246 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_248 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_250 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_250 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_252 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_252 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_254 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_256 ∷ T_MeetSemilattice_204 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_258 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_260 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_262 ∷ T_MeetSemilattice_204 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_264 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_266 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_270 ∷ T_MeetSemilattice_204 → T_IsPartialEquivalence_16 Source #

d_refl_272 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny Source #

d_reflexive_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_274 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_276 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_278 ∷ T_MeetSemilattice_204 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_poset_280 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → T_Poset_492 Source #

du_poset_280 ∷ T_MeetSemilattice_204 → T_Poset_492 Source #

d_preorder_284 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_204 → T_Preorder_142 Source #

du_preorder_284 ∷ T_MeetSemilattice_204 → T_Preorder_142 Source #

d_BoundedMeetSemilattice_294 ∷ p → p → p → () Source #

data T_BoundedMeetSemilattice_294 Source #

d_Carrier_314 ∷ T_BoundedMeetSemilattice_294 → () Source #

d__'8776'__316 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → () Source #

d__'8804'__318 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → () Source #

d__'8743'__320 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8868'_322 ∷ T_BoundedMeetSemilattice_294 → AgdaAny Source #

d_isBoundedMeetSemilattice_324 ∷ T_BoundedMeetSemilattice_294 → T_IsBoundedMeetSemilattice_280 Source #

d_antisym_328 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_330 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_332 ∷ T_BoundedMeetSemilattice_294 → T_IsEquivalence_28 Source #

d_isMeetSemilattice_334 ∷ T_BoundedMeetSemilattice_294 → T_IsMeetSemilattice_184 Source #

d_isPartialOrder_336 ∷ T_BoundedMeetSemilattice_294 → T_IsPartialOrder_248 Source #

d_isPreorder_338 ∷ T_BoundedMeetSemilattice_294 → T_IsPreorder_76 Source #

d_maximum_340 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny Source #

d_refl_342 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny Source #

du_refl_342 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny Source #

d_reflexive_344 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_346 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_348 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_348 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_350 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_350 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_352 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_352 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_354 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_354 ∷ T_BoundedMeetSemilattice_294 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_356 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_356 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_358 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_358 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_360 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_360 ∷ T_BoundedMeetSemilattice_294 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_362 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_362 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_364 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_364 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_368 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_368 ∷ T_BoundedMeetSemilattice_294 → T_IsPartialEquivalence_16 Source #

d_refl_370 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny Source #

d_reflexive_372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_372 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_374 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_376 ∷ T_BoundedMeetSemilattice_294 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_meetSemilattice_378 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → T_MeetSemilattice_204 Source #

du_meetSemilattice_378 ∷ T_BoundedMeetSemilattice_294 → T_MeetSemilattice_204 Source #

d_poset_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → T_Poset_492 Source #

du_poset_382 ∷ T_BoundedMeetSemilattice_294 → T_Poset_492 Source #

d_preorder_384 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_294 → T_Preorder_142 Source #

du_preorder_384 ∷ T_BoundedMeetSemilattice_294 → T_Preorder_142 Source #

d_Lattice_394 ∷ p → p → p → () Source #

data T_Lattice_394 Source #

d_Carrier_414 ∷ T_Lattice_394 → () Source #

d__'8776'__416 ∷ T_Lattice_394 → AgdaAny → AgdaAny → () Source #

d__'8804'__418 ∷ T_Lattice_394 → AgdaAny → AgdaAny → () Source #

d__'8744'__420 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__422 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny Source #

d_isLattice_424 ∷ T_Lattice_394 → T_IsLattice_348 Source #

d_antisym_428 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_430 ∷ T_Lattice_394 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_432 ∷ T_Lattice_394 → T_IsEquivalence_28 Source #

d_isJoinSemilattice_434 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_434 ∷ T_Lattice_394 → T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_436 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → T_IsMeetSemilattice_184 Source #

du_isMeetSemilattice_436 ∷ T_Lattice_394 → T_IsMeetSemilattice_184 Source #

d_isPartialOrder_438 ∷ T_Lattice_394 → T_IsPartialOrder_248 Source #

d_isPreorder_440 ∷ T_Lattice_394 → T_IsPreorder_76 Source #

d_refl_442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny Source #

du_refl_442 ∷ T_Lattice_394 → AgdaAny → AgdaAny Source #

d_reflexive_444 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_446 ∷ T_Lattice_394 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_448 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_450 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_450 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_452 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_452 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_454 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_454 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_456 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_456 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_458 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_460 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_462 ∷ T_Lattice_394 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_464 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_464 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_466 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_466 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_468 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_468 ∷ T_Lattice_394 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_470 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_470 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_472 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_472 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_476 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_476 ∷ T_Lattice_394 → T_IsPartialEquivalence_16 Source #

d_refl_478 ∷ T_Lattice_394 → AgdaAny → AgdaAny Source #

d_reflexive_480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_480 ∷ T_Lattice_394 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_482 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_484 ∷ T_Lattice_394 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_486 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → T_Setoid_46 Source #

du_setoid_486 ∷ T_Lattice_394 → T_Setoid_46 Source #

d_joinSemilattice_488 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → T_JoinSemilattice_14 Source #

du_joinSemilattice_488 ∷ T_Lattice_394 → T_JoinSemilattice_14 Source #

d_meetSemilattice_490 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → T_MeetSemilattice_204 Source #

du_meetSemilattice_490 ∷ T_Lattice_394 → T_MeetSemilattice_204 Source #

d_poset_494 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → T_Poset_492 Source #

du_poset_494 ∷ T_Lattice_394 → T_Poset_492 Source #

d_preorder_496 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_394 → T_Preorder_142 Source #

du_preorder_496 ∷ T_Lattice_394 → T_Preorder_142 Source #

d_DistributiveLattice_506 ∷ p → p → p → () Source #

data T_DistributiveLattice_506 Source #

d_Carrier_526 ∷ T_DistributiveLattice_506 → () Source #

d__'8776'__528 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → () Source #

d__'8804'__530 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → () Source #

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

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

d_isDistributiveLattice_536 ∷ T_DistributiveLattice_506 → T_IsDistributiveLattice_430 Source #

d_'8743''45'distrib'737''45''8744'_540 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lattice_546 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_Lattice_394 Source #

du_lattice_546 ∷ T_DistributiveLattice_506 → T_Lattice_394 Source #

d_antisym_550 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_550 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_infimum_552 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_554 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_IsEquivalence_28 Source #

du_isEquivalence_554 ∷ T_DistributiveLattice_506 → T_IsEquivalence_28 Source #

d_isJoinSemilattice_556 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_556 ∷ T_DistributiveLattice_506 → T_IsJoinSemilattice_22 Source #

d_isLattice_558 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_IsLattice_348 Source #

du_isLattice_558 ∷ T_DistributiveLattice_506 → T_IsLattice_348 Source #

d_isMeetSemilattice_560 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_IsMeetSemilattice_184 Source #

du_isMeetSemilattice_560 ∷ T_DistributiveLattice_506 → T_IsMeetSemilattice_184 Source #

d_isPartialOrder_562 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_IsPartialOrder_248 Source #

du_isPartialOrder_562 ∷ T_DistributiveLattice_506 → T_IsPartialOrder_248 Source #

d_isPreorder_564 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_IsPreorder_76 Source #

du_isPreorder_564 ∷ T_DistributiveLattice_506 → T_IsPreorder_76 Source #

d_joinSemilattice_566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_JoinSemilattice_14 Source #

du_joinSemilattice_566 ∷ T_DistributiveLattice_506 → T_JoinSemilattice_14 Source #

d_meetSemilattice_568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_MeetSemilattice_204 Source #

du_meetSemilattice_568 ∷ T_DistributiveLattice_506 → T_MeetSemilattice_204 Source #

d_poset_570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_Poset_492 Source #

du_poset_570 ∷ T_DistributiveLattice_506 → T_Poset_492 Source #

d_preorder_572 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_Preorder_142 Source #

du_preorder_572 ∷ T_DistributiveLattice_506 → T_Preorder_142 Source #

d_refl_574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny Source #

du_refl_574 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny Source #

d_reflexive_576 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_576 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_578 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_Setoid_46 Source #

du_setoid_578 ∷ T_DistributiveLattice_506 → T_Setoid_46 Source #

d_supremum_580 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_supremum_580 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_582 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_584 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_584 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_586 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_588 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_588 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_590 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_590 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_592 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_592 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_594 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_596 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_596 ∷ T_DistributiveLattice_506 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_598 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_598 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_600 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_600 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_602 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_602 ∷ T_DistributiveLattice_506 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_604 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_604 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_606 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_606 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_610 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_610 ∷ T_DistributiveLattice_506 → T_IsPartialEquivalence_16 Source #

d_refl_612 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny Source #

du_refl_612 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny Source #

d_reflexive_614 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_614 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_616 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_616 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_618 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_618 ∷ T_DistributiveLattice_506 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_BoundedLattice_628 ∷ p → p → p → () Source #

data T_BoundedLattice_628 Source #

d_Carrier_652 ∷ T_BoundedLattice_628 → () Source #

d__'8776'__654 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → () Source #

d__'8804'__656 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → () Source #

d__'8744'__658 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__660 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8868'_662 ∷ T_BoundedLattice_628 → AgdaAny Source #

d_'8869'_664 ∷ T_BoundedLattice_628 → AgdaAny Source #

d_isBoundedLattice_666 ∷ T_BoundedLattice_628 → T_IsBoundedLattice_514 Source #

d_antisym_670 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_672 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_674 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_IsBoundedJoinSemilattice_118 Source #

du_isBoundedJoinSemilattice_674 ∷ T_BoundedLattice_628 → T_IsBoundedJoinSemilattice_118 Source #

d_isBoundedMeetSemilattice_676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_IsBoundedMeetSemilattice_280 Source #

du_isBoundedMeetSemilattice_676 ∷ T_BoundedLattice_628 → T_IsBoundedMeetSemilattice_280 Source #

d_isEquivalence_678 ∷ T_BoundedLattice_628 → T_IsEquivalence_28 Source #

d_isJoinSemilattice_680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_680 ∷ T_BoundedLattice_628 → T_IsJoinSemilattice_22 Source #

d_isLattice_682 ∷ T_BoundedLattice_628 → T_IsLattice_348 Source #

d_isMeetSemilattice_684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_IsMeetSemilattice_184 Source #

du_isMeetSemilattice_684 ∷ T_BoundedLattice_628 → T_IsMeetSemilattice_184 Source #

d_isPartialOrder_686 ∷ T_BoundedLattice_628 → T_IsPartialOrder_248 Source #

d_isPreorder_688 ∷ T_BoundedLattice_628 → T_IsPreorder_76 Source #

d_maximum_690 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny Source #

d_minimum_692 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny Source #

d_refl_694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny Source #

du_refl_694 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny Source #

d_reflexive_696 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_698 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_700 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_702 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_704 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_706 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_708 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_708 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_710 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_712 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_714 ∷ T_BoundedLattice_628 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_716 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_718 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_718 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_720 ∷ T_BoundedLattice_628 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_722 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_724 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_724 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_728 ∷ T_BoundedLattice_628 → T_IsPartialEquivalence_16 Source #

d_refl_730 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny Source #

d_reflexive_732 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_732 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_734 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_736 ∷ T_BoundedLattice_628 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedJoinSemilattice_738 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_BoundedJoinSemilattice_104 Source #

du_boundedJoinSemilattice_738 ∷ T_BoundedLattice_628 → T_BoundedJoinSemilattice_104 Source #

d_boundedMeetSemilattice_740 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_BoundedMeetSemilattice_294 Source #

du_boundedMeetSemilattice_740 ∷ T_BoundedLattice_628 → T_BoundedMeetSemilattice_294 Source #

d_lattice_742 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_Lattice_394 Source #

du_lattice_742 ∷ T_BoundedLattice_628 → T_Lattice_394 Source #

d_joinSemilattice_746 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_JoinSemilattice_14 Source #

du_joinSemilattice_746 ∷ T_BoundedLattice_628 → T_JoinSemilattice_14 Source #

d_meetSemilattice_748 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_MeetSemilattice_204 Source #

du_meetSemilattice_748 ∷ T_BoundedLattice_628 → T_MeetSemilattice_204 Source #

d_poset_750 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_Poset_492 Source #

du_poset_750 ∷ T_BoundedLattice_628 → T_Poset_492 Source #

d_preorder_752 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_Preorder_142 Source #

du_preorder_752 ∷ T_BoundedLattice_628 → T_Preorder_142 Source #

d_setoid_754 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_628 → T_Setoid_46 Source #

du_setoid_754 ∷ T_BoundedLattice_628 → T_Setoid_46 Source #

d_HeytingAlgebra_764 ∷ p → p → p → () Source #

data T_HeytingAlgebra_764 Source #

d_Carrier_790 ∷ T_HeytingAlgebra_764 → () Source #

d__'8776'__792 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → () Source #

d__'8804'__794 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → () Source #

d__'8744'__796 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__798 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8680'__800 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8868'_802 ∷ T_HeytingAlgebra_764 → AgdaAny Source #

d_'8869'_804 ∷ T_HeytingAlgebra_764 → AgdaAny Source #

d_isHeytingAlgebra_806 ∷ T_HeytingAlgebra_764 → T_IsHeytingAlgebra_612 Source #

d_boundedLattice_808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_BoundedLattice_628 Source #

du_boundedLattice_808 ∷ T_HeytingAlgebra_764 → T_BoundedLattice_628 Source #

d_exponential_812 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_transpose'45''8680'_814 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8680'_814 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8743'_816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8743'_816 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_820 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedJoinSemilattice_822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_BoundedJoinSemilattice_104 Source #

du_boundedJoinSemilattice_822 ∷ T_HeytingAlgebra_764 → T_BoundedJoinSemilattice_104 Source #

d_boundedMeetSemilattice_824 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_BoundedMeetSemilattice_294 Source #

du_boundedMeetSemilattice_824 ∷ T_HeytingAlgebra_764 → T_BoundedMeetSemilattice_294 Source #

d_infimum_826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_infimum_826 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_828 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_IsBoundedJoinSemilattice_118 Source #

du_isBoundedJoinSemilattice_828 ∷ T_HeytingAlgebra_764 → T_IsBoundedJoinSemilattice_118 Source #

d_isBoundedLattice_830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_IsBoundedLattice_514 Source #

du_isBoundedLattice_830 ∷ T_HeytingAlgebra_764 → T_IsBoundedLattice_514 Source #

d_isBoundedMeetSemilattice_832 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_IsBoundedMeetSemilattice_280 Source #

du_isBoundedMeetSemilattice_832 ∷ T_HeytingAlgebra_764 → T_IsBoundedMeetSemilattice_280 Source #

d_isEquivalence_834 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_IsEquivalence_28 Source #

du_isEquivalence_834 ∷ T_HeytingAlgebra_764 → T_IsEquivalence_28 Source #

d_isJoinSemilattice_836 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_836 ∷ T_HeytingAlgebra_764 → T_IsJoinSemilattice_22 Source #

d_isLattice_838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_IsLattice_348 Source #

du_isLattice_838 ∷ T_HeytingAlgebra_764 → T_IsLattice_348 Source #

d_isMeetSemilattice_840 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_IsMeetSemilattice_184 Source #

du_isMeetSemilattice_840 ∷ T_HeytingAlgebra_764 → T_IsMeetSemilattice_184 Source #

d_isPartialOrder_842 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_IsPartialOrder_248 Source #

du_isPartialOrder_842 ∷ T_HeytingAlgebra_764 → T_IsPartialOrder_248 Source #

d_isPreorder_844 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_IsPreorder_76 Source #

du_isPreorder_844 ∷ T_HeytingAlgebra_764 → T_IsPreorder_76 Source #

d_joinSemilattice_846 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_JoinSemilattice_14 Source #

du_joinSemilattice_846 ∷ T_HeytingAlgebra_764 → T_JoinSemilattice_14 Source #

d_lattice_848 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_Lattice_394 Source #

du_lattice_848 ∷ T_HeytingAlgebra_764 → T_Lattice_394 Source #

d_maximum_850 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny Source #

du_maximum_850 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny Source #

d_meetSemilattice_852 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_MeetSemilattice_204 Source #

du_meetSemilattice_852 ∷ T_HeytingAlgebra_764 → T_MeetSemilattice_204 Source #

d_minimum_854 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny Source #

du_minimum_854 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny Source #

d_poset_856 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_Poset_492 Source #

du_poset_856 ∷ T_HeytingAlgebra_764 → T_Poset_492 Source #

d_preorder_858 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_Preorder_142 Source #

du_preorder_858 ∷ T_HeytingAlgebra_764 → T_Preorder_142 Source #

d_refl_860 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny Source #

du_refl_860 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny Source #

d_reflexive_862 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_862 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_864 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_Setoid_46 Source #

du_setoid_864 ∷ T_HeytingAlgebra_764 → T_Setoid_46 Source #

d_supremum_866 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_supremum_866 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_868 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_868 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_870 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_870 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_872 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_872 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_874 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_874 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_876 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_876 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_878 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_878 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_880 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_880 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_882 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_882 ∷ T_HeytingAlgebra_764 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_884 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_884 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_886 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_886 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_888 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_888 ∷ T_HeytingAlgebra_764 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_890 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_890 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_892 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_892 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_896 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_896 ∷ T_HeytingAlgebra_764 → T_IsPartialEquivalence_16 Source #

d_refl_898 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny Source #

du_refl_898 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny Source #

d_reflexive_900 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_900 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_902 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_902 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_904 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_904 ∷ T_HeytingAlgebra_764 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_BooleanAlgebra_914 ∷ p → p → p → () Source #

data T_BooleanAlgebra_914 Source #

d_Carrier_940 ∷ T_BooleanAlgebra_914 → () Source #

d__'8776'__942 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → () Source #

d__'8804'__944 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → () Source #

d__'8744'__946 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__948 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172'__950 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny Source #

d_'8868'_952 ∷ T_BooleanAlgebra_914 → AgdaAny Source #

d_'8869'_954 ∷ T_BooleanAlgebra_914 → AgdaAny Source #

d_isBooleanAlgebra_956 ∷ T_BooleanAlgebra_914 → T_IsBooleanAlgebra_746 Source #

d_heytingAlgebra_962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_HeytingAlgebra_764 Source #

du_heytingAlgebra_962 ∷ T_BooleanAlgebra_914 → T_HeytingAlgebra_764 Source #

d__'8680'__966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

du__'8680'__966 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_968 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedJoinSemilattice_970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_BoundedJoinSemilattice_104 Source #

du_boundedJoinSemilattice_970 ∷ T_BooleanAlgebra_914 → T_BoundedJoinSemilattice_104 Source #

d_boundedLattice_972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_BoundedLattice_628 Source #

du_boundedLattice_972 ∷ T_BooleanAlgebra_914 → T_BoundedLattice_628 Source #

d_boundedMeetSemilattice_974 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_BoundedMeetSemilattice_294 Source #

du_boundedMeetSemilattice_974 ∷ T_BooleanAlgebra_914 → T_BoundedMeetSemilattice_294 Source #

d_exponential_976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

du_exponential_976 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_infimum_978 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_infimum_978 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_980 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsBoundedJoinSemilattice_118 Source #

du_isBoundedJoinSemilattice_980 ∷ T_BooleanAlgebra_914 → T_IsBoundedJoinSemilattice_118 Source #

d_isBoundedLattice_982 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsBoundedLattice_514 Source #

du_isBoundedLattice_982 ∷ T_BooleanAlgebra_914 → T_IsBoundedLattice_514 Source #

d_isBoundedMeetSemilattice_984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsBoundedMeetSemilattice_280 Source #

du_isBoundedMeetSemilattice_984 ∷ T_BooleanAlgebra_914 → T_IsBoundedMeetSemilattice_280 Source #

d_isEquivalence_986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsEquivalence_28 Source #

du_isEquivalence_986 ∷ T_BooleanAlgebra_914 → T_IsEquivalence_28 Source #

d_isHeytingAlgebra_988 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsHeytingAlgebra_612 Source #

du_isHeytingAlgebra_988 ∷ T_BooleanAlgebra_914 → T_IsHeytingAlgebra_612 Source #

d_isJoinSemilattice_990 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_990 ∷ T_BooleanAlgebra_914 → T_IsJoinSemilattice_22 Source #

d_isLattice_992 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsLattice_348 Source #

du_isLattice_992 ∷ T_BooleanAlgebra_914 → T_IsLattice_348 Source #

d_isMeetSemilattice_994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsMeetSemilattice_184 Source #

du_isMeetSemilattice_994 ∷ T_BooleanAlgebra_914 → T_IsMeetSemilattice_184 Source #

d_isPartialOrder_996 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsPartialOrder_248 Source #

du_isPartialOrder_996 ∷ T_BooleanAlgebra_914 → T_IsPartialOrder_248 Source #

d_isPreorder_998 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsPreorder_76 Source #

du_isPreorder_998 ∷ T_BooleanAlgebra_914 → T_IsPreorder_76 Source #

d_joinSemilattice_1000 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_JoinSemilattice_14 Source #

du_joinSemilattice_1000 ∷ T_BooleanAlgebra_914 → T_JoinSemilattice_14 Source #

d_lattice_1002 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_Lattice_394 Source #

du_lattice_1002 ∷ T_BooleanAlgebra_914 → T_Lattice_394 Source #

d_maximum_1004 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny Source #

du_maximum_1004 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny Source #

d_meetSemilattice_1006 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_MeetSemilattice_204 Source #

du_meetSemilattice_1006 ∷ T_BooleanAlgebra_914 → T_MeetSemilattice_204 Source #

d_minimum_1008 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny Source #

du_minimum_1008 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny Source #

d_poset_1010 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_Poset_492 Source #

du_poset_1010 ∷ T_BooleanAlgebra_914 → T_Poset_492 Source #

d_preorder_1012 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_Preorder_142 Source #

du_preorder_1012 ∷ T_BooleanAlgebra_914 → T_Preorder_142 Source #

d_refl_1014 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny Source #

du_refl_1014 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny Source #

d_reflexive_1016 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_1016 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_1018 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_Setoid_46 Source #

du_setoid_1018 ∷ T_BooleanAlgebra_914 → T_Setoid_46 Source #

d_supremum_1020 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_supremum_1020 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_1022 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1022 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8680'_1024 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8680'_1024 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8743'_1026 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8743'_1026 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_1028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_1028 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_1030 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_1030 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_1032 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_1032 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_1034 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_1034 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_1036 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_1036 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_1038 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_1038 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_1040 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_1040 ∷ T_BooleanAlgebra_914 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_1042 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_1042 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_1044 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_1044 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_1046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_1046 ∷ T_BooleanAlgebra_914 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_1048 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_1048 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_1050 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_1050 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_1054 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1054 ∷ T_BooleanAlgebra_914 → T_IsPartialEquivalence_16 Source #

d_refl_1056 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny Source #

du_refl_1056 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny Source #

d_reflexive_1058 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1058 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_1060 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1060 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1062 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1062 ∷ T_BooleanAlgebra_914 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #