Safe HaskellNone

MAlonzo.Code.Function.Bundles

Documentation

d__'8776'__30 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_32 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> () Source #

d_Bijective_42 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> () Source #

d_Injective_46 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'691'_48 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'737'_50 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'7495'_52 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_54 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> () Source #

d_IsBiInverse_60 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

d_IsBijection_62 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsCongruent_64 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsInjection_66 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsInverse_68 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

d_IsLeftInverse_70 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

d_IsRightInverse_72 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

d_IsSurjection_74 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d__'8776'__226 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__228 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_230 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> () Source #

d_isEquivalence_232 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__252 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_254 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> () Source #

d_isEquivalence_256 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__284 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_286 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> () Source #

d_isEquivalence_288 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__308 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_310 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> () Source #

d_isEquivalence_312 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__414 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_416 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> () Source #

d_isEquivalence_418 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__438 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_440 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> () Source #

d_isEquivalence_442 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_Func_642 Source #

Constructors

C_Func'46'constructor_5617 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_642 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__660 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_642 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_662 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_642 -> () Source #

d_isEquivalence_664 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_642 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__684 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_642 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_686 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_642 -> () Source #

d_isEquivalence_688 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_Injection_704 Source #

Constructors

C_Injection'46'constructor_7429 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_704 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__728 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_704 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_730 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_704 -> () Source #

d_isEquivalence_732 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_704 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__752 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_704 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_754 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_704 -> () Source #

d_isEquivalence_756 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> 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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_Surjection_774 Source #

Constructors

C_Surjection'46'constructor_9411 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> T_Σ_14) 

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_f'8315'_788 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny Source #

du_f'8315'_788 :: T_Surjection_774 -> AgdaAny -> AgdaAny Source #

d_isCongruent_790 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsCongruent_22 Source #

du_isCongruent_790 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsCongruent_22 Source #

d__'8776'__796 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__798 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_800 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> () Source #

d_isEquivalence_802 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsEquivalence_26 Source #

du_isEquivalence_802 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_804 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_804 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsPartialEquivalence_16 Source #

d_partialSetoid_806 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_PartialSetoid_10 Source #

du_partialSetoid_806 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_PartialSetoid_10 Source #

d_refl_808 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny Source #

du_refl_808 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny Source #

d_reflexive_810 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_810 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_812 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_Setoid_44 Source #

du_setoid_812 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_Setoid_44 Source #

d_sym_814 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_814 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_816 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_816 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__820 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__822 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_824 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> () Source #

d_isEquivalence_826 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsEquivalence_26 Source #

du_isEquivalence_826 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_828 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_828 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsPartialEquivalence_16 Source #

d_partialSetoid_830 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_PartialSetoid_10 Source #

du_partialSetoid_830 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_PartialSetoid_10 Source #

d_refl_832 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny Source #

du_refl_832 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny Source #

d_reflexive_834 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_834 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_836 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_Setoid_44 Source #

du_setoid_836 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_Setoid_44 Source #

d_sym_838 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_838 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_840 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_840 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isSurjection_842 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsSurjection_162 Source #

du_isSurjection_842 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_IsSurjection_162 Source #

d_Bijection_844 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_Bijection_844 Source #

Constructors

C_Bijection'46'constructor_12013 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) T_Σ_14 

d_f_852 :: T_Bijection_844 -> AgdaAny -> AgdaAny Source #

d_cong_854 :: T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_bijective_856 :: T_Bijection_844 -> T_Σ_14 Source #

d_injective_858 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_injective_858 :: T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_surjective_860 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> T_Σ_14 Source #

du_surjective_860 :: T_Bijection_844 -> AgdaAny -> T_Σ_14 Source #

d_injection_862 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_Injection_704 Source #

du_injection_862 :: T_Bijection_844 -> T_Injection_704 Source #

d_surjection_864 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_Surjection_774 Source #

du_surjection_864 :: T_Bijection_844 -> T_Surjection_774 Source #

d_isInjection_868 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsInjection_92 Source #

du_isInjection_868 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsInjection_92 Source #

d_f'8315'_872 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny Source #

du_f'8315'_872 :: T_Bijection_844 -> AgdaAny -> AgdaAny Source #

d_isSurjection_874 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsSurjection_162 Source #

du_isSurjection_874 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsSurjection_162 Source #

d_isBijection_876 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsBijection_232 Source #

du_isBijection_876 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsBijection_232 Source #

d__'8776'__882 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__884 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_886 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> () Source #

d_isEquivalence_888 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsEquivalence_26 Source #

du_isEquivalence_888 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_890 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_890 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsPartialEquivalence_16 Source #

d_partialSetoid_892 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_PartialSetoid_10 Source #

du_partialSetoid_892 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_PartialSetoid_10 Source #

d_refl_894 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny Source #

du_refl_894 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny Source #

d_reflexive_896 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_896 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_898 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_Setoid_44 Source #

du_setoid_898 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_Setoid_44 Source #

d_sym_900 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_900 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_902 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_902 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__906 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__908 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_910 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> () Source #

d_isEquivalence_912 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsEquivalence_26 Source #

du_isEquivalence_912 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_914 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_914 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_IsPartialEquivalence_16 Source #

d_partialSetoid_916 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_PartialSetoid_10 Source #

du_partialSetoid_916 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_PartialSetoid_10 Source #

d_refl_918 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny Source #

du_refl_918 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny Source #

d_reflexive_920 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_920 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_922 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_Setoid_44 Source #

du_setoid_922 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_Setoid_44 Source #

d_sym_924 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_924 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_926 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_926 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_Equivalence_928 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_Equivalence_928 Source #

Constructors

C_Equivalence'46'constructor_15319 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

d_f_938 :: T_Equivalence_928 -> AgdaAny -> AgdaAny Source #

d_g_940 :: T_Equivalence_928 -> AgdaAny -> AgdaAny Source #

d_cong'8321'_942 :: T_Equivalence_928 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong'8322'_944 :: T_Equivalence_928 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_LeftInverse_946 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_LeftInverse_946 Source #

Constructors

C_LeftInverse'46'constructor_16097 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) 

d_f_958 :: T_LeftInverse_946 -> AgdaAny -> AgdaAny Source #

d_g_960 :: T_LeftInverse_946 -> AgdaAny -> AgdaAny Source #

d_cong'8321'_962 :: T_LeftInverse_946 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong'8322'_964 :: T_LeftInverse_946 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse'737'_966 :: T_LeftInverse_946 -> AgdaAny -> AgdaAny Source #

d_isCongruent_968 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsCongruent_22 Source #

du_isCongruent_968 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsCongruent_22 Source #

d__'8776'__974 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__976 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_978 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> () Source #

d_isEquivalence_980 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsEquivalence_26 Source #

du_isEquivalence_980 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_982 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_982 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsPartialEquivalence_16 Source #

d_partialSetoid_984 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_PartialSetoid_10 Source #

du_partialSetoid_984 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_PartialSetoid_10 Source #

d_refl_986 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny Source #

du_refl_986 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny Source #

d_reflexive_988 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_988 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_990 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_Setoid_44 Source #

du_setoid_990 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_Setoid_44 Source #

d_sym_992 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_992 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_994 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_994 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__998 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__1000 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_1002 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> () Source #

d_isEquivalence_1004 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsEquivalence_26 Source #

du_isEquivalence_1004 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_1006 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1006 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsPartialEquivalence_16 Source #

d_partialSetoid_1008 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_PartialSetoid_10 Source #

du_partialSetoid_1008 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_PartialSetoid_10 Source #

d_refl_1010 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny Source #

du_refl_1010 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny Source #

d_reflexive_1012 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1012 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1014 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_Setoid_44 Source #

du_setoid_1014 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_Setoid_44 Source #

d_sym_1016 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_1016 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1018 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_1018 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isLeftInverse_1020 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsLeftInverse_312 Source #

du_isLeftInverse_1020 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_IsLeftInverse_312 Source #

d_equivalence_1022 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_Equivalence_928 Source #

du_equivalence_1022 :: T_LeftInverse_946 -> T_Equivalence_928 Source #

d_RightInverse_1024 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_RightInverse_1024 Source #

Constructors

C_RightInverse'46'constructor_18949 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) 

d_f_1036 :: T_RightInverse_1024 -> AgdaAny -> AgdaAny Source #

d_g_1038 :: T_RightInverse_1024 -> AgdaAny -> AgdaAny Source #

d_cong'8321'_1040 :: T_RightInverse_1024 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong'8322'_1042 :: T_RightInverse_1024 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse'691'_1044 :: T_RightInverse_1024 -> AgdaAny -> AgdaAny Source #

d_isCongruent_1046 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1024 -> T_IsCongruent_22 Source #

du_isCongruent_1046 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1024 -> T_IsCongruent_22 Source #

d_isRightInverse_1048 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1024 -> T_IsRightInverse_390 Source #

du_isRightInverse_1048 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1024 -> T_IsRightInverse_390 Source #

d_equivalence_1050 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1024 -> T_Equivalence_928 Source #

du_equivalence_1050 :: T_RightInverse_1024 -> T_Equivalence_928 Source #

d_Inverse_1052 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_Inverse_1052 Source #

Constructors

C_Inverse'46'constructor_20717 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) T_Σ_14 

d_f_1064 :: T_Inverse_1052 -> AgdaAny -> AgdaAny Source #

d_f'8315''185'_1066 :: T_Inverse_1052 -> AgdaAny -> AgdaAny Source #

d_cong'8321'_1068 :: T_Inverse_1052 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong'8322'_1070 :: T_Inverse_1052 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse_1072 :: T_Inverse_1052 -> T_Σ_14 Source #

d_inverse'737'_1074 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny Source #

du_inverse'737'_1074 :: T_Inverse_1052 -> AgdaAny -> AgdaAny Source #

d_inverse'691'_1076 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny Source #

du_inverse'691'_1076 :: T_Inverse_1052 -> AgdaAny -> AgdaAny Source #

d_leftInverse_1078 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_LeftInverse_946 Source #

du_leftInverse_1078 :: T_Inverse_1052 -> T_LeftInverse_946 Source #

d_rightInverse_1080 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_RightInverse_1024 Source #

du_rightInverse_1080 :: T_Inverse_1052 -> T_RightInverse_1024 Source #

d_isLeftInverse_1084 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsLeftInverse_312 Source #

du_isLeftInverse_1084 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsLeftInverse_312 Source #

d_isRightInverse_1088 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsRightInverse_390 Source #

du_isRightInverse_1088 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsRightInverse_390 Source #

d_isInverse_1090 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsInverse_468 Source #

du_isInverse_1090 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsInverse_468 Source #

d__'8776'__1096 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__1098 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_1100 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> () Source #

d_isEquivalence_1102 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsEquivalence_26 Source #

du_isEquivalence_1102 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_1104 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1104 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsPartialEquivalence_16 Source #

d_partialSetoid_1106 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_PartialSetoid_10 Source #

du_partialSetoid_1106 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_PartialSetoid_10 Source #

d_refl_1108 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny Source #

du_refl_1108 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny Source #

d_reflexive_1110 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1110 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1112 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_Setoid_44 Source #

du_setoid_1112 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_Setoid_44 Source #

d_sym_1114 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_1114 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1116 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_1116 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__1120 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__1122 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_1124 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> () Source #

d_isEquivalence_1126 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsEquivalence_26 Source #

du_isEquivalence_1126 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsEquivalence_26 Source #

d_isPartialEquivalence_1128 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1128 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_IsPartialEquivalence_16 Source #

d_partialSetoid_1130 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_PartialSetoid_10 Source #

du_partialSetoid_1130 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_PartialSetoid_10 Source #

d_refl_1132 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny Source #

du_refl_1132 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny Source #

d_reflexive_1134 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_1134 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_setoid_1136 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_Setoid_44 Source #

du_setoid_1136 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_Setoid_44 Source #

d_sym_1138 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_1138 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_1140 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_1140 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_BiEquivalence_1142 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_BiEquivalence_1142 Source #

Constructors

C_BiEquivalence'46'constructor_24487 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

d_f_1156 :: T_BiEquivalence_1142 -> AgdaAny -> AgdaAny Source #

d_g'8321'_1158 :: T_BiEquivalence_1142 -> AgdaAny -> AgdaAny Source #

d_g'8322'_1160 :: T_BiEquivalence_1142 -> AgdaAny -> AgdaAny Source #

d_cong'8321'_1162 :: T_BiEquivalence_1142 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong'8322'_1164 :: T_BiEquivalence_1142 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong'8323'_1166 :: T_BiEquivalence_1142 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_BiInverse_1168 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_BiInverse_1168 Source #

Constructors

C_BiInverse'46'constructor_25741 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) 

d_f_1186 :: T_BiInverse_1168 -> AgdaAny -> AgdaAny Source #

d_g'8321'_1188 :: T_BiInverse_1168 -> AgdaAny -> AgdaAny Source #

d_g'8322'_1190 :: T_BiInverse_1168 -> AgdaAny -> AgdaAny Source #

d_cong'8321'_1192 :: T_BiInverse_1168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong'8322'_1194 :: T_BiInverse_1168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong'8323'_1196 :: T_BiInverse_1168 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse'737'_1198 :: T_BiInverse_1168 -> AgdaAny -> AgdaAny Source #

d_inverse'691'_1200 :: T_BiInverse_1168 -> AgdaAny -> AgdaAny Source #

d_f'45'isCongruent_1202 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_BiInverse_1168 -> T_IsCongruent_22 Source #

du_f'45'isCongruent_1202 :: T_Setoid_44 -> T_Setoid_44 -> T_BiInverse_1168 -> T_IsCongruent_22 Source #

d_isBiInverse_1204 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_BiInverse_1168 -> T_IsBiInverse_636 Source #

du_isBiInverse_1204 :: T_Setoid_44 -> T_Setoid_44 -> T_BiInverse_1168 -> T_IsBiInverse_636 Source #

d_biEquivalence_1206 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_BiInverse_1168 -> T_BiEquivalence_1142 Source #

du_biEquivalence_1206 :: T_BiInverse_1168 -> T_BiEquivalence_1142 Source #

d__'10230'__1208 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d__'8611'__1214 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d__'8608'__1220 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d__'10518'__1226 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d__'8660'__1232 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d__'8617'__1238 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d__'8618'__1244 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d__'8617''8618'__1250 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d__'8596'__1256 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d_Bijective_1276 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> () Source #

d_Injective_1280 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'691'_1282 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'737'_1284 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'7495'_1286 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_1288 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> () Source #

d_mk'10230'_1290 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> T_Func_642 Source #

du_mk'10230'_1290 :: (AgdaAny -> AgdaAny) -> T_Func_642 Source #

d_mk'8611'_1296 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_Injection_704 Source #

du_mk'8611'_1296 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_Injection_704 Source #

d_mk'8608'_1304 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> T_Surjection_774 Source #

du_mk'8608'_1304 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> T_Surjection_774 Source #

d_mk'10518'_1312 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Bijection_844 Source #

du_mk'10518'_1312 :: (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Bijection_844 Source #

d_mk'8660'_1322 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_928 Source #

du_mk'8660'_1322 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_928 Source #

d_mk'8617'_1332 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T_LeftInverse_946 Source #

du_mk'8617'_1332 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T_LeftInverse_946 Source #

d_mk'8618'_1344 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T_RightInverse_1024 Source #

du_mk'8618'_1344 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T_RightInverse_1024 Source #

d_mk'8617''8618'_1358 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> (AgdaAny -> T__'8801'__12) -> T_BiInverse_1168 Source #

du_mk'8617''8618'_1358 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> (AgdaAny -> T__'8801'__12) -> T_BiInverse_1168 Source #

d_mk'8596'_1374 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Inverse_1052 Source #

du_mk'8596'_1374 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Inverse_1052 Source #

d_mk'8596''8242'_1386 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> (AgdaAny -> T__'8801'__12) -> T_Inverse_1052 Source #

du_mk'8596''8242'_1386 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> (AgdaAny -> T__'8801'__12) -> T_Inverse_1052 Source #