| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Function.Consequences.Propositional
Documentation
d_contraInjective_16 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → AgdaAny → AgdaAny → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T_Irrelevant_20 Source #
d_inverse'691''8658'injective_18 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_inverse'691''8658'strictlyInverse'691'_20 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → AgdaAny → T__'8801'__12 Source #
d_inverse'737''8658'strictlyInverse'737'_22 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → AgdaAny → T__'8801'__12 Source #
d_inverse'737''8658'surjective_24 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → AgdaAny → T_Σ_14 Source #
du_inverse'737''8658'surjective_24 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → AgdaAny → T_Σ_14 Source #
d_inverse'7495''8658'bijective_26 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
du_inverse'7495''8658'bijective_26 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
d_surjective'8658'strictlySurjective_34 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → AgdaAny → T_Σ_14 Source #
du_surjective'8658'strictlySurjective_34 ∷ (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → AgdaAny → T_Σ_14 Source #
d_strictlySurjective'8658'surjective_40 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → AgdaAny → T_Σ_14 Source #
du_strictlySurjective'8658'surjective_40 ∷ (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → AgdaAny → T_Σ_14 Source #
d_strictlyInverse'737''8658'inverse'737'_44 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_strictlyInverse'691''8658'inverse'691'_50 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #