| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Function.Consequences.Setoid
Documentation
d__'8776'__20 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → AgdaAny → AgdaAny → () Source #
d_Carrier_24 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → () Source #
d_contraInjective_70 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #
d_inverse'737''8658'surjective_72 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 Source #
du_inverse'737''8658'surjective_72 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 Source #
d_inverse'691''8658'injective_76 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_inverse'691''8658'injective_76 ∷ T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_inverse'7495''8658'bijective_80 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
du_inverse'7495''8658'bijective_80 ∷ T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
d_surjective'8658'strictlySurjective_82 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → AgdaAny → T_Σ_14 Source #
du_surjective'8658'strictlySurjective_82 ∷ T_Setoid_44 → (AgdaAny → T_Σ_14) → AgdaAny → T_Σ_14 Source #
d_strictlySurjective'8658'surjective_84 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → AgdaAny → T_Σ_14 Source #
du_strictlySurjective'8658'surjective_84 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → AgdaAny → T_Σ_14 Source #
d_inverse'737''8658'strictlyInverse'737'_86 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_inverse'737''8658'strictlyInverse'737'_86 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_strictlyInverse'737''8658'inverse'737'_88 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_strictlyInverse'737''8658'inverse'737'_88 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_inverse'691''8658'strictlyInverse'691'_90 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_inverse'691''8658'strictlyInverse'691'_90 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_strictlyInverse'691''8658'inverse'691'_92 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #