Documentation

d__'8776'__44 ∷ T_GeneralizeTel_487 → T_Equivalence_1858 → AgdaAny → AgdaAny → () Source #

d__'8776'__70 ∷ T_GeneralizeTel_487 → T_Equivalence_1858 → AgdaAny → AgdaAny → () Source #

d_mkRightInverse_94 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Equivalence_1858 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_RightInverse_2036 Source #

du_mkRightInverse_94 ∷ T_Equivalence_1858 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_RightInverse_2036 Source #

d_RightInverse'8658'LeftInverse_172 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_RightInverse_2036 → T_LeftInverse_1942 Source #

du_RightInverse'8658'LeftInverse_172 ∷ T_RightInverse_2036 → T_LeftInverse_1942 Source #

d_LeftInverse'8658'RightInverse_252 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_LeftInverse_1942 → T_RightInverse_2036 Source #

du_LeftInverse'8658'RightInverse_252 ∷ T_LeftInverse_1942 → T_RightInverse_2036 Source #

d_RightInverse'8658'Surjection_338 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_RightInverse_2036 → T_Surjection_918 Source #

du_RightInverse'8658'Surjection_338 ∷ T_RightInverse_2036 → T_Surjection_918 Source #

d_'8618''8658''8608'_418 ∷ T_Level_18 → () → T_Level_18 → () → T_RightInverse_2036 → T_Surjection_918 Source #

du_'8618''8658''8608'_418 ∷ T_RightInverse_2036 → T_Surjection_918 Source #

d_'8618''8658''8617'_420 ∷ T_Level_18 → () → T_Level_18 → () → T_RightInverse_2036 → T_LeftInverse_1942 Source #

du_'8618''8658''8617'_420 ∷ T_RightInverse_2036 → T_LeftInverse_1942 Source #

d_'8617''8658''8618'_422 ∷ T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1942 → T_RightInverse_2036 Source #

du_'8617''8658''8618'_422 ∷ T_LeftInverse_1942 → T_RightInverse_2036 Source #

d__'8776'__456 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → () Source #

d_'46'generalizedField'45'S'46'a_475 ∷ T_GeneralizeTel_487 → T_Level_18 Source #

d_'46'generalizedField'45'S'46'ℓ'8321'_477 ∷ T_GeneralizeTel_487 → T_Level_18 Source #

d_'46'generalizedField'45'S_479 ∷ T_GeneralizeTel_487 → T_Setoid_46 Source #

d_'46'generalizedField'45'T'46'a_481 ∷ T_GeneralizeTel_487 → T_Level_18 Source #

d__'8776'__482 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → () Source #

d_'46'generalizedField'45'T'46'ℓ'8321'_483 ∷ T_GeneralizeTel_487 → T_Level_18 Source #

d_'46'generalizedField'45'T_485 ∷ T_GeneralizeTel_487 → T_Setoid_46 Source #

d_GeneralizeTel_487 ∷ () Source #

data T_GeneralizeTel_487 Source #

d_to'45'from_510 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_510 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #