Documentation

d_functor_10 ∷ T_Level_18 → T_RawFunctor_24 Source #

du_functor_10 ∷ T_RawFunctor_24 Source #

d_applicative_12 ∷ T_Level_18 → T_RawApplicative_20 Source #

du_applicative_12 ∷ T_RawApplicative_20 Source #

d_empty_14 ∷ T_Level_18 → T_RawEmpty_16 Source #

du_empty_14 ∷ T_RawEmpty_16 Source #

d_choice_16 ∷ T_Level_18 → T_RawChoice_16 Source #

du_choice_16 ∷ T_RawChoice_16 Source #

d_applicativeZero_18 ∷ T_Level_18 → T_RawApplicativeZero_120 Source #

du_applicativeZero_18 ∷ T_RawApplicativeZero_120 Source #

d_alternative_20 ∷ T_Level_18 → T_RawAlternative_180 Source #

du_alternative_20 ∷ T_RawAlternative_180 Source #

d_monad_24 ∷ T_Level_18 → T_RawMonad_24 Source #

du_monad_24 ∷ T_RawMonad_24 Source #

d_join_26 ∷ T_Level_18 → () → [[AgdaAny]] → [AgdaAny] Source #

du_join_26 ∷ [[AgdaAny]] → [AgdaAny] Source #

d_monadZero_30 ∷ T_Level_18 → T_RawMonadZero_206 Source #

du_monadZero_30 ∷ T_RawMonadZero_206 Source #

d_monadPlus_34 ∷ T_Level_18 → T_RawMonadPlus_284 Source #

du_monadPlus_34 ∷ T_RawMonadPlus_284 Source #

d_sequenceA_82 ∷ T_Level_18 → T_Level_18 → (() → ()) → T_RawApplicative_20 → () → [AgdaAny] → AgdaAny Source #

du_sequenceA_82 ∷ T_RawApplicative_20 → [AgdaAny] → AgdaAny Source #

d_mapA_94 ∷ T_Level_18 → T_Level_18 → (() → ()) → T_RawApplicative_20 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny Source #

du_mapA_94 ∷ T_RawApplicative_20 → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny Source #

d_forA_104 ∷ T_Level_18 → T_Level_18 → (() → ()) → T_RawApplicative_20 → T_Level_18 → () → () → [AgdaAny] → (AgdaAny → AgdaAny) → AgdaAny Source #

du_forA_104 ∷ T_RawApplicative_20 → [AgdaAny] → (AgdaAny → AgdaAny) → AgdaAny Source #

d_forA_170 ∷ T_Level_18 → T_Level_18 → (() → ()) → T_RawMonad_24 → T_Level_18 → () → () → [AgdaAny] → (AgdaAny → AgdaAny) → AgdaAny Source #

du_forA_170 ∷ T_RawMonad_24 → T_Level_18 → () → () → [AgdaAny] → (AgdaAny → AgdaAny) → AgdaAny Source #

d_mapA_172 ∷ T_Level_18 → T_Level_18 → (() → ()) → T_RawMonad_24 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny Source #

du_mapA_172 ∷ T_RawMonad_24 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny Source #

d_sequenceA_174 ∷ T_Level_18 → T_Level_18 → (() → ()) → T_RawMonad_24 → () → [AgdaAny] → AgdaAny Source #

du_sequenceA_174 ∷ T_RawMonad_24 → () → [AgdaAny] → AgdaAny Source #

d__'60''36''62'__184 ∷ T_Level_18 → () → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] Source #

du__'60''36''62'__184 ∷ () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] Source #

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

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

d__'8739'__206 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du__'8739'__206 ∷ () → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

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

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

d_pure_220 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] Source #

du_pure_220 ∷ () → AgdaAny → [AgdaAny] Source #

d_'8709'_248 ∷ T_Level_18 → () → [AgdaAny] Source #

du_'8709'_248 ∷ () → [AgdaAny] Source #

d_left'45'identity_262 ∷ T_Level_18 → () → () → AgdaAny → (AgdaAny → [AgdaAny]) → T__'8801'__12 Source #

d_right'45'identity_274 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #

d_left'45'zero_290 ∷ T_Level_18 → () → () → (AgdaAny → [AgdaAny]) → T__'8801'__12 Source #

d_right'45'zero_302 ∷ T_Level_18 → () → () → [AgdaAny] → T__'8801'__12 Source #

d_right'45'distributive_330 ∷ T_Level_18 → () → () → [AgdaAny] → [AgdaAny] → (AgdaAny → [AgdaAny]) → T__'8801'__12 Source #

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

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

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

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

d_left'45'identity_408 ∷ T_Level_18 → () → () → AgdaAny → (AgdaAny → [AgdaAny]) → T__'8801'__12 Source #

d_left'45'zero_410 ∷ T_Level_18 → () → () → (AgdaAny → [AgdaAny]) → T__'8801'__12 Source #

d_right'45'distributive_412 ∷ T_Level_18 → () → () → [AgdaAny] → [AgdaAny] → (AgdaAny → [AgdaAny]) → T__'8801'__12 Source #

d_right'45'identity_414 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #

d_right'45'zero_416 ∷ T_Level_18 → () → () → [AgdaAny] → T__'8801'__12 Source #

d_pam_424 ∷ T_Level_18 → () → () → [AgdaAny] → (AgdaAny → AgdaAny) → [AgdaAny] Source #

du_pam_424 ∷ [AgdaAny] → (AgdaAny → AgdaAny) → [AgdaAny] Source #

d_left'45'zero_438 ∷ T_Level_18 → () → () → [AgdaAny] → T__'8801'__12 Source #

d_right'45'zero_450 ∷ T_Level_18 → () → () → [AgdaAny → AgdaAny] → T__'8801'__12 Source #

d_unfold'45''60''36''62'_470 ∷ T_Level_18 → () → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #

d_unfold'45''8859'_486 ∷ T_Level_18 → () → () → [AgdaAny → AgdaAny] → [AgdaAny] → T__'8801'__12 Source #

d_right'45'distributive_514 ∷ T_Level_18 → () → () → [AgdaAny → AgdaAny] → [AgdaAny → AgdaAny] → [AgdaAny] → T__'8801'__12 Source #

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

d_pam'45'lemma_556 ∷ T_Level_18 → () → () → () → [AgdaAny] → (AgdaAny → AgdaAny) → (AgdaAny → [AgdaAny]) → T__'8801'__12 Source #

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

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

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