Documentation

d_'44''45'injective'737'_34 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_'44''45'injective'691''45''8801'_46 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12) → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'44''45'injective'691''45'UIP_62 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12) → T__'8801'__12 → T__'8801'__12 Source #

d_'8801''45'dec_70 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → AgdaAny → T_Dec_32) → T_Σ_14 → T_Σ_14 → T_Dec_32 Source #

du_'8801''45'dec_70 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → AgdaAny → T_Dec_32) → T_Σ_14 → T_Σ_14 → T_Dec_32 Source #

d_'44''45'injective'691'_124 ∷ T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_'44''45'injective_134 ∷ T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T_Σ_14 Source #

du_'44''45'injective_134 ∷ T_Σ_14 Source #

d_swap'45'involutive_136 ∷ T_Level_18 → () → T_Level_18 → () → T_Σ_14 → T__'8801'__12 Source #

d_Σ'45''8801''44''8801''8596''8801'_156 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Inverse_1048 Source #

du_Σ'45''8801''44''8801''8596''8801'_156 ∷ T_Inverse_1048 Source #

d_to_180 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_from_196 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T_Σ_14 Source #

du_from_196 ∷ T_Σ_14 Source #

d_left'45'inverse'45'of_214 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_right'45'inverse'45'of_222 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T__'8801'__12 Source #

d_'215''45''8801''44''8801''8596''8801'_236 ∷ T_Level_18 → () → T_Level_18 → () → T_Σ_14 → T_Σ_14 → T_Inverse_1048 Source #

du_'215''45''8801''44''8801''8596''8801'_236 ∷ T_Inverse_1048 Source #

d_'46'extendedlambda0_238 ∷ T_Level_18 → () → T_Level_18 → () → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_'46'extendedlambda1_240 ∷ T_Level_18 → () → T_Level_18 → () → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T_Σ_14 Source #

du_'46'extendedlambda1_240 ∷ T_Σ_14 Source #

d_'46'extendedlambda2_242 ∷ T_Level_18 → () → T_Level_18 → () → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T__'8801'__12 Source #

d_'46'extendedlambda3_244 ∷ T_Level_18 → () → T_Level_18 → () → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_'8707''8707''8596''8707''8707'_256 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Inverse_1048 Source #

du_'8707''8707''8596''8707''8707'_256 ∷ T_Inverse_1048 Source #

d_to_272 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #

du_to_272 ∷ T_Σ_14 → T_Σ_14 Source #

d_from_288 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #

du_from_288 ∷ T_Σ_14 → T_Σ_14 Source #