Safe Haskell	None

MAlonzo.Code.Function.Related

Documentation

d__'8592'__20 :: p1 -> p2 -> p3 -> p4 -> () Source #

newtype T__'8592'__20 Source #

Constructors

C_lam_34 (AgdaAny -> AgdaAny)

d_app'45''8592'_32 :: T__'8592'__20 -> AgdaAny -> AgdaAny Source #

d__'8610'__44 :: p1 -> p2 -> p3 -> p4 -> () Source #

newtype T__'8610'__44 Source #

Constructors

C_lam_58 T_Injection_88

d_app'45''8610'_56 :: T__'8610'__44 -> T_Injection_88 Source #

d__'8764''91'_'93'__64 :: T_Level_14 -> T_Level_14 -> () -> T_Kind_6 -> () -> () Source #

d_toRelated_100 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Kind_6 -> AgdaAny -> AgdaAny Source #

d_fromRelated_138 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Kind_6 -> AgdaAny -> AgdaAny Source #

d_Related_220 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d_'8596''8658'_238 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> () -> () -> T_Inverse_58 -> AgdaAny Source #

du_'8596''8658'_238 :: T_Kind_6 -> T_Inverse_58 -> AgdaAny Source #

d_'8801''8658'_248 :: T_Kind_6 -> T_Level_14 -> () -> () -> T__'8801'__12 -> AgdaAny Source #

du_'8801''8658'_248 :: T_Kind_6 -> AgdaAny Source #

d_Symmetric'45'kind_250 :: () Source #

data T_Symmetric'45'kind_250 Source #

Constructors

C_equivalence_252
C_bijection_254

d_'8970'_'8971'_256 :: T_Symmetric'45'kind_250 -> T_Kind_6 Source #

d_Forward'45'kind_258 :: () Source #

data T_Forward'45'kind_258 Source #

Constructors

C_implication_260
C_equivalence_262
C_injection_264
C_left'45'inverse_266
C_surjection_268
C_bijection_270

d_'8970'_'8971''8594'_272 :: T_Forward'45'kind_258 -> T_Kind_6 Source #

d_'8658''8594'_284 :: T_Forward'45'kind_258 -> T_Level_14 -> T_Level_14 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8658''8594'_284 :: T_Forward'45'kind_258 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_Backward'45'kind_286 :: () Source #

data T_Backward'45'kind_286 Source #

Constructors

C_reverse'45'implication_288
C_equivalence_290
C_reverse'45'injection_292
C_left'45'inverse_294
C_surjection_296
C_bijection_298

d_'8970'_'8971''8592'_300 :: T_Backward'45'kind_286 -> T_Kind_6 Source #

d_'8658''8592'_312 :: T_Backward'45'kind_286 -> T_Level_14 -> T_Level_14 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_'8658''8592'_312 :: T_Backward'45'kind_286 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_Equivalence'45'kind_314 :: () Source #

data T_Equivalence'45'kind_314 Source #

Constructors

C_equivalence_316
C_left'45'inverse_318
C_surjection_320
C_bijection_322

d_'8970'_'8971''8660'_324 :: T_Equivalence'45'kind_314 -> T_Kind_6 Source #

d_'8658''8660'_336 :: T_Equivalence'45'kind_314 -> T_Level_14 -> T_Level_14 -> () -> () -> AgdaAny -> T_Equivalence_16 Source #

du_'8658''8660'_336 :: T_Equivalence'45'kind_314 -> AgdaAny -> T_Equivalence_16 Source #

d_'8660''8970'_'8971'_338 :: T_Symmetric'45'kind_250 -> T_Equivalence'45'kind_314 Source #

d_'8594''8970'_'8971'_340 :: T_Equivalence'45'kind_314 -> T_Forward'45'kind_258 Source #

d_'8592''8970'_'8971'_342 :: T_Equivalence'45'kind_314 -> T_Backward'45'kind_286 Source #

d__op_344 :: T_Kind_6 -> T_Kind_6 Source #

d_reverse_356 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> () -> () -> AgdaAny -> AgdaAny Source #

du_reverse_356 :: T_Kind_6 -> AgdaAny -> AgdaAny Source #

d_K'45'refl_362 :: T_Kind_6 -> T_Level_14 -> () -> AgdaAny Source #

du_K'45'refl_362 :: T_Kind_6 -> AgdaAny Source #

d_K'45'reflexive_368 :: T_Kind_6 -> T_Level_14 -> () -> () -> T__'8801'__12 -> AgdaAny Source #

du_K'45'reflexive_368 :: T_Kind_6 -> AgdaAny Source #

d_K'45'trans_378 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_K'45'trans_378 :: T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_SK'45'sym_394 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Level_14 -> () -> () -> AgdaAny -> AgdaAny Source #

du_SK'45'sym_394 :: T_Symmetric'45'kind_250 -> AgdaAny -> AgdaAny Source #

d_SK'45'isEquivalence_400 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_IsEquivalence_26 Source #

du_SK'45'isEquivalence_400 :: T_Symmetric'45'kind_250 -> T_IsEquivalence_26 Source #

d_SK'45'setoid_408 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Setoid_44 Source #

du_SK'45'setoid_408 :: T_Symmetric'45'kind_250 -> T_Setoid_44 Source #

d_K'45'isPreorder_418 :: T_Kind_6 -> T_Level_14 -> T_IsPreorder_70 Source #

du_K'45'isPreorder_418 :: T_Kind_6 -> T_IsPreorder_70 Source #

d_K'45'preorder_426 :: T_Kind_6 -> T_Level_14 -> T_Preorder_132 Source #

du_K'45'preorder_426 :: T_Kind_6 -> T_Preorder_132 Source #

d__'8764''10216'_'10217'__448 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'8764''10216'_'10217'__448 :: T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8596''10216'_'10217'__468 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> T_Inverse_58 -> AgdaAny -> AgdaAny Source #

du__'8596''10216'_'10217'__468 :: T_Kind_6 -> T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d__'8596''10216''10217'__486 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> () -> () -> AgdaAny -> AgdaAny Source #

du__'8596''10216''10217'__486 :: AgdaAny -> AgdaAny Source #

d__'8801''10216'_'10217'__504 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> () -> () -> () -> T__'8801'__12 -> AgdaAny -> AgdaAny Source #

du__'8801''10216'_'10217'__504 :: T_Kind_6 -> AgdaAny -> AgdaAny Source #

d__'8718'_518 :: T_Kind_6 -> T_Level_14 -> () -> AgdaAny Source #

du__'8718'_518 :: T_Kind_6 -> AgdaAny Source #

d_InducedRelation'8321'_528 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () Source #

d_InducedPreorder'8321'_544 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> T_Preorder_132 Source #

du_InducedPreorder'8321'_544 :: T_Kind_6 -> T_Preorder_132 Source #

d_InducedEquivalence'8321'_608 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> T_Setoid_44 Source #

du_InducedEquivalence'8321'_608 :: T_Symmetric'45'kind_250 -> T_Setoid_44 Source #

d_InducedRelation'8322'_624 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () Source #

d_InducedPreorder'8322'_646 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Preorder_132 Source #

du_InducedPreorder'8322'_646 :: T_Kind_6 -> T_Preorder_132 Source #

d_InducedEquivalence'8322'_722 :: T_Symmetric'45'kind_250 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Setoid_44 Source #

du_InducedEquivalence'8322'_722 :: T_Symmetric'45'kind_250 -> T_Setoid_44 Source #