Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Function.Related.Propositional

Documentation

d_Kind_6 :: () #

data T_Kind_6 #

Constructors

C_implication_8
C_reverseImplication_10
C_equivalence_12
C_injection_14
C_reverseInjection_16
C_leftInverse_18
C_surjection_20
C_bijection_22

d__'8764''91'_'93'__40 :: T_Level_18 -> T_Level_18 -> () -> T_Kind_6 -> () -> () #

d_Related_74 :: T_Level_18 -> T_Level_18 -> T_Kind_6 -> () -> () -> () #

d_'8596''8658'_82 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Kind_6 -> T_Inverse_1960 -> AgdaAny #

du_'8596''8658'_82 :: T_Kind_6 -> T_Inverse_1960 -> AgdaAny #

d_'8801''8658'_84 :: T_Level_18 -> () -> () -> T_Kind_6 -> T__'8801'__12 -> AgdaAny #

du_'8801''8658'_84 :: T_Kind_6 -> AgdaAny #

d_SymmetricKind_86 :: () #

data T_SymmetricKind_86 #

Constructors

C_equivalence_88
C_bijection_90

d_'8970'_'8971'_92 :: T_SymmetricKind_86 -> T_Kind_6 #

d_ForwardKind_94 :: () #

data T_ForwardKind_94 #

Constructors

C_implication_96
C_equivalence_98
C_injection_100
C_leftInverse_102
C_surjection_104
C_bijection_106

d_'8970'_'8971''8594'_108 :: T_ForwardKind_94 -> T_Kind_6 #

d_'8658''8594'_112 :: T_Level_18 -> () -> T_Level_18 -> () -> T_ForwardKind_94 -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8658''8594'_112 :: T_ForwardKind_94 -> AgdaAny -> AgdaAny -> AgdaAny #

d_BackwardKind_114 :: () #

data T_BackwardKind_114 #

Constructors

C_reverseImplication_116
C_equivalence_118
C_reverseInjection_120
C_leftInverse_122
C_surjection_124
C_bijection_126

d_'8970'_'8971''8592'_128 :: T_BackwardKind_114 -> T_Kind_6 #

d_'8658''8592'_132 :: T_Level_18 -> () -> T_Level_18 -> () -> T_BackwardKind_114 -> AgdaAny -> AgdaAny -> AgdaAny #

du_'8658''8592'_132 :: T_BackwardKind_114 -> AgdaAny -> AgdaAny -> AgdaAny #

d_EquivalenceKind_134 :: () #

data T_EquivalenceKind_134 #

Constructors

C_equivalence_136
C_leftInverse_138
C_surjection_140
C_bijection_142

d_'8970'_'8971''8660'_144 :: T_EquivalenceKind_134 -> T_Kind_6 #

d_'8658''8660'_148 :: T_Level_18 -> () -> T_Level_18 -> () -> T_EquivalenceKind_134 -> AgdaAny -> T_Equivalence_1714 #

du_'8658''8660'_148 :: T_EquivalenceKind_134 -> AgdaAny -> T_Equivalence_1714 #

d_'8660''8970'_'8971'_150 :: T_SymmetricKind_86 -> T_EquivalenceKind_134 #

d_'8594''8970'_'8971'_152 :: T_EquivalenceKind_134 -> T_ForwardKind_94 #

d_'8592''8970'_'8971'_154 :: T_EquivalenceKind_134 -> T_BackwardKind_114 #

d__op_156 :: T_Kind_6 -> T_Kind_6 #

d_reverse_158 :: T_Level_18 -> () -> T_Kind_6 -> T_Level_18 -> () -> AgdaAny -> AgdaAny #

du_reverse_158 :: T_Kind_6 -> AgdaAny -> AgdaAny #

d_K'45'refl_160 :: T_Level_18 -> T_Kind_6 -> () -> AgdaAny #

du_K'45'refl_160 :: T_Kind_6 -> AgdaAny #

d_K'45'reflexive_162 :: T_Level_18 -> T_Kind_6 -> () -> () -> T__'8801'__12 -> AgdaAny #

du_K'45'reflexive_162 :: T_Kind_6 -> AgdaAny #

d_K'45'trans_164 :: T_Level_18 -> T_Level_18 -> T_Kind_6 -> T_Level_18 -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny #

du_K'45'trans_164 :: T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny #

d_SK'45'sym_168 :: T_Level_18 -> T_Level_18 -> T_SymmetricKind_86 -> () -> () -> AgdaAny -> AgdaAny #

du_SK'45'sym_168 :: T_SymmetricKind_86 -> AgdaAny -> AgdaAny #

d_SK'45'isEquivalence_172 :: T_Level_18 -> T_SymmetricKind_86 -> T_IsEquivalence_26 #

du_SK'45'isEquivalence_172 :: T_SymmetricKind_86 -> T_IsEquivalence_26 #

d_SK'45'setoid_178 :: T_SymmetricKind_86 -> T_Level_18 -> T_Setoid_44 #

du_SK'45'setoid_178 :: T_SymmetricKind_86 -> T_Setoid_44 #

d_K'45'isPreorder_186 :: T_Level_18 -> T_Kind_6 -> T_IsPreorder_70 #

du_K'45'isPreorder_186 :: T_Kind_6 -> T_IsPreorder_70 #

d_K'45'preorder_192 :: T_Kind_6 -> T_Level_18 -> T_Preorder_132 #

du_K'45'preorder_192 :: T_Kind_6 -> T_Preorder_132 #

d_begin__212 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> () -> () -> AgdaAny -> AgdaAny #

du_begin__212 :: () -> () -> AgdaAny -> AgdaAny #

d_step'45''8801'_216 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_step'45''8801'_216 :: () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_step'45''8801''45''8739'_218 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> () -> () -> AgdaAny -> AgdaAny #

du_step'45''8801''45''8739'_218 :: AgdaAny -> AgdaAny #

d_step'45''8801''45''10216'_220 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_step'45''8801''45''10216'_220 :: () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_step'45''8801''45''10217'_222 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_step'45''8801''45''10217'_222 :: () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_step'45''8801''728'_224 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_step'45''8801''728'_224 :: () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_rel1_236 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> () #

d_rel2_238 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> () #

d_step'45''8764'_242 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny #

du_step'45''8764'_242 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny #

d_step'45''10518'_246 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> () -> AgdaAny -> T_Bijection_926 -> AgdaAny #

du_step'45''10518'_246 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Bijection_926 -> AgdaAny #

d_step'45''11067'_248 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> () -> AgdaAny -> T_Bijection_926 -> AgdaAny #

du_step'45''11067'_248 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Bijection_926 -> AgdaAny #

d_step'45''8596''45''10216'_252 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> () -> AgdaAny -> T_Inverse_1960 -> AgdaAny #

du_step'45''8596''45''10216'_252 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Inverse_1960 -> AgdaAny #

d_step'45''8596''45''10217'_254 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> () -> () -> AgdaAny -> T_Inverse_1960 -> AgdaAny #

du_step'45''8596''45''10217'_254 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Inverse_1960 -> AgdaAny #

d__'8718'_264 :: T_Kind_6 -> T_Level_18 -> () -> AgdaAny #

du__'8718'_264 :: T_Kind_6 -> () -> AgdaAny #

d__'8596''10216''10217'__268 :: T_Kind_6 -> T_Level_18 -> T_Level_18 -> () -> () -> AgdaAny -> AgdaAny #

du__'8596''10216''10217'__268 :: AgdaAny -> AgdaAny #

d_InducedRelation'8321'_276 :: T_Level_18 -> () -> T_Level_18 -> T_Kind_6 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () #

d_InducedPreorder'8321'_288 :: T_Level_18 -> () -> T_Level_18 -> T_Kind_6 -> (AgdaAny -> ()) -> T_Preorder_132 #

du_InducedPreorder'8321'_288 :: T_Kind_6 -> T_Preorder_132 #

d_InducedEquivalence'8321'_362 :: T_Level_18 -> () -> T_Level_18 -> T_SymmetricKind_86 -> (AgdaAny -> ()) -> T_Setoid_44 #

du_InducedEquivalence'8321'_362 :: T_SymmetricKind_86 -> T_Setoid_44 #

d_InducedRelation'8322'_370 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Kind_6 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () #

d_InducedPreorder'8322'_384 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Kind_6 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Preorder_132 #

du_InducedPreorder'8322'_384 :: T_Kind_6 -> T_Preorder_132 #

d_InducedEquivalence'8322'_466 :: T_Level_18 -> () -> T_Level_18 -> () -> T_SymmetricKind_86 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Setoid_44 #

du_InducedEquivalence'8322'_466 :: T_SymmetricKind_86 -> T_Setoid_44 #