Documentation

d_functor_8 ∷ T_Level_18 → T_RawFunctor_24 Source #

du_functor_8 ∷ T_RawFunctor_24 Source #

d_applicative_12 ∷ T_Level_18 → T_RawIApplicative_38 Source #

du_applicative_12 ∷ T_RawIApplicative_38 Source #

d_applicativeZero_22 ∷ T_Level_18 → T_RawIApplicativeZero_156 Source #

du_applicativeZero_22 ∷ T_RawIApplicativeZero_156 Source #

d_alternative_26 ∷ T_Level_18 → T_RawIAlternative_210 Source #

du_alternative_26 ∷ T_RawIAlternative_210 Source #

d_monad_30 ∷ T_Level_18 → T_RawIMonad_32 Source #

du_monad_30 ∷ T_RawIMonad_32 Source #

d_monadZero_34 ∷ T_Level_18 → T_RawIMonadZero_174 Source #

du_monadZero_34 ∷ T_RawIMonadZero_174 Source #

d_monadPlus_38 ∷ T_Level_18 → T_RawIMonadPlus_240 Source #

du_monadPlus_38 ∷ T_RawIMonadPlus_240 Source #

d_sequenceA_74 ∷ T_Level_18 → (() → ()) → T_RawIApplicative_38 → () → [AgdaAny] → AgdaAny Source #

du_sequenceA_74 ∷ T_RawIApplicative_38 → [AgdaAny] → AgdaAny Source #

d_mapA_86 ∷ T_Level_18 → (() → ()) → T_RawIApplicative_38 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny Source #

du_mapA_86 ∷ T_RawIApplicative_38 → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny Source #

d_forA_96 ∷ T_Level_18 → (() → ()) → T_RawIApplicative_38 → T_Level_18 → () → () → [AgdaAny] → (AgdaAny → AgdaAny) → AgdaAny Source #

du_forA_96 ∷ T_RawIApplicative_38 → [AgdaAny] → (AgdaAny → AgdaAny) → AgdaAny Source #

d_forA_148 ∷ T_Level_18 → (() → ()) → T_RawIMonad_32 → T_Level_18 → () → () → [AgdaAny] → (AgdaAny → AgdaAny) → AgdaAny Source #

du_forA_148 ∷ T_RawIMonad_32 → T_Level_18 → () → () → [AgdaAny] → (AgdaAny → AgdaAny) → AgdaAny Source #

d_mapA_150 ∷ T_Level_18 → (() → ()) → T_RawIMonad_32 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny Source #

du_mapA_150 ∷ T_RawIMonad_32 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny Source #

d_sequenceA_152 ∷ T_Level_18 → (() → ()) → T_RawIMonad_32 → () → [AgdaAny] → AgdaAny Source #

du_sequenceA_152 ∷ T_RawIMonad_32 → () → [AgdaAny] → AgdaAny Source #

d_monadT_158 ∷ T_Level_18 → (T_'8868'_6 → T_'8868'_6 → () → ()) → T_RawIMonad_32 → T_RawIMonad_32 Source #

du_monadT_158 ∷ T_RawIMonad_32 → T_RawIMonad_32 Source #

d_forA_208 ∷ T_Level_18 → (T_'8868'_6 → T_'8868'_6 → () → ()) → T_RawIMonad_32 → T_Level_18 → () → () → [AgdaAny] → (AgdaAny → AgdaAny) → AgdaAny Source #

du_forA_208 ∷ T_RawIMonad_32 → T_Level_18 → () → () → [AgdaAny] → (AgdaAny → AgdaAny) → AgdaAny Source #

d_mapA_210 ∷ T_Level_18 → (T_'8868'_6 → T_'8868'_6 → () → ()) → T_RawIMonad_32 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny Source #

du_mapA_210 ∷ T_RawIMonad_32 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny Source #

d_sequenceA_212 ∷ T_Level_18 → (T_'8868'_6 → T_'8868'_6 → () → ()) → T_RawIMonad_32 → () → [AgdaAny] → AgdaAny Source #

du_sequenceA_212 ∷ T_RawIMonad_32 → () → [AgdaAny] → AgdaAny Source #

d__'62''62''61'__240 ∷ T_Level_18 → () → () → T_'8868'_6 → T_'8868'_6 → T_'8868'_6 → [AgdaAny] → (AgdaAny → [AgdaAny]) → [AgdaAny] Source #

du__'62''62''61'__240 ∷ () → () → T_'8868'_6 → T_'8868'_6 → T_'8868'_6 → [AgdaAny] → (AgdaAny → [AgdaAny]) → [AgdaAny] Source #

d__'8739'__242 ∷ T_Level_18 → () → T_'8868'_6 → T_'8868'_6 → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du__'8739'__242 ∷ () → T_'8868'_6 → T_'8868'_6 → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

d__'8859'__246 ∷ T_Level_18 → () → () → T_'8868'_6 → T_'8868'_6 → T_'8868'_6 → [AgdaAny → AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du__'8859'__246 ∷ () → () → T_'8868'_6 → T_'8868'_6 → T_'8868'_6 → [AgdaAny → AgdaAny] → [AgdaAny] → [AgdaAny] Source #

d_return_264 ∷ T_Level_18 → () → T_'8868'_6 → AgdaAny → [AgdaAny] Source #

du_return_264 ∷ () → T_'8868'_6 → AgdaAny → [AgdaAny] Source #

d_'8709'_270 ∷ T_Level_18 → () → T_'8868'_6 → T_'8868'_6 → [AgdaAny] Source #

du_'8709'_270 ∷ () → T_'8868'_6 → T_'8868'_6 → [AgdaAny] Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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