Documentation

d_Reflexive_26 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_Sym_32 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d_Symmetric_38 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_Trans_42 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d_TransFlip_56 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d_Transitive_70 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_Antisym_74 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d_Antisymmetric_86 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d_Irreflexive_92 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d_Asymmetric_102 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_Connex_110 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d_Total_120 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_Tri_136 ∷ p → p → p → p → p → p → () Source #

data T_Tri_136 Source #

d_Trichotomous_168 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d__'62'__178 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → () Source #

d_Max_184 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → () Source #

d_Maximum_192 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → () Source #

d_Min_194 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → () Source #

d_Minimum_198 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → () Source #

d__'10230'_Respects__200 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d__Respects__212 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d__Respects'691'__218 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d__Respects'737'__228 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d__Respects'8322'__236 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #

d_Substitutive_244 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () Source #

d_Decidable_254 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_WeaklyDecidable_262 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_DecidableEquality_272 ∷ T_Level_18 → () → () Source #

d_Irrelevant_276 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_Recomputable_288 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_Universal_296 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_NonEmpty_316 ∷ p → p → p → p → p → p → () Source #

data T_NonEmpty_316 Source #

d_x_330 ∷ T_NonEmpty_316 → AgdaAny Source #

d_y_332 ∷ T_NonEmpty_316 → AgdaAny Source #

d_proof_334 ∷ T_NonEmpty_316 → AgdaAny Source #

d_Conn_338 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → () Source #