Documentation

d_map_22 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Abs_112 -> T_Abs_112 #

du_map_22 :: (AgdaAny -> AgdaAny) -> T_Abs_112 -> T_Abs_112 #

d_abs'45'injective'8321'_30 :: T_String_6 -> T_Level_18 -> () -> AgdaAny -> T_String_6 -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #

d_abs'45'injective'8322'_32 :: T_String_6 -> T_Level_18 -> () -> AgdaAny -> T_String_6 -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #

d_abs'45'injective_34 :: T_String_6 -> T_Level_18 -> () -> AgdaAny -> T_String_6 -> AgdaAny -> T__'8801'__12 -> T_Σ_14 #

du_abs'45'injective_34 :: T__'8801'__12 -> T_Σ_14 #

d_unAbs_36 :: T_Level_18 -> () -> T_Abs_112 -> AgdaAny #

du_unAbs_36 :: T_Abs_112 -> AgdaAny #

d_unAbs'45'dec_46 :: T_Level_18 -> () -> T_Abs_112 -> T_Abs_112 -> T_Dec_20 -> T_Dec_20 #

du_unAbs'45'dec_46 :: T_Abs_112 -> T_Abs_112 -> T_Dec_20 -> T_Dec_20 #

d_'8801''45'dec_58 :: T_Level_18 -> () -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_Abs_112 -> T_Abs_112 -> T_Dec_20 #

du_'8801''45'dec_58 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> T_Abs_112 -> T_Abs_112 -> T_Dec_20 #