Documentation

d__'62''62''61'__36 ∷ T_Level_18 → () → () → [AgdaAny] → (AgdaAny → [AgdaAny]) → [AgdaAny] Source #

du__'62''62''61'__36 ∷ [AgdaAny] → (AgdaAny → [AgdaAny]) → [AgdaAny] Source #

d__'8855'__38 ∷ T_Level_18 → () → () → [AgdaAny] → [AgdaAny] → [T_Σ_14] Source #

du__'8855'__38 ∷ () → () → [AgdaAny] → [AgdaAny] → [T_Σ_14] Source #

d__'8859'__40 ∷ T_Level_18 → () → () → [AgdaAny → AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du__'8859'__40 ∷ () → () → [AgdaAny → AgdaAny] → [AgdaAny] → [AgdaAny] Source #

d_'8712''45'resp'45''8779'_86 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #

du_'8712''45'resp'45''8779'_86 ∷ AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #

d_'8713''45'resp'45''8779'_90 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → (T_Any_34 → T_Irrelevant_20) → T_Any_34 → T_Irrelevant_20 Source #

d_mapWith'8712''45'cong_104 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → (AgdaAny → T_Any_34 → AgdaAny) → (AgdaAny → T_Any_34 → T__'8801'__12) → T__'8801'__12 Source #

d_mapWith'8712''8791'map_130 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #

d_mapWith'8712''45'id_142 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #

d_map'45'mapWith'8712'_152 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → (AgdaAny → AgdaAny) → T__'8801'__12 Source #

d_'8712''45'map'8314'_164 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 Source #

du_'8712''45'map'8314'_164 ∷ AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_'8712''45'map'8315'_168 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

du_'8712''45'map'8315'_168 ∷ [AgdaAny] → T_Any_34 → T_Σ_14 Source #

d_map'45''8712''8596'_172 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Inverse_2122 Source #

du_map'45''8712''8596'_172 ∷ [AgdaAny] → T_Inverse_2122 Source #

d_'8712''45''43''43''8314''737'_194 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #

du_'8712''45''43''43''8314''737'_194 ∷ [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_'8712''45''43''43''8314''691'_200 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #

du_'8712''45''43''43''8314''691'_200 ∷ [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_'8712''45''43''43''8315'_206 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T__'8846'__30 Source #

du_'8712''45''43''43''8315'_206 ∷ [AgdaAny] → [AgdaAny] → T_Any_34 → T__'8846'__30 Source #

d_'43''43''45''8712''8660'_208 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Equivalence_1858 Source #

du_'43''43''45''8712''8660'_208 ∷ [AgdaAny] → [AgdaAny] → T_Equivalence_1858 Source #

d_'8712''45'insert_214 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 Source #

du_'8712''45'insert_214 ∷ AgdaAny → [AgdaAny] → T_Any_34 Source #

d_'8712''45''8707''43''43'_222 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

du_'8712''45''8707''43''43'_222 ∷ [AgdaAny] → T_Any_34 → T_Σ_14 Source #

d_'8712''45'concat'8314'_246 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #

du_'8712''45'concat'8314'_246 ∷ [[AgdaAny]] → T_Any_34 → T_Any_34 Source #

d_'8712''45'concat'8315'_252 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #

du_'8712''45'concat'8315'_252 ∷ [[AgdaAny]] → T_Any_34 → T_Any_34 Source #

d_'8712''45'concat'8314''8242'_258 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [[AgdaAny]] → T_Any_34 → T_Any_34 → T_Any_34 Source #

du_'8712''45'concat'8314''8242'_258 ∷ AgdaAny → [AgdaAny] → [[AgdaAny]] → T_Any_34 → T_Any_34 → T_Any_34 Source #

d_'8712''45'concat'8315''8242'_268 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Σ_14 Source #

du_'8712''45'concat'8315''8242'_268 ∷ [[AgdaAny]] → T_Any_34 → T_Σ_14 Source #

d_concat'45''8712''8596'_282 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Inverse_2122 Source #

du_concat'45''8712''8596'_282 ∷ [[AgdaAny]] → T_Inverse_2122 Source #

d_S'7468'_310 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → [AgdaAny]) → [AgdaAny] → AgdaAny → T_Setoid_46 Source #

du_S'7468'_310 ∷ T_Setoid_46 Source #

d_S'7470'_312 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → [AgdaAny]) → [AgdaAny] → AgdaAny → T_Setoid_46 Source #

du_S'7470'_312 ∷ T_Setoid_46 Source #

d_'8712''45'concatMap'8314'_316 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → [AgdaAny]) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #

du_'8712''45'concatMap'8314'_316 ∷ (AgdaAny → [AgdaAny]) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_'8712''45'concatMap'8315'_320 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → [AgdaAny]) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #

du_'8712''45'concatMap'8315'_320 ∷ (AgdaAny → [AgdaAny]) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_'8712''45'cartesianProductWith'8314'_342 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → T_Any_34 Source #

du_'8712''45'cartesianProductWith'8314'_342 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → T_Any_34 Source #

d_'8712''45'cartesianProductWith'8315'_354 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → T_Any_34 → T_Σ_14 Source #

du_'8712''45'cartesianProductWith'8315'_354 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → T_Any_34 → T_Σ_14 Source #

d_'8712''45'cartesianProduct'8314'_364 ∷ T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 → T_Any_34 Source #

du_'8712''45'cartesianProduct'8314'_364 ∷ AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 → T_Any_34 Source #

d_'8712''45'cartesianProduct'8315'_376 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Σ_14 → T_Any_34 → T_Σ_14 Source #

du_'8712''45'cartesianProduct'8315'_376 ∷ [AgdaAny] → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

d_'8712''45'applyUpTo'8314'_404 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → Integer → T__'8804'__22 → T_Any_34 Source #

du_'8712''45'applyUpTo'8314'_404 ∷ (Integer → AgdaAny) → Integer → T__'8804'__22 → T_Any_34 Source #

d_'8712''45'applyUpTo'8315'_412 ∷ T_Level_18 → () → (Integer → AgdaAny) → AgdaAny → Integer → T_Any_34 → T_Σ_14 Source #

du_'8712''45'applyUpTo'8315'_412 ∷ (Integer → AgdaAny) → Integer → T_Any_34 → T_Σ_14 Source #

d_'8712''45'upTo'8314'_418 ∷ Integer → Integer → T__'8804'__22 → T_Any_34 Source #

du_'8712''45'upTo'8314'_418 ∷ Integer → T__'8804'__22 → T_Any_34 Source #

d_'8712''45'upTo'8315'_424 ∷ Integer → Integer → T_Any_34 → T__'8804'__22 Source #

du_'8712''45'upTo'8315'_424 ∷ T_Any_34 → T__'8804'__22 Source #

d_'8712''45'applyDownFrom'8314'_446 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → Integer → T__'8804'__22 → T_Any_34 Source #

du_'8712''45'applyDownFrom'8314'_446 ∷ (Integer → AgdaAny) → Integer → Integer → T__'8804'__22 → T_Any_34 Source #

d_'8712''45'applyDownFrom'8315'_454 ∷ T_Level_18 → () → (Integer → AgdaAny) → AgdaAny → Integer → T_Any_34 → T_Σ_14 Source #

du_'8712''45'applyDownFrom'8315'_454 ∷ (Integer → AgdaAny) → Integer → T_Any_34 → T_Σ_14 Source #

d_'8712''45'downFrom'8314'_460 ∷ Integer → Integer → T__'8804'__22 → T_Any_34 Source #

d_'8712''45'downFrom'8315'_468 ∷ Integer → Integer → T_Any_34 → T__'8804'__22 Source #

du_'8712''45'downFrom'8315'_468 ∷ Integer → T_Any_34 → T__'8804'__22 Source #

d_'8712''45'tabulate'8314'_490 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → T_Fin_10 → T_Any_34 Source #

du_'8712''45'tabulate'8314'_490 ∷ (T_Fin_10 → AgdaAny) → T_Fin_10 → T_Any_34 Source #

d_'8712''45'tabulate'8315'_496 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → AgdaAny → T_Any_34 → T_Σ_14 Source #

du_'8712''45'tabulate'8315'_496 ∷ T_Any_34 → T_Σ_14 Source #

d_'8712''45'filter'8314'_510 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → T_Any_34 → AgdaAny → T_Any_34 Source #

du_'8712''45'filter'8314'_510 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → AgdaAny → T_Any_34 Source #

d_'8712''45'filter'8315'_512 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

du_'8712''45'filter'8315'_512 ∷ (AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

d_S'7468'_536 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Setoid_46 Source #

du_S'7468'_536 ∷ T_Setoid_46 Source #

d_S'7470'_538 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Setoid_46 Source #

du_S'7470'_538 ∷ T_Setoid_46 Source #

d_respP_540 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny Source #

du_respP_540 ∷ AgdaAny → AgdaAny Source #

d_'8712''45'map'8728'filter'8315'_544 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Any_34 → T_Σ_14 Source #

du_'8712''45'map'8728'filter'8315'_544 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

d_'8712''45'map'8728'filter'8314'_548 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Σ_14 → T_Any_34 Source #

du_'8712''45'map'8728'filter'8314'_548 ∷ (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Σ_14 → T_Any_34 Source #

d_'8712''45'derun'8315'_566 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #

du_'8712''45'derun'8315'_566 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_'8712''45'deduplicate'8315'_576 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #

du_'8712''45'deduplicate'8315'_576 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_'8712''45'derun'8314'_594 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #

du_'8712''45'derun'8314'_594 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #

d_resp'8776'_598 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8712''45'deduplicate'8314'_614 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #

du_'8712''45'deduplicate'8314'_614 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #

d_deduplicate'45''8712''8660'_622 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Equivalence_1858 Source #

du_deduplicate'45''8712''8660'_622 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Equivalence_1858 Source #

d_'62''62''61''45''8712''8596'_632 ∷ T_Level_18 → () → () → [AgdaAny] → (AgdaAny → [AgdaAny]) → AgdaAny → T_Inverse_2122 Source #

du_'62''62''61''45''8712''8596'_632 ∷ [AgdaAny] → (AgdaAny → [AgdaAny]) → T_Inverse_2122 Source #

d_'8859''45''8712''8596'_658 ∷ T_Level_18 → () → () → [AgdaAny → AgdaAny] → [AgdaAny] → AgdaAny → T_Inverse_2122 Source #

du_'8859''45''8712''8596'_658 ∷ [AgdaAny → AgdaAny] → [AgdaAny] → T_Inverse_2122 Source #

d_'8855''45''8712''8596'_690 ∷ T_Level_18 → () → () → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_Inverse_2122 Source #

du_'8855''45''8712''8596'_690 ∷ [AgdaAny] → [AgdaAny] → T_Inverse_2122 Source #

d_'8712''45'length_710 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Any_34 → T__'8804'__22 Source #

du_'8712''45'length_710 ∷ T_Any_34 → T__'8804'__22 Source #

d_'8712''45'lookup_714 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → T_Any_34 Source #

du_'8712''45'lookup_714 ∷ [AgdaAny] → T_Fin_10 → T_Any_34 Source #

d_foldr'45'selective_732 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #

du_foldr'45'selective_732 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #

d_'8712''45'allFin_738 ∷ Integer → T_Fin_10 → T_Any_34 Source #

du_'8712''45'allFin_738 ∷ T_Fin_10 → T_Any_34 Source #

d_'91''93''8712'inits_742 ∷ T_Level_18 → () → [AgdaAny] → T_Any_34 Source #

du_'91''93''8712'inits_742 ∷ T_Any_34 Source #

d_finite_750 ∷ T_Level_18 → () → T_Injection_842 → [AgdaAny] → (Integer → T_Any_34) → T_Irrelevant_20 Source #

d_f_834 ∷ T_Level_18 → () → T_Injection_842 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → AgdaAny Source #

du_f_834 ∷ T_Injection_842 → Integer → AgdaAny Source #

d_not'45'x_838 ∷ T_Level_18 → () → T_Injection_842 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → (T__'8801'__12 → T_Irrelevant_20) → T_Any_34 Source #

du_not'45'x_838 ∷ (Integer → T_Any_34) → Integer → T_Any_34 Source #

d_helper_862 ∷ T_Level_18 → () → T_Injection_842 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → T_Dec_20 → T_Irrelevant_20 Source #

d_f'8242'_876 ∷ T_Level_18 → () → T_Injection_842 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → AgdaAny Source #

du_f'8242'_876 ∷ T_Injection_842 → Integer → Integer → AgdaAny Source #

d_'8712''45'if'45'not'45'i_890 ∷ T_Level_18 → () → T_Injection_842 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → (T__'8801'__12 → T_Irrelevant_20) → T_Any_34 Source #

du_'8712''45'if'45'not'45'i_890 ∷ (Integer → T_Any_34) → Integer → T_Any_34 Source #

d_lemma_898 ∷ T_Level_18 → () → T_Injection_842 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → Integer → T__'8804'__22 → (T__'8804'__22 → T_Irrelevant_20) → T__'8801'__12 → T_Irrelevant_20 Source #

d_f'8242''11388''8712'xs_906 ∷ T_Level_18 → () → T_Injection_842 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → T_Any_34 Source #

du_f'8242''11388''8712'xs_906 ∷ (Integer → T_Any_34) → Integer → Integer → T_Any_34 Source #

d_f'8242''45'injective'8242'_922 ∷ T_Level_18 → () → T_Injection_842 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_f'8242''45'inj_974 ∷ T_Level_18 → () → T_Injection_842 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → T_Injection_842 Source #

du_f'8242''45'inj_974 ∷ T_Injection_842 → Integer → T_Injection_842 Source #

d_there'45'injective'45''8802''8712'_988 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → (T__'8801'__12 → T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 → T_Irrelevant_20 Source #

d_'8712''45'AllPairs'8322'_1010 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → AgdaAny → AgdaAny → T_AllPairs_20 → T_Any_34 → T_Any_34 → T__'8846'__30 Source #

du_'8712''45'AllPairs'8322'_1010 ∷ [AgdaAny] → T_AllPairs_20 → T_Any_34 → T_Any_34 → T__'8846'__30 Source #

d_map'8759''8315'_1030 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Σ_14 Source #

du_map'8759''8315'_1030 ∷ [[AgdaAny]] → T_Any_34 → T_Σ_14 Source #

d_'91''93''8713'map'8759'_1036 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Irrelevant_20 Source #

d_map'8759''45'decomp'8712'_1046 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Σ_14 Source #

du_map'8759''45'decomp'8712'_1046 ∷ [[AgdaAny]] → T_Any_34 → T_Σ_14 Source #

d_'8712''45'map'8759''8315'_1058 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #

du_'8712''45'map'8759''8315'_1058 ∷ [[AgdaAny]] → T_Any_34 → T_Any_34 Source #

d_'46'generalizedField'45'A'46'ℓ_32949 ∷ T_GeneralizeTel_32957 → T_Level_18 Source #

d_'46'generalizedField'45'A_32951 ∷ T_GeneralizeTel_32957 → () Source #

d_'46'generalizedField'45'B'46'ℓ_32953 ∷ T_GeneralizeTel_32957 → T_Level_18 Source #

d_'46'generalizedField'45'B_32955 ∷ T_GeneralizeTel_32957 → () Source #

d_GeneralizeTel_32957 ∷ () Source #

data T_GeneralizeTel_32957 Source #

d_'46'generalizedField'45'A'46'ℓ_60363 ∷ T_GeneralizeTel_60371 → T_Level_18 Source #

d_'46'generalizedField'45'A_60365 ∷ T_GeneralizeTel_60371 → () Source #

d_'46'generalizedField'45'B'46'ℓ_60367 ∷ T_GeneralizeTel_60371 → T_Level_18 Source #

d_'46'generalizedField'45'B_60369 ∷ T_GeneralizeTel_60371 → () Source #

d_GeneralizeTel_60371 ∷ () Source #

data T_GeneralizeTel_60371 Source #