Documentation

d_'44''45'injective'737'_42 ∷ 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'_54 ∷ 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_70 ∷ 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_78 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → T_Dec_20) → T_Σ_14 → T_Σ_14 → T_Dec_20 Source #

du_'8801''45'dec_78 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → T_Dec_20) → T_Σ_14 → T_Σ_14 → T_Dec_20 Source #

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

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

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

d_map'45'cong_152 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → (AgdaAny → T__'8801'__12) → T_Σ_14 → T__'8801'__12 Source #

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

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

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

du_Σ'45''8801''44''8801''8592''8801'_194 ∷ T_Σ_14 Source #

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

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

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

du_Σ'45''8801''44''8801''8596''8801'_208 ∷ T_Inverse_1960 Source #

d_'215''45''8801''44''8801''8594''8801'_230 ∷ T_Level_18 → () → T_Level_18 → () → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #

d_'215''45''8801''44''8801''8592''8801'_232 ∷ T_Level_18 → () → T_Level_18 → () → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T_Σ_14 Source #

du_'215''45''8801''44''8801''8592''8801'_232 ∷ T_Σ_14 Source #

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

du_'215''45''8801''44''8801''8596''8801'_234 ∷ T_Inverse_1960 Source #

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

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

d_'8707''8707''8596''8707''8707'_250 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Inverse_1960 Source #

du_'8707''8707''8596''8707''8707'_250 ∷ T_Inverse_1960 Source #

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

du_to_266 ∷ T_Σ_14 → T_Σ_14 Source #

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

du_from_282 ∷ T_Σ_14 → T_Σ_14 Source #