| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.Product.Function.NonDependent.Propositional
Documentation
d_liftViaInverse_66 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → ()) → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny) → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_liftViaInverse_66 ∷ (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny) → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d__'215''45''10230'__78 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Func_714 → T_Func_714 → T_Func_714 Source #
d__'215''45''8660'__80 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Equivalence_1714 → T_Equivalence_1714 → T_Equivalence_1714 Source #
d__'215''45''8611'__82 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Injection_776 → T_Injection_776 → T_Injection_776 Source #
d__'215''45''8608'__84 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Surjection_846 → T_Surjection_846 → T_Surjection_846 Source #
d__'215''45''10518'__86 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Bijection_926 → T_Bijection_926 → T_Bijection_926 Source #
d__'215''45''8617'__88 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1792 → T_LeftInverse_1792 → T_LeftInverse_1792 Source #
d__'215''45''8618'__90 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_RightInverse_1880 → T_RightInverse_1880 → T_RightInverse_1880 Source #
d__'215''45''8596'__92 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #
d__'215''45'cong__96 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Kind_6 → AgdaAny → AgdaAny → AgdaAny Source #