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_26 Source #

d_isPartialOrder_48 ∷ T_JoinSemilattice_14 → T_IsPartialOrder_174 Source #

d_isPreorder_50 ∷ T_JoinSemilattice_14 → T_IsPreorder_70 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_314 Source #

du_poset_90 ∷ T_JoinSemilattice_14 → T_Poset_314 Source #

d_preorder_94 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_14 → T_Preorder_132 Source #

du_preorder_94 ∷ T_JoinSemilattice_14 → T_Preorder_132 Source #

d_BoundedJoinSemilattice_102 ∷ p → p → p → () Source #

data T_BoundedJoinSemilattice_102 Source #

d_Carrier_122 ∷ T_BoundedJoinSemilattice_102 → () Source #

d__'8776'__124 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → () Source #

d__'8804'__126 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → () Source #

d__'8744'__128 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8869'_130 ∷ T_BoundedJoinSemilattice_102 → AgdaAny Source #

d_isBoundedJoinSemilattice_132 ∷ T_BoundedJoinSemilattice_102 → T_IsBoundedJoinSemilattice_116 Source #

d_antisym_136 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_138 ∷ T_BoundedJoinSemilattice_102 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_140 ∷ T_BoundedJoinSemilattice_102 → T_IsJoinSemilattice_22 Source #

d_isPartialOrder_142 ∷ T_BoundedJoinSemilattice_102 → T_IsPartialOrder_174 Source #

d_isPreorder_144 ∷ T_BoundedJoinSemilattice_102 → T_IsPreorder_70 Source #

d_minimum_146 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny Source #

d_refl_148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny Source #

du_refl_148 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny Source #

d_reflexive_150 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_152 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_154 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_156 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_158 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_160 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_162 ∷ T_BoundedJoinSemilattice_102 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_164 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_166 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_168 ∷ T_BoundedJoinSemilattice_102 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_170 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_172 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_176 ∷ T_BoundedJoinSemilattice_102 → T_IsPartialEquivalence_16 Source #

d_refl_178 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny Source #

d_reflexive_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_180 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_182 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_184 ∷ T_BoundedJoinSemilattice_102 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_joinSemilattice_186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → T_JoinSemilattice_14 Source #

du_joinSemilattice_186 ∷ T_BoundedJoinSemilattice_102 → T_JoinSemilattice_14 Source #

d_poset_190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → T_Poset_314 Source #

du_poset_190 ∷ T_BoundedJoinSemilattice_102 → T_Poset_314 Source #

d_preorder_192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_102 → T_Preorder_132 Source #

du_preorder_192 ∷ T_BoundedJoinSemilattice_102 → T_Preorder_132 Source #

d_MeetSemilattice_200 ∷ p → p → p → () Source #

data T_MeetSemilattice_200 Source #

d_Carrier_218 ∷ T_MeetSemilattice_200 → () Source #

d__'8776'__220 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → () Source #

d__'8804'__222 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → () Source #

d__'8743'__224 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMeetSemilattice_226 ∷ T_MeetSemilattice_200 → T_IsMeetSemilattice_180 Source #

d_antisym_230 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_232 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_234 ∷ T_MeetSemilattice_200 → T_IsEquivalence_26 Source #

d_isPartialOrder_236 ∷ T_MeetSemilattice_200 → T_IsPartialOrder_174 Source #

d_isPreorder_238 ∷ T_MeetSemilattice_200 → T_IsPreorder_70 Source #

d_refl_240 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → AgdaAny → AgdaAny Source #

du_refl_240 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny Source #

d_reflexive_242 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_244 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_246 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_246 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_248 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_248 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_250 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_250 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_252 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_252 ∷ T_MeetSemilattice_200 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_254 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_256 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_258 ∷ T_MeetSemilattice_200 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_260 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_262 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_266 ∷ T_MeetSemilattice_200 → T_IsPartialEquivalence_16 Source #

d_refl_268 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny Source #

d_reflexive_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_270 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_272 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_274 ∷ T_MeetSemilattice_200 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_poset_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → T_Poset_314 Source #

du_poset_276 ∷ T_MeetSemilattice_200 → T_Poset_314 Source #

d_preorder_280 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_200 → T_Preorder_132 Source #

du_preorder_280 ∷ T_MeetSemilattice_200 → T_Preorder_132 Source #

d_BoundedMeetSemilattice_288 ∷ p → p → p → () Source #

data T_BoundedMeetSemilattice_288 Source #

d_Carrier_308 ∷ T_BoundedMeetSemilattice_288 → () Source #

d__'8776'__310 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → () Source #

d__'8804'__312 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → () Source #

d__'8743'__314 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8868'_316 ∷ T_BoundedMeetSemilattice_288 → AgdaAny Source #

d_isBoundedMeetSemilattice_318 ∷ T_BoundedMeetSemilattice_288 → T_IsBoundedMeetSemilattice_274 Source #

d_antisym_322 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_324 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_326 ∷ T_BoundedMeetSemilattice_288 → T_IsEquivalence_26 Source #

d_isMeetSemilattice_328 ∷ T_BoundedMeetSemilattice_288 → T_IsMeetSemilattice_180 Source #

d_isPartialOrder_330 ∷ T_BoundedMeetSemilattice_288 → T_IsPartialOrder_174 Source #

d_isPreorder_332 ∷ T_BoundedMeetSemilattice_288 → T_IsPreorder_70 Source #

d_maximum_334 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny Source #

d_refl_336 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny Source #

du_refl_336 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny Source #

d_reflexive_338 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_340 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_342 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_342 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_344 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_344 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_346 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_346 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_348 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_348 ∷ T_BoundedMeetSemilattice_288 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_350 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_350 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_352 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_352 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_354 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_354 ∷ T_BoundedMeetSemilattice_288 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_356 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_356 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_358 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_358 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_362 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_362 ∷ T_BoundedMeetSemilattice_288 → T_IsPartialEquivalence_16 Source #

d_refl_364 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny Source #

d_reflexive_366 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_366 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_368 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_370 ∷ T_BoundedMeetSemilattice_288 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_meetSemilattice_372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → T_MeetSemilattice_200 Source #

du_meetSemilattice_372 ∷ T_BoundedMeetSemilattice_288 → T_MeetSemilattice_200 Source #

d_poset_376 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → T_Poset_314 Source #

du_poset_376 ∷ T_BoundedMeetSemilattice_288 → T_Poset_314 Source #

d_preorder_378 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_288 → T_Preorder_132 Source #

du_preorder_378 ∷ T_BoundedMeetSemilattice_288 → T_Preorder_132 Source #

d_Lattice_386 ∷ p → p → p → () Source #

data T_Lattice_386 Source #

d_Carrier_406 ∷ T_Lattice_386 → () Source #

d__'8776'__408 ∷ T_Lattice_386 → AgdaAny → AgdaAny → () Source #

d__'8804'__410 ∷ T_Lattice_386 → AgdaAny → AgdaAny → () Source #

d__'8744'__412 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__414 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny Source #

d_isLattice_416 ∷ T_Lattice_386 → T_IsLattice_340 Source #

d_antisym_420 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_422 ∷ T_Lattice_386 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_424 ∷ T_Lattice_386 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_426 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_426 ∷ T_Lattice_386 → T_IsJoinSemilattice_22 Source #

d_isMeetSemilattice_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → T_IsMeetSemilattice_180 Source #

du_isMeetSemilattice_428 ∷ T_Lattice_386 → T_IsMeetSemilattice_180 Source #

d_isPartialOrder_430 ∷ T_Lattice_386 → T_IsPartialOrder_174 Source #

d_isPreorder_432 ∷ T_Lattice_386 → T_IsPreorder_70 Source #

d_refl_434 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny Source #

du_refl_434 ∷ T_Lattice_386 → AgdaAny → AgdaAny Source #

d_reflexive_436 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_438 ∷ T_Lattice_386 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_440 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_442 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_444 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_446 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_446 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_448 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_448 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_450 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_450 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_452 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_452 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_454 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_454 ∷ T_Lattice_386 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_456 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_456 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_458 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_460 ∷ T_Lattice_386 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_462 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_464 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_464 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_468 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_468 ∷ T_Lattice_386 → T_IsPartialEquivalence_16 Source #

d_refl_470 ∷ T_Lattice_386 → AgdaAny → AgdaAny Source #

d_reflexive_472 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_472 ∷ T_Lattice_386 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_474 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_476 ∷ T_Lattice_386 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_478 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → T_Setoid_44 Source #

du_setoid_478 ∷ T_Lattice_386 → T_Setoid_44 Source #

d_joinSemilattice_480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → T_JoinSemilattice_14 Source #

du_joinSemilattice_480 ∷ T_Lattice_386 → T_JoinSemilattice_14 Source #

d_meetSemilattice_482 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → T_MeetSemilattice_200 Source #

du_meetSemilattice_482 ∷ T_Lattice_386 → T_MeetSemilattice_200 Source #

d_poset_486 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → T_Poset_314 Source #

du_poset_486 ∷ T_Lattice_386 → T_Poset_314 Source #

d_preorder_488 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_386 → T_Preorder_132 Source #

du_preorder_488 ∷ T_Lattice_386 → T_Preorder_132 Source #

d_DistributiveLattice_496 ∷ p → p → p → () Source #

data T_DistributiveLattice_496 Source #

d_Carrier_516 ∷ T_DistributiveLattice_496 → () Source #

d__'8776'__518 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → () Source #

d__'8804'__520 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → () Source #

d__'8744'__522 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__524 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny Source #

d_isDistributiveLattice_526 ∷ T_DistributiveLattice_496 → T_IsDistributiveLattice_420 Source #

d_'8743''45'distrib'737''45''8744'_530 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_lattice_536 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_Lattice_386 Source #

du_lattice_536 ∷ T_DistributiveLattice_496 → T_Lattice_386 Source #

d_antisym_540 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_540 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_542 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_infimum_542 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_IsEquivalence_26 Source #

du_isEquivalence_544 ∷ T_DistributiveLattice_496 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_546 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_546 ∷ T_DistributiveLattice_496 → T_IsJoinSemilattice_22 Source #

d_isLattice_548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_IsLattice_340 Source #

du_isLattice_548 ∷ T_DistributiveLattice_496 → T_IsLattice_340 Source #

d_isMeetSemilattice_550 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_IsMeetSemilattice_180 Source #

du_isMeetSemilattice_550 ∷ T_DistributiveLattice_496 → T_IsMeetSemilattice_180 Source #

d_isPartialOrder_552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_IsPartialOrder_174 Source #

du_isPartialOrder_552 ∷ T_DistributiveLattice_496 → T_IsPartialOrder_174 Source #

d_isPreorder_554 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_IsPreorder_70 Source #

du_isPreorder_554 ∷ T_DistributiveLattice_496 → T_IsPreorder_70 Source #

d_joinSemilattice_556 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_JoinSemilattice_14 Source #

du_joinSemilattice_556 ∷ T_DistributiveLattice_496 → T_JoinSemilattice_14 Source #

d_meetSemilattice_558 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_MeetSemilattice_200 Source #

du_meetSemilattice_558 ∷ T_DistributiveLattice_496 → T_MeetSemilattice_200 Source #

d_poset_560 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_Poset_314 Source #

du_poset_560 ∷ T_DistributiveLattice_496 → T_Poset_314 Source #

d_preorder_562 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_Preorder_132 Source #

du_preorder_562 ∷ T_DistributiveLattice_496 → T_Preorder_132 Source #

d_refl_564 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny Source #

du_refl_564 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny Source #

d_reflexive_566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_566 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_Setoid_44 Source #

du_setoid_568 ∷ T_DistributiveLattice_496 → T_Setoid_44 Source #

d_supremum_570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_supremum_570 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_572 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_572 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_574 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_576 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_576 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_578 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_578 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_580 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_580 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_582 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_584 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_584 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_586 ∷ T_DistributiveLattice_496 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_588 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_588 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_590 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_590 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_592 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_592 ∷ T_DistributiveLattice_496 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_594 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_596 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_596 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_600 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_600 ∷ T_DistributiveLattice_496 → T_IsPartialEquivalence_16 Source #

d_refl_602 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny Source #

du_refl_602 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny Source #

d_reflexive_604 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_604 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_606 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_606 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_608 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_608 ∷ T_DistributiveLattice_496 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_BoundedLattice_616 ∷ p → p → p → () Source #

data T_BoundedLattice_616 Source #

d_Carrier_640 ∷ T_BoundedLattice_616 → () Source #

d__'8776'__642 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → () Source #

d__'8804'__644 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → () Source #

d__'8744'__646 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__648 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8868'_650 ∷ T_BoundedLattice_616 → AgdaAny Source #

d_'8869'_652 ∷ T_BoundedLattice_616 → AgdaAny Source #

d_isBoundedLattice_654 ∷ T_BoundedLattice_616 → T_IsBoundedLattice_502 Source #

d_antisym_658 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_660 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_662 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_IsBoundedJoinSemilattice_116 Source #

du_isBoundedJoinSemilattice_662 ∷ T_BoundedLattice_616 → T_IsBoundedJoinSemilattice_116 Source #

d_isBoundedMeetSemilattice_664 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_IsBoundedMeetSemilattice_274 Source #

du_isBoundedMeetSemilattice_664 ∷ T_BoundedLattice_616 → T_IsBoundedMeetSemilattice_274 Source #

d_isEquivalence_666 ∷ T_BoundedLattice_616 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_668 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_668 ∷ T_BoundedLattice_616 → T_IsJoinSemilattice_22 Source #

d_isLattice_670 ∷ T_BoundedLattice_616 → T_IsLattice_340 Source #

d_isMeetSemilattice_672 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_IsMeetSemilattice_180 Source #

du_isMeetSemilattice_672 ∷ T_BoundedLattice_616 → T_IsMeetSemilattice_180 Source #

d_isPartialOrder_674 ∷ T_BoundedLattice_616 → T_IsPartialOrder_174 Source #

d_isPreorder_676 ∷ T_BoundedLattice_616 → T_IsPreorder_70 Source #

d_maximum_678 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny Source #

d_minimum_680 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny Source #

d_refl_682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny Source #

du_refl_682 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny Source #

d_reflexive_684 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_686 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_688 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_690 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_692 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_692 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_694 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_696 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_698 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_700 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_702 ∷ T_BoundedLattice_616 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_704 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_706 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_708 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_708 ∷ T_BoundedLattice_616 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_710 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_712 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_716 ∷ T_BoundedLattice_616 → T_IsPartialEquivalence_16 Source #

d_refl_718 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny Source #

d_reflexive_720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_720 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_722 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_724 ∷ T_BoundedLattice_616 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedJoinSemilattice_726 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_BoundedJoinSemilattice_102 Source #

du_boundedJoinSemilattice_726 ∷ T_BoundedLattice_616 → T_BoundedJoinSemilattice_102 Source #

d_boundedMeetSemilattice_728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_BoundedMeetSemilattice_288 Source #

du_boundedMeetSemilattice_728 ∷ T_BoundedLattice_616 → T_BoundedMeetSemilattice_288 Source #

d_lattice_730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_Lattice_386 Source #

du_lattice_730 ∷ T_BoundedLattice_616 → T_Lattice_386 Source #

d_joinSemilattice_734 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_JoinSemilattice_14 Source #

du_joinSemilattice_734 ∷ T_BoundedLattice_616 → T_JoinSemilattice_14 Source #

d_meetSemilattice_736 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_MeetSemilattice_200 Source #

du_meetSemilattice_736 ∷ T_BoundedLattice_616 → T_MeetSemilattice_200 Source #

d_poset_738 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_Poset_314 Source #

du_poset_738 ∷ T_BoundedLattice_616 → T_Poset_314 Source #

d_preorder_740 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_Preorder_132 Source #

du_preorder_740 ∷ T_BoundedLattice_616 → T_Preorder_132 Source #

d_setoid_742 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_616 → T_Setoid_44 Source #

du_setoid_742 ∷ T_BoundedLattice_616 → T_Setoid_44 Source #

d_HeytingAlgebra_750 ∷ p → p → p → () Source #

data T_HeytingAlgebra_750 Source #

d_Carrier_776 ∷ T_HeytingAlgebra_750 → () Source #

d__'8776'__778 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → () Source #

d__'8804'__780 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → () Source #

d__'8744'__782 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__784 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8680'__786 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8868'_788 ∷ T_HeytingAlgebra_750 → AgdaAny Source #

d_'8869'_790 ∷ T_HeytingAlgebra_750 → AgdaAny Source #

d_isHeytingAlgebra_792 ∷ T_HeytingAlgebra_750 → T_IsHeytingAlgebra_598 Source #

d_boundedLattice_794 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_BoundedLattice_616 Source #

du_boundedLattice_794 ∷ T_HeytingAlgebra_750 → T_BoundedLattice_616 Source #

d_exponential_798 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_transpose'45''8680'_800 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8680'_800 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8743'_802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8743'_802 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_806 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedJoinSemilattice_808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_BoundedJoinSemilattice_102 Source #

du_boundedJoinSemilattice_808 ∷ T_HeytingAlgebra_750 → T_BoundedJoinSemilattice_102 Source #

d_boundedMeetSemilattice_810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_BoundedMeetSemilattice_288 Source #

du_boundedMeetSemilattice_810 ∷ T_HeytingAlgebra_750 → T_BoundedMeetSemilattice_288 Source #

d_infimum_812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_infimum_812 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_814 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_IsBoundedJoinSemilattice_116 Source #

du_isBoundedJoinSemilattice_814 ∷ T_HeytingAlgebra_750 → T_IsBoundedJoinSemilattice_116 Source #

d_isBoundedLattice_816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_IsBoundedLattice_502 Source #

du_isBoundedLattice_816 ∷ T_HeytingAlgebra_750 → T_IsBoundedLattice_502 Source #

d_isBoundedMeetSemilattice_818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_IsBoundedMeetSemilattice_274 Source #

du_isBoundedMeetSemilattice_818 ∷ T_HeytingAlgebra_750 → T_IsBoundedMeetSemilattice_274 Source #

d_isEquivalence_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_IsEquivalence_26 Source #

du_isEquivalence_820 ∷ T_HeytingAlgebra_750 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_822 ∷ T_HeytingAlgebra_750 → T_IsJoinSemilattice_22 Source #

d_isLattice_824 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_IsLattice_340 Source #

du_isLattice_824 ∷ T_HeytingAlgebra_750 → T_IsLattice_340 Source #

d_isMeetSemilattice_826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_IsMeetSemilattice_180 Source #

du_isMeetSemilattice_826 ∷ T_HeytingAlgebra_750 → T_IsMeetSemilattice_180 Source #

d_isPartialOrder_828 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_IsPartialOrder_174 Source #

du_isPartialOrder_828 ∷ T_HeytingAlgebra_750 → T_IsPartialOrder_174 Source #

d_isPreorder_830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_IsPreorder_70 Source #

du_isPreorder_830 ∷ T_HeytingAlgebra_750 → T_IsPreorder_70 Source #

d_joinSemilattice_832 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_JoinSemilattice_14 Source #

du_joinSemilattice_832 ∷ T_HeytingAlgebra_750 → T_JoinSemilattice_14 Source #

d_lattice_834 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_Lattice_386 Source #

du_lattice_834 ∷ T_HeytingAlgebra_750 → T_Lattice_386 Source #

d_maximum_836 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny Source #

du_maximum_836 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny Source #

d_meetSemilattice_838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_MeetSemilattice_200 Source #

du_meetSemilattice_838 ∷ T_HeytingAlgebra_750 → T_MeetSemilattice_200 Source #

d_minimum_840 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny Source #

du_minimum_840 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny Source #

d_poset_842 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_Poset_314 Source #

du_poset_842 ∷ T_HeytingAlgebra_750 → T_Poset_314 Source #

d_preorder_844 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_Preorder_132 Source #

du_preorder_844 ∷ T_HeytingAlgebra_750 → T_Preorder_132 Source #

d_refl_846 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny Source #

du_refl_846 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny Source #

d_reflexive_848 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_848 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_850 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_Setoid_44 Source #

du_setoid_850 ∷ T_HeytingAlgebra_750 → T_Setoid_44 Source #

d_supremum_852 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_supremum_852 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_854 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_854 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_856 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_856 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_858 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_858 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_860 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_860 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_862 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_862 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_864 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_864 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_866 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_866 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_868 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_868 ∷ T_HeytingAlgebra_750 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_870 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_870 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_872 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_872 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_874 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_874 ∷ T_HeytingAlgebra_750 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_876 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_876 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_878 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_878 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_882 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_882 ∷ T_HeytingAlgebra_750 → T_IsPartialEquivalence_16 Source #

d_refl_884 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny Source #

du_refl_884 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny Source #

d_reflexive_886 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_886 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_888 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_888 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_890 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_890 ∷ T_HeytingAlgebra_750 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_BooleanAlgebra_898 ∷ p → p → p → () Source #

data T_BooleanAlgebra_898 Source #

d_Carrier_924 ∷ T_BooleanAlgebra_898 → () Source #

d__'8776'__926 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → () Source #

d__'8804'__928 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → () Source #

d__'8744'__930 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__932 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_'172'__934 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny Source #

d_'8868'_936 ∷ T_BooleanAlgebra_898 → AgdaAny Source #

d_'8869'_938 ∷ T_BooleanAlgebra_898 → AgdaAny Source #

d_isBooleanAlgebra_940 ∷ T_BooleanAlgebra_898 → T_IsBooleanAlgebra_730 Source #

d_heytingAlgebra_946 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_HeytingAlgebra_750 Source #

du_heytingAlgebra_946 ∷ T_BooleanAlgebra_898 → T_HeytingAlgebra_750 Source #

d__'8680'__950 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

du__'8680'__950 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_952 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_952 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedJoinSemilattice_954 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_BoundedJoinSemilattice_102 Source #

du_boundedJoinSemilattice_954 ∷ T_BooleanAlgebra_898 → T_BoundedJoinSemilattice_102 Source #

d_boundedLattice_956 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_BoundedLattice_616 Source #

du_boundedLattice_956 ∷ T_BooleanAlgebra_898 → T_BoundedLattice_616 Source #

d_boundedMeetSemilattice_958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_BoundedMeetSemilattice_288 Source #

du_boundedMeetSemilattice_958 ∷ T_BooleanAlgebra_898 → T_BoundedMeetSemilattice_288 Source #

d_exponential_960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

du_exponential_960 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_infimum_962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_infimum_962 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsBoundedJoinSemilattice_116 Source #

du_isBoundedJoinSemilattice_964 ∷ T_BooleanAlgebra_898 → T_IsBoundedJoinSemilattice_116 Source #

d_isBoundedLattice_966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsBoundedLattice_502 Source #

du_isBoundedLattice_966 ∷ T_BooleanAlgebra_898 → T_IsBoundedLattice_502 Source #

d_isBoundedMeetSemilattice_968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsBoundedMeetSemilattice_274 Source #

du_isBoundedMeetSemilattice_968 ∷ T_BooleanAlgebra_898 → T_IsBoundedMeetSemilattice_274 Source #

d_isEquivalence_970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsEquivalence_26 Source #

du_isEquivalence_970 ∷ T_BooleanAlgebra_898 → T_IsEquivalence_26 Source #

d_isHeytingAlgebra_972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsHeytingAlgebra_598 Source #

du_isHeytingAlgebra_972 ∷ T_BooleanAlgebra_898 → T_IsHeytingAlgebra_598 Source #

d_isJoinSemilattice_974 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsJoinSemilattice_22 Source #

du_isJoinSemilattice_974 ∷ T_BooleanAlgebra_898 → T_IsJoinSemilattice_22 Source #

d_isLattice_976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsLattice_340 Source #

du_isLattice_976 ∷ T_BooleanAlgebra_898 → T_IsLattice_340 Source #

d_isMeetSemilattice_978 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsMeetSemilattice_180 Source #

du_isMeetSemilattice_978 ∷ T_BooleanAlgebra_898 → T_IsMeetSemilattice_180 Source #

d_isPartialOrder_980 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsPartialOrder_174 Source #

du_isPartialOrder_980 ∷ T_BooleanAlgebra_898 → T_IsPartialOrder_174 Source #

d_isPreorder_982 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsPreorder_70 Source #

du_isPreorder_982 ∷ T_BooleanAlgebra_898 → T_IsPreorder_70 Source #

d_joinSemilattice_984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_JoinSemilattice_14 Source #

du_joinSemilattice_984 ∷ T_BooleanAlgebra_898 → T_JoinSemilattice_14 Source #

d_lattice_986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_Lattice_386 Source #

du_lattice_986 ∷ T_BooleanAlgebra_898 → T_Lattice_386 Source #

d_maximum_988 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny Source #

du_maximum_988 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny Source #

d_meetSemilattice_990 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_MeetSemilattice_200 Source #

du_meetSemilattice_990 ∷ T_BooleanAlgebra_898 → T_MeetSemilattice_200 Source #

d_minimum_992 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny Source #

du_minimum_992 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny Source #

d_poset_994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_Poset_314 Source #

du_poset_994 ∷ T_BooleanAlgebra_898 → T_Poset_314 Source #

d_preorder_996 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_Preorder_132 Source #

du_preorder_996 ∷ T_BooleanAlgebra_898 → T_Preorder_132 Source #

d_refl_998 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny Source #

du_refl_998 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny Source #

d_reflexive_1000 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_1000 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_1002 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_Setoid_44 Source #

du_setoid_1002 ∷ T_BooleanAlgebra_898 → T_Setoid_44 Source #

d_supremum_1004 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_supremum_1004 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_1006 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1006 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8680'_1008 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8680'_1008 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8743'_1010 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8743'_1010 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_1012 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_1012 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_1014 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_1014 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_1016 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_1016 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_1018 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_1018 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_1020 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_1020 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_1022 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_1022 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_1024 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_1024 ∷ T_BooleanAlgebra_898 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_1026 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_1026 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_1028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_1028 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'45''8776'_1030 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_Σ_14 Source #

du_'8818''45'resp'45''8776'_1030 ∷ T_BooleanAlgebra_898 → T_Σ_14 Source #

d_'8818''45'resp'691''45''8776'_1032 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'691''45''8776'_1032 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8818''45'resp'737''45''8776'_1034 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8818''45'resp'737''45''8776'_1034 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_1038 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1038 ∷ T_BooleanAlgebra_898 → T_IsPartialEquivalence_16 Source #

d_refl_1040 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny Source #

du_refl_1040 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny Source #

d_reflexive_1042 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1042 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_1044 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1044 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1046 ∷ T_BooleanAlgebra_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #