| 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'__128 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du__'9702'__128 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_sel'45''8801'_130 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_sel'45''8801'_130 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_distrib_152 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_distrib_152 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d__'9702'__186 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du__'9702'__186 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_sel_188 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_sel_188 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_idem_194 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → AgdaAny → AgdaAny Source #
du_idem_194 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → AgdaAny → AgdaAny Source #
d__'9702'__212 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du__'9702'__212 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_cong_214 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → 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_214 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc_306 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_assoc_306 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_comm_316 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_comm_316 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d__'9702'__356 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → AgdaAny → AgdaAny → AgdaAny Source #
du__'9702'__356 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_isMagma_358 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → T_IsMagma_176 Source #
du_isMagma_358 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → T_IsMagma_176 Source #
d_isSemigroup_362 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 Source #
du_isSemigroup_362 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 Source #
d_isBand_368 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 Source #
du_isBand_368 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 Source #
d_isSelectiveMagma_372 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → T_IsSelectiveMagma_436 Source #
du_isSelectiveMagma_372 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → T_IsSelectiveMagma_436 Source #
d__'9702'__386 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du__'9702'__386 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_preserves'7506'_400 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → 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'_400 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 → AgdaAny Source #
d_preserves'691'_482 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_preserves'691'_482 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_preserves'7495'_520 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_preserves'7495'_520 ∷ T_IsSelectiveMagma_436 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_forces'7495'_562 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSelectiveMagma_436 → 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 #