Documentation

d_map_22 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Abs_112 → T_Abs_112 Source #

du_map_22 ∷ (AgdaAny → AgdaAny) → T_Abs_112 → T_Abs_112 Source #

d_abs'45'injective'8321'_30 ∷ T_String_6 → T_Level_18 → () → AgdaAny → T_String_6 → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_abs'45'injective'8322'_32 ∷ T_String_6 → T_Level_18 → () → AgdaAny → T_String_6 → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_abs'45'injective_34 ∷ T_String_6 → T_Level_18 → () → AgdaAny → T_String_6 → AgdaAny → T__'8801'__12 → T_Σ_14 Source #

du_abs'45'injective_34 ∷ T__'8801'__12 → T_Σ_14 Source #

d_unAbs_36 ∷ T_Abs_112 → AgdaAny Source #

d_unAbs'45'dec_46 ∷ T_Level_18 → () → T_Abs_112 → T_Abs_112 → T_Dec_20 → T_Dec_20 Source #

du_unAbs'45'dec_46 ∷ T_Abs_112 → T_Abs_112 → T_Dec_20 → T_Dec_20 Source #

d_'8801''45'dec_58 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → T_Abs_112 → T_Abs_112 → T_Dec_20 Source #

du_'8801''45'dec_58 ∷ (AgdaAny → AgdaAny → T_Dec_20) → T_Abs_112 → T_Abs_112 → T_Dec_20 Source #