Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Function.Bundles

Documentation

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

d_Carrier_32 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> () #

d_IsBijection_46 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsCongruent_48 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsInjection_50 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsSurjection_60 :: p -> p -> p -> p -> p -> p -> p -> () #

d_isInjection_204 :: T_IsBijection_238 -> T_IsInjection_92 #

d_surjective_210 :: T_IsBijection_238 -> AgdaAny -> T_Σ_14 #

d__'8776'__214 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> () #

d__'8777'__216 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> () #

d_Carrier_218 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> () #

d_isEquivalence_220 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsEquivalence_26 #

du_isEquivalence_220 :: T_IsBijection_238 -> T_IsEquivalence_26 #

d_isPartialEquivalence_222 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_222 :: T_IsBijection_238 -> T_IsPartialEquivalence_16 #

d_partialSetoid_224 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_PartialSetoid_10 #

du_partialSetoid_224 :: T_IsBijection_238 -> T_PartialSetoid_10 #

d_refl_226 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny #

du_refl_226 :: T_IsBijection_238 -> AgdaAny -> AgdaAny #

d_reflexive_228 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_228 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_230 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_Setoid_44 #

du_setoid_230 :: T_IsBijection_238 -> T_Setoid_44 #

d_sym_232 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_232 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_234 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_234 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__238 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> () #

d__'8777'__240 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> () #

d_Carrier_242 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> () #

d_isEquivalence_244 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsEquivalence_26 #

du_isEquivalence_244 :: T_IsBijection_238 -> T_IsEquivalence_26 #

d_isPartialEquivalence_246 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_246 :: T_IsBijection_238 -> T_IsPartialEquivalence_16 #

d_partialSetoid_248 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_PartialSetoid_10 #

du_partialSetoid_248 :: T_IsBijection_238 -> T_PartialSetoid_10 #

d_refl_250 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny #

du_refl_250 :: T_IsBijection_238 -> AgdaAny -> AgdaAny #

d_reflexive_252 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_252 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_254 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_Setoid_44 #

du_setoid_254 :: T_IsBijection_238 -> T_Setoid_44 #

d_sym_256 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_256 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_258 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_258 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_262 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence'8321'_264 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_266 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

d__'8776'__270 :: 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 -> () #

d__'8777'__272 :: 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 -> () #

d_Carrier_274 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> () #

d_isEquivalence_276 :: 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 #

du_isEquivalence_276 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

d_isPartialEquivalence_278 :: 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 #

du_isPartialEquivalence_278 :: T_IsCongruent_22 -> T_IsPartialEquivalence_16 #

d_partialSetoid_280 :: 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 #

du_partialSetoid_280 :: T_IsCongruent_22 -> T_PartialSetoid_10 #

d_refl_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 #

du_refl_282 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny #

d_reflexive_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 -> T__'8801'__12 -> AgdaAny #

du_reflexive_284 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_286 :: 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 #

du_setoid_286 :: (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> T_Setoid_44 #

d_sym_288 :: 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 #

du_sym_288 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_290 :: 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 #

du_trans_290 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__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 -> () #

d__'8777'__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 -> () #

d_Carrier_298 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> () #

d_isEquivalence_300 :: 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 #

du_isEquivalence_300 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

d_isPartialEquivalence_302 :: 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 #

du_isPartialEquivalence_302 :: T_IsCongruent_22 -> T_IsPartialEquivalence_16 #

d_partialSetoid_304 :: 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 #

du_partialSetoid_304 :: T_IsCongruent_22 -> T_PartialSetoid_10 #

d_refl_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 #

du_refl_306 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny #

d_reflexive_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 -> T__'8801'__12 -> AgdaAny #

du_reflexive_308 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_310 :: 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 #

du_setoid_310 :: (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> T_Setoid_44 #

d_sym_312 :: 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 #

du_sym_312 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_314 :: 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 #

du_trans_314 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_320 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_322 :: T_IsInjection_92 -> T_IsCongruent_22 #

d_isCongruent_656 :: T_IsSurjection_162 -> T_IsCongruent_22 #

d_strictlySurjective_662 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> AgdaAny -> T_Σ_14 #

du_strictlySurjective_662 :: (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> AgdaAny -> T_Σ_14 #

d_surjective_664 :: T_IsSurjection_162 -> AgdaAny -> T_Σ_14 #

d_Func_714 :: p -> p -> p -> p -> p -> p -> () #

data T_Func_714 #

Constructors

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

d_to_720 :: T_Func_714 -> AgdaAny -> AgdaAny #

d_cong_722 :: T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_724 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_IsCongruent_22 #

du_isCongruent_724 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_IsCongruent_22 #

d__'8776'__730 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> () #

d__'8777'__732 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> () #

d_Carrier_734 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> () #

d_isEquivalence_736 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_IsEquivalence_26 #

du_isEquivalence_736 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_IsEquivalence_26 #

d_isPartialEquivalence_738 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_738 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_IsPartialEquivalence_16 #

d_partialSetoid_740 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_PartialSetoid_10 #

du_partialSetoid_740 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_PartialSetoid_10 #

d_refl_742 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny #

du_refl_742 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny #

d_reflexive_744 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_744 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_746 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_Setoid_44 #

du_setoid_746 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_Setoid_44 #

d_sym_748 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_748 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_750 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_750 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__754 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> () #

d__'8777'__756 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> () #

d_Carrier_758 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> () #

d_isEquivalence_760 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_IsEquivalence_26 #

du_isEquivalence_760 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_IsEquivalence_26 #

d_isPartialEquivalence_762 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_762 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_IsPartialEquivalence_16 #

d_partialSetoid_764 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_PartialSetoid_10 #

du_partialSetoid_764 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_PartialSetoid_10 #

d_refl_766 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny #

du_refl_766 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny #

d_reflexive_768 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_768 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_770 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_Setoid_44 #

du_setoid_770 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_Setoid_44 #

d_sym_772 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_772 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_774 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_774 :: T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_Injection_776 :: p -> p -> p -> p -> p -> p -> () #

data T_Injection_776 #

Constructors

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

d_to_784 :: T_Injection_776 -> AgdaAny -> AgdaAny #

d_cong_786 :: T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_788 :: T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_function_790 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_Func_714 #

du_function_790 :: T_Injection_776 -> T_Func_714 #

d_isCongruent_794 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsCongruent_22 #

du_isCongruent_794 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsCongruent_22 #

d__'8776'__798 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> () #

d__'8777'__800 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> () #

d_Carrier_802 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> () #

d_isEquivalence_804 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsEquivalence_26 #

du_isEquivalence_804 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsEquivalence_26 #

d_isPartialEquivalence_806 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_806 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsPartialEquivalence_16 #

d_partialSetoid_808 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_PartialSetoid_10 #

du_partialSetoid_808 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_PartialSetoid_10 #

d_refl_810 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny #

du_refl_810 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny #

d_reflexive_812 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_812 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_814 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_Setoid_44 #

du_setoid_814 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_Setoid_44 #

d_sym_816 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_816 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_818 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_818 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__822 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> () #

d__'8777'__824 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> () #

d_Carrier_826 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> () #

d_isEquivalence_828 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsEquivalence_26 #

du_isEquivalence_828 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsEquivalence_26 #

d_isPartialEquivalence_830 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_830 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsPartialEquivalence_16 #

d_partialSetoid_832 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_PartialSetoid_10 #

du_partialSetoid_832 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_PartialSetoid_10 #

d_refl_834 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny #

du_refl_834 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny #

d_reflexive_836 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_836 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_838 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_Setoid_44 #

du_setoid_838 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_Setoid_44 #

d_sym_840 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_840 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_842 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_842 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isInjection_844 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsInjection_92 #

du_isInjection_844 :: T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_IsInjection_92 #

d_Surjection_846 :: p -> p -> p -> p -> p -> p -> () #

data T_Surjection_846 #

Constructors

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

d_to_854 :: T_Surjection_846 -> AgdaAny -> AgdaAny #

d_cong_856 :: T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_surjective_858 :: T_Surjection_846 -> AgdaAny -> T_Σ_14 #

d_function_860 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_Func_714 #

du_function_860 :: T_Surjection_846 -> T_Func_714 #

d_isCongruent_864 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsCongruent_22 #

du_isCongruent_864 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsCongruent_22 #

d__'8776'__868 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> () #

d__'8777'__870 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> () #

d_Carrier_872 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> () #

d_isEquivalence_874 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsEquivalence_26 #

du_isEquivalence_874 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsEquivalence_26 #

d_isPartialEquivalence_876 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_876 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsPartialEquivalence_16 #

d_partialSetoid_878 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_PartialSetoid_10 #

du_partialSetoid_878 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_PartialSetoid_10 #

d_refl_880 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny #

du_refl_880 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny #

d_reflexive_882 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_882 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_884 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_Setoid_44 #

du_setoid_884 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_Setoid_44 #

d_sym_886 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_886 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_888 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_888 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__892 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> () #

d__'8777'__894 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> () #

d_Carrier_896 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> () #

d_isEquivalence_898 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsEquivalence_26 #

du_isEquivalence_898 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsEquivalence_26 #

d_isPartialEquivalence_900 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_900 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsPartialEquivalence_16 #

d_partialSetoid_902 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_PartialSetoid_10 #

du_partialSetoid_902 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_PartialSetoid_10 #

d_refl_904 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny #

du_refl_904 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny #

d_reflexive_906 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_906 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_908 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_Setoid_44 #

du_setoid_908 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_Setoid_44 #

d_sym_910 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_910 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_912 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_912 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isSurjection_914 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsSurjection_162 #

du_isSurjection_914 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_IsSurjection_162 #

d_strictlySurjective_918 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> T_Σ_14 #

du_strictlySurjective_918 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> T_Σ_14 #

d_to'8315'_920 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny #

du_to'8315'_920 :: T_Surjection_846 -> AgdaAny -> AgdaAny #

d_to'8728'to'8315'_924 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny #

du_to'8728'to'8315'_924 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> AgdaAny -> AgdaAny #

d_Bijection_926 :: p -> p -> p -> p -> p -> p -> () #

data T_Bijection_926 #

Constructors

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

d_to_934 :: T_Bijection_926 -> AgdaAny -> AgdaAny #

d_cong_936 :: T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_bijective_938 :: T_Bijection_926 -> T_Σ_14 #

d_injective_940 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_injective_940 :: T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_surjective_942 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> T_Σ_14 #

du_surjective_942 :: T_Bijection_926 -> AgdaAny -> T_Σ_14 #

d_injection_944 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Injection_776 #

du_injection_944 :: T_Bijection_926 -> T_Injection_776 #

d_surjection_946 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Surjection_846 #

du_surjection_946 :: T_Bijection_926 -> T_Surjection_846 #

d_isInjection_950 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsInjection_92 #

du_isInjection_950 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsInjection_92 #

d_isSurjection_954 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsSurjection_162 #

du_isSurjection_954 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsSurjection_162 #

d_strictlySurjective_956 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> T_Σ_14 #

du_strictlySurjective_956 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> T_Σ_14 #

d_to'8315'_958 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny #

du_to'8315'_958 :: T_Bijection_926 -> AgdaAny -> AgdaAny #

d_isBijection_960 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238 #

du_isBijection_960 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238 #

d__'8776'__966 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> () #

d__'8777'__968 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> () #

d_Carrier_970 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> () #

d_isEquivalence_972 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsEquivalence_26 #

du_isEquivalence_972 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsEquivalence_26 #

d_isPartialEquivalence_974 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_974 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsPartialEquivalence_16 #

d_partialSetoid_976 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_PartialSetoid_10 #

du_partialSetoid_976 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_PartialSetoid_10 #

d_refl_978 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny #

du_refl_978 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny #

d_reflexive_980 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_980 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_982 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Setoid_44 #

du_setoid_982 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Setoid_44 #

d_sym_984 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_984 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_986 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_986 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__990 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> () #

d__'8777'__992 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> () #

d_Carrier_994 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> () #

d_isEquivalence_996 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsEquivalence_26 #

du_isEquivalence_996 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsEquivalence_26 #

d_isPartialEquivalence_998 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_998 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1000 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_PartialSetoid_10 #

du_partialSetoid_1000 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_PartialSetoid_10 #

d_refl_1002 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny #

du_refl_1002 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny #

d_reflexive_1004 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1004 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1006 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Setoid_44 #

du_setoid_1006 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Setoid_44 #

d_sym_1008 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1008 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1010 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1010 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__1030 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1032 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> () #

d_IsBiInverse_1044 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsCongruent_1048 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsInverse_1052 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsLeftInverse_1054 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsRightInverse_1056 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsSplitSurjection_1058 :: p -> p -> p -> p -> p -> p -> p -> () #

d_from'8321''45'cong_1126 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'8322''45'cong_1128 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'691'_1130 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'737'_1132 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_to'45'isCongruent_1140 :: T_IsBiInverse_666 -> T_IsCongruent_22 #

d_cong_1262 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence'8321'_1264 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_1266 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

d_inverse'691'_1382 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isLeftInverse_1392 :: T_IsInverse_490 -> T_IsLeftInverse_322 #

d__'8776'__1406 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1408 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1410 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> () #

d_isEquivalence_1412 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsEquivalence_26 #

du_isEquivalence_1412 :: T_IsInverse_490 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1414 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1414 :: T_IsInverse_490 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1416 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_PartialSetoid_10 #

du_partialSetoid_1416 :: T_IsInverse_490 -> T_PartialSetoid_10 #

d_refl_1418 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny #

du_refl_1418 :: T_IsInverse_490 -> AgdaAny -> AgdaAny #

d_reflexive_1420 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1420 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1422 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_Setoid_44 #

du_setoid_1422 :: T_IsInverse_490 -> T_Setoid_44 #

d_sym_1424 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1424 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1426 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1426 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__1430 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1432 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1434 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> () #

d_isEquivalence_1436 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsEquivalence_26 #

du_isEquivalence_1436 :: T_IsInverse_490 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1438 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1438 :: T_IsInverse_490 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1440 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_PartialSetoid_10 #

du_partialSetoid_1440 :: T_IsInverse_490 -> T_PartialSetoid_10 #

d_refl_1442 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny #

du_refl_1442 :: T_IsInverse_490 -> AgdaAny -> AgdaAny #

d_reflexive_1444 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1444 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1446 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_Setoid_44 #

du_setoid_1446 :: T_IsInverse_490 -> T_Setoid_44 #

d_sym_1448 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1448 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1450 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1450 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'45'cong_1454 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'737'_1456 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_1458 :: T_IsLeftInverse_322 -> T_IsCongruent_22 #

d_isSurjection_1464 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsSurjection_162 #

du_isSurjection_1464 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsSurjection_162 #

d_strictlyInverse'737'_1466 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

du_strictlyInverse'737'_1466 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

d__'8776'__1472 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1474 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1476 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> () #

d_isEquivalence_1478 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsEquivalence_26 #

du_isEquivalence_1478 :: T_IsLeftInverse_322 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1480 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1480 :: T_IsLeftInverse_322 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1482 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_PartialSetoid_10 #

du_partialSetoid_1482 :: T_IsLeftInverse_322 -> T_PartialSetoid_10 #

d_refl_1484 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

du_refl_1484 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

d_reflexive_1486 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1486 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1488 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_Setoid_44 #

du_setoid_1488 :: T_IsLeftInverse_322 -> T_Setoid_44 #

d_sym_1490 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1490 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1492 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1492 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__1496 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1498 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1500 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> () #

d_isEquivalence_1502 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsEquivalence_26 #

du_isEquivalence_1502 :: T_IsLeftInverse_322 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1504 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1504 :: T_IsLeftInverse_322 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1506 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_PartialSetoid_10 #

du_partialSetoid_1506 :: T_IsLeftInverse_322 -> T_PartialSetoid_10 #

d_refl_1508 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

du_refl_1508 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

d_reflexive_1510 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1510 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1512 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_Setoid_44 #

du_setoid_1512 :: T_IsLeftInverse_322 -> T_Setoid_44 #

d_sym_1514 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1514 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1516 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1516 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'45'cong_1520 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'691'_1522 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_1524 :: T_IsRightInverse_408 -> T_IsCongruent_22 #

d_strictlyInverse'691'_1530 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

du_strictlyInverse'691'_1530 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

d__'8776'__1536 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1538 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1540 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> () #

d_isEquivalence_1542 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_IsEquivalence_26 #

du_isEquivalence_1542 :: T_IsRightInverse_408 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1544 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1544 :: T_IsRightInverse_408 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1546 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_PartialSetoid_10 #

du_partialSetoid_1546 :: T_IsRightInverse_408 -> T_PartialSetoid_10 #

d_refl_1548 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

du_refl_1548 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

d_reflexive_1550 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1550 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1552 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_Setoid_44 #

du_setoid_1552 :: T_IsRightInverse_408 -> T_Setoid_44 #

d_sym_1554 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1554 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1556 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1556 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__1560 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1562 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1564 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> () #

d_isEquivalence_1566 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_IsEquivalence_26 #

du_isEquivalence_1566 :: T_IsRightInverse_408 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1568 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1568 :: T_IsRightInverse_408 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1570 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_PartialSetoid_10 #

du_partialSetoid_1570 :: T_IsRightInverse_408 -> T_PartialSetoid_10 #

d_refl_1572 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

du_refl_1572 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

d_reflexive_1574 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1574 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1576 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_Setoid_44 #

du_setoid_1576 :: T_IsRightInverse_408 -> T_Setoid_44 #

d_sym_1578 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1578 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1580 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1580 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from_1584 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny #

d_isLeftInverse_1596 :: T_IsSplitSurjection_752 -> T_IsLeftInverse_322 #

d_Equivalence_1714 :: p -> p -> p -> p -> p -> p -> () #

data T_Equivalence_1714 #

Constructors

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

d_to_1724 :: T_Equivalence_1714 -> AgdaAny -> AgdaAny #

d_from_1726 :: T_Equivalence_1714 -> AgdaAny -> AgdaAny #

d_to'45'cong_1728 :: T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'45'cong_1730 :: T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_toFunction_1732 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_Func_714 #

du_toFunction_1732 :: T_Equivalence_1714 -> T_Func_714 #

d_isCongruent_1736 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsCongruent_22 #

du_isCongruent_1736 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsCongruent_22 #

d__'8776'__1740 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1742 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1744 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> () #

d_isEquivalence_1746 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsEquivalence_26 #

du_isEquivalence_1746 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1748 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1748 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1750 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_PartialSetoid_10 #

du_partialSetoid_1750 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_PartialSetoid_10 #

d_refl_1752 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny #

du_refl_1752 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny #

d_reflexive_1754 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1754 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1756 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_Setoid_44 #

du_setoid_1756 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_Setoid_44 #

d_sym_1758 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1758 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1760 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1760 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__1764 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1766 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1768 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> () #

d_isEquivalence_1770 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsEquivalence_26 #

du_isEquivalence_1770 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1772 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1772 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1774 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_PartialSetoid_10 #

du_partialSetoid_1774 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_PartialSetoid_10 #

d_refl_1776 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny #

du_refl_1776 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny #

d_reflexive_1778 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1778 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1780 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_Setoid_44 #

du_setoid_1780 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_Setoid_44 #

d_sym_1782 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1782 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1784 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1784 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_fromFunction_1786 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_Func_714 #

du_fromFunction_1786 :: T_Equivalence_1714 -> T_Func_714 #

d_isCongruent_1790 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsCongruent_22 #

du_isCongruent_1790 :: T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_IsCongruent_22 #

d_LeftInverse_1792 :: p -> p -> p -> p -> p -> p -> () #

data T_LeftInverse_1792 #

Constructors

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

d_to_1804 :: T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

d_from_1806 :: T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

d_to'45'cong_1808 :: T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'45'cong_1810 :: T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'737'_1812 :: T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_1814 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsCongruent_22 #

du_isCongruent_1814 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsCongruent_22 #

d_isLeftInverse_1816 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsLeftInverse_322 #

du_isLeftInverse_1816 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsLeftInverse_322 #

d_isSurjection_1820 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsSurjection_162 #

du_isSurjection_1820 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsSurjection_162 #

d_strictlyInverse'737'_1822 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

du_strictlyInverse'737'_1822 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

d__'8776'__1826 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1828 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1830 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> () #

d_isEquivalence_1832 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsEquivalence_26 #

du_isEquivalence_1832 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1834 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1834 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1836 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_PartialSetoid_10 #

du_partialSetoid_1836 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_PartialSetoid_10 #

d_refl_1838 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

du_refl_1838 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

d_reflexive_1840 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1840 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1842 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Setoid_44 #

du_setoid_1842 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Setoid_44 #

d_sym_1844 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1844 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1846 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1846 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__1850 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1852 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1854 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> () #

d_isEquivalence_1856 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsEquivalence_26 #

du_isEquivalence_1856 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1858 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1858 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1860 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_PartialSetoid_10 #

du_partialSetoid_1860 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_PartialSetoid_10 #

d_refl_1862 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

du_refl_1862 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

d_reflexive_1864 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1864 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1866 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Setoid_44 #

du_setoid_1866 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Setoid_44 #

d_sym_1868 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1868 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1870 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1870 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_equivalence_1872 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Equivalence_1714 #

du_equivalence_1872 :: T_LeftInverse_1792 -> T_Equivalence_1714 #

d_isSplitSurjection_1874 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsSplitSurjection_752 #

du_isSplitSurjection_1874 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsSplitSurjection_752 #

d_surjection_1876 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Surjection_846 #

du_surjection_1876 :: T_LeftInverse_1792 -> T_Surjection_846 #

d_RightInverse_1880 :: p -> p -> p -> p -> p -> p -> () #

data T_RightInverse_1880 #

Constructors

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

d_to_1892 :: T_RightInverse_1880 -> AgdaAny -> AgdaAny #

d_from_1894 :: T_RightInverse_1880 -> AgdaAny -> AgdaAny #

d_to'45'cong_1896 :: T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'45'cong_1898 :: T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'691'_1900 :: T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_1902 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsCongruent_22 #

du_isCongruent_1902 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsCongruent_22 #

d_isRightInverse_1904 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsRightInverse_408 #

du_isRightInverse_1904 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsRightInverse_408 #

d_strictlyInverse'691'_1908 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny #

du_strictlyInverse'691'_1908 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny #

d__'8776'__1912 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1914 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1916 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> () #

d_isEquivalence_1918 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsEquivalence_26 #

du_isEquivalence_1918 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1920 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1920 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1922 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_PartialSetoid_10 #

du_partialSetoid_1922 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_PartialSetoid_10 #

d_refl_1924 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny #

du_refl_1924 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny #

d_reflexive_1926 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1926 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1928 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_Setoid_44 #

du_setoid_1928 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_Setoid_44 #

d_sym_1930 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1930 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1932 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1932 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__1936 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> () #

d__'8777'__1938 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> () #

d_Carrier_1940 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> () #

d_isEquivalence_1942 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsEquivalence_26 #

du_isEquivalence_1942 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsEquivalence_26 #

d_isPartialEquivalence_1944 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_1944 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsPartialEquivalence_16 #

d_partialSetoid_1946 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_PartialSetoid_10 #

du_partialSetoid_1946 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_PartialSetoid_10 #

d_refl_1948 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny #

du_refl_1948 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny #

d_reflexive_1950 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_1950 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_1952 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_Setoid_44 #

du_setoid_1952 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_Setoid_44 #

d_sym_1954 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_1954 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_1956 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_1956 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_equivalence_1958 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_Equivalence_1714 #

du_equivalence_1958 :: T_RightInverse_1880 -> T_Equivalence_1714 #

d_Inverse_1960 :: p -> p -> p -> p -> p -> p -> () #

data T_Inverse_1960 #

Constructors

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

d_to_1972 :: T_Inverse_1960 -> AgdaAny -> AgdaAny #

d_from_1974 :: T_Inverse_1960 -> AgdaAny -> AgdaAny #

d_to'45'cong_1976 :: T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'45'cong_1978 :: T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse_1980 :: T_Inverse_1960 -> T_Σ_14 #

d_inverse'737'_1982 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_inverse'737'_1982 :: T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'691'_1984 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_inverse'691'_1984 :: T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_leftInverse_1986 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_LeftInverse_1792 #

du_leftInverse_1986 :: T_Inverse_1960 -> T_LeftInverse_1792 #

d_rightInverse_1988 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_RightInverse_1880 #

du_rightInverse_1988 :: T_Inverse_1960 -> T_RightInverse_1880 #

d_isLeftInverse_1992 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsLeftInverse_322 #

du_isLeftInverse_1992 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsLeftInverse_322 #

d_strictlyInverse'737'_1994 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny #

du_strictlyInverse'737'_1994 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny #

d_isRightInverse_1998 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsRightInverse_408 #

du_isRightInverse_1998 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsRightInverse_408 #

d_strictlyInverse'691'_2000 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny #

du_strictlyInverse'691'_2000 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny #

d_isInverse_2002 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsInverse_490 #

du_isInverse_2002 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsInverse_490 #

d__'8776'__2008 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> () #

d__'8777'__2010 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> () #

d_Carrier_2012 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> () #

d_isEquivalence_2014 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsEquivalence_26 #

du_isEquivalence_2014 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsEquivalence_26 #

d_isPartialEquivalence_2016 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_2016 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsPartialEquivalence_16 #

d_partialSetoid_2018 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_PartialSetoid_10 #

du_partialSetoid_2018 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_PartialSetoid_10 #

d_refl_2020 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny #

du_refl_2020 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny #

d_reflexive_2022 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_2022 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_2024 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Setoid_44 #

du_setoid_2024 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Setoid_44 #

d_sym_2026 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_2026 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_2028 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_2028 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__2032 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> () #

d__'8777'__2034 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> () #

d_Carrier_2036 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> () #

d_isEquivalence_2038 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsEquivalence_26 #

du_isEquivalence_2038 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsEquivalence_26 #

d_isPartialEquivalence_2040 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_2040 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_IsPartialEquivalence_16 #

d_partialSetoid_2042 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_PartialSetoid_10 #

du_partialSetoid_2042 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_PartialSetoid_10 #

d_refl_2044 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny #

du_refl_2044 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny #

d_reflexive_2046 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_2046 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_2048 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Setoid_44 #

du_setoid_2048 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Setoid_44 #

d_sym_2050 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_2050 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_2052 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_2052 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_BiEquivalence_2054 :: p -> p -> p -> p -> p -> p -> () #

data T_BiEquivalence_2054 #

Constructors

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

d_to_2068 :: T_BiEquivalence_2054 -> AgdaAny -> AgdaAny #

d_from'8321'_2070 :: T_BiEquivalence_2054 -> AgdaAny -> AgdaAny #

d_from'8322'_2072 :: T_BiEquivalence_2054 -> AgdaAny -> AgdaAny #

d_to'45'cong_2074 :: T_BiEquivalence_2054 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'8321''45'cong_2076 :: T_BiEquivalence_2054 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'8322''45'cong_2078 :: T_BiEquivalence_2054 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_BiInverse_2080 :: p -> p -> p -> p -> p -> p -> () #

data T_BiInverse_2080 #

Constructors

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

d_to_2098 :: T_BiInverse_2080 -> AgdaAny -> AgdaAny #

d_from'8321'_2100 :: T_BiInverse_2080 -> AgdaAny -> AgdaAny #

d_from'8322'_2102 :: T_BiInverse_2080 -> AgdaAny -> AgdaAny #

d_to'45'cong_2104 :: T_BiInverse_2080 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'8321''45'cong_2106 :: T_BiInverse_2080 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'8322''45'cong_2108 :: T_BiInverse_2080 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'737'_2110 :: T_BiInverse_2080 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'691'_2112 :: T_BiInverse_2080 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_to'45'isCongruent_2114 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_BiInverse_2080 -> T_IsCongruent_22 #

du_to'45'isCongruent_2114 :: T_Setoid_44 -> T_Setoid_44 -> T_BiInverse_2080 -> T_IsCongruent_22 #

d_isBiInverse_2116 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_BiInverse_2080 -> T_IsBiInverse_666 #

du_isBiInverse_2116 :: T_Setoid_44 -> T_Setoid_44 -> T_BiInverse_2080 -> T_IsBiInverse_666 #

d_biEquivalence_2118 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_BiInverse_2080 -> T_BiEquivalence_2054 #

du_biEquivalence_2118 :: T_BiInverse_2080 -> T_BiEquivalence_2054 #

d_SplitSurjection_2120 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> () #

d_equivalence_2126 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Equivalence_1714 #

du_equivalence_2126 :: T_LeftInverse_1792 -> T_Equivalence_1714 #

d_from_2128 :: T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

d_from'45'cong_2130 :: T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'737'_2132 :: T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_2134 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsCongruent_22 #

du_isCongruent_2134 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsCongruent_22 #

d_isLeftInverse_2136 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsLeftInverse_322 #

du_isLeftInverse_2136 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsLeftInverse_322 #

d_isSplitSurjection_2138 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsSplitSurjection_752 #

du_isSplitSurjection_2138 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsSplitSurjection_752 #

d_isSurjection_2140 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsSurjection_162 #

du_isSurjection_2140 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsSurjection_162 #

d_strictlyInverse'737'_2142 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

du_strictlyInverse'737'_2142 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

d_surjection_2144 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Surjection_846 #

du_surjection_2144 :: T_LeftInverse_1792 -> T_Surjection_846 #

d_to_2146 :: T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

d_to'45'cong_2148 :: T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__2152 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> () #

d__'8777'__2154 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> () #

d_Carrier_2156 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> () #

d_isEquivalence_2158 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsEquivalence_26 #

du_isEquivalence_2158 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsEquivalence_26 #

d_isPartialEquivalence_2160 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_2160 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsPartialEquivalence_16 #

d_partialSetoid_2162 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_PartialSetoid_10 #

du_partialSetoid_2162 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_PartialSetoid_10 #

d_refl_2164 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

du_refl_2164 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

d_reflexive_2166 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_2166 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_2168 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Setoid_44 #

du_setoid_2168 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Setoid_44 #

d_sym_2170 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_2170 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_2172 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_2172 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__2176 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> () #

d__'8777'__2178 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> () #

d_Carrier_2180 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> () #

d_isEquivalence_2182 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsEquivalence_26 #

du_isEquivalence_2182 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsEquivalence_26 #

d_isPartialEquivalence_2184 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_2184 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_IsPartialEquivalence_16 #

d_partialSetoid_2186 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_PartialSetoid_10 #

du_partialSetoid_2186 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_PartialSetoid_10 #

d_refl_2188 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

du_refl_2188 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny #

d_reflexive_2190 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_2190 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_2192 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Setoid_44 #

du_setoid_2192 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_Setoid_44 #

d_sym_2194 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_2194 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_2196 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_2196 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'10230''8347'__2198 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> () #

d__'10230'__2200 :: T_Level_18 -> T_Level_18 -> () -> () -> () #

d__'8611'__2206 :: T_Level_18 -> T_Level_18 -> () -> () -> () #

d__'8608'__2212 :: T_Level_18 -> T_Level_18 -> () -> () -> () #

d__'10518'__2218 :: T_Level_18 -> T_Level_18 -> () -> () -> () #

d__'8660'__2224 :: T_Level_18 -> T_Level_18 -> () -> () -> () #

d__'8617'__2230 :: T_Level_18 -> T_Level_18 -> () -> () -> () #

d__'8618'__2236 :: T_Level_18 -> T_Level_18 -> () -> () -> () #

d__'8617''8618'__2242 :: T_Level_18 -> T_Level_18 -> () -> () -> () #

d__'8596'__2248 :: T_Level_18 -> T_Level_18 -> () -> () -> () #

d_mk'10230'_2266 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> T_Func_714 #

du_mk'10230'_2266 :: (AgdaAny -> AgdaAny) -> T_Func_714 #

d_mk'8611'_2272 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_Injection_776 #

du_mk'8611'_2272 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_Injection_776 #

d_mk'8608'_2280 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> T_Surjection_846 #

du_mk'8608'_2280 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> T_Surjection_846 #

d_mk'10518'_2288 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Bijection_926 #

du_mk'10518'_2288 :: (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Bijection_926 #

d_mk'8660'_2298 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714 #

du_mk'8660'_2298 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714 #

d_mk'8617'_2308 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_LeftInverse_1792 #

du_mk'8617'_2308 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_LeftInverse_1792 #

d_mk'8618'_2320 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_RightInverse_1880 #

du_mk'8618'_2320 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_RightInverse_1880 #

d_mk'8617''8618'_2334 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_BiInverse_2080 #

du_mk'8617''8618'_2334 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_BiInverse_2080 #

d_mk'8596'_2350 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Inverse_1960 #

du_mk'8596'_2350 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Inverse_1960 #

d_mk'8608''8347'_2360 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> T_Surjection_846 #

du_mk'8608''8347'_2360 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> T_Surjection_846 #

d_mk'8596''8347''8242'_2366 :: T_Level_18 -> T_Level_18 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> (AgdaAny -> T__'8801'__12) -> T_Inverse_1960 #

du_mk'8596''8347''8242'_2366 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960 #

d__'10216''36''10217'__2392 :: T_Func_714 -> AgdaAny -> AgdaAny #