Documentation

d__'8779'__28 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> () Source #

d__'60'__30 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> () Source #

d_'172''8804''45'this_40 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> (AgdaAny -> T_'8869'_4) -> (AgdaAny -> T_'8869'_4) -> T_Lex_32 -> T_'8869'_4 Source #

d_'172''8804''45'next_64 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> (AgdaAny -> T_'8869'_4) -> (T_Lex_32 -> T_'8869'_4) -> T_Lex_32 -> T_'8869'_4 Source #

d_antisymmetric_78 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4) -> [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48 Source #

du_antisymmetric_78 :: [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48 Source #

d_as_90 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48 Source #

du_as_90 :: [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48 Source #

d_toSum_124 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T__'8846'__30 Source #

du_toSum_124 :: T_Lex_32 -> T__'8846'__30 Source #

d_transitive_132 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Lex_32 Source #

du_transitive_132 :: T_IsEquivalence_26 -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Lex_32 Source #

d_trans_144 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Lex_32 Source #

du_trans_144 :: T_IsEquivalence_26 -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Lex_32 Source #

d_respects'8322'_180 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14 Source #

du_respects'8322'_180 :: T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14 Source #

d_resp'185'_200 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32 -> T_Lex_32 Source #

du_resp'185'_200 :: T_IsEquivalence_26 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32 -> T_Lex_32 Source #

d_resp'178'_218 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32 -> T_Lex_32 Source #

du_resp'178'_218 :: T_IsEquivalence_26 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32 -> T_Lex_32 Source #

d_'91''93''60''91''93''45''8660'_234 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Equivalence_928 Source #

du_'91''93''60''91''93''45''8660'_234 :: T_Equivalence_928 Source #

d_'8759''60''8759''45''8660'_248 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> T_Equivalence_928 Source #

du_'8759''60''8759''45''8660'_248 :: T_Equivalence_928 Source #

d_decidable_260 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Dec_32 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Dec_32 Source #

du_decidable_260 :: T_Dec_32 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> [AgdaAny] -> [AgdaAny] -> T_Dec_32 Source #