Documentation

d_isEquivalence_56 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsEquivalence_26 Source #

du_isEquivalence_56 :: T_IsEquivalence_26 -> T_IsEquivalence_26 Source #

d_isDecEquivalence_76 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 Source #

du_isDecEquivalence_76 :: T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 Source #

d_isPreorder_100 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_IsPreorder_70 Source #

du_isPreorder_100 :: T_IsPreorder_70 -> T_IsPreorder_70 Source #

d_isPartialOrder_136 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_162 -> T_IsPartialOrder_162 Source #

du_isPartialOrder_136 :: T_IsPartialOrder_162 -> T_IsPartialOrder_162 Source #

d_setoid_176 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 Source #

du_setoid_176 :: T_Setoid_44 -> T_Setoid_44 Source #

d_decSetoid_180 :: T_Level_14 -> T_Level_14 -> T_DecSetoid_84 -> T_DecSetoid_84 Source #

du_decSetoid_180 :: T_DecSetoid_84 -> T_DecSetoid_84 Source #

d_preorder_184 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Preorder_132 -> T_Preorder_132 Source #

du_preorder_184 :: T_Preorder_132 -> T_Preorder_132 Source #

d_poset_188 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Poset_282 -> T_Poset_282 Source #

du_poset_188 :: T_Poset_282 -> T_Poset_282 Source #

d_All'45'resp'45'Pointwise_194 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_All_44 -> T_All_44 Source #

du_All'45'resp'45'Pointwise_194 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_All_44 -> T_All_44 Source #

d_Any'45'resp'45'Pointwise_210 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Any_34 -> T_Any_34 Source #

du_Any'45'resp'45'Pointwise_210 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Any_34 -> T_Any_34 Source #

d_AllPairs'45'resp'45'Pointwise_228 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_AllPairs_20 -> T_AllPairs_20 Source #

du_AllPairs'45'resp'45'Pointwise_228 :: T_Σ_14 -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_AllPairs_20 -> T_AllPairs_20 Source #

d_Pointwise'45'length_244 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T__'8801'__12 Source #

d_tabulate'8314'_258 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> Integer -> (T_Fin_6 -> AgdaAny) -> (T_Fin_6 -> AgdaAny) -> (T_Fin_6 -> AgdaAny) -> T_Pointwise_48 Source #

du_tabulate'8314'_258 :: Integer -> (T_Fin_6 -> AgdaAny) -> T_Pointwise_48 Source #

d_tabulate'8315'_274 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> Integer -> (T_Fin_6 -> AgdaAny) -> (T_Fin_6 -> AgdaAny) -> T_Pointwise_48 -> T_Fin_6 -> AgdaAny Source #

du_tabulate'8315'_274 :: T_Pointwise_48 -> T_Fin_6 -> AgdaAny Source #

d_'43''43''8314'_290 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 Source #

du_'43''43''8314'_290 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 Source #

d_'43''43''45'cancel'737'_302 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 Source #

du_'43''43''45'cancel'737'_302 :: [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 Source #

d_'43''43''45'cancel'691'_316 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 Source #

du_'43''43''45'cancel'691'_316 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 Source #

d_concat'8314'_350 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [[AgdaAny]] -> [[AgdaAny]] -> T_Pointwise_48 -> T_Pointwise_48 Source #

du_concat'8314'_350 :: [[AgdaAny]] -> [[AgdaAny]] -> T_Pointwise_48 -> T_Pointwise_48 Source #

d_reverseAcc'8314'_356 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 Source #

du_reverseAcc'8314'_356 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 Source #

d_'691''43''43''8314'_366 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 Source #

du_'691''43''43''8314'_366 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 Source #

d_reverse'8314'_372 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 Source #

du_reverse'8314'_372 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 Source #

d_map'8314'_382 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Pointwise_48 -> T_Pointwise_48 Source #

du_map'8314'_382 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 Source #

d_map'8315'_404 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Pointwise_48 -> T_Pointwise_48 Source #

du_map'8315'_404 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 Source #

d_foldr'8314'_434 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_48 -> AgdaAny Source #

du_foldr'8314'_434 :: [AgdaAny] -> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T_Pointwise_48 -> AgdaAny Source #

d_filter'8314'_480 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T_Dec_32) -> (AgdaAny -> T_Dec_32) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 Source #

du_filter'8314'_480 :: (AgdaAny -> T_Dec_32) -> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 Source #

d_replicate'8314'_536 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> Integer -> T_Pointwise_48 Source #

du_replicate'8314'_536 :: AgdaAny -> Integer -> T_Pointwise_48 Source #

d_lookup'8315'_548 :: T_Level_14 -> () -> [AgdaAny] -> T_Level_14 -> () -> [AgdaAny] -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T__'8801'__12 -> (T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> AgdaAny) -> T_Pointwise_48 Source #

du_lookup'8315'_548 :: [AgdaAny] -> [AgdaAny] -> (T_Fin_6 -> T_Fin_6 -> T__'8801'__12 -> AgdaAny) -> T_Pointwise_48 Source #

d_lookup'8314'_560 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Fin_6 -> AgdaAny Source #

du_lookup'8314'_560 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Fin_6 -> AgdaAny Source #

d_Pointwise'45''8801''8658''8801'_568 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T__'8801'__12 Source #

d_'8801''8658'Pointwise'45''8801'_578 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> T__'8801'__12 -> T_Pointwise_48 Source #

du_'8801''8658'Pointwise'45''8801'_578 :: [AgdaAny] -> T_Pointwise_48 Source #

d_Pointwise'45''8801''8596''8801'_580 :: T_Level_14 -> () -> T_Inverse_58 Source #

du_Pointwise'45''8801''8596''8801'_580 :: T_Inverse_58 Source #

d_decidable'45''8801'_586 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Dec_32 Source #