Documentation

d_'172'Fin0_20 ∷ T_Fin_10 → T_Irrelevant_20 Source #

d_nonZeroIndex_22 ∷ Integer → T_Fin_10 → T_NonZero_112 Source #

du_nonZeroIndex_22 ∷ T_NonZero_112 Source #

d_0'8596''8869'_24 ∷ T_Inverse_1960 Source #

d_1'8596''8868'_26 ∷ T_Inverse_1960 Source #

d_'46'extendedlambda3_34 ∷ T_Fin_10 → T__'8801'__12 Source #

d_2'8596'Bool_36 ∷ T_Inverse_1960 Source #

d_'46'extendedlambda4_38 ∷ T_Fin_10 → Bool Source #

d_'46'extendedlambda7_44 ∷ T_Fin_10 → T__'8801'__12 Source #

d_0'8802'1'43'n_46 ∷ Integer → T_Fin_10 → T__'8801'__12 → T_Irrelevant_20 Source #

d_suc'45'injective_48 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d__'8799'__50 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Dec_20 Source #

du__'8799'__50 ∷ T_Fin_10 → T_Fin_10 → T_Dec_20 Source #

d_'8801''45'isDecEquivalence_60 ∷ Integer → T_IsDecEquivalence_44 Source #

du_'8801''45'isDecEquivalence_60 ∷ T_IsDecEquivalence_44 Source #

d_'8801''45'preorder_62 ∷ Integer → T_Preorder_132 Source #

du_'8801''45'preorder_62 ∷ T_Preorder_132 Source #

d_'8801''45'setoid_66 ∷ Integer → T_Setoid_44 Source #

du_'8801''45'setoid_66 ∷ T_Setoid_44 Source #

d_'8801''45'decSetoid_70 ∷ Integer → T_DecSetoid_84 Source #

du_'8801''45'decSetoid_70 ∷ T_DecSetoid_84 Source #

d_toℕ'45'injective_74 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_toℕ'45'strengthen_90 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_toℕ'45''8593''737'_98 ∷ Integer → T_Fin_10 → Integer → T__'8801'__12 Source #

d_'8593''737''45'injective_112 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_toℕ'45''8593''691'_128 ∷ Integer → Integer → T_Fin_10 → T__'8801'__12 Source #

d_'8593''691''45'injective_142 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_toℕ'60'n_156 ∷ Integer → T_Fin_10 → T__'8804'__22 Source #

du_toℕ'60'n_156 ∷ T_Fin_10 → T__'8804'__22 Source #

d_toℕ'8804'pred'91'n'93'_162 ∷ Integer → T_Fin_10 → T__'8804'__22 Source #

du_toℕ'8804'pred'91'n'93'_162 ∷ T_Fin_10 → T__'8804'__22 Source #

d_toℕ'8804'n_170 ∷ Integer → T_Fin_10 → T__'8804'__22 Source #

du_toℕ'8804'n_170 ∷ T_Fin_10 → T__'8804'__22 Source #

d_toℕ'8804'pred'91'n'93''8242'_178 ∷ Integer → T_Fin_10 → T__'8804'__22 Source #

du_toℕ'8804'pred'91'n'93''8242'_178 ∷ T_Fin_10 → T__'8804'__22 Source #

d_toℕ'45'mono'45''60'_182 ∷ Integer → T_Fin_10 → Integer → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_toℕ'45'mono'45''60'_182 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_toℕ'45'mono'45''8804'_186 ∷ Integer → T_Fin_10 → Integer → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_toℕ'45'mono'45''8804'_186 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_toℕ'45'cancel'45''8804'_190 ∷ Integer → T_Fin_10 → Integer → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_toℕ'45'cancel'45''8804'_190 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_toℕ'45'cancel'45''60'_194 ∷ Integer → T_Fin_10 → Integer → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_toℕ'45'cancel'45''60'_194 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_toℕ'45'fromℕ_200 ∷ Integer → T__'8801'__12 Source #

d_fromℕ'45'toℕ_206 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_'8804'fromℕ_212 ∷ Integer → T_Fin_10 → T__'8804'__22 Source #

du_'8804'fromℕ_212 ∷ T_Fin_10 → T__'8804'__22 Source #

d_fromℕ'60''45'toℕ_226 ∷ Integer → T_Fin_10 → T__'8804'__22 → T__'8801'__12 Source #

d_toℕ'45'fromℕ'60'_234 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_fromℕ'45'def_242 ∷ Integer → T__'8801'__12 Source #

d_fromℕ'60''45'cong_256 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_fromℕ'60''45'injective_274 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 → T__'8801'__12 Source #

d_fromℕ'60''8801'fromℕ'60''8243'_286 ∷ Integer → Integer → T__'8804'__22 → T__'8739''737'__26 → T__'8801'__12 Source #

d_toℕ'45'fromℕ'60''8243'_296 ∷ Integer → Integer → T__'8739''737'__26 → T__'8801'__12 Source #

d_toℕ'45'cast_312 ∷ Integer → Integer → T__'8801'__12 → T_Fin_10 → T__'8801'__12 Source #

d_cast'45'is'45'id_328 ∷ Integer → T__'8801'__12 → T_Fin_10 → T__'8801'__12 Source #

d_subst'45'is'45'cast_340 ∷ Integer → Integer → T__'8801'__12 → T_Fin_10 → T__'8801'__12 Source #

d_cast'45'trans_350 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T_Fin_10 → T__'8801'__12 Source #

d_'8804''45'reflexive_362 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8804'__22 Source #

du_'8804''45'reflexive_362 ∷ T_Fin_10 → T__'8804'__22 Source #

d_'8804''45'refl_364 ∷ Integer → T_Fin_10 → T__'8804'__22 Source #

du_'8804''45'refl_364 ∷ T_Fin_10 → T__'8804'__22 Source #

d_'8804''45'trans_366 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'8804''45'trans_366 ∷ T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8804''45'antisym_368 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_'8804''45'total_374 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8846'__30 Source #

du_'8804''45'total_374 ∷ T_Fin_10 → T_Fin_10 → T__'8846'__30 Source #

d_'8804''45'irrelevant_380 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d__'8804''63'__382 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Dec_20 Source #

du__'8804''63'__382 ∷ T_Fin_10 → T_Fin_10 → T_Dec_20 Source #

d__'60''63'__388 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Dec_20 Source #

du__'60''63'__388 ∷ T_Fin_10 → T_Fin_10 → T_Dec_20 Source #

d_'8804''45'isPreorder_394 ∷ Integer → T_IsPreorder_70 Source #

du_'8804''45'isPreorder_394 ∷ T_IsPreorder_70 Source #

d_'8804''45'isPartialOrder_396 ∷ Integer → T_IsPartialOrder_174 Source #

du_'8804''45'isPartialOrder_396 ∷ T_IsPartialOrder_174 Source #

d_'8804''45'isTotalOrder_398 ∷ Integer → T_IsTotalOrder_404 Source #

du_'8804''45'isTotalOrder_398 ∷ T_IsTotalOrder_404 Source #

d_'8804''45'isDecTotalOrder_400 ∷ Integer → T_IsDecTotalOrder_460 Source #

du_'8804''45'isDecTotalOrder_400 ∷ T_IsDecTotalOrder_460 Source #

d_'8804''45'preorder_402 ∷ Integer → T_Preorder_132 Source #

du_'8804''45'preorder_402 ∷ T_Preorder_132 Source #

d_'8804''45'poset_406 ∷ Integer → T_Poset_314 Source #

du_'8804''45'poset_406 ∷ T_Poset_314 Source #

d_'8804''45'totalOrder_410 ∷ Integer → T_TotalOrder_764 Source #

du_'8804''45'totalOrder_410 ∷ T_TotalOrder_764 Source #

d_'8804''45'decTotalOrder_414 ∷ Integer → T_DecTotalOrder_866 Source #

du_'8804''45'decTotalOrder_414 ∷ T_DecTotalOrder_866 Source #

d_'60''45'irrefl_418 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8804'__22 → T_Irrelevant_20 Source #

d_'60''45'asym_420 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 → T_Irrelevant_20 Source #

d_'60''45'trans_422 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'60''45'trans_422 ∷ T_Fin_10 → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'60''45'cmp_424 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Tri_158 Source #

du_'60''45'cmp_424 ∷ T_Fin_10 → T_Fin_10 → T_Tri_158 Source #

d_'60''45'resp'737''45''8801'_468 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'60''45'resp'737''45''8801'_468 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_'60''45'resp'691''45''8801'_472 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8804'__22 → T__'8804'__22 Source #

du_'60''45'resp'691''45''8801'_472 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_'60''45'resp'8322''45''8801'_476 ∷ Integer → T_Σ_14 Source #

du_'60''45'resp'8322''45''8801'_476 ∷ T_Σ_14 Source #

d_'60''45'irrelevant_478 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_'60''45'isStrictPartialOrder_480 ∷ Integer → T_IsStrictPartialOrder_290 Source #

du_'60''45'isStrictPartialOrder_480 ∷ T_IsStrictPartialOrder_290 Source #

d_'60''45'isStrictTotalOrder_482 ∷ Integer → T_IsStrictTotalOrder_534 Source #

du_'60''45'isStrictTotalOrder_482 ∷ T_IsStrictTotalOrder_534 Source #

d_'60''45'strictPartialOrder_484 ∷ Integer → T_StrictPartialOrder_556 Source #

du_'60''45'strictPartialOrder_484 ∷ T_StrictPartialOrder_556 Source #

d_'60''45'strictTotalOrder_488 ∷ Integer → T_StrictTotalOrder_1036 Source #

du_'60''45'strictTotalOrder_488 ∷ T_StrictTotalOrder_1036 Source #

d_i'60'1'43'i_494 ∷ Integer → T_Fin_10 → T__'8804'__22 Source #

du_i'60'1'43'i_494 ∷ T_Fin_10 → T__'8804'__22 Source #

d_'60''8658''8802'_496 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #

d_'8804''8743''8802''8658''60'_500 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8804'__22 → (T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #

du_'8804''8743''8802''8658''60'_500 ∷ T_Fin_10 → T_Fin_10 → T__'8804'__22 Source #

d_toℕ'45'inject_518 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 Source #

d_fromℕ'8802'inject'8321'_526 ∷ Integer → T_Fin_10 → T__'8801'__12 → T_Irrelevant_20 Source #

d_inject'8321''45'injective_532 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_toℕ'45'inject'8321'_544 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_toℕ'45'inject'8321''45''8802'_550 ∷ Integer → T_Fin_10 → T__'8801'__12 → T_Irrelevant_20 Source #

d_inject'8321'ℕ'60'_556 ∷ Integer → T_Fin_10 → T__'8804'__22 Source #

du_inject'8321'ℕ'60'_556 ∷ T_Fin_10 → T__'8804'__22 Source #

d_inject'8321'ℕ'8804'_566 ∷ Integer → T_Fin_10 → T__'8804'__22 Source #

du_inject'8321'ℕ'8804'_566 ∷ T_Fin_10 → T__'8804'__22 Source #

d_'8804''772''8658'inject'8321''60'_568 ∷ Integer → T_Fin_10 → Integer → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_'8804''772''8658'inject'8321''60'_568 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_ℕ'60''8658'inject'8321''60'_582 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_ℕ'60''8658'inject'8321''60'_582 ∷ T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

d_i'8804'inject'8321''91'j'93''8658'i'8804'1'43'j_588 ∷ Integer → T_Fin_10 → Integer → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_i'8804'inject'8321''91'j'93''8658'i'8804'1'43'j_588 ∷ T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

d_toℕ'45'lower'8321'_602 ∷ Integer → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #

d_lower'8321''45'injective_620 ∷ Integer → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 Source #

d_inject'8321''45'lower'8321'_644 ∷ Integer → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #

d_lower'8321''45'inject'8321''8242'_660 ∷ Integer → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #

d_lower'8321''45'inject'8321'_668 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_lower'8321''45'irrelevant_678 ∷ Integer → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #

d_inject'8321''8801''8658'lower'8321''8801'_694 ∷ Integer → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 Source #

d_toℕ'45'inject'8804'_704 ∷ Integer → Integer → T_Fin_10 → T__'8804'__22 → T__'8801'__12 Source #

d_inject'8804''45'refl_716 ∷ Integer → T_Fin_10 → T__'8804'__22 → T__'8801'__12 Source #

d_inject'8804''45'idempotent_732 ∷ Integer → Integer → Integer → T_Fin_10 → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_inject'8804''45'trans_750 ∷ Integer → Integer → Integer → T_Fin_10 → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #

d_inject'8804''45'injective_762 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_inject'8804''45'irrelevant_778 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T_Fin_10 → T__'8801'__12 Source #

d_pred'60'_784 ∷ Integer → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #

du_pred'60'_784 ∷ T_Fin_10 → T__'8804'__22 Source #

d_splitAt'45''8593''737'_796 ∷ Integer → T_Fin_10 → Integer → T__'8801'__12 Source #

d_splitAt'8315''185''45''8593''737'_820 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_splitAt'45''8593''691'_854 ∷ Integer → Integer → T_Fin_10 → T__'8801'__12 Source #

d_splitAt'8315''185''45''8593''691'_878 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_splitAt'45'join_914 ∷ Integer → Integer → T__'8846'__30 → T__'8801'__12 Source #

d_join'45'splitAt_934 ∷ Integer → Integer → T_Fin_10 → T__'8801'__12 Source #

d_splitAt'45''60'_974 ∷ Integer → Integer → T_Fin_10 → T__'8804'__22 → T__'8801'__12 Source #

d_splitAt'45''8805'_992 ∷ Integer → Integer → T_Fin_10 → T__'8804'__22 → T__'8801'__12 Source #

d_'43''8596''8846'_1002 ∷ Integer → Integer → T_Inverse_1960 Source #

du_'43''8596''8846'_1002 ∷ Integer → T_Inverse_1960 Source #

d_remQuot'45'combine_1016 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 Source #

d_combine'45'remQuot_1046 ∷ Integer → Integer → T_Fin_10 → T__'8801'__12 Source #

d_toℕ'45'combine_1090 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 Source #

d_combine'45'mono'737''45''60'_1132 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_combine'45'mono'737''45''60'_1132 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

d_combine'45'injective'737'_1162 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_combine'45'injective'691'_1222 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_combine'45'injective_1254 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T_Σ_14 Source #

du_combine'45'injective_1254 ∷ T_Σ_14 Source #

d_combine'45'surjective_1272 ∷ Integer → Integer → T_Fin_10 → T_Σ_14 Source #

du_combine'45'surjective_1272 ∷ Integer → T_Fin_10 → T_Σ_14 Source #

d_'42''8596''215'_1294 ∷ Integer → Integer → T_Inverse_1960 Source #

du_'42''8596''215'_1294 ∷ Integer → T_Inverse_1960 Source #

d_funToFin'45'finToFin_1300 ∷ Integer → Integer → T_Fin_10 → T__'8801'__12 Source #

d_finToFun'45'funToFin_1316 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → T_Fin_10 → T__'8801'__12 Source #

d_'94''8596''8594'_1342 ∷ Integer → Integer → (() → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12) → T_Inverse_1960 Source #

du_'94''8596''8594'_1342 ∷ Integer → Integer → T_Inverse_1960 Source #

d_lift'45'injective_1354 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12) → Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_'60''8658''8804'pred_1378 ∷ Integer → T_Fin_10 → Integer → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_'60''8658''8804'pred_1378 ∷ T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

d_toℕ'8255'ℕ'45'_1396 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_ℕ'45'ℕ'8801'toℕ'8255'ℕ'45'_1408 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_nℕ'45'ℕi'8804'n_1420 ∷ Integer → T_Fin_10 → T__'8804'__22 Source #

d_punchIn'45'injective_1438 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_punchIn'7522''8802'i_1454 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T_Irrelevant_20 Source #

d_punchOut'45'cong_1470 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 Source #

d_punchOut'45'cong'8242'_1504 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 Source #

d_punchOut'45'injective_1520 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 Source #

d_punchIn'45'punchOut_1556 ∷ Integer → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #

d_punchOut'45'punchIn_1580 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 Source #

d_pinch'45'surjective_1596 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Σ_14 Source #

du_pinch'45'surjective_1596 ∷ T_Fin_10 → T_Fin_10 → T_Σ_14 Source #

d_'46'extendedlambda8_1598 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_'46'extendedlambda9_1602 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_'46'extendedlambda10_1608 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → (T_Fin_10 → T__'8801'__12 → T__'8801'__12) → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_pinch'45'mono'45''8804'_1614 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_pinch'45'mono'45''8804'_1614 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

d_pinch'45'injective_1646 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 Source #

d_'8704''45'cons_1690 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → AgdaAny → (T_Fin_10 → AgdaAny) → T_Fin_10 → AgdaAny Source #

du_'8704''45'cons_1690 ∷ AgdaAny → (T_Fin_10 → AgdaAny) → T_Fin_10 → AgdaAny Source #

d_'8704''45'cons'45''8660'_1702 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → T_Equivalence_1714 Source #

du_'8704''45'cons'45''8660'_1702 ∷ T_Equivalence_1714 Source #

d_'8707''45'here_1708 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → AgdaAny → T_Σ_14 Source #

du_'8707''45'here_1708 ∷ AgdaAny → T_Σ_14 Source #

d_'8707''45'there_1712 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → T_Σ_14 → T_Σ_14 Source #

du_'8707''45'there_1712 ∷ T_Σ_14 → T_Σ_14 Source #

d_'8707''45'toSum_1714 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → T_Σ_14 → T__'8846'__30 Source #

du_'8707''45'toSum_1714 ∷ T_Σ_14 → T__'8846'__30 Source #

d_'8846''8660''8707'_1722 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → T_Equivalence_1714 Source #

du_'8846''8660''8707'_1722 ∷ T_Equivalence_1714 Source #

d_decFinSubset_1734 ∷ Integer → T_Level_18 → T_Level_18 → (T_Fin_10 → ()) → (T_Fin_10 → ()) → (T_Fin_10 → T_Dec_20) → (T_Fin_10 → AgdaAny → T_Dec_20) → T_Dec_20 Source #

du_decFinSubset_1734 ∷ Integer → (T_Fin_10 → T_Dec_20) → (T_Fin_10 → AgdaAny → T_Dec_20) → T_Dec_20 Source #

d_any'63'_1814 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → (T_Fin_10 → T_Dec_20) → T_Dec_20 Source #

du_any'63'_1814 ∷ Integer → (T_Fin_10 → T_Dec_20) → T_Dec_20 Source #

d_all'63'_1832 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → (T_Fin_10 → T_Dec_20) → T_Dec_20 Source #

du_all'63'_1832 ∷ Integer → (T_Fin_10 → T_Dec_20) → T_Dec_20 Source #

d_'172''8704''10230''8707''172''45'smallest_1874 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → (T_Fin_10 → T_Dec_20) → ((T_Fin_10 → AgdaAny) → T_Irrelevant_20) → T_Σ_14 Source #

du_'172''8704''10230''8707''172''45'smallest_1874 ∷ Integer → (T_Fin_10 → T_Dec_20) → T_Σ_14 Source #

d_'172''8704''10230''8707''172'_1924 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → (T_Fin_10 → T_Dec_20) → ((T_Fin_10 → AgdaAny) → T_Irrelevant_20) → T_Σ_14 Source #

du_'172''8704''10230''8707''172'_1924 ∷ Integer → (T_Fin_10 → T_Dec_20) → T_Σ_14 Source #

d_pigeonhole_1940 ∷ Integer → Integer → T__'8804'__22 → (T_Fin_10 → T_Fin_10) → T_Σ_14 Source #

du_pigeonhole_1940 ∷ Integer → T__'8804'__22 → (T_Fin_10 → T_Fin_10) → T_Σ_14 Source #

d_injective'8658''8804'_1988 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12) → T__'8804'__22 Source #

du_injective'8658''8804'_1988 ∷ Integer → Integer → T__'8804'__22 Source #

d_'60''8658'notInjective_2002 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → T__'8804'__22 → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12) → T_Irrelevant_20 Source #

d_ℕ'8594'Fin'45'notInjective_2010 ∷ Integer → (Integer → T_Fin_10) → (Integer → Integer → T__'8801'__12 → T__'8801'__12) → T_Irrelevant_20 Source #

d_cantor'45'schröder'45'bernstein_2020 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12) → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12) → T__'8801'__12 Source #

d_sequence_2078 ∷ T_Level_18 → (() → ()) → T_RawApplicative_20 → Integer → (T_Fin_10 → ()) → (T_Fin_10 → AgdaAny) → AgdaAny Source #

du_sequence_2078 ∷ T_RawApplicative_20 → Integer → (T_Fin_10 → AgdaAny) → AgdaAny Source #

d_sequence'8315''185'_2114 ∷ T_Level_18 → (() → ()) → T_RawFunctor_24 → () → (AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny Source #

du_sequence'8315''185'_2114 ∷ T_RawFunctor_24 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__2138 ∷ T_Level_18 → Integer → T_Level_18 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny → () Source #

d_inj'8658''8799'_2158 ∷ T_Level_18 → Integer → T_Level_18 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny → T_Dec_20 Source #

du_inj'8658''8799'_2158 ∷ T_Injection_776 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_inj'8658'decSetoid_2160 ∷ T_Level_18 → Integer → T_Level_18 → T_Setoid_44 → T_Injection_776 → T_DecSetoid_84 Source #

du_inj'8658'decSetoid_2160 ∷ T_Setoid_44 → T_Injection_776 → T_DecSetoid_84 Source #

d_opposite'45'prop_2164 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_opposite'45'involutive_2176 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_opposite'45'suc_2190 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_inject'43''45'raise'45'splitAt_2200 ∷ Integer → Integer → T_Fin_10 → T__'8801'__12 Source #

d_toℕ'45'raise_2202 ∷ Integer → Integer → T_Fin_10 → T__'8801'__12 Source #

d_toℕ'45'inject'43'_2210 ∷ Integer → Integer → T_Fin_10 → T__'8801'__12 Source #

d_splitAt'45'inject'43'_2222 ∷ Integer → Integer → T_Fin_10 → T__'8801'__12 Source #

d_splitAt'45'raise_2236 ∷ Integer → Integer → T_Fin_10 → T__'8801'__12 Source #

d_Fin0'8596''8869'_2238 ∷ T_Inverse_1960 Source #

d_eq'63'_2240 ∷ T_Level_18 → () → Integer → T_Injection_776 → AgdaAny → AgdaAny → T_Dec_20 Source #

du_eq'63'_2240 ∷ T_Injection_776 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_z'8826's_2244 ∷ Integer → T__'8826'__518 Source #

du_z'8826's_2244 ∷ T__'8826'__518 Source #

d_s'8826's_2250 ∷ Integer → Integer → T__'8826'__518 → T__'8826'__518 Source #

du_s'8826's_2250 ∷ T__'8826'__518 → T__'8826'__518 Source #

d_'60''8658''8826'_2256 ∷ Integer → Integer → T__'8804'__22 → T__'8826'__518 Source #

du_'60''8658''8826'_2256 ∷ Integer → T__'8804'__22 → T__'8826'__518 Source #

d_'8826''8658''60'_2262 ∷ Integer → Integer → T__'8826'__518 → T__'8804'__22 Source #

du_'8826''8658''60'_2262 ∷ T__'8826'__518 → T__'8804'__22 Source #

d_'8826''8658''60''8242'_2268 ∷ Integer → Integer → T__'8826'__518 → T__'8804''8242'__338 Source #

du_'8826''8658''60''8242'_2268 ∷ Integer → T__'8826'__518 → T__'8804''8242'__338 Source #

d_'60''8242''8658''8826'_2272 ∷ Integer → Integer → T__'8804''8242'__338 → T__'8826'__518 Source #

du_'60''8242''8658''8826'_2272 ∷ Integer → T__'8804''8242'__338 → T__'8826'__518 Source #