| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algebra.Construct.LiftedChoice
Documentation
d_Lift_30 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_Level_18 → () → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_Lift_30 ∷ (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d__'9702'__132 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du__'9702'__132 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_sel'45''8801'_134 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_sel'45''8801'_134 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_distrib_156 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_distrib_156 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d__'9702'__190 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du__'9702'__190 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_sel_192 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_sel_192 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_idem_198 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → AgdaAny → AgdaAny Source #
du_idem_198 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → AgdaAny → AgdaAny Source #
d__'9702'__216 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du__'9702'__216 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_cong_218 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_cong_218 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc_310 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_assoc_310 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_comm_320 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_comm_320 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d__'9702'__360 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → AgdaAny → AgdaAny → AgdaAny Source #
du__'9702'__360 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_isMagma_362 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → T_IsMagma_86 Source #
du_isMagma_362 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → T_IsMagma_86 Source #
d_isSemigroup_368 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 Source #
du_isSemigroup_368 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_194 Source #
d_isBand_376 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 Source #
du_isBand_376 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsBand_230 Source #
d_isSemilattice_380 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 Source #
du_isSemilattice_380 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemilattice_312 Source #
d_isSelectiveMagma_390 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → T_IsSelectiveMagma_158 Source #
du_isSelectiveMagma_390 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → T_IsSelectiveMagma_158 Source #
d__'9702'__404 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du__'9702'__404 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_preserves'7506'_418 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 → AgdaAny Source #
du_preserves'7506'_418 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 → AgdaAny Source #
d_preserves'691'_500 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_preserves'691'_500 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_preserves'7495'_538 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_preserves'7495'_538 ∷ T_IsSelectiveMagma_158 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_forces'7495'_580 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_158 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #