Documentation

d_'172'Fin0_6 :: T_Fin_6 -> T_'8869'_4 Source #

d_0'8596''8869'_8 :: T_Inverse_1052 Source #

d_1'8596''8868'_10 :: T_Inverse_1052 Source #

d_suc'45'injective_26 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d__'8799'__30 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Dec_32 Source #

du__'8799'__30 :: T_Fin_6 -> T_Fin_6 -> T_Dec_32 Source #

d_'8801''45'isDecEquivalence_42 :: Integer -> T_IsDecEquivalence_44 Source #

du_'8801''45'isDecEquivalence_42 :: T_IsDecEquivalence_44 Source #

d_'8801''45'preorder_44 :: Integer -> T_Preorder_132 Source #

du_'8801''45'preorder_44 :: T_Preorder_132 Source #

d_'8801''45'setoid_48 :: Integer -> T_Setoid_44 Source #

du_'8801''45'setoid_48 :: T_Setoid_44 Source #

d_'8801''45'decSetoid_52 :: Integer -> T_DecSetoid_84 Source #

du_'8801''45'decSetoid_52 :: T_DecSetoid_84 Source #

d_toℕ'45'injective_62 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_toℕ'45'strengthen_80 :: Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_toℕ'45''8593''737'_90 :: Integer -> T_Fin_6 -> Integer -> T__'8801'__12 Source #

d_'8593''737''45'injective_106 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_toℕ'45''8593''691'_124 :: Integer -> Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_'8593''691''45'injective_140 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_toℕ'60'n_156 :: Integer -> T_Fin_6 -> T__'8804'__18 Source #

du_toℕ'60'n_156 :: T_Fin_6 -> T__'8804'__18 Source #

d_toℕ'8804'n_164 :: Integer -> T_Fin_6 -> T__'8804'__18 Source #

du_toℕ'8804'n_164 :: T_Fin_6 -> T__'8804'__18 Source #

d_toℕ'8804'pred'91'n'93'_170 :: Integer -> T_Fin_6 -> T__'8804'__18 Source #

du_toℕ'8804'pred'91'n'93'_170 :: T_Fin_6 -> T__'8804'__18 Source #

d_toℕ'8804'pred'91'n'93''8242'_180 :: Integer -> T_Fin_6 -> T__'8804'__18 Source #

du_toℕ'8804'pred'91'n'93''8242'_180 :: T_Fin_6 -> T__'8804'__18 Source #

d_toℕ'45'mono'45''60'_190 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

du_toℕ'45'mono'45''60'_190 :: T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

d_toℕ'45'mono'45''8804'_206 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

du_toℕ'45'mono'45''8804'_206 :: T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

d_toℕ'45'cancel'45''8804'_222 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

du_toℕ'45'cancel'45''8804'_222 :: T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

d_toℕ'45'cancel'45''60'_238 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

du_toℕ'45'cancel'45''60'_238 :: T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

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

d_fromℕ'45'toℕ_258 :: Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_'8804'fromℕ_266 :: Integer -> T_Fin_6 -> T__'8804'__18 Source #

du_'8804'fromℕ_266 :: T_Fin_6 -> T__'8804'__18 Source #

d_fromℕ'60''45'toℕ_280 :: Integer -> T_Fin_6 -> T__'8804'__18 -> T__'8801'__12 Source #

d_toℕ'45'fromℕ'60'_292 :: Integer -> Integer -> T__'8804'__18 -> T__'8801'__12 Source #

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

d_fromℕ'60''45'cong_312 :: Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 -> T__'8801'__12 Source #

d_fromℕ'60''45'injective_332 :: Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18 -> T__'8801'__12 -> T__'8801'__12 Source #

d_fromℕ'60''8801'fromℕ'60''8243'_350 :: Integer -> Integer -> T__'8804'__18 -> T__'8804''8243'__210 -> T__'8801'__12 Source #

d_toℕ'45'fromℕ'60''8243'_360 :: Integer -> Integer -> T__'8804''8243'__210 -> T__'8801'__12 Source #

d_toℕ'45'cast_380 :: Integer -> Integer -> T__'8801'__12 -> T_Fin_6 -> T__'8801'__12 Source #

d_'8804''45'reflexive_394 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8804'__18 Source #

du_'8804''45'reflexive_394 :: T_Fin_6 -> T__'8804'__18 Source #

d_'8804''45'refl_398 :: Integer -> T_Fin_6 -> T__'8804'__18 Source #

du_'8804''45'refl_398 :: T_Fin_6 -> T__'8804'__18 Source #

d_'8804''45'trans_402 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18 Source #

du_'8804''45'trans_402 :: T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18 Source #

d_'8804''45'antisym_406 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 -> T__'8801'__12 Source #

d_'8804''45'total_414 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8846'__30 Source #

du_'8804''45'total_414 :: T_Fin_6 -> T_Fin_6 -> T__'8846'__30 Source #

d_'8804''45'irrelevant_424 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 -> T__'8801'__12 Source #

d__'8804''63'__430 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Dec_32 Source #

du__'8804''63'__430 :: T_Fin_6 -> T_Fin_6 -> T_Dec_32 Source #

d__'60''63'__440 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Dec_32 Source #

du__'60''63'__440 :: T_Fin_6 -> T_Fin_6 -> T_Dec_32 Source #

d_'8804''45'isPreorder_448 :: Integer -> T_IsPreorder_70 Source #

du_'8804''45'isPreorder_448 :: T_IsPreorder_70 Source #

d_'8804''45'isPartialOrder_452 :: Integer -> T_IsPartialOrder_162 Source #

du_'8804''45'isPartialOrder_452 :: T_IsPartialOrder_162 Source #

d_'8804''45'isTotalOrder_456 :: Integer -> T_IsTotalOrder_380 Source #

du_'8804''45'isTotalOrder_456 :: T_IsTotalOrder_380 Source #

d_'8804''45'isDecTotalOrder_460 :: Integer -> T_IsDecTotalOrder_430 Source #

du_'8804''45'isDecTotalOrder_460 :: T_IsDecTotalOrder_430 Source #

d_'8804''45'preorder_462 :: Integer -> T_Preorder_132 Source #

du_'8804''45'preorder_462 :: T_Preorder_132 Source #

d_'8804''45'poset_466 :: Integer -> T_Poset_282 Source #

du_'8804''45'poset_466 :: T_Poset_282 Source #

d_'8804''45'totalOrder_470 :: Integer -> T_TotalOrder_648 Source #

du_'8804''45'totalOrder_470 :: T_TotalOrder_648 Source #

d_'8804''45'decTotalOrder_474 :: Integer -> T_DecTotalOrder_736 Source #

du_'8804''45'decTotalOrder_474 :: T_DecTotalOrder_736 Source #

d_'60''45'irrefl_480 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8804'__18 -> T_'8869'_4 Source #

d_'60''45'asym_484 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 -> T_'8869'_4 Source #

d_'60''45'trans_488 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18 Source #

du_'60''45'trans_488 :: T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18 Source #

d_'60''45'cmp_492 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Tri_136 Source #

du_'60''45'cmp_492 :: T_Fin_6 -> T_Fin_6 -> T_Tri_136 Source #

d_'60''45'resp'737''45''8801'_540 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 Source #

du_'60''45'resp'737''45''8801'_540 :: T__'8804'__18 -> T__'8804'__18 Source #

d_'60''45'resp'691''45''8801'_548 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8804'__18 -> T__'8804'__18 Source #

du_'60''45'resp'691''45''8801'_548 :: T__'8804'__18 -> T__'8804'__18 Source #

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

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

d_'60''45'irrelevant_560 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 -> T__'8801'__12 Source #

d_'60''45'isStrictPartialOrder_564 :: Integer -> T_IsStrictPartialOrder_266 Source #

du_'60''45'isStrictPartialOrder_564 :: T_IsStrictPartialOrder_266 Source #

d_'60''45'isStrictTotalOrder_568 :: Integer -> T_IsStrictTotalOrder_498 Source #

du_'60''45'isStrictTotalOrder_568 :: T_IsStrictTotalOrder_498 Source #

d_'60''45'strictPartialOrder_570 :: Integer -> T_StrictPartialOrder_472 Source #

du_'60''45'strictPartialOrder_570 :: T_StrictPartialOrder_472 Source #

d_'60''45'strictTotalOrder_574 :: Integer -> T_StrictTotalOrder_860 Source #

du_'60''45'strictTotalOrder_574 :: T_StrictTotalOrder_860 Source #

d_'60''8658''8802'_584 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8801'__12 -> T_'8869'_4 Source #

d_'8804''8743''8802''8658''60'_594 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> (T__'8801'__12 -> T_'8869'_4) -> T__'8804'__18 Source #

du_'8804''8743''8802''8658''60'_594 :: T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

d_toℕ'45'inject_614 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 Source #

d_inject'8321''45'injective_628 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_toℕ'45'inject'8321'_642 :: Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_toℕ'45'inject'8321''45''8802'_650 :: Integer -> T_Fin_6 -> T__'8801'__12 -> T_'8869'_4 Source #

d_inject'8321'ℕ'60'_658 :: Integer -> T_Fin_6 -> T__'8804'__18 Source #

du_inject'8321'ℕ'60'_658 :: T_Fin_6 -> T__'8804'__18 Source #

d_inject'8321'ℕ'8804'_670 :: Integer -> T_Fin_6 -> T__'8804'__18 Source #

du_inject'8321'ℕ'8804'_670 :: T_Fin_6 -> T__'8804'__18 Source #

d_'8804''772''8658'inject'8321''60'_678 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

du_'8804''772''8658'inject'8321''60'_678 :: T__'8804'__18 -> T__'8804'__18 Source #

d_ℕ'60''8658'inject'8321''60'_694 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

du_ℕ'60''8658'inject'8321''60'_694 :: T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

d_toℕ'45'lower'8321'_706 :: Integer -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T__'8801'__12 Source #

d_inject'8321''45'lower'8321'_726 :: Integer -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T__'8801'__12 Source #

d_lower'8321''45'inject'8321''8242'_744 :: Integer -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T__'8801'__12 Source #

d_lower'8321''45'inject'8321'_754 :: Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_lower'8321''45'irrelevant_766 :: Integer -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> (T__'8801'__12 -> T_'8869'_4) -> T__'8801'__12 Source #

d_inject'8321''8801''8658'lower'8321''8801'_784 :: Integer -> T_Fin_6 -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T__'8801'__12 -> T__'8801'__12 Source #

d_toℕ'45'inject'8804'_798 :: Integer -> Integer -> T_Fin_6 -> T__'8804'__18 -> T__'8801'__12 Source #

d_inject'8804''45'refl_814 :: Integer -> T_Fin_6 -> T__'8804'__18 -> T__'8801'__12 Source #

d_inject'8804''45'idempotent_838 :: Integer -> Integer -> Integer -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18 -> T__'8801'__12 Source #

d_inject'8804''45'injective_866 :: Integer -> Integer -> T__'8804'__18 -> T__'8804'__18 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_pred'60'_888 :: Integer -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T__'8804'__18 Source #

du_pred'60'_888 :: T_Fin_6 -> T__'8804'__18 Source #

d_splitAt'45''8593''737'_902 :: Integer -> T_Fin_6 -> Integer -> T__'8801'__12 Source #

d_splitAt'45''8593''691'_924 :: Integer -> Integer -> T_Fin_6 -> T__'8801'__12 Source #

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

d_join'45'splitAt_966 :: Integer -> Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_splitAt'45''60'_1006 :: Integer -> Integer -> T_Fin_6 -> T__'8804'__18 -> T__'8801'__12 Source #

d_splitAt'45''8805'_1024 :: Integer -> Integer -> T_Fin_6 -> T__'8804'__18 -> T__'8801'__12 Source #

d_'43''8596''8846'_1038 :: Integer -> Integer -> T_Inverse_1052 Source #

du_'43''8596''8846'_1038 :: Integer -> T_Inverse_1052 Source #

d_remQuot'45'combine_1052 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 Source #

d_combine'45'remQuot_1082 :: Integer -> Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_toℕ'45'combine_1132 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 Source #

d_combine'45'injective'737'_1178 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_combine'45'injective'691'_1206 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_combine'45'injective_1236 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T_Σ_14 Source #

du_combine'45'injective_1236 :: T_Σ_14 Source #

d_lemma'8321'_1264 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

du_lemma'8321'_1264 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

d_lemma'8322'_1298 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_lemma'8323'_1362 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_combine'45'surjective_1390 :: Integer -> Integer -> T_Fin_6 -> T_Σ_14 Source #

du_combine'45'surjective_1390 :: Integer -> T_Fin_6 -> T_Σ_14 Source #

d_'42''8596''215'_1422 :: Integer -> Integer -> T_Inverse_1052 Source #

du_'42''8596''215'_1422 :: Integer -> T_Inverse_1052 Source #

d_funToFin'45'finToFin_1432 :: Integer -> Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_finToFun'45'funToFin_1452 :: Integer -> Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T__'8801'__12 Source #

d_'94''8596''8594'_1482 :: Integer -> Integer -> (() -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12) -> T_Inverse_1052 Source #

du_'94''8596''8594'_1482 :: Integer -> Integer -> T_Inverse_1052 Source #

d_lift'45'injective_1506 :: Integer -> Integer -> (T_Fin_6 -> T_Fin_6) -> (T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12) -> Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_'8826''8658''60''8242'_1534 :: Integer -> Integer -> T__'8826'__558 -> T__'8804''8242'__176 Source #

du_'8826''8658''60''8242'_1534 :: Integer -> T__'8826'__558 -> T__'8804''8242'__176 Source #

d_'60''8242''8658''8826'_1540 :: Integer -> Integer -> T__'8804''8242'__176 -> T__'8826'__558 Source #

du_'60''8242''8658''8826'_1540 :: Integer -> T__'8804''8242'__176 -> T__'8826'__558 Source #

d_'60''8658''8804'pred_1566 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

du_'60''8658''8804'pred_1566 :: T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

d_toℕ'8255'ℕ'45'_1584 :: Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_nℕ'45'ℕi'8804'n_1596 :: Integer -> T_Fin_6 -> T__'8804'__18 Source #

d_punchIn'45'injective_1616 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T__'8801'__12 Source #

d_punchIn'7522''8802'i_1634 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> T_'8869'_4 Source #

d_punchOut'45'cong_1652 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> (T__'8801'__12 -> T_'8869'_4) -> T__'8801'__12 -> T__'8801'__12 Source #

d_punchOut'45'cong'8242'_1688 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T__'8801'__12 -> T__'8801'__12 Source #

d_punchOut'45'injective_1706 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> (T__'8801'__12 -> T_'8869'_4) -> T__'8801'__12 -> T__'8801'__12 Source #

d_punchIn'45'punchOut_1744 :: Integer -> T_Fin_6 -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T__'8801'__12 Source #

d_punchOut'45'punchIn_1770 :: Integer -> T_Fin_6 -> T_Fin_6 -> T__'8801'__12 Source #

d_pinch'45'surjective_1788 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Σ_14 Source #

du_pinch'45'surjective_1788 :: T_Fin_6 -> T_Fin_6 -> T_Σ_14 Source #

d_pinch'45'mono'45''8804'_1800 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

du_pinch'45'mono'45''8804'_1800 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 Source #

d_'8704''45'cons_1836 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> AgdaAny -> (T_Fin_6 -> AgdaAny) -> T_Fin_6 -> AgdaAny Source #

du_'8704''45'cons_1836 :: AgdaAny -> (T_Fin_6 -> AgdaAny) -> T_Fin_6 -> AgdaAny Source #

d_'8704''45'cons'45''8660'_1848 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> T_Equivalence_928 Source #

du_'8704''45'cons'45''8660'_1848 :: T_Equivalence_928 Source #

d_'8707''45'here_1854 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> AgdaAny -> T_Σ_14 Source #

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

d_'8707''45'there_1858 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> T_Σ_14 -> T_Σ_14 Source #

du_'8707''45'there_1858 :: T_Σ_14 -> T_Σ_14 Source #

d_'8707''45'toSum_1860 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> T_Σ_14 -> T__'8846'__30 Source #

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

d_'8846''8660''8707'_1868 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> T_Equivalence_928 Source #

du_'8846''8660''8707'_1868 :: T_Equivalence_928 Source #

d_decFinSubset_1882 :: Integer -> T_Level_14 -> T_Level_14 -> (T_Fin_6 -> ()) -> (T_Fin_6 -> ()) -> (T_Fin_6 -> T_Dec_32) -> (T_Fin_6 -> AgdaAny -> T_Dec_32) -> T_Dec_32 Source #

du_decFinSubset_1882 :: Integer -> (T_Fin_6 -> T_Dec_32) -> (T_Fin_6 -> AgdaAny -> T_Dec_32) -> T_Dec_32 Source #

d_any'63'_1964 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> (T_Fin_6 -> T_Dec_32) -> T_Dec_32 Source #

du_any'63'_1964 :: Integer -> (T_Fin_6 -> T_Dec_32) -> T_Dec_32 Source #

d_all'63'_1984 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> (T_Fin_6 -> T_Dec_32) -> T_Dec_32 Source #

du_all'63'_1984 :: Integer -> (T_Fin_6 -> T_Dec_32) -> T_Dec_32 Source #

d_'172''8704''10230''8707''172''45'smallest_2026 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> (T_Fin_6 -> T_Dec_32) -> ((T_Fin_6 -> AgdaAny) -> T_'8869'_4) -> T_Σ_14 Source #

du_'172''8704''10230''8707''172''45'smallest_2026 :: Integer -> (T_Fin_6 -> T_Dec_32) -> T_Σ_14 Source #

d_'172''8704''10230''8707''172'_2076 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> (T_Fin_6 -> T_Dec_32) -> ((T_Fin_6 -> AgdaAny) -> T_'8869'_4) -> T_Σ_14 Source #

du_'172''8704''10230''8707''172'_2076 :: Integer -> (T_Fin_6 -> T_Dec_32) -> T_Σ_14 Source #

d_pigeonhole_2096 :: Integer -> Integer -> T__'8804'__18 -> (T_Fin_6 -> T_Fin_6) -> T_Σ_14 Source #

du_pigeonhole_2096 :: Integer -> T__'8804'__18 -> (T_Fin_6 -> T_Fin_6) -> T_Σ_14 Source #

d_sequence_2190 :: T_Level_14 -> (() -> ()) -> T_RawIApplicative_38 -> Integer -> (T_Fin_6 -> ()) -> (T_Fin_6 -> AgdaAny) -> AgdaAny Source #

du_sequence_2190 :: T_RawIApplicative_38 -> Integer -> (T_Fin_6 -> AgdaAny) -> AgdaAny Source #

d_sequence'8315''185'_2224 :: T_Level_14 -> (() -> ()) -> T_RawFunctor_24 -> () -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sequence'8315''185'_2224 :: T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_eq'63'_2242 :: T_Level_14 -> () -> Integer -> T_Injection_704 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

du_eq'63'_2242 :: T_Injection_704 -> AgdaAny -> AgdaAny -> T_Dec_32 Source #

d_opposite'45'prop_2250 :: Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_opposite'45'involutive_2264 :: Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_opposite'45'suc_2280 :: Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_'8804''45'irrelevance_2290 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 -> T__'8801'__12 Source #

d_'60''45'irrelevance_2292 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T__'8804'__18 -> T__'8804'__18 -> T__'8801'__12 Source #

d__'43''8242'__2302 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

du__'43''8242'__2302 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

d_fromℕ'8804''45'toℕ_2308 :: Integer -> T_Fin_6 -> T__'8804'__18 -> T__'8801'__12 Source #

d_toℕ'45'fromℕ'8804'_2310 :: Integer -> Integer -> T__'8804'__18 -> T__'8801'__12 Source #

d_fromℕ'8804''8801'fromℕ'8804''8243'_2312 :: Integer -> Integer -> T__'8804'__18 -> T__'8804''8243'__210 -> T__'8801'__12 Source #

d_toℕ'45'fromℕ'8804''8243'_2314 :: Integer -> Integer -> T__'8804''8243'__210 -> T__'8801'__12 Source #

d_isDecEquivalence_2316 :: Integer -> T_IsDecEquivalence_44 Source #

d_preorder_2318 :: Integer -> T_Preorder_132 Source #

d_setoid_2320 :: Integer -> T_Setoid_44 Source #

d_decSetoid_2322 :: Integer -> T_DecSetoid_84 Source #

d_inject'43''45'raise'45'splitAt_2324 :: Integer -> Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_toℕ'45'raise_2326 :: Integer -> Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_toℕ'45'inject'43'_2334 :: Integer -> Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_splitAt'45'inject'43'_2346 :: Integer -> Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_splitAt'45'raise_2360 :: Integer -> Integer -> T_Fin_6 -> T__'8801'__12 Source #

d_Fin0'8596''8869'_2362 :: T_Inverse_1052 Source #