Documentation

d_dmap_12 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → ((AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20) → T_Dec_20 → T_Dec_20 Source #

du_dmap_12 ∷ (AgdaAny → AgdaAny) → T_Dec_20 → T_Dec_20 Source #

d_dcong_40 ∷ T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → (T__'8801'__12 → T__'8801'__12) → T_Dec_20 → T_Dec_20 Source #

du_dcong_40 ∷ T_Dec_20 → T_Dec_20 Source #

d_dcong'8322'_70 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (T__'8801'__12 → T_Σ_14) → T_Dec_20 → T_Dec_20 → T_Dec_20 Source #

du_dcong'8322'_70 ∷ T_Dec_20 → T_Dec_20 → T_Dec_20 Source #

d_dhcong_120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → () → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (T__'8801'__12 → T_Σ_14) → T_Dec_20 → (AgdaAny → T_Dec_20) → T_Dec_20 Source #

du_dhcong_120 ∷ AgdaAny → T_Dec_20 → (AgdaAny → T_Dec_20) → T_Dec_20 Source #

d_dhcong'8322'_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → () → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (T__'8801'__12 → T_Σ_14) → T_Dec_20 → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → T_Dec_20 Source #

du_dhcong'8322'_180 ∷ AgdaAny → AgdaAny → T_Dec_20 → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → T_Dec_20 Source #