Documentation

d_Kind_6 ∷ () Source #

data T_Kind_6 Source #

d__'8764''91'_'93'__40 ∷ T_Level_18 → T_Level_18 → () → T_Kind_6 → () → () Source #

d_Related_74 ∷ T_Level_18 → T_Level_18 → T_Kind_6 → () → () → () Source #

d_'8596''8658'_82 ∷ T_Level_18 → () → T_Level_18 → () → T_Kind_6 → T_Inverse_2122 → AgdaAny Source #

du_'8596''8658'_82 ∷ T_Kind_6 → T_Inverse_2122 → AgdaAny Source #

d_'8801''8658'_84 ∷ T_Level_18 → () → () → T_Kind_6 → T__'8801'__12 → AgdaAny Source #

du_'8801''8658'_84 ∷ T_Kind_6 → AgdaAny Source #

d_SymmetricKind_86 ∷ () Source #

data T_SymmetricKind_86 Source #

d_'8970'_'8971'_92 ∷ T_SymmetricKind_86 → T_Kind_6 Source #

d_ForwardKind_94 ∷ () Source #

data T_ForwardKind_94 Source #

d_'8970'_'8971''8594'_108 ∷ T_ForwardKind_94 → T_Kind_6 Source #

d_'8658''8594'_112 ∷ T_Level_18 → () → T_Level_18 → () → T_ForwardKind_94 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8658''8594'_112 ∷ T_ForwardKind_94 → AgdaAny → AgdaAny → AgdaAny Source #

d_BackwardKind_114 ∷ () Source #

data T_BackwardKind_114 Source #

d_'8970'_'8971''8592'_128 ∷ T_BackwardKind_114 → T_Kind_6 Source #

d_'8658''8592'_132 ∷ T_Level_18 → () → T_Level_18 → () → T_BackwardKind_114 → AgdaAny → AgdaAny → AgdaAny Source #

du_'8658''8592'_132 ∷ T_BackwardKind_114 → AgdaAny → AgdaAny → AgdaAny Source #

d_EquivalenceKind_134 ∷ () Source #

data T_EquivalenceKind_134 Source #

d_'8970'_'8971''8660'_144 ∷ T_EquivalenceKind_134 → T_Kind_6 Source #

d_'8658''8660'_148 ∷ T_Level_18 → () → T_Level_18 → () → T_EquivalenceKind_134 → AgdaAny → T_Equivalence_1858 Source #

du_'8658''8660'_148 ∷ T_EquivalenceKind_134 → AgdaAny → T_Equivalence_1858 Source #

d_'8660''8970'_'8971'_150 ∷ T_SymmetricKind_86 → T_EquivalenceKind_134 Source #

d_'8594''8970'_'8971'_152 ∷ T_EquivalenceKind_134 → T_ForwardKind_94 Source #

d_'8592''8970'_'8971'_154 ∷ T_EquivalenceKind_134 → T_BackwardKind_114 Source #

d__op_156 ∷ T_Kind_6 → T_Kind_6 Source #

d_reverse_158 ∷ T_Level_18 → () → T_Kind_6 → T_Level_18 → () → AgdaAny → AgdaAny Source #

du_reverse_158 ∷ T_Kind_6 → AgdaAny → AgdaAny Source #

d_K'45'refl_160 ∷ T_Level_18 → T_Kind_6 → () → AgdaAny Source #

du_K'45'refl_160 ∷ T_Kind_6 → AgdaAny Source #

d_K'45'reflexive_162 ∷ T_Level_18 → T_Kind_6 → () → () → T__'8801'__12 → AgdaAny Source #

du_K'45'reflexive_162 ∷ T_Kind_6 → AgdaAny Source #

d_K'45'trans_164 ∷ T_Level_18 → T_Level_18 → T_Kind_6 → T_Level_18 → () → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du_K'45'trans_164 ∷ T_Kind_6 → AgdaAny → AgdaAny → AgdaAny Source #

d_SK'45'sym_168 ∷ T_Level_18 → T_Level_18 → T_SymmetricKind_86 → () → () → AgdaAny → AgdaAny Source #

du_SK'45'sym_168 ∷ T_SymmetricKind_86 → AgdaAny → AgdaAny Source #

d_SK'45'isEquivalence_172 ∷ T_Level_18 → T_SymmetricKind_86 → T_IsEquivalence_28 Source #

du_SK'45'isEquivalence_172 ∷ T_SymmetricKind_86 → T_IsEquivalence_28 Source #

d_SK'45'setoid_178 ∷ T_SymmetricKind_86 → T_Level_18 → T_Setoid_46 Source #

du_SK'45'setoid_178 ∷ T_SymmetricKind_86 → T_Setoid_46 Source #

d_K'45'isPreorder_186 ∷ T_Level_18 → T_Kind_6 → T_IsPreorder_76 Source #

du_K'45'isPreorder_186 ∷ T_Kind_6 → T_IsPreorder_76 Source #

d_K'45'preorder_192 ∷ T_Kind_6 → T_Level_18 → T_Preorder_142 Source #

du_K'45'preorder_192 ∷ T_Kind_6 → T_Preorder_142 Source #

d_begin__212 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny Source #

du_begin__212 ∷ () → () → AgdaAny → AgdaAny Source #

d_step'45''8801'_216 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_step'45''8801'_216 ∷ () → () → () → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_step'45''8801''45''8739'_218 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny Source #

du_step'45''8801''45''8739'_218 ∷ AgdaAny → AgdaAny Source #

d_step'45''8801''45''10216'_220 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_step'45''8801''45''10216'_220 ∷ () → () → () → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_step'45''8801''45''10217'_222 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_step'45''8801''45''10217'_222 ∷ () → () → () → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_step'45''8801''728'_224 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_step'45''8801''728'_224 ∷ () → () → () → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_rel1_236 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () Source #

d_rel2_238 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () Source #

d_step'45''8764'_242 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du_step'45''8764'_242 ∷ T_Kind_6 → () → () → () → AgdaAny → AgdaAny → AgdaAny Source #

d_step'45''10518'_246 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → T_Bijection_1004 → AgdaAny Source #

du_step'45''10518'_246 ∷ T_Kind_6 → () → () → () → AgdaAny → T_Bijection_1004 → AgdaAny Source #

d_step'45''11067'_248 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → T_Bijection_1004 → AgdaAny Source #

du_step'45''11067'_248 ∷ T_Kind_6 → () → () → () → AgdaAny → T_Bijection_1004 → AgdaAny Source #

d_step'45''8596''45''10216'_252 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → T_Inverse_2122 → AgdaAny Source #

du_step'45''8596''45''10216'_252 ∷ T_Kind_6 → () → () → () → AgdaAny → T_Inverse_2122 → AgdaAny Source #

d_step'45''8596''45''10217'_254 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → T_Inverse_2122 → AgdaAny Source #

du_step'45''8596''45''10217'_254 ∷ T_Kind_6 → () → () → () → AgdaAny → T_Inverse_2122 → AgdaAny Source #

d__'8718'_264 ∷ T_Kind_6 → T_Level_18 → () → AgdaAny Source #

du__'8718'_264 ∷ T_Kind_6 → () → AgdaAny Source #

d__'8596''10216''10217'__268 ∷ T_Kind_6 → T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny Source #

du__'8596''10216''10217'__268 ∷ AgdaAny → AgdaAny Source #

d_InducedRelation'8321'_276 ∷ T_Level_18 → () → T_Level_18 → T_Kind_6 → (AgdaAny → ()) → AgdaAny → AgdaAny → () Source #

d_InducedPreorder'8321'_288 ∷ T_Level_18 → () → T_Level_18 → T_Kind_6 → (AgdaAny → ()) → T_Preorder_142 Source #

du_InducedPreorder'8321'_288 ∷ T_Kind_6 → T_Preorder_142 Source #

d_InducedEquivalence'8321'_370 ∷ T_Level_18 → () → T_Level_18 → T_SymmetricKind_86 → (AgdaAny → ()) → T_Setoid_46 Source #

du_InducedEquivalence'8321'_370 ∷ T_SymmetricKind_86 → T_Setoid_46 Source #

d_InducedRelation'8322'_378 ∷ T_Level_18 → () → T_Level_18 → () → T_Kind_6 → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → () Source #

d_InducedPreorder'8322'_392 ∷ T_Level_18 → () → T_Level_18 → () → T_Kind_6 → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Preorder_142 Source #

du_InducedPreorder'8322'_392 ∷ T_Kind_6 → T_Preorder_142 Source #

d_InducedEquivalence'8322'_482 ∷ T_Level_18 → () → T_Level_18 → () → T_SymmetricKind_86 → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Setoid_46 Source #

du_InducedEquivalence'8322'_482 ∷ T_SymmetricKind_86 → T_Setoid_46 Source #