Documentation

d_Product'8868'_12 ∷ Integer → AgdaAny → AgdaAny → () Source #

d_Product_26 ∷ Integer → AgdaAny → AgdaAny → () Source #

d_HomoProduct'8242'_40 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → () Source #

d_HomoProduct_50 ∷ Integer → T_Level_18 → () → () Source #

d_Pointwise'8345'_70 ∷ (T_Level_18 → () → AgdaAny → AgdaAny → ()) → Integer → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Equal'8345'_106 ∷ Integer → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_toProduct_114 ∷ Integer → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_toProduct_114 ∷ Integer → AgdaAny → AgdaAny Source #

d_toProduct'8868'_130 ∷ Integer → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_toProduct'8868'_130 ∷ Integer → AgdaAny → AgdaAny Source #

d_curry'8345'_150 ∷ Integer → AgdaAny → AgdaAny → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny Source #

du_curry'8345'_150 ∷ Integer → (AgdaAny → AgdaAny) → AgdaAny Source #

d_uncurry'8345'_170 ∷ Integer → AgdaAny → AgdaAny → T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny Source #

du_uncurry'8345'_170 ∷ Integer → AgdaAny → AgdaAny → AgdaAny Source #

d_curry'8868''8345'_190 ∷ Integer → AgdaAny → AgdaAny → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny Source #

du_curry'8868''8345'_190 ∷ Integer → (AgdaAny → AgdaAny) → AgdaAny Source #

d_uncurry'8868''8345'_208 ∷ Integer → AgdaAny → AgdaAny → T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny Source #

du_uncurry'8868''8345'_208 ∷ Integer → AgdaAny → AgdaAny → AgdaAny Source #

d_Product'8868''45'dec_222 ∷ Integer → AgdaAny → AgdaAny → AgdaAny → T_Dec_20 Source #

du_Product'8868''45'dec_222 ∷ Integer → AgdaAny → T_Dec_20 Source #

d_Product'45'dec_236 ∷ Integer → AgdaAny → AgdaAny → AgdaAny → T_Dec_20 Source #

du_Product'45'dec_236 ∷ Integer → AgdaAny → T_Dec_20 Source #

d_toEqual'8345'_256 ∷ Integer → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_toEqual'8345'_256 ∷ Integer → T__'8801'__12 → AgdaAny Source #

d_fromEqual'8345'_276 ∷ Integer → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_Level'8345'_288 ∷ Integer → AgdaAny → T_Fin_10 → T_Level_18 Source #

du_Level'8345'_288 ∷ AgdaAny → T_Fin_10 → T_Level_18 Source #

d_Proj'8345'_302 ∷ Integer → AgdaAny → AgdaAny → T_Fin_10 → () Source #

d_proj'8345'_318 ∷ Integer → AgdaAny → AgdaAny → T_Fin_10 → AgdaAny → AgdaAny Source #

du_proj'8345'_318 ∷ Integer → T_Fin_10 → AgdaAny → AgdaAny Source #

d_zipWith_348 ∷ Integer → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (T_Fin_10 → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_zipWith_348 ∷ Integer → (T_Fin_10 → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_Level'8345''8315'_374 ∷ Integer → AgdaAny → T_Fin_10 → AgdaAny Source #

du_Level'8345''8315'_374 ∷ AgdaAny → T_Fin_10 → AgdaAny Source #

d_Remove'8345'_390 ∷ Integer → AgdaAny → AgdaAny → T_Fin_10 → AgdaAny Source #

du_Remove'8345'_390 ∷ AgdaAny → T_Fin_10 → AgdaAny Source #

d_remove'8345'_408 ∷ Integer → AgdaAny → AgdaAny → T_Fin_10 → AgdaAny → AgdaAny Source #

du_remove'8345'_408 ∷ Integer → T_Fin_10 → AgdaAny → AgdaAny Source #

d_Level'8345''8314'_424 ∷ Integer → AgdaAny → T_Fin_10 → T_Level_18 → T_Σ_14 Source #

du_Level'8345''8314'_424 ∷ AgdaAny → T_Fin_10 → T_Level_18 → T_Σ_14 Source #

d_Insert'8345'_448 ∷ Integer → AgdaAny → T_Level_18 → AgdaAny → T_Fin_10 → () → T_Σ_14 Source #

du_Insert'8345'_448 ∷ AgdaAny → T_Fin_10 → () → T_Σ_14 Source #

d_insert'8345'_476 ∷ Integer → AgdaAny → T_Level_18 → AgdaAny → () → T_Fin_10 → AgdaAny → AgdaAny → AgdaAny Source #

du_insert'8345'_476 ∷ Integer → T_Fin_10 → AgdaAny → AgdaAny → AgdaAny Source #

d_Level'8345''7512'_506 ∷ Integer → AgdaAny → T_Fin_10 → T_Level_18 → AgdaAny Source #

du_Level'8345''7512'_506 ∷ AgdaAny → T_Fin_10 → T_Level_18 → AgdaAny Source #

d_Update'8345'_532 ∷ Integer → AgdaAny → T_Level_18 → AgdaAny → T_Fin_10 → () → AgdaAny Source #

du_Update'8345'_532 ∷ AgdaAny → T_Fin_10 → () → AgdaAny Source #

d_update'8345'_564 ∷ Integer → AgdaAny → T_Level_18 → AgdaAny → T_Fin_10 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_update'8345'_564 ∷ Integer → T_Fin_10 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_update'8345''8242'_600 ∷ Integer → AgdaAny → T_Level_18 → AgdaAny → T_Fin_10 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_update'8345''8242'_600 ∷ Integer → T_Fin_10 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_All'8345'_606 ∷ (T_Level_18 → () → AgdaAny → AgdaAny → ()) → Integer → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #