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

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

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

d_2'8596'Bool_36 ∷ T_Inverse_2122 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_48 Source #

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

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

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

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

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

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

du_'8801''45'decSetoid_70 ∷ T_DecSetoid_90 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 ∷ 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 ∷ 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 ∷ 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 ∷ 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'__28 → T__'8801'__12 Source #

d_toℕ'45'fromℕ'60''8243'_296 ∷ Integer → Integer → T__'8739''737'__28 → 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_cast'45'involutive_368 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 → T_Fin_10 → T__'8801'__12 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'8804''45'isPreorder_408 ∷ Integer → T_IsPreorder_76 Source #

du_'8804''45'isPreorder_408 ∷ T_IsPreorder_76 Source #

d_'8804''45'isPartialOrder_410 ∷ Integer → T_IsPartialOrder_248 Source #

du_'8804''45'isPartialOrder_410 ∷ T_IsPartialOrder_248 Source #

d_'8804''45'isTotalOrder_412 ∷ Integer → T_IsTotalOrder_488 Source #

du_'8804''45'isTotalOrder_412 ∷ T_IsTotalOrder_488 Source #

d_'8804''45'isDecTotalOrder_414 ∷ Integer → T_IsDecTotalOrder_546 Source #

du_'8804''45'isDecTotalOrder_414 ∷ T_IsDecTotalOrder_546 Source #

d_'8804''45'preorder_416 ∷ Integer → T_Preorder_142 Source #

du_'8804''45'preorder_416 ∷ T_Preorder_142 Source #

d_'8804''45'poset_420 ∷ Integer → T_Poset_492 Source #

du_'8804''45'poset_420 ∷ T_Poset_492 Source #

d_'8804''45'totalOrder_424 ∷ Integer → T_TotalOrder_986 Source #

du_'8804''45'totalOrder_424 ∷ T_TotalOrder_986 Source #

d_'8804''45'decTotalOrder_428 ∷ Integer → T_DecTotalOrder_1098 Source #

du_'8804''45'decTotalOrder_428 ∷ T_DecTotalOrder_1098 Source #

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

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

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

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

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

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

d_'60''45'resp'737''45''8801'_482 ∷ 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'_482 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_'60''45'resp'691''45''8801'_486 ∷ 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'_486 ∷ T__'8804'__22 → T__'8804'__22 Source #

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

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

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

d_'60''45'isStrictPartialOrder_494 ∷ Integer → T_IsStrictPartialOrder_370 Source #

du_'60''45'isStrictPartialOrder_494 ∷ T_IsStrictPartialOrder_370 Source #

d_'60''45'isStrictTotalOrder_496 ∷ Integer → T_IsStrictTotalOrder_624 Source #

du_'60''45'isStrictTotalOrder_496 ∷ T_IsStrictTotalOrder_624 Source #

d_'60''45'strictPartialOrder_498 ∷ Integer → T_StrictPartialOrder_760 Source #

du_'60''45'strictPartialOrder_498 ∷ T_StrictPartialOrder_760 Source #

d_'60''45'strictTotalOrder_502 ∷ Integer → T_StrictTotalOrder_1280 Source #

du_'60''45'strictTotalOrder_502 ∷ T_StrictTotalOrder_1280 Source #

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

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

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

d_'8804''8743''8802''8658''60'_514 ∷ 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'_514 ∷ T_Fin_10 → T_Fin_10 → T__'8804'__22 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

d_i'8804'inject'8321''91'j'93''8658'i'8804'1'43'j_602 ∷ 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_602 ∷ T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

d_inject'33''45'injective_614 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

d_inject'33''45''60'_634 ∷ Integer → T_Fin_10 → T_Fin_10 → T__'8804'__22 Source #

du_inject'33''45''60'_634 ∷ T_Fin_10 → T_Fin_10 → T__'8804'__22 Source #

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

d_lower'8321''45'injective_668 ∷ 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'_692 ∷ Integer → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #

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

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

d_lower'8321''45'irrelevant_726 ∷ 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'_742 ∷ Integer → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 Source #

d_lower'45'injective_756 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 → T__'8801'__12 Source #

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

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

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

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

d_inject'8804''45'injective_832 ∷ 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_848 ∷ T__'8804'__22 → T__'8804'__22 → T_Fin_10 → T__'8801'__12 Source #

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

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

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

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

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

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

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

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

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

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

d_'43''8596''8846'_1072 ∷ Integer → Integer → T_Inverse_2122 Source #

du_'43''8596''8846'_1072 ∷ Integer → T_Inverse_2122 Source #

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

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

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

d_combine'45'mono'737''45''60'_1202 ∷ 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'_1202 ∷ 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'_1232 ∷ 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'_1292 ∷ 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_1324 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T_Σ_14 Source #

du_combine'45'injective_1324 ∷ T_Σ_14 Source #

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

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

d_'42''8596''215'_1364 ∷ Integer → Integer → T_Inverse_2122 Source #

du_'42''8596''215'_1364 ∷ Integer → T_Inverse_2122 Source #

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

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

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

du_'94''8596''8594'_1412 ∷ Integer → Integer → T_Inverse_2122 Source #

d_lift'45'injective_1424 ∷ 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_1448 ∷ Integer → T_Fin_10 → Integer → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

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

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

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

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

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

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

d_punchIn'45'mono'45''8804'_1536 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_punchIn'45'mono'45''8804'_1536 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

d_punchIn'45'cancel'45''8804'_1554 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

du_punchIn'45'cancel'45''8804'_1554 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

d_punchOut'45'cong_1576 ∷ 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'_1610 ∷ 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_1626 ∷ 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'mono'45''8804'_1666 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → (T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 → T__'8804'__22 Source #

du_punchOut'45'mono'45''8804'_1666 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

d_punchOut'45'cancel'45''8804'_1688 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → (T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 → T__'8804'__22 Source #

du_punchOut'45'cancel'45''8804'_1688 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

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

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

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

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

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

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

d_'46'extendedlambda10_1760 ∷ 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'_1766 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 → T__'8804'__22 → T__'8804'__22 Source #

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

d_pinch'45'injective_1798 ∷ 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_1842 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → AgdaAny → (T_Fin_10 → AgdaAny) → T_Fin_10 → AgdaAny Source #

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

d_'8704''45'cons'45''8660'_1854 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → T_Equivalence_1858 Source #

du_'8704''45'cons'45''8660'_1854 ∷ T_Equivalence_1858 Source #

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

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

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

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

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

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

d_'8846''8660''8707'_1874 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → T_Equivalence_1858 Source #

du_'8846''8660''8707'_1874 ∷ T_Equivalence_1858 Source #

d_decFinSubset_1886 ∷ 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_1886 ∷ Integer → (T_Fin_10 → T_Dec_20) → (T_Fin_10 → AgdaAny → T_Dec_20) → T_Dec_20 Source #

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

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

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

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

d_'172''8704''10230''8707''172''45'smallest_2026 ∷ 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_2026 ∷ Integer → (T_Fin_10 → T_Dec_20) → T_Σ_14 Source #

d_'172''8704''10230''8707''172'_2076 ∷ 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'_2076 ∷ Integer → (T_Fin_10 → T_Dec_20) → T_Σ_14 Source #

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

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

d_injective'8658''8804'_2140 ∷ 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'_2140 ∷ Integer → Integer → T__'8804'__22 Source #

d_'60''8658'notInjective_2154 ∷ 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_2162 ∷ Integer → (Integer → T_Fin_10) → (Integer → Integer → T__'8801'__12 → T__'8801'__12) → T_Irrelevant_20 Source #

d_cantor'45'schröder'45'bernstein_2172 ∷ 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_injective'8658'existsPivot_2184 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12) → T_Fin_10 → T_Σ_14 Source #

du_injective'8658'existsPivot_2184 ∷ Integer → (T_Fin_10 → T_Fin_10) → T_Fin_10 → T_Σ_14 Source #

d_fj'60'i_2220 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → T_Fin_10 → (T_Σ_14 → T_Irrelevant_20) → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12) → T_Fin_10 → T__'8804'__22 Source #

du_fj'60'i_2220 ∷ (T_Fin_10 → T_Fin_10) → T_Fin_10 → T_Fin_10 → T__'8804'__22 Source #

d_f'8728'inject'33'_2236 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → T_Fin_10 → (T_Σ_14 → T_Irrelevant_20) → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12) → T_Fin_10 → T_Fin_10 Source #

du_f'8728'inject'33'_2236 ∷ (T_Fin_10 → T_Fin_10) → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d_f'8728'inject'33''45'injective_2240 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → T_Fin_10 → (T_Σ_14 → T_Irrelevant_20) → (T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12) → T_Fin_10 → T_Fin_10 → T__'8801'__12 → T__'8801'__12 Source #

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

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

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

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

d__'8776'__2354 ∷ T_Level_18 → Integer → T_Level_18 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → () Source #

d_inj'8658''8799'_2376 ∷ T_Level_18 → Integer → T_Level_18 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → T_Dec_20 Source #

du_inj'8658''8799'_2376 ∷ T_Injection_842 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_inj'8658'decSetoid_2378 ∷ T_Level_18 → Integer → T_Level_18 → T_Setoid_46 → T_Injection_842 → T_DecSetoid_90 Source #

du_inj'8658'decSetoid_2378 ∷ T_Setoid_46 → T_Injection_842 → T_DecSetoid_90 Source #

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

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

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

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

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

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

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

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

d_Fin0'8596''8869'_2456 ∷ T_Inverse_2122 Source #

d_eq'63'_2458 ∷ T_Level_18 → () → Integer → T_Injection_842 → AgdaAny → AgdaAny → T_Dec_20 Source #

du_eq'63'_2458 ∷ T_Injection_842 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_z'8826's_2462 ∷ Integer → T__'8826'__548 Source #

du_z'8826's_2462 ∷ T__'8826'__548 Source #

d_s'8826's_2468 ∷ Integer → Integer → T__'8826'__548 → T__'8826'__548 Source #

du_s'8826's_2468 ∷ T__'8826'__548 → T__'8826'__548 Source #

d_'60''8658''8826'_2474 ∷ Integer → Integer → T__'8804'__22 → T__'8826'__548 Source #

du_'60''8658''8826'_2474 ∷ Integer → T__'8804'__22 → T__'8826'__548 Source #

d_'8826''8658''60'_2480 ∷ Integer → Integer → T__'8826'__548 → T__'8804'__22 Source #

du_'8826''8658''60'_2480 ∷ T__'8826'__548 → T__'8804'__22 Source #

d_'8826''8658''60''8242'_2486 ∷ Integer → Integer → T__'8826'__548 → T__'8804''8242'__342 Source #

du_'8826''8658''60''8242'_2486 ∷ Integer → T__'8826'__548 → T__'8804''8242'__342 Source #

d_'60''8242''8658''8826'_2490 ∷ Integer → Integer → T__'8804''8242'__342 → T__'8826'__548 Source #

du_'60''8242''8658''8826'_2490 ∷ Integer → T__'8804''8242'__342 → T__'8826'__548 Source #