Documentation

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

d_isPreorder_36 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_IsPreorder_70 Source #

du_isPreorder_36 ∷ T_Setoid_44 → T_IsPreorder_70 Source #

d_'8776''45'isPreorder_38 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_IsPreorder_70 Source #

du_'8776''45'isPreorder_38 ∷ T_Setoid_44 → T_IsPreorder_70 Source #

d_'8776''45'isPartialOrder_40 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_IsPartialOrder_174 Source #

du_'8776''45'isPartialOrder_40 ∷ T_Setoid_44 → T_IsPartialOrder_174 Source #

d_preorder_46 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Preorder_132 Source #

du_preorder_46 ∷ T_Setoid_44 → T_Preorder_132 Source #

d_'8776''45'preorder_48 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Preorder_132 Source #

du_'8776''45'preorder_48 ∷ T_Setoid_44 → T_Preorder_132 Source #

d_'8776''45'poset_50 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Poset_314 Source #

du_'8776''45'poset_50 ∷ T_Setoid_44 → T_Poset_314 Source #

d_'8777''45'sym_52 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #

d_'8777''45'resp'737'_56 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #

d_'8777''45'resp'691'_62 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #

d_'8777''45'resp'8322'_70 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Σ_14 Source #

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

d_'8777''45'irrefl_72 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → T_Irrelevant_20 Source #

d_'8776''894''8776''8658''8776'_78 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny Source #

du_'8776''894''8776''8658''8776'_78 ∷ T_Setoid_44 → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny Source #

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

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

d_resp'691''45'flip_82 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_resp'691''45'flip_82 ∷ T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_resp'737''45'flip_88 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_resp'737''45'flip_88 ∷ T_Setoid_44 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #