| 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 #
du_Σ'45''10230'_36 :: T_Func_714 -> (AgdaAny -> T_Func_714) -> T_Func_714 #
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 #
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 #
du_Σ'45''8611'_66 :: T_Inverse_1960 -> (AgdaAny -> T_Injection_776) -> T_Injection_776 #
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 #
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 #
du_from_88 :: T_Inverse_1960 -> AgdaAny -> AgdaAny #
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 #
du_to_98 :: T_Inverse_1960 -> AgdaAny -> AgdaAny #
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 #
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 #
du_from_130 :: T_Inverse_1960 -> AgdaAny -> AgdaAny #
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 #
du_to_140 :: T_Inverse_1960 -> AgdaAny -> AgdaAny #
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 #
du_g'8242'_144 :: T_Inverse_1960 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #
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 #
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 #
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 #
du_to'8242'_172 :: T_Inverse_1960 -> (AgdaAny -> T_Injection_776) -> T_Σ_14 -> T_Σ_14 #
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 #
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 #
du_Σ'45''8608'_210 :: T_Surjection_846 -> (AgdaAny -> T_Surjection_846) -> T_Surjection_846 #
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 #
du_to'8242'_228 :: T_Surjection_846 -> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14 #
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 #
du_backcast_232 :: AgdaAny -> AgdaAny #
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 #
du_to'8315''8242'_234 :: T_Surjection_846 -> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14 #
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 #
du_strictlySurjective'8242'_236 :: T_Surjection_846 -> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14 #
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 #
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 #
du_to'8242'_272 :: T_LeftInverse_1792 -> (AgdaAny -> T_LeftInverse_1792) -> T_Σ_14 -> T_Σ_14 #
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 #
du_backcast_276 :: AgdaAny -> AgdaAny #
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 #
du_from'8242'_278 :: T_LeftInverse_1792 -> (AgdaAny -> T_LeftInverse_1792) -> T_Σ_14 -> T_Σ_14 #
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 #
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 #
du_Σ'45''8596'_298 :: T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Inverse_1960 #
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 #
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 #
du_surjection'8242'_318 :: T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Surjection_846 #
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 #
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 #
du_swap'45'coercions_346 :: (AgdaAny -> ()) -> T_Kind_6 -> (AgdaAny -> ()) -> T_Inverse_1960 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #
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 #
du_cong_368 :: T_Kind_6 -> T_Inverse_1960 -> (AgdaAny -> AgdaAny) -> AgdaAny #