Documentation

d_JoinSemilattice_14 :: p1 -> p2 -> p3 -> () 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_26 Source #

d_isPartialOrder_48 :: T_JoinSemilattice_14 -> T_IsPartialOrder_162 Source #

d_isPreorder_50 :: T_JoinSemilattice_14 -> T_IsPreorder_70 Source #

d_refl_52 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> 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_isPartialEquivalence_74 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_JoinSemilattice_14 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_74 :: T_JoinSemilattice_14 -> T_IsPartialEquivalence_16 Source #

d_refl_76 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny Source #

d_reflexive_78 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_78 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_80 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_82 :: T_JoinSemilattice_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_poset_84 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_JoinSemilattice_14 -> T_Poset_282 Source #

du_poset_84 :: T_JoinSemilattice_14 -> T_Poset_282 Source #

d_preorder_88 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_JoinSemilattice_14 -> T_Preorder_132 Source #

du_preorder_88 :: T_JoinSemilattice_14 -> T_Preorder_132 Source #

d_BoundedJoinSemilattice_96 :: p1 -> p2 -> p3 -> () Source #

data T_BoundedJoinSemilattice_96 Source #

d_Carrier_116 :: T_BoundedJoinSemilattice_96 -> () Source #

d__'8776'__118 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__120 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__122 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8869'_124 :: T_BoundedJoinSemilattice_96 -> AgdaAny Source #

d_isBoundedJoinSemilattice_126 :: T_BoundedJoinSemilattice_96 -> T_IsBoundedJoinSemilattice_110 Source #

d_antisym_130 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_132 :: T_BoundedJoinSemilattice_96 -> T_IsEquivalence_26 Source #

d_isJoinSemilattice_134 :: T_BoundedJoinSemilattice_96 -> T_IsJoinSemilattice_22 Source #

d_isPartialOrder_136 :: T_BoundedJoinSemilattice_96 -> T_IsPartialOrder_162 Source #

d_isPreorder_138 :: T_BoundedJoinSemilattice_96 -> T_IsPreorder_70 Source #

d_minimum_140 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny Source #

d_refl_142 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny Source #

du_refl_142 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny Source #

d_reflexive_144 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_supremum_146 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_148 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_150 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_150 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_152 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_152 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_154 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_154 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_156 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_156 :: T_BoundedJoinSemilattice_96 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_158 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_158 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_160 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_160 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_164 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_164 :: T_BoundedJoinSemilattice_96 -> T_IsPartialEquivalence_16 Source #

d_refl_166 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny Source #

d_reflexive_168 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_168 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_170 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_172 :: T_BoundedJoinSemilattice_96 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_joinSemilattice_174 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> T_JoinSemilattice_14 Source #

du_joinSemilattice_174 :: T_BoundedJoinSemilattice_96 -> T_JoinSemilattice_14 Source #

d_poset_178 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> T_Poset_282 Source #

du_poset_178 :: T_BoundedJoinSemilattice_96 -> T_Poset_282 Source #

d_preorder_180 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedJoinSemilattice_96 -> T_Preorder_132 Source #

du_preorder_180 :: T_BoundedJoinSemilattice_96 -> T_Preorder_132 Source #

d_MeetSemilattice_188 :: p1 -> p2 -> p3 -> () Source #

data T_MeetSemilattice_188 Source #

d_Carrier_206 :: T_MeetSemilattice_188 -> () Source #

d__'8776'__208 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__210 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> () Source #

d__'8743'__212 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isMeetSemilattice_214 :: T_MeetSemilattice_188 -> T_IsMeetSemilattice_168 Source #

d_antisym_218 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_infimum_220 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isEquivalence_222 :: T_MeetSemilattice_188 -> T_IsEquivalence_26 Source #

d_isPartialOrder_224 :: T_MeetSemilattice_188 -> T_IsPartialOrder_162 Source #

d_isPreorder_226 :: T_MeetSemilattice_188 -> T_IsPreorder_70 Source #

d_refl_228 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> AgdaAny -> AgdaAny Source #

du_refl_228 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny Source #

d_reflexive_230 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_232 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_234 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_234 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_236 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_236 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_238 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_238 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_240 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_240 :: T_MeetSemilattice_188 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_242 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_242 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_244 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_244 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_248 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_248 :: T_MeetSemilattice_188 -> T_IsPartialEquivalence_16 Source #

d_refl_250 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny Source #

d_reflexive_252 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_252 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_254 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_256 :: T_MeetSemilattice_188 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_poset_258 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> T_Poset_282 Source #

du_poset_258 :: T_MeetSemilattice_188 -> T_Poset_282 Source #

d_preorder_262 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_MeetSemilattice_188 -> T_Preorder_132 Source #

du_preorder_262 :: T_MeetSemilattice_188 -> T_Preorder_132 Source #

d_BoundedMeetSemilattice_270 :: p1 -> p2 -> p3 -> () Source #

data T_BoundedMeetSemilattice_270 Source #

d_Carrier_290 :: T_BoundedMeetSemilattice_270 -> () Source #

d__'8776'__292 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__294 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> () Source #

d__'8743'__296 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8868'_298 :: T_BoundedMeetSemilattice_270 -> AgdaAny Source #

d_isBoundedMeetSemilattice_300 :: T_BoundedMeetSemilattice_270 -> T_IsBoundedMeetSemilattice_256 Source #

d_antisym_304 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_infimum_306 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isEquivalence_308 :: T_BoundedMeetSemilattice_270 -> T_IsEquivalence_26 Source #

d_isMeetSemilattice_310 :: T_BoundedMeetSemilattice_270 -> T_IsMeetSemilattice_168 Source #

d_isPartialOrder_312 :: T_BoundedMeetSemilattice_270 -> T_IsPartialOrder_162 Source #

d_isPreorder_314 :: T_BoundedMeetSemilattice_270 -> T_IsPreorder_70 Source #

d_maximum_316 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny Source #

d_refl_318 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny Source #

du_refl_318 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny Source #

d_reflexive_320 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_322 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_324 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_324 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_326 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_326 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_328 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_328 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_330 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_330 :: T_BoundedMeetSemilattice_270 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_332 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_332 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_334 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_334 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_338 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_338 :: T_BoundedMeetSemilattice_270 -> T_IsPartialEquivalence_16 Source #

d_refl_340 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny Source #

d_reflexive_342 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_342 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_344 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_346 :: T_BoundedMeetSemilattice_270 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_meetSemilattice_348 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> T_MeetSemilattice_188 Source #

du_meetSemilattice_348 :: T_BoundedMeetSemilattice_270 -> T_MeetSemilattice_188 Source #

d_poset_352 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> T_Poset_282 Source #

du_poset_352 :: T_BoundedMeetSemilattice_270 -> T_Poset_282 Source #

d_preorder_354 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedMeetSemilattice_270 -> T_Preorder_132 Source #

du_preorder_354 :: T_BoundedMeetSemilattice_270 -> T_Preorder_132 Source #

d_Lattice_362 :: p1 -> p2 -> p3 -> () Source #

data T_Lattice_362 Source #

d_Carrier_382 :: T_Lattice_362 -> () Source #

d__'8776'__384 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__386 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__388 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8743'__390 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isLattice_392 :: T_Lattice_362 -> T_IsLattice_316 Source #

d_antisym_396 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_infimum_398 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isEquivalence_400 :: T_Lattice_362 -> T_IsEquivalence_26 Source #

d_isJoinSemilattice_402 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_402 :: T_Lattice_362 -> T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_404 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> T_IsMeetSemilattice_168 Source #

du_isMeetSemilattice_404 :: T_Lattice_362 -> T_IsMeetSemilattice_168 Source #

d_isPartialOrder_406 :: T_Lattice_362 -> T_IsPartialOrder_162 Source #

d_isPreorder_408 :: T_Lattice_362 -> T_IsPreorder_70 Source #

d_refl_410 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> AgdaAny -> AgdaAny Source #

du_refl_410 :: T_Lattice_362 -> AgdaAny -> AgdaAny Source #

d_reflexive_412 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_supremum_414 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_416 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_418 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_418 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_420 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_420 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_422 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_422 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_424 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_424 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_426 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_426 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_428 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_428 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_430 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_430 :: T_Lattice_362 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_432 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_432 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_434 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_434 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_438 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_438 :: T_Lattice_362 -> T_IsPartialEquivalence_16 Source #

d_refl_440 :: T_Lattice_362 -> AgdaAny -> AgdaAny Source #

d_reflexive_442 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_442 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_444 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_446 :: T_Lattice_362 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_setoid_448 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> T_Setoid_44 Source #

du_setoid_448 :: T_Lattice_362 -> T_Setoid_44 Source #

d_joinSemilattice_450 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> T_JoinSemilattice_14 Source #

du_joinSemilattice_450 :: T_Lattice_362 -> T_JoinSemilattice_14 Source #

d_meetSemilattice_452 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> T_MeetSemilattice_188 Source #

du_meetSemilattice_452 :: T_Lattice_362 -> T_MeetSemilattice_188 Source #

d_poset_456 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> T_Poset_282 Source #

du_poset_456 :: T_Lattice_362 -> T_Poset_282 Source #

d_preorder_458 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Lattice_362 -> T_Preorder_132 Source #

du_preorder_458 :: T_Lattice_362 -> T_Preorder_132 Source #

d_DistributiveLattice_466 :: p1 -> p2 -> p3 -> () Source #

data T_DistributiveLattice_466 Source #

d_Carrier_486 :: T_DistributiveLattice_466 -> () Source #

d__'8776'__488 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__490 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__492 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8743'__494 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isDistributiveLattice_496 :: T_DistributiveLattice_466 -> T_IsDistributiveLattice_390 Source #

d_'8743''45'distrib'737''45''8744'_500 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_lattice_506 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_Lattice_362 Source #

du_lattice_506 :: T_DistributiveLattice_466 -> T_Lattice_362 Source #

d_antisym_510 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_antisym_510 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_infimum_512 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_infimum_512 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isEquivalence_514 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_IsEquivalence_26 Source #

du_isEquivalence_514 :: T_DistributiveLattice_466 -> T_IsEquivalence_26 Source #

d_isJoinSemilattice_516 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_516 :: T_DistributiveLattice_466 -> T_IsJoinSemilattice_22 Source #

d_isLattice_518 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_IsLattice_316 Source #

du_isLattice_518 :: T_DistributiveLattice_466 -> T_IsLattice_316 Source #

d_isMeetSemilattice_520 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_IsMeetSemilattice_168 Source #

du_isMeetSemilattice_520 :: T_DistributiveLattice_466 -> T_IsMeetSemilattice_168 Source #

d_isPartialOrder_522 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_IsPartialOrder_162 Source #

du_isPartialOrder_522 :: T_DistributiveLattice_466 -> T_IsPartialOrder_162 Source #

d_isPreorder_524 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_IsPreorder_70 Source #

du_isPreorder_524 :: T_DistributiveLattice_466 -> T_IsPreorder_70 Source #

d_joinSemilattice_526 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_JoinSemilattice_14 Source #

du_joinSemilattice_526 :: T_DistributiveLattice_466 -> T_JoinSemilattice_14 Source #

d_meetSemilattice_528 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_MeetSemilattice_188 Source #

du_meetSemilattice_528 :: T_DistributiveLattice_466 -> T_MeetSemilattice_188 Source #

d_poset_530 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_Poset_282 Source #

du_poset_530 :: T_DistributiveLattice_466 -> T_Poset_282 Source #

d_preorder_532 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_Preorder_132 Source #

du_preorder_532 :: T_DistributiveLattice_466 -> T_Preorder_132 Source #

d_refl_534 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny Source #

du_refl_534 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny Source #

d_reflexive_536 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_reflexive_536 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_setoid_538 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_Setoid_44 Source #

du_setoid_538 :: T_DistributiveLattice_466 -> T_Setoid_44 Source #

d_supremum_540 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_supremum_540 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_542 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_542 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_544 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_544 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_546 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_546 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_548 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_548 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_550 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_550 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_552 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_552 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_554 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_554 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_556 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_556 :: T_DistributiveLattice_466 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_558 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_558 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_560 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_560 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_564 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_564 :: T_DistributiveLattice_466 -> T_IsPartialEquivalence_16 Source #

d_refl_566 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny Source #

du_refl_566 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny Source #

d_reflexive_568 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_568 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_570 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_570 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_572 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_572 :: T_DistributiveLattice_466 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_BoundedLattice_580 :: p1 -> p2 -> p3 -> () Source #

data T_BoundedLattice_580 Source #

d_Carrier_604 :: T_BoundedLattice_580 -> () Source #

d__'8776'__606 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__608 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__610 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8743'__612 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8868'_614 :: T_BoundedLattice_580 -> AgdaAny Source #

d_'8869'_616 :: T_BoundedLattice_580 -> AgdaAny Source #

d_isBoundedLattice_618 :: T_BoundedLattice_580 -> T_IsBoundedLattice_466 Source #

d_antisym_622 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_infimum_624 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isBoundedJoinSemilattice_626 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_IsBoundedJoinSemilattice_110 Source #

du_isBoundedJoinSemilattice_626 :: T_BoundedLattice_580 -> T_IsBoundedJoinSemilattice_110 Source #

d_isBoundedMeetSemilattice_628 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_IsBoundedMeetSemilattice_256 Source #

du_isBoundedMeetSemilattice_628 :: T_BoundedLattice_580 -> T_IsBoundedMeetSemilattice_256 Source #

d_isEquivalence_630 :: T_BoundedLattice_580 -> T_IsEquivalence_26 Source #

d_isJoinSemilattice_632 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_632 :: T_BoundedLattice_580 -> T_IsJoinSemilattice_22 Source #

d_isLattice_634 :: T_BoundedLattice_580 -> T_IsLattice_316 Source #

d_isMeetSemilattice_636 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_IsMeetSemilattice_168 Source #

du_isMeetSemilattice_636 :: T_BoundedLattice_580 -> T_IsMeetSemilattice_168 Source #

d_isPartialOrder_638 :: T_BoundedLattice_580 -> T_IsPartialOrder_162 Source #

d_isPreorder_640 :: T_BoundedLattice_580 -> T_IsPreorder_70 Source #

d_maximum_642 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny Source #

d_minimum_644 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny Source #

d_refl_646 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> AgdaAny -> AgdaAny Source #

du_refl_646 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny Source #

d_reflexive_648 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_supremum_650 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_652 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_654 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_654 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_656 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_656 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_658 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_658 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_660 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_660 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_662 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_662 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_664 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_664 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_666 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_666 :: T_BoundedLattice_580 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_668 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_668 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_670 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_670 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_674 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_674 :: T_BoundedLattice_580 -> T_IsPartialEquivalence_16 Source #

d_refl_676 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny Source #

d_reflexive_678 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_678 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_680 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_682 :: T_BoundedLattice_580 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_boundedJoinSemilattice_684 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_BoundedJoinSemilattice_96 Source #

du_boundedJoinSemilattice_684 :: T_BoundedLattice_580 -> T_BoundedJoinSemilattice_96 Source #

d_boundedMeetSemilattice_686 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_BoundedMeetSemilattice_270 Source #

du_boundedMeetSemilattice_686 :: T_BoundedLattice_580 -> T_BoundedMeetSemilattice_270 Source #

d_lattice_688 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_Lattice_362 Source #

du_lattice_688 :: T_BoundedLattice_580 -> T_Lattice_362 Source #

d_joinSemilattice_692 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_JoinSemilattice_14 Source #

du_joinSemilattice_692 :: T_BoundedLattice_580 -> T_JoinSemilattice_14 Source #

d_meetSemilattice_694 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_MeetSemilattice_188 Source #

du_meetSemilattice_694 :: T_BoundedLattice_580 -> T_MeetSemilattice_188 Source #

d_poset_696 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_Poset_282 Source #

du_poset_696 :: T_BoundedLattice_580 -> T_Poset_282 Source #

d_preorder_698 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_Preorder_132 Source #

du_preorder_698 :: T_BoundedLattice_580 -> T_Preorder_132 Source #

d_setoid_700 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BoundedLattice_580 -> T_Setoid_44 Source #

du_setoid_700 :: T_BoundedLattice_580 -> T_Setoid_44 Source #

d_HeytingAlgebra_708 :: p1 -> p2 -> p3 -> () Source #

data T_HeytingAlgebra_708 Source #

d_Carrier_734 :: T_HeytingAlgebra_708 -> () Source #

d__'8776'__736 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__738 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__740 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8743'__742 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8680'__744 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8868'_746 :: T_HeytingAlgebra_708 -> AgdaAny Source #

d_'8869'_748 :: T_HeytingAlgebra_708 -> AgdaAny Source #

d_isHeytingAlgebra_750 :: T_HeytingAlgebra_708 -> T_IsHeytingAlgebra_556 Source #

d_boundedLattice_752 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_BoundedLattice_580 Source #

du_boundedLattice_752 :: T_HeytingAlgebra_708 -> T_BoundedLattice_580 Source #

d_exponential_756 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_transpose'45''8680'_758 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_transpose'45''8680'_758 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_transpose'45''8743'_760 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_transpose'45''8743'_760 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_764 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_antisym_764 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_boundedJoinSemilattice_766 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_BoundedJoinSemilattice_96 Source #

du_boundedJoinSemilattice_766 :: T_HeytingAlgebra_708 -> T_BoundedJoinSemilattice_96 Source #

d_boundedMeetSemilattice_768 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_BoundedMeetSemilattice_270 Source #

du_boundedMeetSemilattice_768 :: T_HeytingAlgebra_708 -> T_BoundedMeetSemilattice_270 Source #

d_infimum_770 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_infimum_770 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isBoundedJoinSemilattice_772 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_IsBoundedJoinSemilattice_110 Source #

du_isBoundedJoinSemilattice_772 :: T_HeytingAlgebra_708 -> T_IsBoundedJoinSemilattice_110 Source #

d_isBoundedLattice_774 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_IsBoundedLattice_466 Source #

du_isBoundedLattice_774 :: T_HeytingAlgebra_708 -> T_IsBoundedLattice_466 Source #

d_isBoundedMeetSemilattice_776 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_IsBoundedMeetSemilattice_256 Source #

du_isBoundedMeetSemilattice_776 :: T_HeytingAlgebra_708 -> T_IsBoundedMeetSemilattice_256 Source #

d_isEquivalence_778 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_IsEquivalence_26 Source #

du_isEquivalence_778 :: T_HeytingAlgebra_708 -> T_IsEquivalence_26 Source #

d_isJoinSemilattice_780 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_780 :: T_HeytingAlgebra_708 -> T_IsJoinSemilattice_22 Source #

d_isLattice_782 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_IsLattice_316 Source #

du_isLattice_782 :: T_HeytingAlgebra_708 -> T_IsLattice_316 Source #

d_isMeetSemilattice_784 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_IsMeetSemilattice_168 Source #

du_isMeetSemilattice_784 :: T_HeytingAlgebra_708 -> T_IsMeetSemilattice_168 Source #

d_isPartialOrder_786 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_IsPartialOrder_162 Source #

du_isPartialOrder_786 :: T_HeytingAlgebra_708 -> T_IsPartialOrder_162 Source #

d_isPreorder_788 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_IsPreorder_70 Source #

du_isPreorder_788 :: T_HeytingAlgebra_708 -> T_IsPreorder_70 Source #

d_joinSemilattice_790 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_JoinSemilattice_14 Source #

du_joinSemilattice_790 :: T_HeytingAlgebra_708 -> T_JoinSemilattice_14 Source #

d_lattice_792 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_Lattice_362 Source #

du_lattice_792 :: T_HeytingAlgebra_708 -> T_Lattice_362 Source #

d_maximum_794 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny Source #

du_maximum_794 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny Source #

d_meetSemilattice_796 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_MeetSemilattice_188 Source #

du_meetSemilattice_796 :: T_HeytingAlgebra_708 -> T_MeetSemilattice_188 Source #

d_minimum_798 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny Source #

du_minimum_798 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny Source #

d_poset_800 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_Poset_282 Source #

du_poset_800 :: T_HeytingAlgebra_708 -> T_Poset_282 Source #

d_preorder_802 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_Preorder_132 Source #

du_preorder_802 :: T_HeytingAlgebra_708 -> T_Preorder_132 Source #

d_refl_804 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny Source #

du_refl_804 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny Source #

d_reflexive_806 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_reflexive_806 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_setoid_808 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_Setoid_44 Source #

du_setoid_808 :: T_HeytingAlgebra_708 -> T_Setoid_44 Source #

d_supremum_810 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_supremum_810 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_812 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_812 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_814 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_814 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_816 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_816 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_818 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_818 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_820 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_820 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_822 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_822 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_824 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_824 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_826 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_826 :: T_HeytingAlgebra_708 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_828 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_828 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_830 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_830 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_834 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_834 :: T_HeytingAlgebra_708 -> T_IsPartialEquivalence_16 Source #

d_refl_836 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny Source #

du_refl_836 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny Source #

d_reflexive_838 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_838 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_840 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_840 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_842 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_842 :: T_HeytingAlgebra_708 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_BooleanAlgebra_850 :: p1 -> p2 -> p3 -> () Source #

data T_BooleanAlgebra_850 Source #

d_Carrier_876 :: T_BooleanAlgebra_850 -> () Source #

d__'8776'__878 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> () Source #

d__'8804'__880 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> () Source #

d__'8744'__882 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8743'__884 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'172'__886 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny Source #

d_'8868'_888 :: T_BooleanAlgebra_850 -> AgdaAny Source #

d_'8869'_890 :: T_BooleanAlgebra_850 -> AgdaAny Source #

d_isBooleanAlgebra_892 :: T_BooleanAlgebra_850 -> T_IsBooleanAlgebra_682 Source #

d_heytingAlgebra_898 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_HeytingAlgebra_708 Source #

du_heytingAlgebra_898 :: T_BooleanAlgebra_850 -> T_HeytingAlgebra_708 Source #

d__'8680'__902 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'8680'__902 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_antisym_904 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_antisym_904 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_boundedJoinSemilattice_906 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_BoundedJoinSemilattice_96 Source #

du_boundedJoinSemilattice_906 :: T_BooleanAlgebra_850 -> T_BoundedJoinSemilattice_96 Source #

d_boundedLattice_908 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_BoundedLattice_580 Source #

du_boundedLattice_908 :: T_BooleanAlgebra_850 -> T_BoundedLattice_580 Source #

d_boundedMeetSemilattice_910 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_BoundedMeetSemilattice_270 Source #

du_boundedMeetSemilattice_910 :: T_BooleanAlgebra_850 -> T_BoundedMeetSemilattice_270 Source #

d_exponential_912 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_exponential_912 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_infimum_914 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_infimum_914 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_isBoundedJoinSemilattice_916 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsBoundedJoinSemilattice_110 Source #

du_isBoundedJoinSemilattice_916 :: T_BooleanAlgebra_850 -> T_IsBoundedJoinSemilattice_110 Source #

d_isBoundedLattice_918 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsBoundedLattice_466 Source #

du_isBoundedLattice_918 :: T_BooleanAlgebra_850 -> T_IsBoundedLattice_466 Source #

d_isBoundedMeetSemilattice_920 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsBoundedMeetSemilattice_256 Source #

du_isBoundedMeetSemilattice_920 :: T_BooleanAlgebra_850 -> T_IsBoundedMeetSemilattice_256 Source #

d_isEquivalence_922 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsEquivalence_26 Source #

du_isEquivalence_922 :: T_BooleanAlgebra_850 -> T_IsEquivalence_26 Source #

d_isHeytingAlgebra_924 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsHeytingAlgebra_556 Source #

du_isHeytingAlgebra_924 :: T_BooleanAlgebra_850 -> T_IsHeytingAlgebra_556 Source #

d_isJoinSemilattice_926 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_926 :: T_BooleanAlgebra_850 -> T_IsJoinSemilattice_22 Source #

d_isLattice_928 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsLattice_316 Source #

du_isLattice_928 :: T_BooleanAlgebra_850 -> T_IsLattice_316 Source #

d_isMeetSemilattice_930 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsMeetSemilattice_168 Source #

du_isMeetSemilattice_930 :: T_BooleanAlgebra_850 -> T_IsMeetSemilattice_168 Source #

d_isPartialOrder_932 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsPartialOrder_162 Source #

du_isPartialOrder_932 :: T_BooleanAlgebra_850 -> T_IsPartialOrder_162 Source #

d_isPreorder_934 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsPreorder_70 Source #

du_isPreorder_934 :: T_BooleanAlgebra_850 -> T_IsPreorder_70 Source #

d_joinSemilattice_936 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_JoinSemilattice_14 Source #

du_joinSemilattice_936 :: T_BooleanAlgebra_850 -> T_JoinSemilattice_14 Source #

d_lattice_938 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_Lattice_362 Source #

du_lattice_938 :: T_BooleanAlgebra_850 -> T_Lattice_362 Source #

d_maximum_940 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny Source #

du_maximum_940 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny Source #

d_meetSemilattice_942 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_MeetSemilattice_188 Source #

du_meetSemilattice_942 :: T_BooleanAlgebra_850 -> T_MeetSemilattice_188 Source #

d_minimum_944 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny Source #

du_minimum_944 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny Source #

d_poset_946 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_Poset_282 Source #

du_poset_946 :: T_BooleanAlgebra_850 -> T_Poset_282 Source #

d_preorder_948 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_Preorder_132 Source #

du_preorder_948 :: T_BooleanAlgebra_850 -> T_Preorder_132 Source #

d_refl_950 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny Source #

du_refl_950 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny Source #

d_reflexive_952 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_reflexive_952 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_setoid_954 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_Setoid_44 Source #

du_setoid_954 :: T_BooleanAlgebra_850 -> T_Setoid_44 Source #

d_supremum_956 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

du_supremum_956 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_trans_958 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_958 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_transpose'45''8680'_960 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_transpose'45''8680'_960 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_transpose'45''8743'_962 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_transpose'45''8743'_962 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'x_964 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'x_964 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8743'y'8804'y_966 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8743'y'8804'y_966 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_x'8804'x'8744'y_968 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_x'8804'x'8744'y_968 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_y'8804'x'8744'y_970 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_y'8804'x'8744'y_970 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8743''45'greatest_972 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8743''45'greatest_972 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8744''45'least_974 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8744''45'least_974 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'45''8776'_976 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_Σ_14 Source #

du_'8764''45'resp'45''8776'_976 :: T_BooleanAlgebra_850 -> T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_978 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'691''45''8776'_978 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'8764''45'resp'737''45''8776'_980 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8764''45'resp'737''45''8776'_980 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isPartialEquivalence_984 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_984 :: T_BooleanAlgebra_850 -> T_IsPartialEquivalence_16 Source #

d_refl_986 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny Source #

du_refl_986 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny Source #

d_reflexive_988 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_988 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_990 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_990 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_992 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_992 :: T_BooleanAlgebra_850 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #