Documentation

d_Reflexive_26 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Sym_32 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Symmetric_38 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

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 -> ()) -> () #

d_RightTrans_56 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d_LeftTrans_62 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d_TransFlip_68 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Transitive_82 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Antisym_86 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Antisymmetric_98 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Irreflexive_104 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Asymmetric_114 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Dense_122 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Connex_132 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Total_142 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Tri_158 :: p -> p -> p -> p -> p -> p -> () #

data T_Tri_158 #

d_Trichotomous_190 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d__'62'__200 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () #

d_Max_206 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> () #

d_Maximum_214 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> () #

d_Min_216 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> () #

d_Minimum_220 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> () #

d_Cotransitive_222 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Tight_232 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Monotonic'8321'_242 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () #

d_Antitonic'8321'_250 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () #

d_Monotonic'8322'_258 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_MonotonicAntitonic_268 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_AntitonicMonotonic_278 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Antitonic'8322'_288 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Adjoint_298 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d__'10230'_Respects__312 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d__Respects__324 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d__Respects'691'__330 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d__Respects'737'__340 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d__Respects'8322'__348 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Substitutive_356 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () #

d_Irrelevant_366 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Recomputable_374 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Stable_382 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_WeaklyDecidable_390 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Decidable_398 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_DecidableEquality_408 :: T_Level_18 -> () -> () #

d_Universal_412 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_Empty_420 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #

d_NonEmpty_440 :: p -> p -> p -> p -> p -> p -> () #

data T_NonEmpty_440 #

d_x_454 :: T_NonEmpty_440 -> AgdaAny #

d_y_456 :: T_NonEmpty_440 -> AgdaAny #

d_proof_458 :: T_NonEmpty_440 -> AgdaAny #