Documentation

d__'8777'__18 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → () Source #

d_isPreorder_38 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_IsPreorder_76 Source #

du_isPreorder_38 ∷ T_Setoid_46 → T_IsPreorder_76 Source #

d_'8776''45'isPreorder_40 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_IsPreorder_76 Source #

du_'8776''45'isPreorder_40 ∷ T_Setoid_46 → T_IsPreorder_76 Source #

d_'8776''45'isPartialOrder_42 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_IsPartialOrder_248 Source #

du_'8776''45'isPartialOrder_42 ∷ T_Setoid_46 → T_IsPartialOrder_248 Source #

d_preorder_48 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Preorder_142 Source #

du_preorder_48 ∷ T_Setoid_46 → T_Preorder_142 Source #

d_'8776''45'preorder_50 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Preorder_142 Source #

du_'8776''45'preorder_50 ∷ T_Setoid_46 → T_Preorder_142 Source #

d_'8776''45'poset_52 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Poset_492 Source #

du_'8776''45'poset_52 ∷ T_Setoid_46 → T_Poset_492 Source #

d_'8777''45'sym_54 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #

d_'8777''45'resp'737'_58 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #

d_'8777''45'resp'691'_64 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #

d_'8777''45'resp'8322'_72 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Σ_14 Source #

du_'8777''45'resp'8322'_72 ∷ T_Σ_14 Source #

d_'8777''45'irrefl_74 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → T_Irrelevant_20 Source #

d_'8776''894''8776''8658''8776'_80 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny Source #

du_'8776''894''8776''8658''8776'_80 ∷ T_Setoid_46 → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny Source #

d_'8776''8658''8776''894''8776'_82 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

du_'8776''8658''8776''894''8776'_82 ∷ T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 Source #

d_resp'691''45'flip_84 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_resp'691''45'flip_84 ∷ T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_resp'737''45'flip_90 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_resp'737''45'flip_90 ∷ T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #