Documentation

d__'8776'__30 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → AgdaAny → AgdaAny → () Source #

d_Carrier_32 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → () Source #

d_Bijective_42 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → () Source #

d_Injective_46 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → () Source #

d_Inverse'691'_48 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Inverse'737'_50 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Inverse'7495'_52 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Surjective_54 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → () → (AgdaAny → AgdaAny) → () Source #

d_IsBiInverse_60 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_IsBijection_62 ∷ p → p → p → p → p → p → p → () Source #

d_IsCongruent_64 ∷ p → p → p → p → p → p → p → () Source #

d_IsInjection_66 ∷ p → p → p → p → p → p → p → () Source #

d_IsInverse_68 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsLeftInverse_70 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsRightInverse_72 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSurjection_74 ∷ p → p → p → p → p → p → p → () Source #

d__'8776'__226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → () Source #

d__'8777'__228 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → () Source #

d_Carrier_230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → () Source #

d_isEquivalence_232 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_IsEquivalence_26 Source #

du_isEquivalence_232 ∷ T_IsBijection_232 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_234 ∷ T_IsBijection_232 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_236 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_PartialSetoid_10 Source #

du_partialSetoid_236 ∷ T_IsBijection_232 → T_PartialSetoid_10 Source #

d_refl_238 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny Source #

du_refl_238 ∷ T_IsBijection_232 → AgdaAny → AgdaAny Source #

d_reflexive_240 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_240 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_242 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_Setoid_44 Source #

du_setoid_242 ∷ T_IsBijection_232 → T_Setoid_44 Source #

d_sym_244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_244 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_246 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_246 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__250 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → () Source #

d__'8777'__252 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → () Source #

d_Carrier_254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → () Source #

d_isEquivalence_256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_IsEquivalence_26 Source #

du_isEquivalence_256 ∷ T_IsBijection_232 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_258 ∷ T_IsBijection_232 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_PartialSetoid_10 Source #

du_partialSetoid_260 ∷ T_IsBijection_232 → T_PartialSetoid_10 Source #

d_refl_262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny Source #

du_refl_262 ∷ T_IsBijection_232 → AgdaAny → AgdaAny Source #

d_reflexive_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_264 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_Setoid_44 Source #

du_setoid_266 ∷ T_IsBijection_232 → T_Setoid_44 Source #

d_sym_268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_268 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_270 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__282 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → () Source #

d__'8777'__284 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → () Source #

d_Carrier_286 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → () Source #

d_isEquivalence_288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsEquivalence_26 Source #

du_isEquivalence_288 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_290 ∷ T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_PartialSetoid_10 Source #

du_partialSetoid_292 ∷ T_IsCongruent_22 → T_PartialSetoid_10 Source #

d_refl_294 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny Source #

du_refl_294 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny Source #

d_reflexive_296 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_296 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_Setoid_44 Source #

du_setoid_298 ∷ (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_Setoid_44 Source #

d_sym_300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_300 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_302 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → () Source #

d__'8777'__308 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → () Source #

d_Carrier_310 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → () Source #

d_isEquivalence_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsEquivalence_26 Source #

du_isEquivalence_312 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_314 ∷ T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_PartialSetoid_10 Source #

du_partialSetoid_316 ∷ T_IsCongruent_22 → T_PartialSetoid_10 Source #

d_refl_318 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny Source #

du_refl_318 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny Source #

d_reflexive_320 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_320 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_Setoid_44 Source #

du_setoid_322 ∷ (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_Setoid_44 Source #

d_sym_324 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_324 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_326 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_326 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__412 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → () Source #

d__'8777'__414 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → () Source #

d_Carrier_416 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → () Source #

d_isEquivalence_418 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_IsEquivalence_26 Source #

du_isEquivalence_418 ∷ T_IsInverse_468 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_420 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_420 ∷ T_IsInverse_468 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_422 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_PartialSetoid_10 Source #

du_partialSetoid_422 ∷ T_IsInverse_468 → T_PartialSetoid_10 Source #

d_refl_424 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny Source #

du_refl_424 ∷ T_IsInverse_468 → AgdaAny → AgdaAny Source #

d_reflexive_426 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_426 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_Setoid_44 Source #

du_setoid_428 ∷ T_IsInverse_468 → T_Setoid_44 Source #

d_sym_430 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_430 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_432 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_432 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__436 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → () Source #

d__'8777'__438 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → () Source #

d_Carrier_440 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → () Source #

d_isEquivalence_442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_IsEquivalence_26 Source #

du_isEquivalence_442 ∷ T_IsInverse_468 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_444 ∷ T_IsInverse_468 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_446 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_PartialSetoid_10 Source #

du_partialSetoid_446 ∷ T_IsInverse_468 → T_PartialSetoid_10 Source #

d_refl_448 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny Source #

du_refl_448 ∷ T_IsInverse_468 → AgdaAny → AgdaAny Source #

d_reflexive_450 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_450 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_452 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_Setoid_44 Source #

du_setoid_452 ∷ T_IsInverse_468 → T_Setoid_44 Source #

d_sym_454 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_454 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_456 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_456 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Func_642 ∷ p → p → p → p → p → p → () Source #

data T_Func_642 Source #

d_f_648 ∷ T_Func_642 → AgdaAny → AgdaAny Source #

d_cong_650 ∷ T_Func_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_652 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_IsCongruent_22 Source #

du_isCongruent_652 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_IsCongruent_22 Source #

d__'8776'__658 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → () Source #

d__'8777'__660 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → () Source #

d_Carrier_662 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → () Source #

d_isEquivalence_664 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_IsEquivalence_26 Source #

du_isEquivalence_664 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_666 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_666 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_668 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_PartialSetoid_10 Source #

du_partialSetoid_668 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_PartialSetoid_10 Source #

d_refl_670 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny Source #

du_refl_670 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny Source #

d_reflexive_672 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_672 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_674 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_Setoid_44 Source #

du_setoid_674 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_Setoid_44 Source #

d_sym_676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_676 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_678 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_678 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → () Source #

d__'8777'__684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → () Source #

d_Carrier_686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → () Source #

d_isEquivalence_688 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_IsEquivalence_26 Source #

du_isEquivalence_688 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_690 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_692 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_PartialSetoid_10 Source #

du_partialSetoid_692 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_PartialSetoid_10 Source #

d_refl_694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny Source #

du_refl_694 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny Source #

d_reflexive_696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_696 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_Setoid_44 Source #

du_setoid_698 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → T_Setoid_44 Source #

d_sym_700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_700 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_702 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_642 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Injection_704 ∷ p → p → p → p → p → p → () Source #

data T_Injection_704 Source #

d_f_712 ∷ T_Injection_704 → AgdaAny → AgdaAny Source #

d_cong_714 ∷ T_Injection_704 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_716 ∷ T_Injection_704 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_function_718 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_Func_642 Source #

du_function_718 ∷ T_Injection_704 → T_Func_642 Source #

d_isCongruent_722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsCongruent_22 Source #

du_isCongruent_722 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsCongruent_22 Source #

d__'8776'__726 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → () Source #

d__'8777'__728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → () Source #

d_Carrier_730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → () Source #

d_isEquivalence_732 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsEquivalence_26 Source #

du_isEquivalence_732 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_734 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_734 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_736 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_PartialSetoid_10 Source #

du_partialSetoid_736 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_PartialSetoid_10 Source #

d_refl_738 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny Source #

du_refl_738 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny Source #

d_reflexive_740 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_740 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_742 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_Setoid_44 Source #

du_setoid_742 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_Setoid_44 Source #

d_sym_744 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_744 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_746 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_746 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__750 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → () Source #

d__'8777'__752 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → () Source #

d_Carrier_754 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → () Source #

d_isEquivalence_756 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsEquivalence_26 Source #

du_isEquivalence_756 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_758 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_758 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_760 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_PartialSetoid_10 Source #

du_partialSetoid_760 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_PartialSetoid_10 Source #

d_refl_762 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny Source #

du_refl_762 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny Source #

d_reflexive_764 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_764 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_Setoid_44 Source #

du_setoid_766 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_Setoid_44 Source #

d_sym_768 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_768 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_770 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_770 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isInjection_772 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsInjection_92 Source #

du_isInjection_772 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_704 → T_IsInjection_92 Source #

d_Surjection_774 ∷ p → p → p → p → p → p → () Source #

data T_Surjection_774 Source #

d_f_782 ∷ T_Surjection_774 → AgdaAny → AgdaAny Source #

d_cong_784 ∷ T_Surjection_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_surjective_786 ∷ T_Surjection_774 → AgdaAny → T_Σ_14 Source #

d_isCongruent_788 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsCongruent_22 Source #

du_isCongruent_788 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsCongruent_22 Source #

d__'8776'__794 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → () Source #

d__'8777'__796 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → () Source #

d_Carrier_798 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → () Source #

d_isEquivalence_800 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsEquivalence_26 Source #

du_isEquivalence_800 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_802 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_PartialSetoid_10 Source #

du_partialSetoid_804 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_PartialSetoid_10 Source #

d_refl_806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny Source #

du_refl_806 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny Source #

d_reflexive_808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_808 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_Setoid_44 Source #

du_setoid_810 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_Setoid_44 Source #

d_sym_812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_812 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_814 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_814 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → () Source #

d__'8777'__820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → () Source #

d_Carrier_822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → () Source #

d_isEquivalence_824 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsEquivalence_26 Source #

du_isEquivalence_824 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_826 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_828 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_PartialSetoid_10 Source #

du_partialSetoid_828 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_PartialSetoid_10 Source #

d_refl_830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny Source #

du_refl_830 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny Source #

d_reflexive_832 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_832 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_834 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_Setoid_44 Source #

du_setoid_834 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_Setoid_44 Source #

d_sym_836 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_836 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_838 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isSurjection_840 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsSurjection_162 Source #

du_isSurjection_840 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_774 → T_IsSurjection_162 Source #

d_Bijection_842 ∷ p → p → p → p → p → p → () Source #

data T_Bijection_842 Source #

d_f_850 ∷ T_Bijection_842 → AgdaAny → AgdaAny Source #

d_cong_852 ∷ T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_bijective_854 ∷ T_Bijection_842 → T_Σ_14 Source #

d_injective_856 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_injective_856 ∷ T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_surjective_858 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → T_Σ_14 Source #

du_surjective_858 ∷ T_Bijection_842 → AgdaAny → T_Σ_14 Source #

d_injection_860 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_Injection_704 Source #

du_injection_860 ∷ T_Bijection_842 → T_Injection_704 Source #

d_surjection_862 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_Surjection_774 Source #

du_surjection_862 ∷ T_Bijection_842 → T_Surjection_774 Source #

d_isInjection_866 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsInjection_92 Source #

du_isInjection_866 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsInjection_92 Source #

d_isSurjection_870 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsSurjection_162 Source #

du_isSurjection_870 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsSurjection_162 Source #

d_isBijection_872 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsBijection_232 Source #

du_isBijection_872 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsBijection_232 Source #

d__'8776'__878 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → () Source #

d__'8777'__880 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → () Source #

d_Carrier_882 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → () Source #

d_isEquivalence_884 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsEquivalence_26 Source #

du_isEquivalence_884 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_886 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_886 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_888 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_PartialSetoid_10 Source #

du_partialSetoid_888 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_PartialSetoid_10 Source #

d_refl_890 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny Source #

du_refl_890 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny Source #

d_reflexive_892 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_892 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_894 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_Setoid_44 Source #

du_setoid_894 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_Setoid_44 Source #

d_sym_896 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_896 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_898 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_898 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__902 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → () Source #

d__'8777'__904 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → () Source #

d_Carrier_906 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → () Source #

d_isEquivalence_908 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsEquivalence_26 Source #

du_isEquivalence_908 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_910 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_910 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_912 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_PartialSetoid_10 Source #

du_partialSetoid_912 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_PartialSetoid_10 Source #

d_refl_914 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny Source #

du_refl_914 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny Source #

d_reflexive_916 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_916 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_918 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_Setoid_44 Source #

du_setoid_918 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → T_Setoid_44 Source #

d_sym_920 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_920 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_922 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_922 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Equivalence_924 ∷ p → p → p → p → p → p → () Source #

data T_Equivalence_924 Source #

d_f_934 ∷ T_Equivalence_924 → AgdaAny → AgdaAny Source #

d_g_936 ∷ T_Equivalence_924 → AgdaAny → AgdaAny Source #

d_cong'8321'_938 ∷ T_Equivalence_924 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8322'_940 ∷ T_Equivalence_924 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_LeftInverse_942 ∷ p → p → p → p → p → p → () Source #

data T_LeftInverse_942 Source #

d_f_954 ∷ T_LeftInverse_942 → AgdaAny → AgdaAny Source #

d_g_956 ∷ T_LeftInverse_942 → AgdaAny → AgdaAny Source #

d_cong'8321'_958 ∷ T_LeftInverse_942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8322'_960 ∷ T_LeftInverse_942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_962 ∷ T_LeftInverse_942 → AgdaAny → AgdaAny Source #

d_isCongruent_964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsCongruent_22 Source #

du_isCongruent_964 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsCongruent_22 Source #

d__'8776'__970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → () Source #

d__'8777'__972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → () Source #

d_Carrier_974 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → () Source #

d_isEquivalence_976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsEquivalence_26 Source #

du_isEquivalence_976 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_978 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_978 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_980 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_PartialSetoid_10 Source #

du_partialSetoid_980 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_PartialSetoid_10 Source #

d_refl_982 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny Source #

du_refl_982 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny Source #

d_reflexive_984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_984 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_Setoid_44 Source #

du_setoid_986 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_Setoid_44 Source #

d_sym_988 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_988 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_990 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_990 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → () Source #

d__'8777'__996 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → () Source #

d_Carrier_998 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → () Source #

d_isEquivalence_1000 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsEquivalence_26 Source #

du_isEquivalence_1000 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1002 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1002 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1004 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_PartialSetoid_10 Source #

du_partialSetoid_1004 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_PartialSetoid_10 Source #

d_refl_1006 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny Source #

du_refl_1006 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny Source #

d_reflexive_1008 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1008 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1010 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_Setoid_44 Source #

du_setoid_1010 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_Setoid_44 Source #

d_sym_1012 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1012 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1014 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1014 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isLeftInverse_1016 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsLeftInverse_312 Source #

du_isLeftInverse_1016 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_IsLeftInverse_312 Source #

d_equivalence_1018 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_942 → T_Equivalence_924 Source #

du_equivalence_1018 ∷ T_LeftInverse_942 → T_Equivalence_924 Source #

d_RightInverse_1020 ∷ p → p → p → p → p → p → () Source #

data T_RightInverse_1020 Source #

d_f_1032 ∷ T_RightInverse_1020 → AgdaAny → AgdaAny Source #

d_g_1034 ∷ T_RightInverse_1020 → AgdaAny → AgdaAny Source #

d_cong'8321'_1036 ∷ T_RightInverse_1020 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8322'_1038 ∷ T_RightInverse_1020 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_1040 ∷ T_RightInverse_1020 → AgdaAny → AgdaAny Source #

d_isCongruent_1042 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_RightInverse_1020 → T_IsCongruent_22 Source #

du_isCongruent_1042 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1020 → T_IsCongruent_22 Source #

d_isRightInverse_1044 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_RightInverse_1020 → T_IsRightInverse_390 Source #

du_isRightInverse_1044 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1020 → T_IsRightInverse_390 Source #

d_equivalence_1046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_RightInverse_1020 → T_Equivalence_924 Source #

du_equivalence_1046 ∷ T_RightInverse_1020 → T_Equivalence_924 Source #

d_Inverse_1048 ∷ p → p → p → p → p → p → () Source #

data T_Inverse_1048 Source #

d_f_1060 ∷ T_Inverse_1048 → AgdaAny → AgdaAny Source #

d_f'8315''185'_1062 ∷ T_Inverse_1048 → AgdaAny → AgdaAny Source #

d_cong'8321'_1064 ∷ T_Inverse_1048 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8322'_1066 ∷ T_Inverse_1048 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse_1068 ∷ T_Inverse_1048 → T_Σ_14 Source #

d_inverse'737'_1070 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny Source #

du_inverse'737'_1070 ∷ T_Inverse_1048 → AgdaAny → AgdaAny Source #

d_inverse'691'_1072 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny Source #

du_inverse'691'_1072 ∷ T_Inverse_1048 → AgdaAny → AgdaAny Source #

d_leftInverse_1074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_LeftInverse_942 Source #

du_leftInverse_1074 ∷ T_Inverse_1048 → T_LeftInverse_942 Source #

d_rightInverse_1076 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_RightInverse_1020 Source #

du_rightInverse_1076 ∷ T_Inverse_1048 → T_RightInverse_1020 Source #

d_isLeftInverse_1080 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsLeftInverse_312 Source #

du_isLeftInverse_1080 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsLeftInverse_312 Source #

d_isRightInverse_1084 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsRightInverse_390 Source #

du_isRightInverse_1084 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsRightInverse_390 Source #

d_isInverse_1086 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsInverse_468 Source #

du_isInverse_1086 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsInverse_468 Source #

d__'8776'__1092 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → () Source #

d__'8777'__1094 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → () Source #

d_Carrier_1096 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → () Source #

d_isEquivalence_1098 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsEquivalence_26 Source #

du_isEquivalence_1098 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1100 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_PartialSetoid_10 Source #

du_partialSetoid_1102 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_PartialSetoid_10 Source #

d_refl_1104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny Source #

du_refl_1104 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny Source #

d_reflexive_1106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1106 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_Setoid_44 Source #

du_setoid_1108 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_Setoid_44 Source #

d_sym_1110 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1110 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1112 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1112 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → () Source #

d__'8777'__1118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → () Source #

d_Carrier_1120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → () Source #

d_isEquivalence_1122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsEquivalence_26 Source #

du_isEquivalence_1122 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_1124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1124 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_PartialSetoid_10 Source #

du_partialSetoid_1126 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_PartialSetoid_10 Source #

d_refl_1128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny Source #

du_refl_1128 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny Source #

d_reflexive_1130 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1130 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_Setoid_44 Source #

du_setoid_1132 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → T_Setoid_44 Source #

d_sym_1134 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1134 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1136 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1136 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1048 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_BiEquivalence_1138 ∷ p → p → p → p → p → p → () Source #

data T_BiEquivalence_1138 Source #

d_f_1152 ∷ T_BiEquivalence_1138 → AgdaAny → AgdaAny Source #

d_g'8321'_1154 ∷ T_BiEquivalence_1138 → AgdaAny → AgdaAny Source #

d_g'8322'_1156 ∷ T_BiEquivalence_1138 → AgdaAny → AgdaAny Source #

d_cong'8321'_1158 ∷ T_BiEquivalence_1138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8322'_1160 ∷ T_BiEquivalence_1138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8323'_1162 ∷ T_BiEquivalence_1138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_BiInverse_1164 ∷ p → p → p → p → p → p → () Source #

data T_BiInverse_1164 Source #

d_f_1182 ∷ T_BiInverse_1164 → AgdaAny → AgdaAny Source #

d_g'8321'_1184 ∷ T_BiInverse_1164 → AgdaAny → AgdaAny Source #

d_g'8322'_1186 ∷ T_BiInverse_1164 → AgdaAny → AgdaAny Source #

d_cong'8321'_1188 ∷ T_BiInverse_1164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8322'_1190 ∷ T_BiInverse_1164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8323'_1192 ∷ T_BiInverse_1164 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_1194 ∷ T_BiInverse_1164 → AgdaAny → AgdaAny Source #

d_inverse'691'_1196 ∷ T_BiInverse_1164 → AgdaAny → AgdaAny Source #

d_f'45'isCongruent_1198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_BiInverse_1164 → T_IsCongruent_22 Source #

du_f'45'isCongruent_1198 ∷ T_Setoid_44 → T_Setoid_44 → T_BiInverse_1164 → T_IsCongruent_22 Source #

d_isBiInverse_1200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_BiInverse_1164 → T_IsBiInverse_636 Source #

du_isBiInverse_1200 ∷ T_Setoid_44 → T_Setoid_44 → T_BiInverse_1164 → T_IsBiInverse_636 Source #

d_biEquivalence_1202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_BiInverse_1164 → T_BiEquivalence_1138 Source #

du_biEquivalence_1202 ∷ T_BiInverse_1164 → T_BiEquivalence_1138 Source #

d__'10230'__1204 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

d__'8611'__1210 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

d__'8608'__1216 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

d__'10518'__1222 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

d__'8660'__1228 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

d__'8617'__1234 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

d__'8618'__1240 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

d__'8617''8618'__1246 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

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

d_Bijective_1272 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → () Source #

d_Injective_1276 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → () Source #

d_Inverse'691'_1278 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Inverse'737'_1280 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Inverse'7495'_1282 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Surjective_1284 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → () → (AgdaAny → AgdaAny) → () Source #

d_mk'10230'_1286 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → T_Func_642 Source #

du_mk'10230'_1286 ∷ (AgdaAny → AgdaAny) → T_Func_642 Source #

d_mk'8611'_1292 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → T_Injection_704 Source #

du_mk'8611'_1292 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → T_Injection_704 Source #

d_mk'8608'_1300 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → T_Surjection_774 Source #

du_mk'8608'_1300 ∷ (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → T_Surjection_774 Source #

d_mk'10518'_1308 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → T_Σ_14 → T_Bijection_842 Source #

du_mk'10518'_1308 ∷ (AgdaAny → AgdaAny) → T_Σ_14 → T_Bijection_842 Source #

d_mk'8660'_1318 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Equivalence_924 Source #

du_mk'8660'_1318 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Equivalence_924 Source #

d_mk'8617'_1328 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T_LeftInverse_942 Source #

du_mk'8617'_1328 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T_LeftInverse_942 Source #

d_mk'8618'_1340 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T_RightInverse_1020 Source #

du_mk'8618'_1340 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T_RightInverse_1020 Source #

d_mk'8617''8618'_1354 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → (AgdaAny → T__'8801'__12) → T_BiInverse_1164 Source #

du_mk'8617''8618'_1354 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → (AgdaAny → T__'8801'__12) → T_BiInverse_1164 Source #

d_mk'8596'_1370 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Inverse_1048 Source #

du_mk'8596'_1370 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Inverse_1048 Source #

d_mk'8596''8242'_1382 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → (AgdaAny → T__'8801'__12) → T_Inverse_1048 Source #

du_mk'8596''8242'_1382 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → (AgdaAny → T__'8801'__12) → T_Inverse_1048 Source #