Documentation

d__'8592'__12 ∷ p → p → p → p → () Source #

newtype T__'8592'__12 Source #

d_app'45''8592'_24 ∷ T__'8592'__12 → AgdaAny → AgdaAny Source #

d__'8610'__36 ∷ p → p → p → p → () Source #

newtype T__'8610'__36 Source #

d_app'45''8610'_48 ∷ T__'8610'__36 → T_Injection_88 Source #

d_Kind_52 ∷ () Source #

data T_Kind_52 Source #

d__'8764''91'_'93'__74 ∷ T_Level_18 → T_Level_18 → () → T_Kind_52 → () → () Source #

d_Related_112 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → () → () → () Source #

d_'8596''8658'_130 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → () → () → T_Inverse_58 → AgdaAny Source #

du_'8596''8658'_130 ∷ T_Kind_52 → T_Inverse_58 → AgdaAny Source #

d_'8801''8658'_140 ∷ T_Kind_52 → T_Level_18 → () → () → T__'8801'__12 → AgdaAny Source #

du_'8801''8658'_140 ∷ T_Kind_52 → AgdaAny Source #

d_Symmetric'45'kind_142 ∷ () Source #

data T_Symmetric'45'kind_142 Source #

d_'8970'_'8971'_148 ∷ T_Symmetric'45'kind_142 → T_Kind_52 Source #

d_Forward'45'kind_150 ∷ () Source #

data T_Forward'45'kind_150 Source #

d_'8970'_'8971''8594'_164 ∷ T_Forward'45'kind_150 → T_Kind_52 Source #

d_'8658''8594'_176 ∷ T_Forward'45'kind_150 → T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du_'8658''8594'_176 ∷ T_Forward'45'kind_150 → AgdaAny → AgdaAny → AgdaAny Source #

d_Backward'45'kind_178 ∷ () Source #

data T_Backward'45'kind_178 Source #

d_'8970'_'8971''8592'_192 ∷ T_Backward'45'kind_178 → T_Kind_52 Source #

d_'8658''8592'_204 ∷ T_Backward'45'kind_178 → T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du_'8658''8592'_204 ∷ T_Backward'45'kind_178 → AgdaAny → AgdaAny → AgdaAny Source #

d_Equivalence'45'kind_206 ∷ () Source #

data T_Equivalence'45'kind_206 Source #

d_'8970'_'8971''8660'_216 ∷ T_Equivalence'45'kind_206 → T_Kind_52 Source #

d_'8658''8660'_228 ∷ T_Equivalence'45'kind_206 → T_Level_18 → T_Level_18 → () → () → AgdaAny → T_Equivalence_16 Source #

du_'8658''8660'_228 ∷ T_Equivalence'45'kind_206 → AgdaAny → T_Equivalence_16 Source #

d_'8660''8970'_'8971'_230 ∷ T_Symmetric'45'kind_142 → T_Equivalence'45'kind_206 Source #

d_'8594''8970'_'8971'_232 ∷ T_Equivalence'45'kind_206 → T_Forward'45'kind_150 Source #

d_'8592''8970'_'8971'_234 ∷ T_Equivalence'45'kind_206 → T_Backward'45'kind_178 Source #

d__op_236 ∷ T_Kind_52 → T_Kind_52 Source #

d_reverse_248 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny Source #

du_reverse_248 ∷ T_Kind_52 → AgdaAny → AgdaAny Source #

d_K'45'refl_254 ∷ T_Kind_52 → T_Level_18 → () → AgdaAny Source #

du_K'45'refl_254 ∷ T_Kind_52 → AgdaAny Source #

d_K'45'reflexive_260 ∷ T_Kind_52 → T_Level_18 → () → () → T__'8801'__12 → AgdaAny Source #

du_K'45'reflexive_260 ∷ T_Kind_52 → AgdaAny Source #

d_K'45'trans_270 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du_K'45'trans_270 ∷ T_Kind_52 → AgdaAny → AgdaAny → AgdaAny Source #

d_SK'45'sym_286 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny Source #

du_SK'45'sym_286 ∷ T_Symmetric'45'kind_142 → AgdaAny → AgdaAny Source #

d_SK'45'isEquivalence_292 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_IsEquivalence_26 Source #

du_SK'45'isEquivalence_292 ∷ T_Symmetric'45'kind_142 → T_IsEquivalence_26 Source #

d_SK'45'setoid_300 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Setoid_44 Source #

du_SK'45'setoid_300 ∷ T_Symmetric'45'kind_142 → T_Setoid_44 Source #

d_K'45'isPreorder_310 ∷ T_Kind_52 → T_Level_18 → T_IsPreorder_70 Source #

du_K'45'isPreorder_310 ∷ T_Kind_52 → T_IsPreorder_70 Source #

d_K'45'preorder_318 ∷ T_Kind_52 → T_Level_18 → T_Preorder_132 Source #

du_K'45'preorder_318 ∷ T_Kind_52 → T_Preorder_132 Source #

d__'8764''10216'_'10217'__340 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du__'8764''10216'_'10217'__340 ∷ T_Kind_52 → AgdaAny → AgdaAny → AgdaAny Source #

d__'8596''10216'_'10217'__360 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → T_Inverse_58 → AgdaAny → AgdaAny Source #

du__'8596''10216'_'10217'__360 ∷ T_Kind_52 → T_Inverse_58 → AgdaAny → AgdaAny Source #

d__'8596''10216''10217'__378 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny Source #

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

d__'8801''10216'_'10217'__396 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → () → () → () → T__'8801'__12 → AgdaAny → AgdaAny Source #

du__'8801''10216'_'10217'__396 ∷ T_Kind_52 → AgdaAny → AgdaAny Source #

d__'8718'_410 ∷ T_Kind_52 → T_Level_18 → () → AgdaAny Source #

du__'8718'_410 ∷ T_Kind_52 → AgdaAny Source #

d_sym_414 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Level_18 → () → () → AgdaAny → AgdaAny Source #

d_InducedRelation'8321'_422 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → AgdaAny → () Source #

d_InducedPreorder'8321'_438 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Preorder_132 Source #

du_InducedPreorder'8321'_438 ∷ T_Kind_52 → T_Preorder_132 Source #

d_InducedEquivalence'8321'_502 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Setoid_44 Source #

du_InducedEquivalence'8321'_502 ∷ T_Symmetric'45'kind_142 → T_Setoid_44 Source #

d_InducedRelation'8322'_518 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → () Source #

d_InducedPreorder'8322'_540 ∷ T_Kind_52 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → T_Preorder_132 Source #

du_InducedPreorder'8322'_540 ∷ T_Kind_52 → T_Preorder_132 Source #

d_InducedEquivalence'8322'_616 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → T_Setoid_44 Source #

du_InducedEquivalence'8322'_616 ∷ T_Symmetric'45'kind_142 → T_Setoid_44 Source #

d_preorder_654 ∷ T_Kind_52 → T_Level_18 → T_Preorder_132 Source #

d_setoid_656 ∷ T_Symmetric'45'kind_142 → T_Level_18 → T_Setoid_44 Source #