Documentation

d_just'45'injective_22 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_'8801''45'dec_24 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → Maybe AgdaAny → Maybe AgdaAny → T_Dec_32 Source #

du_'8801''45'dec_24 ∷ (AgdaAny → AgdaAny → T_Dec_32) → Maybe AgdaAny → Maybe AgdaAny → T_Dec_32 Source #

d_map'45'id_42 ∷ T_Level_18 → () → Maybe AgdaAny → T__'8801'__12 Source #

d_map'45'id'8322'_52 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 → T__'8801'__12 Source #

d_map'45''60''8739''62''45'commute_62 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 Source #

d_map'45'cong_78 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → Maybe AgdaAny → T__'8801'__12 Source #

d_map'45'cong'8322'_94 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 → T__'8801'__12 Source #

d_map'45'injective_100 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_map'45'compose_118 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → Maybe AgdaAny → T__'8801'__12 Source #

d_map'45'nothing_126 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → Maybe AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_map'45'just_134 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → Maybe AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_maybe'45'map_148 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (Maybe AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → Maybe AgdaAny → T__'8801'__12 Source #

d_maybe'8242''45'map_172 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → Maybe AgdaAny → T__'8801'__12 Source #

d_Associative_202 ∷ T_Level_18 → () → (Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny) → () Source #

d_Identity_218 ∷ T_Level_18 → () → Maybe AgdaAny → (Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny) → () Source #

d_LeftIdentity_232 ∷ T_Level_18 → () → Maybe AgdaAny → (Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny) → () Source #

d_RightIdentity_244 ∷ T_Level_18 → () → Maybe AgdaAny → (Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny) → () Source #

d_'60''8739''62''45'assoc_254 ∷ T_Level_18 → () → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 Source #

d_'60''8739''62''45'identity'737'_266 ∷ T_Level_18 → () → Maybe AgdaAny → T__'8801'__12 Source #

d_'60''8739''62''45'identity'691'_270 ∷ T_Level_18 → () → Maybe AgdaAny → T__'8801'__12 Source #

d_'60''8739''62''45'identity_274 ∷ T_Level_18 → () → T_Σ_14 Source #

du_'60''8739''62''45'identity_274 ∷ T_Σ_14 Source #

d_IsMagma_316 ∷ p → p → p → () Source #

d_IsMonoid_318 ∷ p → p → p → p → () Source #

d_IsSemigroup_326 ∷ p → p → p → () Source #

d_'60''8739''62''45'isMagma_1708 ∷ T_Level_18 → () → T_IsMagma_86 Source #

du_'60''8739''62''45'isMagma_1708 ∷ T_IsMagma_86 Source #

d_'60''8739''62''45'isSemigroup_1710 ∷ T_Level_18 → () → T_IsSemigroup_194 Source #

du_'60''8739''62''45'isSemigroup_1710 ∷ T_IsSemigroup_194 Source #

d_'60''8739''62''45'isMonoid_1712 ∷ T_Level_18 → () → T_IsMonoid_358 Source #

du_'60''8739''62''45'isMonoid_1712 ∷ T_IsMonoid_358 Source #

d_'60''8739''62''45'semigroup_1714 ∷ T_Level_18 → () → T_Semigroup_206 Source #

du_'60''8739''62''45'semigroup_1714 ∷ T_Semigroup_206 Source #

d_'60''8739''62''45'monoid_1716 ∷ T_Level_18 → () → T_Monoid_506 Source #

du_'60''8739''62''45'monoid_1716 ∷ T_Monoid_506 Source #