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'_78 ∷ T_Level_18 → () → T_Level_18 → () → T__'8771'__24 → T_Inverse_1960 Source #

du_'8771''8658''8596'_78 ∷ T__'8771'__24 → T_Inverse_1960 Source #

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

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

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

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

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

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

d_'8596''8658''8771'_100 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T__'8771'__24 Source #

du_'8596''8658''8771'_100 ∷ T_Inverse_1960 → T__'8771'__24 Source #

d_strictlyInverse'691'_130 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → AgdaAny → T__'8801'__12 Source #

d_right'45'inverse'45'of_188 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → AgdaAny → T__'8801'__12 Source #

d_left'45'right_194 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → AgdaAny → T__'8801'__12 Source #

d_lemma_202 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → AgdaAny → T__'8801'__12 Source #