| 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_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Func_774 Source #
d_inj'8322''8347'_54 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Func_774 Source #
d_'91'_'44'_'93''8347'_56 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Func_774 → T_Func_774 → T_Func_774 Source #
d_'46'extendedlambda0_66 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Func_774 → T_Func_774 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → AgdaAny Source #
du_'46'extendedlambda0_66 ∷ T_Func_774 → T_Func_774 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → AgdaAny Source #
d_swap'8347'_72 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Func_774 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_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Func_774 → T_Func_774 → T_Func_774 Source #
d__'8846''45'equivalence__142 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Equivalence_1858 → T_Equivalence_1858 → T_Equivalence_1858 Source #
du__'8846''45'equivalence__142 ∷ T_Equivalence_1858 → T_Equivalence_1858 → T_Equivalence_1858 Source #
d__'8846''45'injection__152 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Injection_842 → T_Injection_842 → T_Injection_842 Source #
d__'8846''45'surjection__162 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Surjection_918 → T_Surjection_918 → T_Surjection_918 Source #
d__'8846''45'bijection__172 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Bijection_1004 → T_Bijection_1004 → T_Bijection_1004 Source #
d__'8846''45'leftInverse__182 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_LeftInverse_1942 → T_LeftInverse_1942 → T_LeftInverse_1942 Source #
du__'8846''45'leftInverse__182 ∷ T_LeftInverse_1942 → T_LeftInverse_1942 → T_LeftInverse_1942 Source #
d_'46'extendedlambda2_192 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_LeftInverse_1942 → T_LeftInverse_1942 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'46'extendedlambda2_192 ∷ T_LeftInverse_1942 → T_LeftInverse_1942 → 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_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_RightInverse_2036 → T_RightInverse_2036 → T_RightInverse_2036 Source #
du__'8846''45'rightInverse__198 ∷ T_RightInverse_2036 → T_RightInverse_2036 → T_RightInverse_2036 Source #
d_'46'extendedlambda2_208 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_RightInverse_2036 → T_RightInverse_2036 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'46'extendedlambda2_208 ∷ T_RightInverse_2036 → T_RightInverse_2036 → 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_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → T_Inverse_2122 → T_Inverse_2122 Source #
d_'46'extendedlambda2_224 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → T_Inverse_2122 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'46'extendedlambda2_224 ∷ T_Inverse_2122 → T_Inverse_2122 → 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_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → T_Inverse_2122 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #