Documentation

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

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

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

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

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

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

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

du_unAbs_50 ∷ T_Abs_112 → AgdaAny Source #

d_unAbs'45'dec_60 ∷ T_Level_18 → () → T_Abs_112 → T_Abs_112 → T_Dec_32 → T_Dec_32 Source #

du_unAbs'45'dec_60 ∷ T_Abs_112 → T_Abs_112 → T_Dec_32 → T_Dec_32 Source #

d_'8801''45'dec_72 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → T_Abs_112 → T_Abs_112 → T_Dec_32 Source #

du_'8801''45'dec_72 ∷ (AgdaAny → AgdaAny → T_Dec_32) → T_Abs_112 → T_Abs_112 → T_Dec_32 Source #