Documentation

d_Supremum_12 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Infimum_30 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Exponential_40 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsJoinSemilattice_68 ∷ p → p → p → p → p → p → p → () Source #

data T_IsJoinSemilattice_68 Source #

d_isPartialOrder_88 ∷ T_IsJoinSemilattice_68 → T_IsPartialOrder_162 Source #

d_supremum_90 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_x'8804'x'8744'y_96 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_96 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_108 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_122 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_134 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_136 ∷ T_IsJoinSemilattice_68 → T_IsEquivalence_26 Source #

d_isPreorder_138 ∷ T_IsJoinSemilattice_68 → T_IsPreorder_70 Source #

d_refl_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_68 → AgdaAny → AgdaAny Source #

du_refl_140 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny Source #

d_reflexive_142 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_144 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_68 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_146 ∷ T_IsJoinSemilattice_68 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_148 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_150 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_68 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_154 ∷ T_IsJoinSemilattice_68 → T_IsPartialEquivalence_16 Source #

d_refl_156 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny Source #

d_reflexive_158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_158 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_160 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_162 ∷ T_IsJoinSemilattice_68 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_JoinSemilattice_170 ∷ p → p → p → () Source #

data T_JoinSemilattice_170 Source #

d_Carrier_188 ∷ T_JoinSemilattice_170 → () Source #

d__'8776'__190 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → () Source #

d__'8804'__192 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → () Source #

d__'8744'__194 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny Source #

d_isJoinSemilattice_196 ∷ T_JoinSemilattice_170 → T_IsJoinSemilattice_68 Source #

d_antisym_200 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_202 ∷ T_JoinSemilattice_170 → T_IsEquivalence_26 Source #

d_isPartialOrder_204 ∷ T_JoinSemilattice_170 → T_IsPartialOrder_162 Source #

d_isPreorder_206 ∷ T_JoinSemilattice_170 → T_IsPreorder_70 Source #

d_refl_208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → AgdaAny → AgdaAny Source #

du_refl_208 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny Source #

d_reflexive_210 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_212 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_214 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_216 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_218 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_220 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_220 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_222 ∷ T_JoinSemilattice_170 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_224 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_226 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_230 ∷ T_JoinSemilattice_170 → T_IsPartialEquivalence_16 Source #

d_refl_232 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny Source #

d_reflexive_234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_234 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_236 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_238 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_poset_240 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → T_Poset_282 Source #

du_poset_240 ∷ T_JoinSemilattice_170 → T_Poset_282 Source #

d_preorder_244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → T_Preorder_132 Source #

du_preorder_244 ∷ T_JoinSemilattice_170 → T_Preorder_132 Source #

d_IsBoundedJoinSemilattice_262 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsBoundedJoinSemilattice_262 Source #

d_isJoinSemilattice_284 ∷ T_IsBoundedJoinSemilattice_262 → T_IsJoinSemilattice_68 Source #

d_minimum_286 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny Source #

d_antisym_290 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_292 ∷ T_IsBoundedJoinSemilattice_262 → T_IsEquivalence_26 Source #

d_isPartialOrder_294 ∷ T_IsBoundedJoinSemilattice_262 → T_IsPartialOrder_162 Source #

d_isPreorder_296 ∷ T_IsBoundedJoinSemilattice_262 → T_IsPreorder_70 Source #

d_refl_298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny Source #

du_refl_298 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny Source #

d_reflexive_300 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_302 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_304 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_306 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_308 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_308 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_310 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_310 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_262 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_312 ∷ T_IsBoundedJoinSemilattice_262 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_314 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_316 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_320 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_262 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_320 ∷ T_IsBoundedJoinSemilattice_262 → T_IsPartialEquivalence_16 Source #

d_refl_322 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny Source #

d_reflexive_324 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_324 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_326 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_328 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_BoundedJoinSemilattice_336 ∷ p → p → p → () Source #

data T_BoundedJoinSemilattice_336 Source #

d_Carrier_356 ∷ T_BoundedJoinSemilattice_336 → () Source #

d__'8776'__358 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → () Source #

d__'8804'__360 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → () Source #

d__'8744'__362 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8869'_364 ∷ T_BoundedJoinSemilattice_336 → AgdaAny Source #

d_isBoundedJoinSemilattice_366 ∷ T_BoundedJoinSemilattice_336 → T_IsBoundedJoinSemilattice_262 Source #

d_antisym_370 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_372 ∷ T_BoundedJoinSemilattice_336 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_374 ∷ T_BoundedJoinSemilattice_336 → T_IsJoinSemilattice_68 Source #

d_isPartialOrder_376 ∷ T_BoundedJoinSemilattice_336 → T_IsPartialOrder_162 Source #

d_isPreorder_378 ∷ T_BoundedJoinSemilattice_336 → T_IsPreorder_70 Source #

d_minimum_380 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny Source #

d_refl_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny Source #

du_refl_382 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny Source #

d_reflexive_384 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_386 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_388 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_390 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_390 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_392 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_392 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_394 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_396 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_396 ∷ T_BoundedJoinSemilattice_336 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_398 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_398 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_400 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_400 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_404 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_404 ∷ T_BoundedJoinSemilattice_336 → T_IsPartialEquivalence_16 Source #

d_refl_406 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny Source #

d_reflexive_408 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_408 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_410 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_412 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_joinSemilattice_414 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → T_JoinSemilattice_170 Source #

du_joinSemilattice_414 ∷ T_BoundedJoinSemilattice_336 → T_JoinSemilattice_170 Source #

d_joinSemiLattice_416 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → T_JoinSemilattice_170 Source #

du_joinSemiLattice_416 ∷ T_BoundedJoinSemilattice_336 → T_JoinSemilattice_170 Source #

d_poset_420 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → T_Poset_282 Source #

du_poset_420 ∷ T_BoundedJoinSemilattice_336 → T_Poset_282 Source #

d_preorder_422 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → T_Preorder_132 Source #

du_preorder_422 ∷ T_BoundedJoinSemilattice_336 → T_Preorder_132 Source #

d_IsMeetSemilattice_438 ∷ p → p → p → p → p → p → p → () Source #

data T_IsMeetSemilattice_438 Source #

d_isPartialOrder_458 ∷ T_IsMeetSemilattice_438 → T_IsPartialOrder_162 Source #

d_infimum_460 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_x'8743'y'8804'x_466 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_466 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_478 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_478 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_492 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_492 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_504 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_506 ∷ T_IsMeetSemilattice_438 → T_IsEquivalence_26 Source #

d_isPreorder_508 ∷ T_IsMeetSemilattice_438 → T_IsPreorder_70 Source #

d_refl_510 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_438 → AgdaAny → AgdaAny Source #

du_refl_510 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny Source #

d_reflexive_512 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_514 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_516 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_438 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_516 ∷ T_IsMeetSemilattice_438 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_518 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_518 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_520 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_520 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_524 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_438 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_524 ∷ T_IsMeetSemilattice_438 → T_IsPartialEquivalence_16 Source #

d_refl_526 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny Source #

d_reflexive_528 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_528 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_530 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_532 ∷ T_IsMeetSemilattice_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_MeetSemilattice_540 ∷ p → p → p → () Source #

data T_MeetSemilattice_540 Source #

d_Carrier_558 ∷ T_MeetSemilattice_540 → () Source #

d__'8776'__560 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → () Source #

d__'8804'__562 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → () Source #

d__'8743'__564 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny Source #

d_isMeetSemilattice_566 ∷ T_MeetSemilattice_540 → T_IsMeetSemilattice_438 Source #

d_antisym_570 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_572 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_574 ∷ T_MeetSemilattice_540 → T_IsEquivalence_26 Source #

d_isPartialOrder_576 ∷ T_MeetSemilattice_540 → T_IsPartialOrder_162 Source #

d_isPreorder_578 ∷ T_MeetSemilattice_540 → T_IsPreorder_70 Source #

d_refl_580 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → AgdaAny → AgdaAny Source #

du_refl_580 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny Source #

d_reflexive_582 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_584 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_586 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_588 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_588 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_590 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_590 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_592 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_592 ∷ T_MeetSemilattice_540 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_594 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_596 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_596 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_600 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_600 ∷ T_MeetSemilattice_540 → T_IsPartialEquivalence_16 Source #

d_refl_602 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny Source #

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

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

d_sym_606 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_608 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_poset_610 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → T_Poset_282 Source #

du_poset_610 ∷ T_MeetSemilattice_540 → T_Poset_282 Source #

d_preorder_614 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → T_Preorder_132 Source #

du_preorder_614 ∷ T_MeetSemilattice_540 → T_Preorder_132 Source #

d_IsBoundedMeetSemilattice_632 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsBoundedMeetSemilattice_632 Source #

d_isMeetSemilattice_654 ∷ T_IsBoundedMeetSemilattice_632 → T_IsMeetSemilattice_438 Source #

d_maximum_656 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny Source #

d_antisym_660 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_662 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_664 ∷ T_IsBoundedMeetSemilattice_632 → T_IsEquivalence_26 Source #

d_isPartialOrder_666 ∷ T_IsBoundedMeetSemilattice_632 → T_IsPartialOrder_162 Source #

d_isPreorder_668 ∷ T_IsBoundedMeetSemilattice_632 → T_IsPreorder_70 Source #

d_refl_670 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny Source #

du_refl_670 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny Source #

d_reflexive_672 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_674 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_676 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_678 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_678 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_680 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_632 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_682 ∷ T_IsBoundedMeetSemilattice_632 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_684 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_686 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_632 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_690 ∷ T_IsBoundedMeetSemilattice_632 → T_IsPartialEquivalence_16 Source #

d_refl_692 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny Source #

d_reflexive_694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_694 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_696 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_698 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_BoundedMeetSemilattice_706 ∷ p → p → p → () Source #

data T_BoundedMeetSemilattice_706 Source #

d_Carrier_726 ∷ T_BoundedMeetSemilattice_706 → () Source #

d__'8776'__728 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → () Source #

d__'8804'__730 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → () Source #

d__'8743'__732 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8868'_734 ∷ T_BoundedMeetSemilattice_706 → AgdaAny Source #

d_isBoundedMeetSemilattice_736 ∷ T_BoundedMeetSemilattice_706 → T_IsBoundedMeetSemilattice_632 Source #

d_antisym_740 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_742 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_744 ∷ T_BoundedMeetSemilattice_706 → T_IsEquivalence_26 Source #

d_isMeetSemilattice_746 ∷ T_BoundedMeetSemilattice_706 → T_IsMeetSemilattice_438 Source #

d_isPartialOrder_748 ∷ T_BoundedMeetSemilattice_706 → T_IsPartialOrder_162 Source #

d_isPreorder_750 ∷ T_BoundedMeetSemilattice_706 → T_IsPreorder_70 Source #

d_maximum_752 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny Source #

d_refl_754 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny Source #

du_refl_754 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny Source #

d_reflexive_756 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_758 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_760 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_760 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_762 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_762 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_764 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_764 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_766 ∷ T_BoundedMeetSemilattice_706 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_768 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_768 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_770 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_770 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_774 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_774 ∷ T_BoundedMeetSemilattice_706 → T_IsPartialEquivalence_16 Source #

d_refl_776 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny Source #

d_reflexive_778 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_778 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_780 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_782 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_meetSemilattice_784 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → T_MeetSemilattice_540 Source #

du_meetSemilattice_784 ∷ T_BoundedMeetSemilattice_706 → T_MeetSemilattice_540 Source #

d_meetSemiLattice_786 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → T_MeetSemilattice_540 Source #

du_meetSemiLattice_786 ∷ T_BoundedMeetSemilattice_706 → T_MeetSemilattice_540 Source #

d_poset_790 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → T_Poset_282 Source #

du_poset_790 ∷ T_BoundedMeetSemilattice_706 → T_Poset_282 Source #

d_preorder_792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → T_Preorder_132 Source #

du_preorder_792 ∷ T_BoundedMeetSemilattice_706 → T_Preorder_132 Source #

d_IsLattice_810 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsLattice_810 Source #

d_isPartialOrder_834 ∷ T_IsLattice_810 → T_IsPartialOrder_162 Source #

d_supremum_836 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_infimum_838 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isJoinSemilattice_840 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → T_IsJoinSemilattice_68 Source #

du_isJoinSemilattice_840 ∷ T_IsLattice_810 → T_IsJoinSemilattice_68 Source #

d_isMeetSemilattice_842 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → T_IsMeetSemilattice_438 Source #

du_isMeetSemilattice_842 ∷ T_IsLattice_810 → T_IsMeetSemilattice_438 Source #

d_x'8804'x'8744'y_846 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_846 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_848 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_848 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_850 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_850 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_854 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_854 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_856 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_856 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_858 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_858 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_862 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence_864 ∷ T_IsLattice_810 → T_IsEquivalence_26 Source #

d_isPreorder_866 ∷ T_IsLattice_810 → T_IsPreorder_70 Source #

d_refl_868 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → AgdaAny → AgdaAny Source #

du_refl_868 ∷ T_IsLattice_810 → AgdaAny → AgdaAny Source #

d_reflexive_870 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_872 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_874 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_874 ∷ T_IsLattice_810 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_876 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_876 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_878 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_878 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_882 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_882 ∷ T_IsLattice_810 → T_IsPartialEquivalence_16 Source #

d_refl_884 ∷ T_IsLattice_810 → AgdaAny → AgdaAny Source #

d_reflexive_886 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsLattice_810 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_sym_888 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_890 ∷ T_IsLattice_810 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Lattice_898 ∷ p → p → p → () Source #

data T_Lattice_898 Source #

d_Carrier_918 ∷ T_Lattice_898 → () Source #

d__'8776'__920 ∷ T_Lattice_898 → AgdaAny → AgdaAny → () Source #

d__'8804'__922 ∷ T_Lattice_898 → AgdaAny → AgdaAny → () Source #

d__'8744'__924 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__926 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_isLattice_928 ∷ T_Lattice_898 → T_IsLattice_810 Source #

d_antisym_932 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_934 ∷ T_Lattice_898 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_936 ∷ T_Lattice_898 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_938 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → T_IsJoinSemilattice_68 Source #

du_isJoinSemilattice_938 ∷ T_Lattice_898 → T_IsJoinSemilattice_68 Source #

d_isMeetSemilattice_940 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → T_IsMeetSemilattice_438 Source #

du_isMeetSemilattice_940 ∷ T_Lattice_898 → T_IsMeetSemilattice_438 Source #

d_isPartialOrder_942 ∷ T_Lattice_898 → T_IsPartialOrder_162 Source #

d_isPreorder_944 ∷ T_Lattice_898 → T_IsPreorder_70 Source #

d_refl_946 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → AgdaAny → AgdaAny Source #

du_refl_946 ∷ T_Lattice_898 → AgdaAny → AgdaAny Source #

d_reflexive_948 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_950 ∷ T_Lattice_898 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_952 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_954 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_954 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_956 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_956 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_958 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_960 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_962 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_964 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_966 ∷ T_Lattice_898 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_968 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_970 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_974 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_974 ∷ T_Lattice_898 → T_IsPartialEquivalence_16 Source #

d_refl_976 ∷ T_Lattice_898 → AgdaAny → AgdaAny Source #

d_reflexive_978 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_978 ∷ T_Lattice_898 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_980 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_982 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → T_Setoid_44 Source #

du_setoid_984 ∷ T_Lattice_898 → T_Setoid_44 Source #

d_joinSemilattice_986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → T_JoinSemilattice_170 Source #

du_joinSemilattice_986 ∷ T_Lattice_898 → T_JoinSemilattice_170 Source #

d_meetSemilattice_988 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → T_MeetSemilattice_540 Source #

du_meetSemilattice_988 ∷ T_Lattice_898 → T_MeetSemilattice_540 Source #

d_poset_992 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → T_Poset_282 Source #

du_poset_992 ∷ T_Lattice_898 → T_Poset_282 Source #

d_preorder_994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Lattice_898 → T_Preorder_132 Source #

du_preorder_994 ∷ T_Lattice_898 → T_Preorder_132 Source #

d_IsDistributiveLattice_1012 ∷ p → p → p → p → p → p → p → p → () Source #

data T_IsDistributiveLattice_1012 Source #

d_isLattice_1034 ∷ T_IsDistributiveLattice_1012 → T_IsLattice_810 Source #

d_'8743''45'distrib'737''45''8744'_1036 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_1040 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_1042 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_1044 ∷ T_IsDistributiveLattice_1012 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_1046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → T_IsJoinSemilattice_68 Source #

du_isJoinSemilattice_1046 ∷ T_IsDistributiveLattice_1012 → T_IsJoinSemilattice_68 Source #

d_isMeetSemilattice_1048 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → T_IsMeetSemilattice_438 Source #

du_isMeetSemilattice_1048 ∷ T_IsDistributiveLattice_1012 → T_IsMeetSemilattice_438 Source #

d_isPartialOrder_1050 ∷ T_IsDistributiveLattice_1012 → T_IsPartialOrder_162 Source #

d_isPreorder_1052 ∷ T_IsDistributiveLattice_1012 → T_IsPreorder_70 Source #

d_refl_1054 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny Source #

du_refl_1054 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny Source #

d_reflexive_1056 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_1058 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_1060 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_1062 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_1062 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_1064 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_1064 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_1066 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_1066 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_1068 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_1068 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_1070 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_1070 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_1072 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_1072 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_1074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_1074 ∷ T_IsDistributiveLattice_1012 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_1076 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_1076 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_1078 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_1078 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_1082 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1082 ∷ T_IsDistributiveLattice_1012 → T_IsPartialEquivalence_16 Source #

d_refl_1084 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny Source #

d_reflexive_1086 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1086 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_1088 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1090 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_DistributiveLattice_1098 ∷ p → p → p → () Source #

data T_DistributiveLattice_1098 Source #

d_Carrier_1118 ∷ T_DistributiveLattice_1098 → () Source #

d__'8776'__1120 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → () Source #

d__'8804'__1122 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → () Source #

d__'8744'__1124 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__1126 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny Source #

d_isDistributiveLattice_1128 ∷ T_DistributiveLattice_1098 → T_IsDistributiveLattice_1012 Source #

d_'8743''45'distrib'737''45''8744'_1132 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isLattice_1136 ∷ T_DistributiveLattice_1098 → T_IsLattice_810 Source #

d_lattice_1138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_Lattice_898 Source #

du_lattice_1138 ∷ T_DistributiveLattice_1098 → T_Lattice_898 Source #

d_antisym_1142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_antisym_1142 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_1144 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_infimum_1144 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_1146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_IsEquivalence_26 Source #

du_isEquivalence_1146 ∷ T_DistributiveLattice_1098 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_1148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_IsJoinSemilattice_68 Source #

du_isJoinSemilattice_1148 ∷ T_DistributiveLattice_1098 → T_IsJoinSemilattice_68 Source #

d_isLattice_1150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_IsLattice_810 Source #

du_isLattice_1150 ∷ T_DistributiveLattice_1098 → T_IsLattice_810 Source #

d_isMeetSemilattice_1152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_IsMeetSemilattice_438 Source #

du_isMeetSemilattice_1152 ∷ T_DistributiveLattice_1098 → T_IsMeetSemilattice_438 Source #

d_isPartialOrder_1154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_IsPartialOrder_162 Source #

du_isPartialOrder_1154 ∷ T_DistributiveLattice_1098 → T_IsPartialOrder_162 Source #

d_isPreorder_1156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_IsPreorder_70 Source #

du_isPreorder_1156 ∷ T_DistributiveLattice_1098 → T_IsPreorder_70 Source #

d_joinSemilattice_1158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_JoinSemilattice_170 Source #

du_joinSemilattice_1158 ∷ T_DistributiveLattice_1098 → T_JoinSemilattice_170 Source #

d_meetSemilattice_1160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_MeetSemilattice_540 Source #

du_meetSemilattice_1160 ∷ T_DistributiveLattice_1098 → T_MeetSemilattice_540 Source #

d_poset_1162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_Poset_282 Source #

du_poset_1162 ∷ T_DistributiveLattice_1098 → T_Poset_282 Source #

d_preorder_1164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_Preorder_132 Source #

du_preorder_1164 ∷ T_DistributiveLattice_1098 → T_Preorder_132 Source #

d_refl_1166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny Source #

du_refl_1166 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny Source #

d_reflexive_1168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_reflexive_1168 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_1170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_Setoid_44 Source #

du_setoid_1170 ∷ T_DistributiveLattice_1098 → T_Setoid_44 Source #

d_supremum_1172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → T_Σ_14 Source #

du_supremum_1172 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_1174 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1174 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_1176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_1176 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_1178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_1178 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_1180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_1180 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_1182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_1182 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_1184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_1184 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_1186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_1186 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_1188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_1188 ∷ T_DistributiveLattice_1098 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_1190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_1190 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_1192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_1192 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_1196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1196 ∷ T_DistributiveLattice_1098 → T_IsPartialEquivalence_16 Source #

d_refl_1198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny Source #

du_refl_1198 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny Source #

d_reflexive_1200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1200 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_1202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1202 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1204 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1204 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBoundedLattice_1226 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsBoundedLattice_1226 Source #

d_isLattice_1254 ∷ T_IsBoundedLattice_1226 → T_IsLattice_810 Source #

d_maximum_1256 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny Source #

d_minimum_1258 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny Source #

d_antisym_1262 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_1264 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isEquivalence_1266 ∷ T_IsBoundedLattice_1226 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_1268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → T_IsJoinSemilattice_68 Source #

du_isJoinSemilattice_1268 ∷ T_IsBoundedLattice_1226 → T_IsJoinSemilattice_68 Source #

d_isMeetSemilattice_1270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → T_IsMeetSemilattice_438 Source #

du_isMeetSemilattice_1270 ∷ T_IsBoundedLattice_1226 → T_IsMeetSemilattice_438 Source #

d_isPartialOrder_1272 ∷ T_IsBoundedLattice_1226 → T_IsPartialOrder_162 Source #

d_isPreorder_1274 ∷ T_IsBoundedLattice_1226 → T_IsPreorder_70 Source #

d_refl_1276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → AgdaAny → AgdaAny Source #

du_refl_1276 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny Source #

d_reflexive_1278 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_1280 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_1282 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_1284 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_1284 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_1286 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_1286 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_1288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_1288 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_1290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_1290 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_1292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_1292 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_1294 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_1294 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_1296 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_1296 ∷ T_IsBoundedLattice_1226 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_1298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_1298 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_1300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_1300 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_1304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1304 ∷ T_IsBoundedLattice_1226 → T_IsPartialEquivalence_16 Source #

d_refl_1306 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny Source #

d_reflexive_1308 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1308 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_1310 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1312 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isBoundedJoinSemilattice_1314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → T_IsBoundedJoinSemilattice_262 Source #

du_isBoundedJoinSemilattice_1314 ∷ T_IsBoundedLattice_1226 → T_IsBoundedJoinSemilattice_262 Source #

d_isBoundedMeetSemilattice_1316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBoundedLattice_1226 → T_IsBoundedMeetSemilattice_632 Source #

du_isBoundedMeetSemilattice_1316 ∷ T_IsBoundedLattice_1226 → T_IsBoundedMeetSemilattice_632 Source #

d_BoundedLattice_1324 ∷ p → p → p → () Source #

data T_BoundedLattice_1324 Source #

d_Carrier_1348 ∷ T_BoundedLattice_1324 → () Source #

d__'8776'__1350 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → () Source #

d__'8804'__1352 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → () Source #

d__'8744'__1354 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__1356 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8868'_1358 ∷ T_BoundedLattice_1324 → AgdaAny Source #

d_'8869'_1360 ∷ T_BoundedLattice_1324 → AgdaAny Source #

d_isBoundedLattice_1362 ∷ T_BoundedLattice_1324 → T_IsBoundedLattice_1226 Source #

d_antisym_1366 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_1368 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_1370 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_IsBoundedJoinSemilattice_262 Source #

du_isBoundedJoinSemilattice_1370 ∷ T_BoundedLattice_1324 → T_IsBoundedJoinSemilattice_262 Source #

d_isBoundedMeetSemilattice_1372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_IsBoundedMeetSemilattice_632 Source #

du_isBoundedMeetSemilattice_1372 ∷ T_BoundedLattice_1324 → T_IsBoundedMeetSemilattice_632 Source #

d_isEquivalence_1374 ∷ T_BoundedLattice_1324 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_1376 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_IsJoinSemilattice_68 Source #

du_isJoinSemilattice_1376 ∷ T_BoundedLattice_1324 → T_IsJoinSemilattice_68 Source #

d_isLattice_1378 ∷ T_BoundedLattice_1324 → T_IsLattice_810 Source #

d_isMeetSemilattice_1380 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_IsMeetSemilattice_438 Source #

du_isMeetSemilattice_1380 ∷ T_BoundedLattice_1324 → T_IsMeetSemilattice_438 Source #

d_isPartialOrder_1382 ∷ T_BoundedLattice_1324 → T_IsPartialOrder_162 Source #

d_isPreorder_1384 ∷ T_BoundedLattice_1324 → T_IsPreorder_70 Source #

d_maximum_1386 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny Source #

d_minimum_1388 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny Source #

d_refl_1390 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny Source #

du_refl_1390 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny Source #

d_reflexive_1392 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_1394 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_1396 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_1398 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_1398 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_1400 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_1400 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_1402 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_1402 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_1404 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_1404 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_1406 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_1406 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_1408 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_1408 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_1410 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_1410 ∷ T_BoundedLattice_1324 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_1412 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_1412 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_1414 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_1414 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_1418 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1418 ∷ T_BoundedLattice_1324 → T_IsPartialEquivalence_16 Source #

d_refl_1420 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny Source #

d_reflexive_1422 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1422 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_1424 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1426 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_boundedJoinSemilattice_1428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_BoundedJoinSemilattice_336 Source #

du_boundedJoinSemilattice_1428 ∷ T_BoundedLattice_1324 → T_BoundedJoinSemilattice_336 Source #

d_boundedMeetSemilattice_1430 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_BoundedMeetSemilattice_706 Source #

du_boundedMeetSemilattice_1430 ∷ T_BoundedLattice_1324 → T_BoundedMeetSemilattice_706 Source #

d_lattice_1432 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_Lattice_898 Source #

du_lattice_1432 ∷ T_BoundedLattice_1324 → T_Lattice_898 Source #

d_joinSemilattice_1436 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_JoinSemilattice_170 Source #

du_joinSemilattice_1436 ∷ T_BoundedLattice_1324 → T_JoinSemilattice_170 Source #

d_meetSemilattice_1438 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_MeetSemilattice_540 Source #

du_meetSemilattice_1438 ∷ T_BoundedLattice_1324 → T_MeetSemilattice_540 Source #

d_poset_1440 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_Poset_282 Source #

du_poset_1440 ∷ T_BoundedLattice_1324 → T_Poset_282 Source #

d_preorder_1442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_Preorder_132 Source #

du_preorder_1442 ∷ T_BoundedLattice_1324 → T_Preorder_132 Source #

d_setoid_1444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_Setoid_44 Source #

du_setoid_1444 ∷ T_BoundedLattice_1324 → T_Setoid_44 Source #

d_IsHeytingAlgebra_1468 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsHeytingAlgebra_1468 Source #

d_isBoundedLattice_1496 ∷ T_IsHeytingAlgebra_1468 → T_IsBoundedLattice_1226 Source #

d_exponential_1498 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_transpose'45''8680'_1506 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8680'_1506 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_transpose'45''8743'_1522 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_transpose'45''8743'_1522 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_antisym_1534 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_infimum_1536 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_isBoundedJoinSemilattice_1538 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → T_IsBoundedJoinSemilattice_262 Source #

du_isBoundedJoinSemilattice_1538 ∷ T_IsHeytingAlgebra_1468 → T_IsBoundedJoinSemilattice_262 Source #

d_isBoundedMeetSemilattice_1540 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → T_IsBoundedMeetSemilattice_632 Source #

du_isBoundedMeetSemilattice_1540 ∷ T_IsHeytingAlgebra_1468 → T_IsBoundedMeetSemilattice_632 Source #

d_isEquivalence_1542 ∷ T_IsHeytingAlgebra_1468 → T_IsEquivalence_26 Source #

d_isJoinSemilattice_1544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → T_IsJoinSemilattice_68 Source #

du_isJoinSemilattice_1544 ∷ T_IsHeytingAlgebra_1468 → T_IsJoinSemilattice_68 Source #

d_isLattice_1546 ∷ T_IsHeytingAlgebra_1468 → T_IsLattice_810 Source #

d_isMeetSemilattice_1548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → T_IsMeetSemilattice_438 Source #

du_isMeetSemilattice_1548 ∷ T_IsHeytingAlgebra_1468 → T_IsMeetSemilattice_438 Source #

d_isPartialOrder_1550 ∷ T_IsHeytingAlgebra_1468 → T_IsPartialOrder_162 Source #

d_isPreorder_1552 ∷ T_IsHeytingAlgebra_1468 → T_IsPreorder_70 Source #

d_maximum_1554 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny Source #

d_minimum_1556 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny Source #

d_refl_1558 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny Source #

du_refl_1558 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny Source #

d_reflexive_1560 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_supremum_1562 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → T_Σ_14 Source #

d_trans_1564 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'x_1566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'x_1566 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8743'y'8804'y_1568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8743'y'8804'y_1568 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny Source #

d_x'8804'x'8744'y_1570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny Source #

du_x'8804'x'8744'y_1570 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny Source #

d_y'8804'x'8744'y_1572 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny Source #

du_y'8804'x'8744'y_1572 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8743''45'greatest_1574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8743''45'greatest_1574 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8744''45'least_1576 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8744''45'least_1576 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'45''8776'_1578 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → T_Σ_14 Source #

du_'8764''45'resp'45''8776'_1578 ∷ T_IsHeytingAlgebra_1468 → T_Σ_14 Source #

d_'8764''45'resp'691''45''8776'_1580 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'691''45''8776'_1580 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8764''45'resp'737''45''8776'_1582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8764''45'resp'737''45''8776'_1582 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isPartialEquivalence_1586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1586 ∷ T_IsHeytingAlgebra_1468 → T_IsPartialEquivalence_16 Source #

d_refl_1588 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny Source #

d_reflexive_1590 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1590 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_1592 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1594 ∷ T_IsHeytingAlgebra_1468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_HeytingAlgebra_1602 ∷ p → p → p → () Source #

data T_HeytingAlgebra_1602 Source #

d_Carrier_1628 ∷ T_HeytingAlgebra_1602 → () Source #

d__'8776'__1630 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → () Source #

d__'8804'__1632 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → () Source #

d__'8744'__1634 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8743'__1636 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny Source #