Documentation

d__InverseOf__20 ∷ p → p → p → p → p → p → p → p → () Source #

data T__InverseOf__20 Source #

d_left'45'inverse'45'of_42 ∷ T__InverseOf__20 → AgdaAny → AgdaAny Source #

d_right'45'inverse'45'of_44 ∷ T__InverseOf__20 → AgdaAny → AgdaAny Source #

d_Inverse_58 ∷ p → p → p → p → p → p → () Source #

data T_Inverse_58 Source #

d_to_78 ∷ T_Inverse_58 → T_Π_16 Source #

d_from_80 ∷ T_Inverse_58 → T_Π_16 Source #

d_inverse'45'of_82 ∷ T_Inverse_58 → T__InverseOf__20 Source #

d_left'45'inverse'45'of_86 ∷ T_Inverse_58 → AgdaAny → AgdaAny Source #

d_right'45'inverse'45'of_88 ∷ T_Inverse_58 → AgdaAny → AgdaAny Source #

d_left'45'inverse_90 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_LeftInverse_82 Source #

du_left'45'inverse_90 ∷ T_Inverse_58 → T_LeftInverse_82 Source #

d_injection_94 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Injection_88 Source #

du_injection_94 ∷ T_Setoid_44 → T_Inverse_58 → T_Injection_88 Source #

d_injective_96 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_injective_96 ∷ T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_bijection_98 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Bijection_64 Source #

du_bijection_98 ∷ T_Setoid_44 → T_Inverse_58 → T_Bijection_64 Source #

d_equivalence_102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Equivalence_16 Source #

du_equivalence_102 ∷ T_Setoid_44 → T_Inverse_58 → T_Equivalence_16 Source #

d_to'45'from_104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_104 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_right'45'inverse_106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_LeftInverse_82 Source #

du_right'45'inverse_106 ∷ T_Setoid_44 → T_Inverse_58 → T_LeftInverse_82 Source #

d_surjection_108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Surjection_54 Source #

du_surjection_108 ∷ T_Setoid_44 → T_Inverse_58 → T_Surjection_54 Source #

d_surjective_110 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Surjective_18 Source #

du_surjective_110 ∷ T_Setoid_44 → T_Inverse_58 → T_Surjective_18 Source #

d_to'45'from_112 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_112 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8596'__118 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

d__'8596''775'__132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → () Source #

d_inverse_156 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → (AgdaAny → T__'8801'__12) → T_Inverse_58 Source #

du_inverse_156 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → (AgdaAny → T__'8801'__12) → T_Inverse_58 Source #

d_fromBijection_178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_64 → T_Inverse_58 Source #

du_fromBijection_178 ∷ T_Bijection_64 → T_Inverse_58 Source #

d_id_186 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_58 Source #

du_id_186 ∷ T_Setoid_44 → T_Inverse_58 Source #

d_id'8242'_194 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_LeftInverse_82 Source #

du_id'8242'_194 ∷ T_Setoid_44 → T_LeftInverse_82 Source #

d__'8728'__208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Inverse_58 → T_Inverse_58 Source #

du__'8728'__208 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Inverse_58 → T_Inverse_58 Source #

d_sym_226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Inverse_58 Source #

du_sym_226 ∷ T_Inverse_58 → T_Inverse_58 Source #

d_bijection_236 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Bijection_64 Source #

du_bijection_236 ∷ T_Setoid_44 → T_Inverse_58 → T_Bijection_64 Source #

d_equivalence_238 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Equivalence_16 Source #

du_equivalence_238 ∷ T_Setoid_44 → T_Inverse_58 → T_Equivalence_16 Source #

d_from_240 ∷ T_Inverse_58 → T_Π_16 Source #

d_to'45'from_242 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_242 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injection_244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Injection_88 Source #

du_injection_244 ∷ T_Setoid_44 → T_Inverse_58 → T_Injection_88 Source #

d_injective_246 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_injective_246 ∷ T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'45'of_248 ∷ T_Inverse_58 → T__InverseOf__20 Source #

d_left'45'inverse_250 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_LeftInverse_82 Source #

du_left'45'inverse_250 ∷ T_Inverse_58 → T_LeftInverse_82 Source #

d_left'45'inverse'45'of_252 ∷ T_Inverse_58 → AgdaAny → AgdaAny Source #

d_right'45'inverse_254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_LeftInverse_82 Source #

du_right'45'inverse_254 ∷ T_Setoid_44 → T_Inverse_58 → T_LeftInverse_82 Source #

d_right'45'inverse'45'of_256 ∷ T_Inverse_58 → AgdaAny → AgdaAny Source #

d_surjection_258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Surjection_54 Source #

du_surjection_258 ∷ T_Setoid_44 → T_Inverse_58 → T_Surjection_54 Source #

d_surjective_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → T_Surjective_18 Source #

du_surjective_260 ∷ T_Setoid_44 → T_Inverse_58 → T_Surjective_18 Source #

d_to_262 ∷ T_Inverse_58 → T_Π_16 Source #

d_to'45'from_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_264 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_map_298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_Inverse_58 Source #

du_map_298 ∷ (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_Inverse_58 Source #

d_bijection_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_Bijection_64 Source #

du_bijection_314 ∷ T_Setoid_44 → T_Inverse_58 → T_Bijection_64 Source #

d_equivalence_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_Equivalence_16 Source #

du_equivalence_316 ∷ T_Setoid_44 → T_Inverse_58 → T_Equivalence_16 Source #

d_from_318 ∷ T_Inverse_58 → T_Π_16 Source #

d_to'45'from_320 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_320 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injection_322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_Injection_88 Source #

du_injection_322 ∷ T_Setoid_44 → T_Inverse_58 → T_Injection_88 Source #

d_injective_324 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_injective_324 ∷ T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'45'of_326 ∷ T_Inverse_58 → T__InverseOf__20 Source #

d_left'45'inverse_328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_LeftInverse_82 Source #

du_left'45'inverse_328 ∷ T_Inverse_58 → T_LeftInverse_82 Source #

d_left'45'inverse'45'of_330 ∷ T_Inverse_58 → AgdaAny → AgdaAny Source #

d_right'45'inverse_332 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_LeftInverse_82 Source #

du_right'45'inverse_332 ∷ T_Setoid_44 → T_Inverse_58 → T_LeftInverse_82 Source #

d_right'45'inverse'45'of_334 ∷ T_Inverse_58 → AgdaAny → AgdaAny Source #

d_surjection_336 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_Surjection_54 Source #

du_surjection_336 ∷ T_Setoid_44 → T_Inverse_58 → T_Surjection_54 Source #

d_surjective_338 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_Surjective_18 Source #

du_surjective_338 ∷ T_Setoid_44 → T_Inverse_58 → T_Surjective_18 Source #

d_to_340 ∷ T_Inverse_58 → T_Π_16 Source #

d_to'45'from_342 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_342 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_58 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zip_392 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_Inverse_58 → T_Inverse_58 Source #

du_zip_392 ∷ (T_Π_16 → T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T_Π_16 → T_Π_16 → T__InverseOf__20 → T__InverseOf__20 → T__InverseOf__20) → T_Inverse_58 → T_Inverse_58 → T_Inverse_58 Source #