| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.Product.Function.Dependent.Propositional
Documentation
d_Σ'45''10230'_36 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Func_774 → (AgdaAny → T_Func_774) → T_Func_774 Source #
du_Σ'45''10230'_36 ∷ T_Func_774 → (AgdaAny → T_Func_774) → T_Func_774 Source #
d_Σ'45''8660'_50 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Surjection_918 → (AgdaAny → T_Equivalence_1858) → T_Equivalence_1858 Source #
d_Σ'45''8611'_66 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → T_Injection_842 Source #
d_I'8771'J_84 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → T__'8771'__24 Source #
d_from_88 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → AgdaAny → AgdaAny Source #
d_to_98 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → AgdaAny → AgdaAny Source #
d_subst'45'application'8242'_112 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → T__'8801'__12 Source #
d_from_130 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → AgdaAny Source #
d_to_140 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → 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 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → AgdaAny → AgdaAny Source #
du_g'8242'_144 ∷ T_Inverse_2122 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_g'8242''45'lemma_152 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → 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 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_to'8242'_172 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → T_Σ_14 → T_Σ_14 Source #
du_to'8242'_172 ∷ T_Inverse_2122 → (AgdaAny → T_Injection_842) → T_Σ_14 → T_Σ_14 Source #
d_to'45'injective_174 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Injection_842) → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T__'8801'__12 Source #
d_Σ'45''8608'_210 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Surjection_918 → (AgdaAny → T_Surjection_918) → T_Surjection_918 Source #
d_to'8242'_228 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Surjection_918 → (AgdaAny → T_Surjection_918) → T_Σ_14 → T_Σ_14 Source #
du_to'8242'_228 ∷ T_Surjection_918 → (AgdaAny → T_Surjection_918) → T_Σ_14 → T_Σ_14 Source #
d_backcast_232 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Surjection_918 → (AgdaAny → T_Surjection_918) → AgdaAny → AgdaAny → AgdaAny Source #
d_to'8315''8242'_234 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Surjection_918 → (AgdaAny → T_Surjection_918) → T_Σ_14 → T_Σ_14 Source #
d_strictlySurjective'8242'_236 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Surjection_918 → (AgdaAny → T_Surjection_918) → T_Σ_14 → T_Σ_14 Source #
du_strictlySurjective'8242'_236 ∷ T_Surjection_918 → (AgdaAny → T_Surjection_918) → T_Σ_14 → T_Σ_14 Source #
d_Σ'45''8617'_254 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_LeftInverse_1942 → (AgdaAny → T_LeftInverse_1942) → T_LeftInverse_1942 Source #
du_Σ'45''8617'_254 ∷ T_LeftInverse_1942 → (AgdaAny → T_LeftInverse_1942) → T_LeftInverse_1942 Source #
d_to'8242'_272 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_LeftInverse_1942 → (AgdaAny → T_LeftInverse_1942) → T_Σ_14 → T_Σ_14 Source #
d_backcast_276 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_LeftInverse_1942 → (AgdaAny → T_LeftInverse_1942) → AgdaAny → AgdaAny → AgdaAny Source #
d_from'8242'_278 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_LeftInverse_1942 → (AgdaAny → T_LeftInverse_1942) → T_Σ_14 → T_Σ_14 Source #
d_inv_280 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_LeftInverse_1942 → (AgdaAny → T_LeftInverse_1942) → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T__'8801'__12 Source #
d_Σ'45''8618'_298 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_RightInverse_2036 → (AgdaAny → T_RightInverse_2036) → T_RightInverse_2036 Source #
du_Σ'45''8618'_298 ∷ T_RightInverse_2036 → (AgdaAny → T_RightInverse_2036) → T_RightInverse_2036 Source #
d_Σ'45''8596'_312 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Inverse_2122) → T_Inverse_2122 Source #
d_I'8771'J_330 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Inverse_2122) → T__'8771'__24 Source #
d_surjection'8242'_332 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Inverse_2122) → T_Surjection_918 Source #
d_left'45'inverse'45'of_336 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → T_Inverse_2122) → T_Σ_14 → T__'8801'__12 Source #
d_swap'45'coercions_360 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Kind_6 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_swap'45'coercions_360 ∷ (AgdaAny → ()) → T_Kind_6 → (AgdaAny → ()) → T_Inverse_2122 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_cong_382 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Kind_6 → T_Inverse_2122 → (AgdaAny → AgdaAny) → AgdaAny Source #
du_cong_382 ∷ T_Kind_6 → T_Inverse_2122 → (AgdaAny → AgdaAny) → AgdaAny Source #
d_cong'737'_426 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Kind_6 → (AgdaAny → AgdaAny) → AgdaAny Source #