Documentation

d_Args_30 ∷ T_Level_18 → () → () Source #

d_map_46 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Arg_88 → T_Arg_88 Source #

du_map_46 ∷ (AgdaAny → AgdaAny) → T_Arg_88 → T_Arg_88 Source #

d_map'45'Args_54 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [T_Arg_88] → [T_Arg_88] Source #

du_map'45'Args_54 ∷ (AgdaAny → AgdaAny) → [T_Arg_88] → [T_Arg_88] Source #

d_arg'45'injective'8321'_68 ∷ T_Level_18 → () → T_ArgInfo_76 → T_ArgInfo_76 → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_arg'45'injective'8322'_78 ∷ T_Level_18 → () → T_ArgInfo_76 → T_ArgInfo_76 → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_arg'45'injective_88 ∷ T_Level_18 → () → T_ArgInfo_76 → T_ArgInfo_76 → AgdaAny → AgdaAny → T__'8801'__12 → T_Σ_14 Source #

du_arg'45'injective_88 ∷ T__'8801'__12 → T_Σ_14 Source #

d_unArg_90 ∷ T_Level_18 → () → T_Arg_88 → AgdaAny Source #

du_unArg_90 ∷ T_Arg_88 → AgdaAny Source #

d_unArg'45'dec_100 ∷ T_Level_18 → () → T_Arg_88 → T_Arg_88 → T_Dec_32 → T_Dec_32 Source #

du_unArg'45'dec_100 ∷ T_Arg_88 → T_Arg_88 → T_Dec_32 → T_Dec_32 Source #

d_'8801''45'dec_112 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → T_Arg_88 → T_Arg_88 → T_Dec_32 Source #

du_'8801''45'dec_112 ∷ (AgdaAny → AgdaAny → T_Dec_32) → T_Arg_88 → T_Arg_88 → T_Dec_32 Source #