| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.Sum.Function.Setoid
Documentation
d_inj'8321''8347'_52 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Func_714 Source #
d_inj'8322''8347'_54 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Func_714 Source #
d_'91'_'44'_'93''8347'_56 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Func_714 → T_Func_714 → T_Func_714 Source #
d_'46'extendedlambda0_66 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Func_714 → T_Func_714 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → AgdaAny Source #
du_'46'extendedlambda0_66 ∷ T_Func_714 → T_Func_714 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → AgdaAny Source #
d_swap'8347'_72 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Func_714 Source #
d_'8846''45'injective_78 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'8846''45'injective_78 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
d_'8846''45'strictlySurjective_104 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → (AgdaAny → T_Σ_14) → T__'8846'__30 → T_Σ_14 Source #
du_'8846''45'strictlySurjective_104 ∷ (AgdaAny → T_Σ_14) → (AgdaAny → T_Σ_14) → T__'8846'__30 → T_Σ_14 Source #
d_'8846''45'surjective_114 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → (AgdaAny → T_Σ_14) → T__'8846'__30 → T_Σ_14 Source #
du_'8846''45'surjective_114 ∷ (AgdaAny → T_Σ_14) → (AgdaAny → T_Σ_14) → T__'8846'__30 → T_Σ_14 Source #
d_'46'extendedlambda0_120 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → (AgdaAny → T_Σ_14) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'46'extendedlambda0_120 ∷ (AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
d_'46'extendedlambda1_126 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → (AgdaAny → T_Σ_14) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'46'extendedlambda1_126 ∷ (AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
d__'8846''45'function__132 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Func_714 → T_Func_714 → T_Func_714 Source #
d__'8846''45'equivalence__142 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Equivalence_1714 → T_Equivalence_1714 → T_Equivalence_1714 Source #
du__'8846''45'equivalence__142 ∷ T_Equivalence_1714 → T_Equivalence_1714 → T_Equivalence_1714 Source #
d__'8846''45'injection__152 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Injection_776 → T_Injection_776 → T_Injection_776 Source #
d__'8846''45'surjection__162 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Surjection_846 → T_Surjection_846 → T_Surjection_846 Source #
d__'8846''45'bijection__172 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Bijection_926 → T_Bijection_926 → T_Bijection_926 Source #
d__'8846''45'leftInverse__182 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_LeftInverse_1792 → T_LeftInverse_1792 → T_LeftInverse_1792 Source #
du__'8846''45'leftInverse__182 ∷ T_LeftInverse_1792 → T_LeftInverse_1792 → T_LeftInverse_1792 Source #
d_'46'extendedlambda2_192 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_LeftInverse_1792 → T_LeftInverse_1792 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'46'extendedlambda2_192 ∷ T_LeftInverse_1792 → T_LeftInverse_1792 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
d__'8846''45'rightInverse__198 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_RightInverse_1880 → T_RightInverse_1880 → T_RightInverse_1880 Source #
du__'8846''45'rightInverse__198 ∷ T_RightInverse_1880 → T_RightInverse_1880 → T_RightInverse_1880 Source #
d_'46'extendedlambda2_208 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_RightInverse_1880 → T_RightInverse_1880 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'46'extendedlambda2_208 ∷ T_RightInverse_1880 → T_RightInverse_1880 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
d__'8846''45'inverse__214 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #
d_'46'extendedlambda2_224 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → T_Inverse_1960 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'46'extendedlambda2_224 ∷ T_Inverse_1960 → T_Inverse_1960 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
d_'46'extendedlambda3_230 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → T_Inverse_1960 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #