| 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_714 → (AgdaAny → T_Func_714) → T_Func_714 Source #
du_Σ'45''10230'_36 ∷ T_Func_714 → (AgdaAny → T_Func_714) → T_Func_714 Source #
d_Σ'45''8660'_50 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Surjection_846 → (AgdaAny → T_Equivalence_1714) → T_Equivalence_1714 Source #
d_Σ'45''8611'_66 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_1960 → (AgdaAny → T_Injection_776) → T_Injection_776 Source #
d_I'8771'J_84 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_1960 → (AgdaAny → T_Injection_776) → T__'8771'__24 Source #
d_from_88 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_1960 → (AgdaAny → T_Injection_776) → AgdaAny → AgdaAny Source #
d_to_98 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_1960 → (AgdaAny → T_Injection_776) → 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_1960 → (AgdaAny → T_Injection_776) → 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_1960 → (AgdaAny → T_Injection_776) → 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_1960 → (AgdaAny → T_Injection_776) → 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_1960 → (AgdaAny → T_Injection_776) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → AgdaAny → AgdaAny Source #
du_g'8242'_144 ∷ T_Inverse_1960 → (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_1960 → (AgdaAny → T_Injection_776) → 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_1960 → (AgdaAny → T_Injection_776) → 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_1960 → (AgdaAny → T_Injection_776) → T_Σ_14 → T_Σ_14 Source #
du_to'8242'_172 ∷ T_Inverse_1960 → (AgdaAny → T_Injection_776) → 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_1960 → (AgdaAny → T_Injection_776) → 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_846 → (AgdaAny → T_Surjection_846) → T_Surjection_846 Source #
d_to'8242'_228 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Surjection_846 → (AgdaAny → T_Surjection_846) → T_Σ_14 → T_Σ_14 Source #
du_to'8242'_228 ∷ T_Surjection_846 → (AgdaAny → T_Surjection_846) → T_Σ_14 → T_Σ_14 Source #
d_backcast_232 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Surjection_846 → (AgdaAny → T_Surjection_846) → 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_846 → (AgdaAny → T_Surjection_846) → 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_846 → (AgdaAny → T_Surjection_846) → T_Σ_14 → T_Σ_14 Source #
du_strictlySurjective'8242'_236 ∷ T_Surjection_846 → (AgdaAny → T_Surjection_846) → 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_1792 → (AgdaAny → T_LeftInverse_1792) → T_LeftInverse_1792 Source #
du_Σ'45''8617'_254 ∷ T_LeftInverse_1792 → (AgdaAny → T_LeftInverse_1792) → T_LeftInverse_1792 Source #
d_to'8242'_272 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_LeftInverse_1792 → (AgdaAny → T_LeftInverse_1792) → T_Σ_14 → T_Σ_14 Source #
d_backcast_276 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_LeftInverse_1792 → (AgdaAny → T_LeftInverse_1792) → AgdaAny → AgdaAny → AgdaAny Source #
d_from'8242'_278 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_LeftInverse_1792 → (AgdaAny → T_LeftInverse_1792) → T_Σ_14 → T_Σ_14 Source #
d_inv_280 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_LeftInverse_1792 → (AgdaAny → T_LeftInverse_1792) → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T__'8801'__12 Source #
d_Σ'45''8596'_298 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_1960 → (AgdaAny → T_Inverse_1960) → T_Inverse_1960 Source #
d_I'8771'J_316 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_1960 → (AgdaAny → T_Inverse_1960) → T__'8771'__24 Source #
d_surjection'8242'_318 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_1960 → (AgdaAny → T_Inverse_1960) → T_Surjection_846 Source #
d_left'45'inverse'45'of_322 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Inverse_1960 → (AgdaAny → T_Inverse_1960) → T_Σ_14 → T__'8801'__12 Source #
d_swap'45'coercions_346 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Kind_6 → (AgdaAny → ()) → T_Inverse_1960 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_swap'45'coercions_346 ∷ (AgdaAny → ()) → T_Kind_6 → (AgdaAny → ()) → T_Inverse_1960 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_cong_368 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Kind_6 → T_Inverse_1960 → (AgdaAny → AgdaAny) → AgdaAny Source #
du_cong_368 ∷ T_Kind_6 → T_Inverse_1960 → (AgdaAny → AgdaAny) → AgdaAny Source #