Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 #
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 #
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 #
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_refl_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsJoinSemilattice_68 → 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 #
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 #
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 #
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__'8776'__190 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → () Source #
d__'8804'__192 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → () Source #
d_antisym_200 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_refl_208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → AgdaAny → AgdaAny 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 #
d_y'8804'x'8744'y_218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
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 #
d_reflexive_234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_trans_238 ∷ T_JoinSemilattice_170 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_preorder_244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_JoinSemilattice_170 → T_Preorder_132 Source #
d_IsBoundedJoinSemilattice_262 ∷ p → p → p → p → p → p → p → p → () Source #
d_antisym_290 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny 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 #
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 #
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 #
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 #
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 #
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_trans_328 ∷ T_IsBoundedJoinSemilattice_262 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_BoundedJoinSemilattice_336 ∷ p → p → p → () Source #
d__'8776'__358 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny → () Source #
d__'8804'__360 ∷ T_BoundedJoinSemilattice_336 → AgdaAny → 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_refl_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → AgdaAny → AgdaAny 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 #
d_y'8804'x'8744'y_392 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
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 #
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_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 #
d_joinSemiLattice_416 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_preorder_422 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedJoinSemilattice_336 → T_Preorder_132 Source #
d_IsMeetSemilattice_438 ∷ p → p → p → p → p → p → p → () 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 #
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 #
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_refl_510 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMeetSemilattice_438 → 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 #
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 #
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 #
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__'8776'__560 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → () Source #
d__'8804'__562 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → () Source #
d_antisym_570 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_refl_580 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → 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 #
d_x'8743'y'8804'y_588 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
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 #
d_reflexive_604 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_trans_608 ∷ T_MeetSemilattice_540 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_preorder_614 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_MeetSemilattice_540 → T_Preorder_132 Source #
d_IsBoundedMeetSemilattice_632 ∷ p → p → p → p → p → p → p → p → () Source #
d_antisym_660 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny 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 #
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 #
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 #
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 #
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 #
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_trans_698 ∷ T_IsBoundedMeetSemilattice_632 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_BoundedMeetSemilattice_706 ∷ p → p → p → () Source #
d__'8776'__728 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → AgdaAny → () Source #
d__'8804'__730 ∷ T_BoundedMeetSemilattice_706 → AgdaAny → 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_refl_754 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedMeetSemilattice_706 → 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 #
d_x'8743'y'8804'y_762 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
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 #
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_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 #
d_meetSemiLattice_786 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_preorder_792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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_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 #
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 #
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 #
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 #
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 #
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 #
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_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 #
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 #
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 #
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 #
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_antisym_932 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_infimum_934 ∷ T_Lattice_898 → AgdaAny → AgdaAny → T_Σ_14 Source #
d_isJoinSemilattice_938 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_refl_946 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_x'8743'y'8804'y_956 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_y'8804'x'8744'y_960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
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 #
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 #
d_trans_982 ∷ T_Lattice_898 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_joinSemilattice_986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_IsDistributiveLattice_1012 ∷ p → p → p → p → p → p → p → p → () 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_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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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_trans_1090 ∷ T_IsDistributiveLattice_1012 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_DistributiveLattice_1098 ∷ p → p → p → () Source #
d__'8776'__1120 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → () Source #
d__'8804'__1122 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → () Source #
d_'8743''45'distrib'737''45''8744'_1132 ∷ T_DistributiveLattice_1098 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_lattice_1138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_isEquivalence_1146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_isLattice_1150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_isPartialOrder_1154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_joinSemilattice_1158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_poset_1162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_refl_1166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_setoid_1170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
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 #
d_x'8743'y'8804'y_1178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_y'8804'x'8744'y_1182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
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 #
d_refl_1198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
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 #
d_antisym_1262 ∷ T_IsBoundedLattice_1226 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny 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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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__'8776'__1350 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → () Source #
d__'8804'__1352 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → () Source #
d_antisym_1366 ∷ T_BoundedLattice_1324 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isBoundedJoinSemilattice_1370 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_isJoinSemilattice_1376 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_IsJoinSemilattice_68 Source #
d_isMeetSemilattice_1380 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_IsMeetSemilattice_438 Source #
d_refl_1390 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → AgdaAny → AgdaAny 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 #
d_x'8743'y'8804'y_1400 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_y'8804'x'8744'y_1404 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
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 #
d_reflexive_1422 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_boundedMeetSemilattice_1430 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_joinSemilattice_1436 ∷ T_Level_18 → T_Level_18 → T_Level_18 → 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 #
d_preorder_1442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BoundedLattice_1324 → T_Preorder_132 Source #
d_IsHeytingAlgebra_1468 ∷ p → p → p → p → p → p → p → p → p → p → p → () 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_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_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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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 #
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__'8776'__1630 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → () Source #
d__'8804'__1632 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → () Source #
d_boundedLattice_1646 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_BoundedLattice_1324 Source #
d_transpose'45''8680'_1652 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_transpose'45''8680'_1652 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_transpose'45''8743'_1654 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_transpose'45''8743'_1654 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_antisym_1658 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_antisym_1658 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_boundedJoinSemilattice_1660 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_BoundedJoinSemilattice_336 Source #
d_boundedMeetSemilattice_1662 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_BoundedMeetSemilattice_706 Source #
d_infimum_1664 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → T_Σ_14 Source #
d_isBoundedJoinSemilattice_1666 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_IsBoundedJoinSemilattice_262 Source #
d_isBoundedLattice_1668 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_IsBoundedLattice_1226 Source #
d_isBoundedMeetSemilattice_1670 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_IsBoundedMeetSemilattice_632 Source #
d_isEquivalence_1672 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_IsEquivalence_26 Source #
d_isJoinSemilattice_1674 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_IsJoinSemilattice_68 Source #
d_isLattice_1676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_IsLattice_810 Source #
d_isMeetSemilattice_1678 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_IsMeetSemilattice_438 Source #
d_isPartialOrder_1680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_IsPartialOrder_162 Source #
d_isPreorder_1682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_IsPreorder_70 Source #
d_joinSemilattice_1684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_JoinSemilattice_170 Source #
d_lattice_1686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_Lattice_898 Source #
d_maximum_1688 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny Source #
d_meetSemilattice_1690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_MeetSemilattice_540 Source #
d_minimum_1692 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny Source #
d_preorder_1696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_Preorder_132 Source #
d_refl_1698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny Source #
d_reflexive_1700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_supremum_1704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → T_Σ_14 Source #
d_trans_1706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_trans_1706 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8743'y'8804'x_1708 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8743'y'8804'y_1710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'x'8744'y_1712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny Source #
d_y'8804'x'8744'y_1714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8743''45'greatest_1716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8743''45'greatest_1716 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8744''45'least_1718 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8744''45'least_1718 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8764''45'resp'45''8776'_1720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_Σ_14 Source #
d_'8764''45'resp'691''45''8776'_1722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8764''45'resp'691''45''8776'_1722 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8764''45'resp'737''45''8776'_1724 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8764''45'resp'737''45''8776'_1724 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_1728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → T_IsPartialEquivalence_16 Source #
d_refl_1730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny Source #
d_reflexive_1732 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_sym_1734 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_sym_1734 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_trans_1736 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_trans_1736 ∷ T_HeytingAlgebra_1602 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_IsBooleanAlgebra_1760 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #
newtype T_IsBooleanAlgebra_1760 Source #
d__'8680'__1792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny Source #
du__'8680'__1792 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_antisym_1802 ∷ T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isBoundedJoinSemilattice_1808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → T_IsBoundedJoinSemilattice_262 Source #
du_isBoundedJoinSemilattice_1808 ∷ T_IsBooleanAlgebra_1760 → T_IsBoundedJoinSemilattice_262 Source #
d_isBoundedMeetSemilattice_1812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → T_IsBoundedMeetSemilattice_632 Source #
du_isBoundedMeetSemilattice_1812 ∷ T_IsBooleanAlgebra_1760 → T_IsBoundedMeetSemilattice_632 Source #
d_isJoinSemilattice_1816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → T_IsJoinSemilattice_68 Source #
d_isMeetSemilattice_1820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → T_IsMeetSemilattice_438 Source #
d_refl_1830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny Source #
d_trans_1836 ∷ T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_transpose'45''8680'_1838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_transpose'45''8680'_1838 ∷ T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_transpose'45''8743'_1840 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_transpose'45''8743'_1840 ∷ T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8743'y'8804'x_1842 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8743'y'8804'y_1844 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'x'8744'y_1846 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny Source #
d_y'8804'x'8744'y_1848 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8743''45'greatest_1850 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8743''45'greatest_1850 ∷ T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8744''45'least_1852 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8744''45'least_1852 ∷ T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8764''45'resp'45''8776'_1854 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → T_Σ_14 Source #
d_'8764''45'resp'691''45''8776'_1856 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8764''45'resp'691''45''8776'_1856 ∷ T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8764''45'resp'737''45''8776'_1858 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8764''45'resp'737''45''8776'_1858 ∷ T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_1862 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → T_IsPartialEquivalence_16 Source #
d_reflexive_1866 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_sym_1868 ∷ T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_trans_1870 ∷ T_IsBooleanAlgebra_1760 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_BooleanAlgebra_1878 ∷ p → p → p → () Source #
data T_BooleanAlgebra_1878 Source #
d__'8776'__1906 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → () Source #
d__'8804'__1908 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → () Source #
d_heytingAlgebra_1926 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_HeytingAlgebra_1602 Source #
d__'8680'__1930 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny Source #
d_antisym_1932 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_antisym_1932 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_boundedJoinSemilattice_1934 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_BoundedJoinSemilattice_336 Source #
d_boundedLattice_1936 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_BoundedLattice_1324 Source #
d_boundedMeetSemilattice_1938 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_BoundedMeetSemilattice_706 Source #
d_exponential_1940 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #
d_infimum_1942 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → T_Σ_14 Source #
d_isBoundedJoinSemilattice_1944 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsBoundedJoinSemilattice_262 Source #
d_isBoundedLattice_1946 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsBoundedLattice_1226 Source #
d_isBoundedMeetSemilattice_1948 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsBoundedMeetSemilattice_632 Source #
d_isEquivalence_1950 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsEquivalence_26 Source #
d_isHeytingAlgebra_1952 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsHeytingAlgebra_1468 Source #
d_isJoinSemilattice_1954 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsJoinSemilattice_68 Source #
d_isLattice_1956 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsLattice_810 Source #
d_isMeetSemilattice_1958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsMeetSemilattice_438 Source #
d_isPartialOrder_1960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsPartialOrder_162 Source #
d_isPreorder_1962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsPreorder_70 Source #
d_joinSemilattice_1964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_JoinSemilattice_170 Source #
d_lattice_1966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_Lattice_898 Source #
d_maximum_1968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny Source #
d_meetSemilattice_1970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_MeetSemilattice_540 Source #
d_minimum_1972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny Source #
d_preorder_1976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_Preorder_132 Source #
d_refl_1978 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny Source #
d_reflexive_1980 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_supremum_1984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → T_Σ_14 Source #
d_trans_1986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_trans_1986 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_transpose'45''8680'_1988 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_transpose'45''8680'_1988 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_transpose'45''8743'_1990 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_transpose'45''8743'_1990 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8743'y'8804'x_1992 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8743'y'8804'y_1994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'x'8744'y_1996 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny Source #
d_y'8804'x'8744'y_1998 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8743''45'greatest_2000 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8743''45'greatest_2000 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8744''45'least_2002 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8744''45'least_2002 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8764''45'resp'45''8776'_2004 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_Σ_14 Source #
d_'8764''45'resp'691''45''8776'_2006 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8764''45'resp'691''45''8776'_2006 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8764''45'resp'737''45''8776'_2008 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8764''45'resp'737''45''8776'_2008 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_isPartialEquivalence_2012 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → T_IsPartialEquivalence_16 Source #
d_refl_2014 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny Source #
d_reflexive_2016 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_sym_2018 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_sym_2018 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_trans_2020 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_trans_2020 ∷ T_BooleanAlgebra_1878 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #