Documentation

d_isEquivalence_56 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsEquivalence_28 Source #

du_isEquivalence_56 ∷ T_IsEquivalence_28 → T_IsEquivalence_28 Source #

d_isDecEquivalence_76 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_48 → T_IsDecEquivalence_48 Source #

du_isDecEquivalence_76 ∷ T_IsDecEquivalence_48 → T_IsDecEquivalence_48 Source #

d_isPreorder_100 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → T_IsPreorder_76 Source #

du_isPreorder_100 ∷ T_IsPreorder_76 → T_IsPreorder_76 Source #

d_isPartialOrder_142 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → T_IsPartialOrder_248 Source #

du_isPartialOrder_142 ∷ T_IsPartialOrder_248 → T_IsPartialOrder_248 Source #

d_setoid_188 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 Source #

du_setoid_188 ∷ T_Setoid_46 → T_Setoid_46 Source #

d_decSetoid_192 ∷ T_Level_18 → T_Level_18 → T_DecSetoid_90 → T_DecSetoid_90 Source #

du_decSetoid_192 ∷ T_DecSetoid_90 → T_DecSetoid_90 Source #

d_preorder_196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_Preorder_142 Source #

du_preorder_196 ∷ T_Preorder_142 → T_Preorder_142 Source #

d_poset_200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_Poset_492 Source #

du_poset_200 ∷ T_Poset_492 → T_Poset_492 Source #

d_All'45'resp'45'Pointwise_206 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #

du_All'45'resp'45'Pointwise_206 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #

d_Any'45'resp'45'Pointwise_222 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #

du_Any'45'resp'45'Pointwise_222 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #

d_AllPairs'45'resp'45'Pointwise_240 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_AllPairs_20 → T_AllPairs_20 Source #

du_AllPairs'45'resp'45'Pointwise_240 ∷ T_Σ_14 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_AllPairs_20 → T_AllPairs_20 Source #

d_tabulate'8314'_264 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → Integer → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → T_Pointwise_48 Source #

du_tabulate'8314'_264 ∷ Integer → (T_Fin_10 → AgdaAny) → T_Pointwise_48 Source #

d_tabulate'8315'_280 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → Integer → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → T_Pointwise_48 → T_Fin_10 → AgdaAny Source #

du_tabulate'8315'_280 ∷ T_Pointwise_48 → T_Fin_10 → AgdaAny Source #

d_'43''43''8314'_296 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #

du_'43''43''8314'_296 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #

d_'43''43''45'cancel'737'_308 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

du_'43''43''45'cancel'737'_308 ∷ [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

d_'43''43''45'cancel'691'_322 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

du_'43''43''45'cancel'691'_322 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

d_'43''43''8314''737'_364 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

du_'43''43''8314''737'_364 ∷ (AgdaAny → AgdaAny) → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

d_'43''43''8314''691'_372 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

du_'43''43''8314''691'_372 ∷ (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

d_concat'8314'_382 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [[AgdaAny]] → [[AgdaAny]] → T_Pointwise_48 → T_Pointwise_48 Source #

du_concat'8314'_382 ∷ [[AgdaAny]] → [[AgdaAny]] → T_Pointwise_48 → T_Pointwise_48 Source #

d_reverseAcc'8314'_388 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #

du_reverseAcc'8314'_388 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #

d_'691''43''43''8314'_398 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #

du_'691''43''43''8314'_398 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #

d_reverse'8314'_404 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

du_reverse'8314'_404 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

d_map'8314'_414 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Pointwise_48 → T_Pointwise_48 Source #

du_map'8314'_414 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

d_map'8315'_436 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Pointwise_48 → T_Pointwise_48 Source #

du_map'8315'_436 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

d_foldr'8314'_466 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_48 → AgdaAny Source #

du_foldr'8314'_466 ∷ [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_48 → AgdaAny Source #

d_filter'8314'_512 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

du_filter'8314'_512 ∷ (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #

d_replicate'8314'_568 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → Integer → T_Pointwise_48 Source #

du_replicate'8314'_568 ∷ AgdaAny → Integer → T_Pointwise_48 Source #

d_lookup'8315'_580 ∷ T_Level_18 → () → [AgdaAny] → T_Level_18 → () → [AgdaAny] → T_Level_18 → (AgdaAny → AgdaAny → ()) → T__'8801'__12 → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → AgdaAny) → T_Pointwise_48 Source #

du_lookup'8315'_580 ∷ [AgdaAny] → [AgdaAny] → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → AgdaAny) → T_Pointwise_48 Source #

d_lookup'8314'_592 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Fin_10 → AgdaAny Source #

du_lookup'8314'_592 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Fin_10 → AgdaAny Source #

d_Pointwise'45''8801''8658''8801'_600 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T__'8801'__12 Source #

d_'8801''8658'Pointwise'45''8801'_606 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T_Pointwise_48 Source #

du_'8801''8658'Pointwise'45''8801'_606 ∷ [AgdaAny] → T_Pointwise_48 Source #

d_Pointwise'45''8801''8596''8801'_608 ∷ T_Level_18 → () → T_Inverse_2122 Source #

du_Pointwise'45''8801''8596''8801'_608 ∷ T_Inverse_2122 Source #