Documentation

d__'8771'__24 ∷ p → p → p → p → () Source #

data T__'8771'__24 Source #

d_to_46 ∷ T__'8771'__24 → AgdaAny → AgdaAny Source #

d_from_48 ∷ T__'8771'__24 → AgdaAny → AgdaAny Source #

d_left'45'inverse'45'of_52 ∷ T__'8771'__24 → AgdaAny → T__'8801'__12 Source #

d_right'45'inverse'45'of_56 ∷ T__'8771'__24 → AgdaAny → T__'8801'__12 Source #

d_left'45'right_60 ∷ T__'8771'__24 → AgdaAny → T__'8801'__12 Source #

d_injective_66 ∷ T_Level_18 → T_Level_18 → () → () → T__'8771'__24 → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_'8771''8658''8596'_80 ∷ T_Level_18 → () → T_Level_18 → () → T__'8771'__24 → T_Inverse_2122 Source #

du_'8771''8658''8596'_80 ∷ T__'8771'__24 → T_Inverse_2122 Source #

d_from_90 ∷ T__'8771'__24 → AgdaAny → AgdaAny Source #

d_injective_92 ∷ T_Level_18 → () → T_Level_18 → () → T__'8771'__24 → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_left'45'inverse'45'of_94 ∷ T__'8771'__24 → AgdaAny → T__'8801'__12 Source #

d_left'45'right_96 ∷ T__'8771'__24 → AgdaAny → T__'8801'__12 Source #

d_right'45'inverse'45'of_98 ∷ T__'8771'__24 → AgdaAny → T__'8801'__12 Source #

d_to_100 ∷ T__'8771'__24 → AgdaAny → AgdaAny Source #

d_'8596''8658''8771'_102 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T__'8771'__24 Source #

du_'8596''8658''8771'_102 ∷ T_Inverse_2122 → T__'8771'__24 Source #

d_strictlyInverse'691'_132 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → AgdaAny → T__'8801'__12 Source #

d_right'45'inverse'45'of_194 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → AgdaAny → T__'8801'__12 Source #

d_left'45'right_200 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → AgdaAny → T__'8801'__12 Source #

d_lemma_208 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → AgdaAny → T__'8801'__12 Source #