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_20) → Maybe AgdaAny → Maybe AgdaAny → T_Dec_20 Source #

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

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

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

d_map'45''60''8739''62'_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'45'local_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''8728'_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_206 ∷ T_Level_18 → () → (Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny) → () Source #

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

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

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

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

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

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

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

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

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

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

d_IsMagma_392 ∷ p → p → p → () Source #

d_IsMonoid_398 ∷ p → p → p → p → () Source #

d_IsSemigroup_420 ∷ p → p → p → () Source #

d_isEquivalence_1692 ∷ T_IsMagma_176 → T_IsEquivalence_26 Source #

d_'8729''45'cong_1706 ∷ T_IsMagma_176 → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1802 ∷ T_IsMonoid_686 → T_Σ_14 Source #

d_isSemigroup_1814 ∷ T_IsMonoid_686 → T_IsSemigroup_472 Source #

d_assoc_2546 ∷ T_IsSemigroup_472 → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny → T__'8801'__12 Source #

d_isMagma_2550 ∷ T_IsSemigroup_472 → T_IsMagma_176 Source #

d_'60''8739''62''45'isMagma_2860 ∷ T_Level_18 → () → T_IsMagma_176 Source #

du_'60''8739''62''45'isMagma_2860 ∷ T_IsMagma_176 Source #

d_'60''8739''62''45'isSemigroup_2862 ∷ T_Level_18 → () → T_IsSemigroup_472 Source #

du_'60''8739''62''45'isSemigroup_2862 ∷ T_IsSemigroup_472 Source #

d_'60''8739''62''45'isMonoid_2864 ∷ T_Level_18 → () → T_IsMonoid_686 Source #

du_'60''8739''62''45'isMonoid_2864 ∷ T_IsMonoid_686 Source #

d_'60''8739''62''45'semigroup_2866 ∷ T_Level_18 → () → T_Semigroup_536 Source #

du_'60''8739''62''45'semigroup_2866 ∷ T_Semigroup_536 Source #

d_'60''8739''62''45'monoid_2868 ∷ T_Level_18 → () → T_Monoid_882 Source #

du_'60''8739''62''45'monoid_2868 ∷ T_Monoid_882 Source #

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

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

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

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