| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.Product.Function.Dependent.Propositional
Documentation
d_'8660'_36 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Equivalence_16 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Equivalence_16 Source #
du_'8660'_36 ∷ T_Equivalence_16 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Equivalence_16 Source #
d_'8660''45''8608'_52 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Surjection_54 → (AgdaAny → T_Equivalence_16) → T_Equivalence_16 Source #
d_'8611'_70 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → T_Injection_88 Source #
d_A'8321''8771'A'8322'_80 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → T__'8771'__12 Source #
d_from_84 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → AgdaAny → AgdaAny Source #
du_from_84 ∷ T_Inverse_58 → AgdaAny → AgdaAny Source #
d_to_96 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → AgdaAny → AgdaAny Source #
d_subst'45'application'8242'_110 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → T__'8801'__12 Source #
d_from_128 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → AgdaAny Source #
du_from_128 ∷ T_Inverse_58 → AgdaAny → AgdaAny Source #
d_to_140 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → AgdaAny Source #
d_g'8242'_144 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → AgdaAny → AgdaAny Source #
du_g'8242'_144 ∷ T_Inverse_58 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_g'8242''45'lemma_152 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → AgdaAny → T__'8801'__12 Source #
d_lemma_168 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_to_172 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → T_Σ_14 → T_Σ_14 Source #
du_to_172 ∷ T_Inverse_58 → (AgdaAny → T_Injection_88) → T_Σ_14 → T_Σ_14 Source #
d_to'45'injective_176 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Injection_88) → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T__'8801'__12 Source #
d_'8606'_214 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_LeftInverse_82 → (AgdaAny → T_LeftInverse_82) → T_LeftInverse_82 Source #
d_from_224 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_LeftInverse_82 → (AgdaAny → T_LeftInverse_82) → T_Σ_14 → T_Σ_14 Source #
du_from_224 ∷ T_LeftInverse_82 → (AgdaAny → T_LeftInverse_82) → T_Σ_14 → T_Σ_14 Source #
d_to_230 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_LeftInverse_82 → (AgdaAny → T_LeftInverse_82) → T_Σ_14 → T_Σ_14 Source #
du_to_230 ∷ T_LeftInverse_82 → (AgdaAny → T_LeftInverse_82) → T_Σ_14 → T_Σ_14 Source #
d_left'45'inverse'45'of_240 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_LeftInverse_82 → (AgdaAny → T_LeftInverse_82) → T_Σ_14 → T__'8801'__12 Source #
d_'8608'_250 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Surjection_54 → (AgdaAny → T_Surjection_54) → T_Surjection_54 Source #
d_to_260 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Surjection_54 → (AgdaAny → T_Surjection_54) → T_Σ_14 → T_Σ_14 Source #
du_to_260 ∷ T_Surjection_54 → (AgdaAny → T_Surjection_54) → T_Σ_14 → T_Σ_14 Source #
d_from_266 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Surjection_54 → (AgdaAny → T_Surjection_54) → T_Σ_14 → T_Σ_14 Source #
du_from_266 ∷ T_Surjection_54 → (AgdaAny → T_Surjection_54) → T_Σ_14 → T_Σ_14 Source #
d_right'45'inverse'45'of_276 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Surjection_54 → (AgdaAny → T_Surjection_54) → T_Σ_14 → T__'8801'__12 Source #
d_'8596'_286 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Inverse_58) → T_Inverse_58 Source #
du_'8596'_286 ∷ T_Inverse_58 → (AgdaAny → T_Inverse_58) → T_Inverse_58 Source #
d_A'8321''8771'A'8322'_296 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Inverse_58) → T__'8771'__12 Source #
d_surjection'8242'_298 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Inverse_58) → T_Surjection_54 Source #
d_left'45'inverse'45'of_302 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → T_Inverse_58) → T_Σ_14 → T__'8801'__12 Source #
d_swap'45'coercions_344 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_swap'45'coercions_344 ∷ T_Kind_52 → T_Inverse_58 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_cong_384 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → ()) → (AgdaAny → ()) → T_Inverse_58 → (AgdaAny → AgdaAny) → AgdaAny Source #
du_cong_384 ∷ T_Kind_52 → T_Inverse_58 → (AgdaAny → AgdaAny) → AgdaAny Source #