Documentation

d_'172'Fin0_20 :: T_Fin_10 -> T_Irrelevant_20 #

d_nonZeroIndex_22 :: Integer -> T_Fin_10 -> T_NonZero_112 #

du_nonZeroIndex_22 :: T_NonZero_112 #

d_0'8596''8869'_24 :: T_Inverse_1960 #

d_1'8596''8868'_26 :: T_Inverse_1960 #

d_'46'extendedlambda3_34 :: T_Fin_10 -> T__'8801'__12 #

d_2'8596'Bool_36 :: T_Inverse_1960 #

d_'46'extendedlambda4_38 :: T_Fin_10 -> Bool #

d_'46'extendedlambda7_44 :: T_Fin_10 -> T__'8801'__12 #

d_0'8802'1'43'n_46 :: Integer -> T_Fin_10 -> T__'8801'__12 -> T_Irrelevant_20 #

d_suc'45'injective_48 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8801'__12 #

d__'8799'__50 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Dec_20 #

du__'8799'__50 :: T_Fin_10 -> T_Fin_10 -> T_Dec_20 #

d_'8801''45'isDecEquivalence_60 :: Integer -> T_IsDecEquivalence_44 #

du_'8801''45'isDecEquivalence_60 :: T_IsDecEquivalence_44 #

d_'8801''45'preorder_62 :: Integer -> T_Preorder_132 #

du_'8801''45'preorder_62 :: T_Preorder_132 #

d_'8801''45'setoid_66 :: Integer -> T_Setoid_44 #

du_'8801''45'setoid_66 :: T_Setoid_44 #

d_'8801''45'decSetoid_70 :: Integer -> T_DecSetoid_84 #

du_'8801''45'decSetoid_70 :: T_DecSetoid_84 #

d_toℕ'45'injective_74 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8801'__12 #

d_toℕ'45'strengthen_90 :: Integer -> T_Fin_10 -> T__'8801'__12 #

d_toℕ'45''8593''737'_98 :: Integer -> T_Fin_10 -> Integer -> T__'8801'__12 #

d_'8593''737''45'injective_112 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8801'__12 #

d_toℕ'45''8593''691'_128 :: Integer -> Integer -> T_Fin_10 -> T__'8801'__12 #

d_'8593''691''45'injective_142 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8801'__12 #

d_toℕ'60'n_156 :: Integer -> T_Fin_10 -> T__'8804'__22 #

du_toℕ'60'n_156 :: T_Fin_10 -> T__'8804'__22 #

d_toℕ'8804'pred'91'n'93'_162 :: Integer -> T_Fin_10 -> T__'8804'__22 #

du_toℕ'8804'pred'91'n'93'_162 :: T_Fin_10 -> T__'8804'__22 #

d_toℕ'8804'n_170 :: Integer -> T_Fin_10 -> T__'8804'__22 #

du_toℕ'8804'n_170 :: T_Fin_10 -> T__'8804'__22 #

d_toℕ'8804'pred'91'n'93''8242'_178 :: Integer -> T_Fin_10 -> T__'8804'__22 #

du_toℕ'8804'pred'91'n'93''8242'_178 :: T_Fin_10 -> T__'8804'__22 #

d_toℕ'45'mono'45''60'_182 :: Integer -> T_Fin_10 -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

du_toℕ'45'mono'45''60'_182 :: T__'8804'__22 -> T__'8804'__22 #

d_toℕ'45'mono'45''8804'_186 :: Integer -> T_Fin_10 -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

du_toℕ'45'mono'45''8804'_186 :: T__'8804'__22 -> T__'8804'__22 #

d_toℕ'45'cancel'45''8804'_190 :: Integer -> T_Fin_10 -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

du_toℕ'45'cancel'45''8804'_190 :: T__'8804'__22 -> T__'8804'__22 #

d_toℕ'45'cancel'45''60'_194 :: Integer -> T_Fin_10 -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

du_toℕ'45'cancel'45''60'_194 :: T__'8804'__22 -> T__'8804'__22 #

d_toℕ'45'fromℕ_200 :: Integer -> T__'8801'__12 #

d_fromℕ'45'toℕ_206 :: Integer -> T_Fin_10 -> T__'8801'__12 #

d_'8804'fromℕ_212 :: Integer -> T_Fin_10 -> T__'8804'__22 #

du_'8804'fromℕ_212 :: T_Fin_10 -> T__'8804'__22 #

d_fromℕ'60''45'toℕ_226 :: Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8801'__12 #

d_toℕ'45'fromℕ'60'_234 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_fromℕ'45'def_242 :: Integer -> T__'8801'__12 #

d_fromℕ'60''45'cong_256 :: Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_fromℕ'60''45'injective_274 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 -> T__'8801'__12 #

d_fromℕ'60''8801'fromℕ'60''8243'_286 :: Integer -> Integer -> T__'8804'__22 -> T__'8739''737'__26 -> T__'8801'__12 #

d_toℕ'45'fromℕ'60''8243'_296 :: Integer -> Integer -> T__'8739''737'__26 -> T__'8801'__12 #

d_toℕ'45'cast_312 :: Integer -> Integer -> T__'8801'__12 -> T_Fin_10 -> T__'8801'__12 #

d_cast'45'is'45'id_328 :: Integer -> T__'8801'__12 -> T_Fin_10 -> T__'8801'__12 #

d_subst'45'is'45'cast_340 :: Integer -> Integer -> T__'8801'__12 -> T_Fin_10 -> T__'8801'__12 #

d_cast'45'trans_350 :: Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T_Fin_10 -> T__'8801'__12 #

d_'8804''45'reflexive_362 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8804'__22 #

du_'8804''45'reflexive_362 :: T_Fin_10 -> T__'8804'__22 #

d_'8804''45'refl_364 :: Integer -> T_Fin_10 -> T__'8804'__22 #

du_'8804''45'refl_364 :: T_Fin_10 -> T__'8804'__22 #

d_'8804''45'trans_366 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'8804''45'trans_366 :: T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8804''45'antisym_368 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_'8804''45'total_374 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8846'__30 #

du_'8804''45'total_374 :: T_Fin_10 -> T_Fin_10 -> T__'8846'__30 #

d_'8804''45'irrelevant_380 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d__'8804''63'__382 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Dec_20 #

du__'8804''63'__382 :: T_Fin_10 -> T_Fin_10 -> T_Dec_20 #

d__'60''63'__388 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Dec_20 #

du__'60''63'__388 :: T_Fin_10 -> T_Fin_10 -> T_Dec_20 #

d_'8804''45'isPreorder_394 :: Integer -> T_IsPreorder_70 #

du_'8804''45'isPreorder_394 :: T_IsPreorder_70 #

d_'8804''45'isPartialOrder_396 :: Integer -> T_IsPartialOrder_174 #

du_'8804''45'isPartialOrder_396 :: T_IsPartialOrder_174 #

d_'8804''45'isTotalOrder_398 :: Integer -> T_IsTotalOrder_404 #

du_'8804''45'isTotalOrder_398 :: T_IsTotalOrder_404 #

d_'8804''45'isDecTotalOrder_400 :: Integer -> T_IsDecTotalOrder_460 #

du_'8804''45'isDecTotalOrder_400 :: T_IsDecTotalOrder_460 #

d_'8804''45'preorder_402 :: Integer -> T_Preorder_132 #

du_'8804''45'preorder_402 :: T_Preorder_132 #

d_'8804''45'poset_406 :: Integer -> T_Poset_314 #

du_'8804''45'poset_406 :: T_Poset_314 #

d_'8804''45'totalOrder_410 :: Integer -> T_TotalOrder_764 #

du_'8804''45'totalOrder_410 :: T_TotalOrder_764 #

d_'8804''45'decTotalOrder_414 :: Integer -> T_DecTotalOrder_866 #

du_'8804''45'decTotalOrder_414 :: T_DecTotalOrder_866 #

d_'60''45'irrefl_418 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8804'__22 -> T_Irrelevant_20 #

d_'60''45'asym_420 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 -> T_Irrelevant_20 #

d_'60''45'trans_422 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'60''45'trans_422 :: T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'60''45'cmp_424 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Tri_158 #

du_'60''45'cmp_424 :: T_Fin_10 -> T_Fin_10 -> T_Tri_158 #

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 #

du_'60''45'resp'737''45''8801'_468 :: T__'8804'__22 -> T__'8804'__22 #

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 #

du_'60''45'resp'691''45''8801'_472 :: T__'8804'__22 -> T__'8804'__22 #

d_'60''45'resp'8322''45''8801'_476 :: Integer -> T_Σ_14 #

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

d_'60''45'irrelevant_478 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_'60''45'isStrictPartialOrder_480 :: Integer -> T_IsStrictPartialOrder_290 #

du_'60''45'isStrictPartialOrder_480 :: T_IsStrictPartialOrder_290 #

d_'60''45'isStrictTotalOrder_482 :: Integer -> T_IsStrictTotalOrder_534 #

du_'60''45'isStrictTotalOrder_482 :: T_IsStrictTotalOrder_534 #

d_'60''45'strictPartialOrder_484 :: Integer -> T_StrictPartialOrder_556 #

du_'60''45'strictPartialOrder_484 :: T_StrictPartialOrder_556 #

d_'60''45'strictTotalOrder_488 :: Integer -> T_StrictTotalOrder_1036 #

du_'60''45'strictTotalOrder_488 :: T_StrictTotalOrder_1036 #

d_i'60'1'43'i_494 :: Integer -> T_Fin_10 -> T__'8804'__22 #

du_i'60'1'43'i_494 :: T_Fin_10 -> T__'8804'__22 #

d_'60''8658''8802'_496 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8801'__12 -> T_Irrelevant_20 #

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 #

du_'8804''8743''8802''8658''60'_500 :: T_Fin_10 -> T_Fin_10 -> T__'8804'__22 #

d_toℕ'45'inject_518 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 #

d_fromℕ'8802'inject'8321'_526 :: Integer -> T_Fin_10 -> T__'8801'__12 -> T_Irrelevant_20 #

d_inject'8321''45'injective_532 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8801'__12 #

d_toℕ'45'inject'8321'_544 :: Integer -> T_Fin_10 -> T__'8801'__12 #

d_toℕ'45'inject'8321''45''8802'_550 :: Integer -> T_Fin_10 -> T__'8801'__12 -> T_Irrelevant_20 #

d_inject'8321'ℕ'60'_556 :: Integer -> T_Fin_10 -> T__'8804'__22 #

du_inject'8321'ℕ'60'_556 :: T_Fin_10 -> T__'8804'__22 #

d_inject'8321'ℕ'8804'_566 :: Integer -> T_Fin_10 -> T__'8804'__22 #

du_inject'8321'ℕ'8804'_566 :: T_Fin_10 -> T__'8804'__22 #

d_'8804''772''8658'inject'8321''60'_568 :: Integer -> T_Fin_10 -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

du_'8804''772''8658'inject'8321''60'_568 :: T__'8804'__22 -> T__'8804'__22 #

d_ℕ'60''8658'inject'8321''60'_582 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

du_ℕ'60''8658'inject'8321''60'_582 :: T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

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 #

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 #

d_toℕ'45'lower'8321'_602 :: Integer -> T_Fin_10 -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8801'__12 #

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 #

d_inject'8321''45'lower'8321'_644 :: Integer -> T_Fin_10 -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8801'__12 #

d_lower'8321''45'inject'8321''8242'_660 :: Integer -> T_Fin_10 -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8801'__12 #

d_lower'8321''45'inject'8321'_668 :: Integer -> T_Fin_10 -> T__'8801'__12 #

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 #

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 #

d_toℕ'45'inject'8804'_704 :: Integer -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8801'__12 #

d_inject'8804''45'refl_716 :: Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8801'__12 #

d_inject'8804''45'idempotent_732 :: Integer -> Integer -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_inject'8804''45'trans_750 :: Integer -> Integer -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

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 #

d_inject'8804''45'irrelevant_778 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T_Fin_10 -> T__'8801'__12 #

d_pred'60'_784 :: Integer -> T_Fin_10 -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8804'__22 #

du_pred'60'_784 :: T_Fin_10 -> T__'8804'__22 #

d_splitAt'45''8593''737'_796 :: Integer -> T_Fin_10 -> Integer -> T__'8801'__12 #

d_splitAt'8315''185''45''8593''737'_820 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8801'__12 #

d_splitAt'45''8593''691'_854 :: Integer -> Integer -> T_Fin_10 -> T__'8801'__12 #

d_splitAt'8315''185''45''8593''691'_878 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8801'__12 #

d_splitAt'45'join_914 :: Integer -> Integer -> T__'8846'__30 -> T__'8801'__12 #

d_join'45'splitAt_934 :: Integer -> Integer -> T_Fin_10 -> T__'8801'__12 #

d_splitAt'45''60'_974 :: Integer -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8801'__12 #

d_splitAt'45''8805'_992 :: Integer -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8801'__12 #

d_'43''8596''8846'_1002 :: Integer -> Integer -> T_Inverse_1960 #

du_'43''8596''8846'_1002 :: Integer -> T_Inverse_1960 #

d_remQuot'45'combine_1016 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 #

d_combine'45'remQuot_1046 :: Integer -> Integer -> T_Fin_10 -> T__'8801'__12 #

d_toℕ'45'combine_1090 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 #

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 #

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 #

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 #

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 #

d_combine'45'injective_1254 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T_Σ_14 #

du_combine'45'injective_1254 :: T_Σ_14 #

d_combine'45'surjective_1272 :: Integer -> Integer -> T_Fin_10 -> T_Σ_14 #

du_combine'45'surjective_1272 :: Integer -> T_Fin_10 -> T_Σ_14 #

d_'42''8596''215'_1294 :: Integer -> Integer -> T_Inverse_1960 #

du_'42''8596''215'_1294 :: Integer -> T_Inverse_1960 #

d_funToFin'45'finToFin_1300 :: Integer -> Integer -> T_Fin_10 -> T__'8801'__12 #

d_finToFun'45'funToFin_1316 :: Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T__'8801'__12 #

d_'94''8596''8594'_1342 :: Integer -> Integer -> (() -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12) -> T_Inverse_1960 #

du_'94''8596''8594'_1342 :: Integer -> Integer -> T_Inverse_1960 #

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 #

d_'60''8658''8804'pred_1378 :: Integer -> T_Fin_10 -> Integer -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

du_'60''8658''8804'pred_1378 :: T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

d_toℕ'8255'ℕ'45'_1396 :: Integer -> T_Fin_10 -> T__'8801'__12 #

d_ℕ'45'ℕ'8801'toℕ'8255'ℕ'45'_1408 :: Integer -> T_Fin_10 -> T__'8801'__12 #

d_nℕ'45'ℕi'8804'n_1420 :: Integer -> T_Fin_10 -> T__'8804'__22 #

d_punchIn'45'injective_1438 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8801'__12 #

d_punchIn'7522''8802'i_1454 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T_Irrelevant_20 #

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 #

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 #

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 #

d_punchIn'45'punchOut_1556 :: Integer -> T_Fin_10 -> T_Fin_10 -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8801'__12 #

d_punchOut'45'punchIn_1580 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 #

d_pinch'45'surjective_1596 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Σ_14 #

du_pinch'45'surjective_1596 :: T_Fin_10 -> T_Fin_10 -> T_Σ_14 #

d_'46'extendedlambda8_1598 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8801'__12 #

d_'46'extendedlambda9_1602 :: Integer -> T_Fin_10 -> T_Fin_10 -> T__'8801'__12 -> T__'8801'__12 #

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 #

d_pinch'45'mono'45''8804'_1614 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

du_pinch'45'mono'45''8804'_1614 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10 -> T__'8804'__22 -> T__'8804'__22 #

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 #

d_'8704''45'cons_1690 :: Integer -> T_Level_18 -> (T_Fin_10 -> ()) -> AgdaAny -> (T_Fin_10 -> AgdaAny) -> T_Fin_10 -> AgdaAny #

du_'8704''45'cons_1690 :: AgdaAny -> (T_Fin_10 -> AgdaAny) -> T_Fin_10 -> AgdaAny #

d_'8704''45'cons'45''8660'_1702 :: Integer -> T_Level_18 -> (T_Fin_10 -> ()) -> T_Equivalence_1714 #

du_'8704''45'cons'45''8660'_1702 :: T_Equivalence_1714 #

d_'8707''45'here_1708 :: Integer -> T_Level_18 -> (T_Fin_10 -> ()) -> AgdaAny -> T_Σ_14 #

du_'8707''45'here_1708 :: AgdaAny -> T_Σ_14 #

d_'8707''45'there_1712 :: Integer -> T_Level_18 -> (T_Fin_10 -> ()) -> T_Σ_14 -> T_Σ_14 #

du_'8707''45'there_1712 :: T_Σ_14 -> T_Σ_14 #

d_'8707''45'toSum_1714 :: Integer -> T_Level_18 -> (T_Fin_10 -> ()) -> T_Σ_14 -> T__'8846'__30 #

du_'8707''45'toSum_1714 :: T_Σ_14 -> T__'8846'__30 #

d_'8846''8660''8707'_1722 :: Integer -> T_Level_18 -> (T_Fin_10 -> ()) -> T_Equivalence_1714 #

du_'8846''8660''8707'_1722 :: T_Equivalence_1714 #

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 #

du_decFinSubset_1734 :: Integer -> (T_Fin_10 -> T_Dec_20) -> (T_Fin_10 -> AgdaAny -> T_Dec_20) -> T_Dec_20 #

d_any'63'_1814 :: Integer -> T_Level_18 -> (T_Fin_10 -> ()) -> (T_Fin_10 -> T_Dec_20) -> T_Dec_20 #

du_any'63'_1814 :: Integer -> (T_Fin_10 -> T_Dec_20) -> T_Dec_20 #

d_all'63'_1832 :: Integer -> T_Level_18 -> (T_Fin_10 -> ()) -> (T_Fin_10 -> T_Dec_20) -> T_Dec_20 #

du_all'63'_1832 :: Integer -> (T_Fin_10 -> T_Dec_20) -> T_Dec_20 #

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 #

du_'172''8704''10230''8707''172''45'smallest_1874 :: Integer -> (T_Fin_10 -> T_Dec_20) -> T_Σ_14 #

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 #

du_'172''8704''10230''8707''172'_1924 :: Integer -> (T_Fin_10 -> T_Dec_20) -> T_Σ_14 #

d_pigeonhole_1940 :: Integer -> Integer -> T__'8804'__22 -> (T_Fin_10 -> T_Fin_10) -> T_Σ_14 #

du_pigeonhole_1940 :: Integer -> T__'8804'__22 -> (T_Fin_10 -> T_Fin_10) -> T_Σ_14 #

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 #

du_injective'8658''8804'_1988 :: Integer -> Integer -> T__'8804'__22 #

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 #

d_ℕ'8594'Fin'45'notInjective_2010 :: Integer -> (Integer -> T_Fin_10) -> (Integer -> Integer -> T__'8801'__12 -> T__'8801'__12) -> T_Irrelevant_20 #

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 #

d_sequence_2078 :: T_Level_18 -> (() -> ()) -> T_RawApplicative_20 -> Integer -> (T_Fin_10 -> ()) -> (T_Fin_10 -> AgdaAny) -> AgdaAny #

du_sequence_2078 :: T_RawApplicative_20 -> Integer -> (T_Fin_10 -> AgdaAny) -> AgdaAny #

d_sequence'8315''185'_2114 :: T_Level_18 -> (() -> ()) -> T_RawFunctor_24 -> () -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny #

du_sequence'8315''185'_2114 :: T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__2138 :: T_Level_18 -> Integer -> T_Level_18 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> () #

d_inj'8658''8799'_2158 :: T_Level_18 -> Integer -> T_Level_18 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du_inj'8658''8799'_2158 :: T_Injection_776 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_inj'8658'decSetoid_2160 :: T_Level_18 -> Integer -> T_Level_18 -> T_Setoid_44 -> T_Injection_776 -> T_DecSetoid_84 #

du_inj'8658'decSetoid_2160 :: T_Setoid_44 -> T_Injection_776 -> T_DecSetoid_84 #

d_opposite'45'prop_2164 :: Integer -> T_Fin_10 -> T__'8801'__12 #

d_opposite'45'involutive_2176 :: Integer -> T_Fin_10 -> T__'8801'__12 #

d_opposite'45'suc_2190 :: Integer -> T_Fin_10 -> T__'8801'__12 #

d_inject'43''45'raise'45'splitAt_2200 :: Integer -> Integer -> T_Fin_10 -> T__'8801'__12 #

d_toℕ'45'raise_2202 :: Integer -> Integer -> T_Fin_10 -> T__'8801'__12 #

d_toℕ'45'inject'43'_2210 :: Integer -> Integer -> T_Fin_10 -> T__'8801'__12 #

d_splitAt'45'inject'43'_2222 :: Integer -> Integer -> T_Fin_10 -> T__'8801'__12 #

d_splitAt'45'raise_2236 :: Integer -> Integer -> T_Fin_10 -> T__'8801'__12 #

d_Fin0'8596''8869'_2238 :: T_Inverse_1960 #

d_eq'63'_2240 :: T_Level_18 -> () -> Integer -> T_Injection_776 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du_eq'63'_2240 :: T_Injection_776 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_z'8826's_2244 :: Integer -> T__'8826'__518 #

du_z'8826's_2244 :: T__'8826'__518 #

d_s'8826's_2250 :: Integer -> Integer -> T__'8826'__518 -> T__'8826'__518 #

du_s'8826's_2250 :: T__'8826'__518 -> T__'8826'__518 #

d_'60''8658''8826'_2256 :: Integer -> Integer -> T__'8804'__22 -> T__'8826'__518 #

du_'60''8658''8826'_2256 :: Integer -> T__'8804'__22 -> T__'8826'__518 #

d_'8826''8658''60'_2262 :: Integer -> Integer -> T__'8826'__518 -> T__'8804'__22 #

du_'8826''8658''60'_2262 :: T__'8826'__518 -> T__'8804'__22 #

d_'8826''8658''60''8242'_2268 :: Integer -> Integer -> T__'8826'__518 -> T__'8804''8242'__338 #

du_'8826''8658''60''8242'_2268 :: Integer -> T__'8826'__518 -> T__'8804''8242'__338 #

d_'60''8242''8658''8826'_2272 :: Integer -> Integer -> T__'8804''8242'__338 -> T__'8826'__518 #

du_'60''8242''8658''8826'_2272 :: Integer -> T__'8804''8242'__338 -> T__'8826'__518 #