Documentation

d__'215''45''8660'__30 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → () → T_Equivalence_16 → T_Equivalence_16 → T_Equivalence_16 Source #

du__'215''45''8660'__30 ∷ T_Equivalence_16 → T_Equivalence_16 → T_Equivalence_16 Source #

d__'215''45''8611'__40 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → () → T_Injection_88 → T_Injection_88 → T_Injection_88 Source #

du__'215''45''8611'__40 ∷ T_Injection_88 → T_Injection_88 → T_Injection_88 Source #

d__'215''45''8606'__50 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → () → T_LeftInverse_82 → T_LeftInverse_82 → T_LeftInverse_82 Source #

du__'215''45''8606'__50 ∷ T_LeftInverse_82 → T_LeftInverse_82 → T_LeftInverse_82 Source #

d__'215''45''8608'__60 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → () → T_Surjection_54 → T_Surjection_54 → T_Surjection_54 Source #

du__'215''45''8608'__60 ∷ T_Surjection_54 → T_Surjection_54 → T_Surjection_54 Source #

d__'215''45''8596'__70 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → () → T_Inverse_58 → T_Inverse_58 → T_Inverse_58 Source #

du__'215''45''8596'__70 ∷ T_Inverse_58 → T_Inverse_58 → T_Inverse_58 Source #

d__'215''45'cong__102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → () → () → T_Kind_52 → AgdaAny → AgdaAny → AgdaAny Source #

du__'215''45'cong__102 ∷ T_Kind_52 → AgdaAny → AgdaAny → AgdaAny Source #