Documentation

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

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

d_IsBijection_46 ∷ p → p → p → p → p → p → p → () Source #

d_IsCongruent_48 ∷ p → p → p → p → p → p → p → () Source #

d_IsInjection_50 ∷ p → p → p → p → p → p → p → () Source #

d_IsSurjection_60 ∷ p → p → p → p → p → p → p → () Source #

d_isInjection_204 ∷ T_IsBijection_238 → T_IsInjection_92 Source #

d_surjective_210 ∷ T_IsBijection_238 → AgdaAny → T_Σ_14 Source #

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 → () Source #

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 → () Source #

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 → () Source #

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

du_isEquivalence_220 ∷ T_IsBijection_238 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_222 ∷ T_IsBijection_238 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_224 ∷ T_IsBijection_238 → T_PartialSetoid_10 Source #

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

du_refl_226 ∷ T_IsBijection_238 → AgdaAny → AgdaAny Source #

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

du_reflexive_228 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_230 ∷ T_IsBijection_238 → T_Setoid_44 Source #

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

du_sym_232 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_234 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

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 → () Source #

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

du_isEquivalence_244 ∷ T_IsBijection_238 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_246 ∷ T_IsBijection_238 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_248 ∷ T_IsBijection_238 → T_PartialSetoid_10 Source #

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

du_refl_250 ∷ T_IsBijection_238 → AgdaAny → AgdaAny Source #

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

du_reflexive_252 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_254 ∷ T_IsBijection_238 → T_Setoid_44 Source #

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

du_sym_256 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_258 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_262 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_264 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_266 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

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 → () Source #

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 → () Source #

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 → () Source #

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

du_isEquivalence_276 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_278 ∷ T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_280 ∷ T_IsCongruent_22 → T_PartialSetoid_10 Source #

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

du_refl_282 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny Source #

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

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

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

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

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

du_sym_288 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_290 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

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 → () Source #

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

du_isEquivalence_300 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_302 ∷ T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_304 ∷ T_IsCongruent_22 → T_PartialSetoid_10 Source #

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

du_refl_306 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny Source #

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

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

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

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

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

du_sym_312 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_314 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_320 ∷ T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_322 ∷ T_IsInjection_92 → T_IsCongruent_22 Source #

d_isCongruent_656 ∷ T_IsSurjection_162 → T_IsCongruent_22 Source #

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

du_strictlySurjective_662 ∷ (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → T_Σ_14 Source #

d_surjective_664 ∷ T_IsSurjection_162 → AgdaAny → T_Σ_14 Source #

d_Func_714 ∷ p → p → p → p → p → p → () Source #

data T_Func_714 Source #

d_to_720 ∷ T_Func_714 → AgdaAny → AgdaAny Source #

d_cong_722 ∷ T_Func_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_isCongruent_724 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → T_IsCongruent_22 Source #

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 → () Source #

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 → () Source #

d_Carrier_734 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_714 → () Source #

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

du_isEquivalence_736 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_738 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_740 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → T_PartialSetoid_10 Source #

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

du_refl_742 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → AgdaAny → AgdaAny Source #

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

du_reflexive_744 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_746 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → T_Setoid_44 Source #

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

du_sym_748 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_750 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

d_Carrier_758 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Func_714 → () Source #

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

du_isEquivalence_760 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_762 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_764 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → T_PartialSetoid_10 Source #

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

du_refl_766 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → AgdaAny → AgdaAny Source #

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

du_reflexive_768 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_770 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → T_Setoid_44 Source #

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

du_sym_772 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_774 ∷ T_Setoid_44 → T_Setoid_44 → T_Func_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Injection_776 ∷ p → p → p → p → p → p → () Source #

data T_Injection_776 Source #

d_to_784 ∷ T_Injection_776 → AgdaAny → AgdaAny Source #

d_cong_786 ∷ T_Injection_776 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_788 ∷ T_Injection_776 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_function_790 ∷ T_Injection_776 → T_Func_714 Source #

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

du_isCongruent_794 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → T_IsCongruent_22 Source #

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 → () Source #

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 → () Source #

d_Carrier_802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_776 → () Source #

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

du_isEquivalence_804 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_806 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_808 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → T_PartialSetoid_10 Source #

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

du_refl_810 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny Source #

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

du_reflexive_812 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_814 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → T_Setoid_44 Source #

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

du_sym_816 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_818 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

d_Carrier_826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Injection_776 → () Source #

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

du_isEquivalence_828 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_830 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_832 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → T_PartialSetoid_10 Source #

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

du_refl_834 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny Source #

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

du_reflexive_836 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_838 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → T_Setoid_44 Source #

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

du_sym_840 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_842 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_isInjection_844 ∷ T_Setoid_44 → T_Setoid_44 → T_Injection_776 → T_IsInjection_92 Source #

d_Surjection_846 ∷ p → p → p → p → p → p → () Source #

data T_Surjection_846 Source #

d_to_854 ∷ T_Surjection_846 → AgdaAny → AgdaAny Source #

d_cong_856 ∷ T_Surjection_846 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_surjective_858 ∷ T_Surjection_846 → AgdaAny → T_Σ_14 Source #

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

du_function_860 ∷ T_Surjection_846 → T_Func_714 Source #

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

du_isCongruent_864 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → T_IsCongruent_22 Source #

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 → () Source #

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 → () Source #

d_Carrier_872 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → () Source #

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

du_isEquivalence_874 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_876 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_878 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → T_PartialSetoid_10 Source #

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

du_refl_880 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → AgdaAny → AgdaAny Source #

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

du_reflexive_882 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_884 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → T_Setoid_44 Source #

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

du_sym_886 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_888 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

d_Carrier_896 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → () Source #

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

du_isEquivalence_898 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_900 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_902 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → T_PartialSetoid_10 Source #

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

du_refl_904 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → AgdaAny → AgdaAny Source #

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

du_reflexive_906 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_908 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → T_Setoid_44 Source #

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

du_sym_910 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_912 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_isSurjection_914 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → T_IsSurjection_162 Source #

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

du_strictlySurjective_918 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → AgdaAny → T_Σ_14 Source #

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

du_to'8315'_920 ∷ T_Surjection_846 → AgdaAny → AgdaAny Source #

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

du_to'8728'to'8315'_924 ∷ T_Setoid_44 → T_Setoid_44 → T_Surjection_846 → AgdaAny → AgdaAny Source #

d_Bijection_926 ∷ p → p → p → p → p → p → () Source #

data T_Bijection_926 Source #

d_to_934 ∷ T_Bijection_926 → AgdaAny → AgdaAny Source #

d_cong_936 ∷ T_Bijection_926 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_bijective_938 ∷ T_Bijection_926 → T_Σ_14 Source #

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

du_injective_940 ∷ T_Bijection_926 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_surjective_942 ∷ T_Bijection_926 → AgdaAny → T_Σ_14 Source #

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

du_injection_944 ∷ T_Bijection_926 → T_Injection_776 Source #

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

du_surjection_946 ∷ T_Bijection_926 → T_Surjection_846 Source #

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

du_isInjection_950 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_IsInjection_92 Source #

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

du_isSurjection_954 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_IsSurjection_162 Source #

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

du_strictlySurjective_956 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → T_Σ_14 Source #

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

du_to'8315'_958 ∷ T_Bijection_926 → AgdaAny → AgdaAny Source #

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

du_isBijection_960 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_IsBijection_238 Source #

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 → () Source #

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 → () Source #

d_Carrier_970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → () Source #

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

du_isEquivalence_972 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_974 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_976 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_PartialSetoid_10 Source #

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

du_refl_978 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny Source #

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

du_reflexive_980 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_982 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_Setoid_44 Source #

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

du_sym_984 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_986 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

d_Carrier_994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → () Source #

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

du_isEquivalence_996 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_998 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1000 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_PartialSetoid_10 Source #

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

du_refl_1002 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny Source #

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

du_reflexive_1004 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1006 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_Setoid_44 Source #

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

du_sym_1008 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1010 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_IsBiInverse_1044 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_IsCongruent_1048 ∷ p → p → p → p → p → p → p → () Source #

d_IsInverse_1052 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsLeftInverse_1054 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsRightInverse_1056 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSplitSurjection_1058 ∷ p → p → p → p → p → p → p → () Source #

d_from'8321''45'cong_1126 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'8322''45'cong_1128 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_1130 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_1132 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_to'45'isCongruent_1140 ∷ T_IsBiInverse_666 → T_IsCongruent_22 Source #

d_cong_1262 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_1264 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_1266 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

d_inverse'691'_1382 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isLeftInverse_1392 ∷ T_IsInverse_490 → T_IsLeftInverse_322 Source #

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 → () Source #

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 → () Source #

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 → () Source #

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

du_isEquivalence_1412 ∷ T_IsInverse_490 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1414 ∷ T_IsInverse_490 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1416 ∷ T_IsInverse_490 → T_PartialSetoid_10 Source #

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

du_refl_1418 ∷ T_IsInverse_490 → AgdaAny → AgdaAny Source #

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

du_reflexive_1420 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1422 ∷ T_IsInverse_490 → T_Setoid_44 Source #

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

du_sym_1424 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1426 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

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 → () Source #

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

du_isEquivalence_1436 ∷ T_IsInverse_490 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1438 ∷ T_IsInverse_490 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1440 ∷ T_IsInverse_490 → T_PartialSetoid_10 Source #

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

du_refl_1442 ∷ T_IsInverse_490 → AgdaAny → AgdaAny Source #

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

du_reflexive_1444 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1446 ∷ T_IsInverse_490 → T_Setoid_44 Source #

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

du_sym_1448 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1450 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_1454 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_1456 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_1458 ∷ T_IsLeftInverse_322 → T_IsCongruent_22 Source #

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

du_isSurjection_1464 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_IsSurjection_162 Source #

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

du_strictlyInverse'737'_1466 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

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 → () Source #

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

du_isEquivalence_1478 ∷ T_IsLeftInverse_322 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1480 ∷ T_IsLeftInverse_322 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1482 ∷ T_IsLeftInverse_322 → T_PartialSetoid_10 Source #

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

du_refl_1484 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny Source #

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

du_reflexive_1486 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1488 ∷ T_IsLeftInverse_322 → T_Setoid_44 Source #

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

du_sym_1490 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1492 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

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 → () Source #

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

du_isEquivalence_1502 ∷ T_IsLeftInverse_322 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1504 ∷ T_IsLeftInverse_322 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1506 ∷ T_IsLeftInverse_322 → T_PartialSetoid_10 Source #

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

du_refl_1508 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny Source #

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

du_reflexive_1510 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1512 ∷ T_IsLeftInverse_322 → T_Setoid_44 Source #

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

du_sym_1514 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1516 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_1520 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_1522 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_1524 ∷ T_IsRightInverse_408 → T_IsCongruent_22 Source #

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

du_strictlyInverse'691'_1530 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

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 → () Source #

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

du_isEquivalence_1542 ∷ T_IsRightInverse_408 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1544 ∷ T_IsRightInverse_408 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1546 ∷ T_IsRightInverse_408 → T_PartialSetoid_10 Source #

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

du_refl_1548 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny Source #

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

du_reflexive_1550 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1552 ∷ T_IsRightInverse_408 → T_Setoid_44 Source #

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

du_sym_1554 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1556 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

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 → () Source #

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

du_isEquivalence_1566 ∷ T_IsRightInverse_408 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1568 ∷ T_IsRightInverse_408 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1570 ∷ T_IsRightInverse_408 → T_PartialSetoid_10 Source #

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

du_refl_1572 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny Source #

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

du_reflexive_1574 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1576 ∷ T_IsRightInverse_408 → T_Setoid_44 Source #

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

du_sym_1578 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1580 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from_1584 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny Source #

d_isLeftInverse_1596 ∷ T_IsSplitSurjection_752 → T_IsLeftInverse_322 Source #

d_Equivalence_1714 ∷ p → p → p → p → p → p → () Source #

data T_Equivalence_1714 Source #

d_to_1724 ∷ T_Equivalence_1714 → AgdaAny → AgdaAny Source #

d_from_1726 ∷ T_Equivalence_1714 → AgdaAny → AgdaAny Source #

d_to'45'cong_1728 ∷ T_Equivalence_1714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_1730 ∷ T_Equivalence_1714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_toFunction_1732 ∷ T_Equivalence_1714 → T_Func_714 Source #

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

du_isCongruent_1736 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_IsCongruent_22 Source #

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 → () Source #

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 → () Source #

d_Carrier_1744 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → () Source #

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

du_isEquivalence_1746 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1748 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1750 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_PartialSetoid_10 Source #

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

du_refl_1752 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → AgdaAny → AgdaAny Source #

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

du_reflexive_1754 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1756 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_Setoid_44 Source #

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

du_sym_1758 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1760 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

d_Carrier_1768 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → () Source #

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

du_isEquivalence_1770 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1772 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1774 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_PartialSetoid_10 Source #

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

du_refl_1776 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → AgdaAny → AgdaAny Source #

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

du_reflexive_1778 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1780 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_Setoid_44 Source #

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

du_sym_1782 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1784 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_fromFunction_1786 ∷ T_Equivalence_1714 → T_Func_714 Source #

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

du_isCongruent_1790 ∷ T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_IsCongruent_22 Source #

d_LeftInverse_1792 ∷ p → p → p → p → p → p → () Source #

data T_LeftInverse_1792 Source #

d_to_1804 ∷ T_LeftInverse_1792 → AgdaAny → AgdaAny Source #

d_from_1806 ∷ T_LeftInverse_1792 → AgdaAny → AgdaAny Source #

d_to'45'cong_1808 ∷ T_LeftInverse_1792 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_1810 ∷ T_LeftInverse_1792 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_1812 ∷ T_LeftInverse_1792 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_isCongruent_1814 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_IsCongruent_22 Source #

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

du_isLeftInverse_1816 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_IsLeftInverse_322 Source #

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

du_isSurjection_1820 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_IsSurjection_162 Source #

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

du_strictlyInverse'737'_1822 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

d_Carrier_1830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → () Source #

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

du_isEquivalence_1832 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1834 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1836 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_PartialSetoid_10 Source #

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

du_refl_1838 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → AgdaAny → AgdaAny Source #

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

du_reflexive_1840 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1842 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_Setoid_44 Source #

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

du_sym_1844 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1846 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

d_Carrier_1854 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → () Source #

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

du_isEquivalence_1856 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1858 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1860 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_PartialSetoid_10 Source #

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

du_refl_1862 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → AgdaAny → AgdaAny Source #

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

du_reflexive_1864 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1866 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_Setoid_44 Source #

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

du_sym_1868 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1870 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_equivalence_1872 ∷ T_LeftInverse_1792 → T_Equivalence_1714 Source #

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

du_isSplitSurjection_1874 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_IsSplitSurjection_752 Source #

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

du_surjection_1876 ∷ T_LeftInverse_1792 → T_Surjection_846 Source #

d_RightInverse_1880 ∷ p → p → p → p → p → p → () Source #

data T_RightInverse_1880 Source #

d_to_1892 ∷ T_RightInverse_1880 → AgdaAny → AgdaAny Source #

d_from_1894 ∷ T_RightInverse_1880 → AgdaAny → AgdaAny Source #

d_to'45'cong_1896 ∷ T_RightInverse_1880 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_1898 ∷ T_RightInverse_1880 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_1900 ∷ T_RightInverse_1880 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_isCongruent_1902 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_IsCongruent_22 Source #

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

du_isRightInverse_1904 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_IsRightInverse_408 Source #

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

du_strictlyInverse'691'_1908 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

d_Carrier_1916 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → () Source #

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

du_isEquivalence_1918 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1920 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1922 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_PartialSetoid_10 Source #

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

du_refl_1924 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny Source #

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

du_reflexive_1926 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1928 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_Setoid_44 Source #

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

du_sym_1930 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1932 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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 → () Source #

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 → () Source #

d_Carrier_1940 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → () Source #

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

du_isEquivalence_1942 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_1944 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_1946 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_PartialSetoid_10 Source #

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

du_refl_1948 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny Source #

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

du_reflexive_1950 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_setoid_1952 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_Setoid_44 Source #

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

du_sym_1954 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_trans_1956 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_equivalence_1958 ∷ T_RightInverse_1880 → T_Equivalence_1714 Source #

d_Inverse_1960 ∷ p → p → p → p → p → p → () Source #

data T_Inverse_1960 Source #

d_to_1972 ∷ T_Inverse_1960 → AgdaAny → AgdaAny Source #

d_from_1974 ∷ T_Inverse_1960 → AgdaAny → AgdaAny Source #

d_to'45'cong_1976 ∷ T_Inverse_1960 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_1978 ∷ T_Inverse_1960 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse_1980 ∷ T_Inverse_1960 → T_Σ_14 Source #

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

du_inverse'737'_1982 ∷ T_Inverse_1960 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_inverse'691'_1984 ∷ T_Inverse_1960 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_leftInverse_1986 ∷ T_Inverse_1960 → T_LeftInverse_1792 Source #

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

du_rightInverse_1988 ∷ T_Inverse_1960 → T_RightInverse_1880 Source #

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

du_isLeftInverse_1992 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → T_IsLeftInverse_322 Source #

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

du_strictlyInverse'737'_1994 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → AgdaAny → AgdaAny Source #

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

du_isRightInverse_1998 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → T_IsRightInverse_408 Source #

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

du_strictlyInverse'691'_2000 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → AgdaAny → AgdaAny Source #

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

du_isInverse_2002 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → T_IsInverse_490 Source #

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 → () Source #

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 → () Source #

d_Carrier_2012 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → () Source #

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

du_isEquivalence_2014 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_2016 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → T_IsPartialEquivalence_16 Source #

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

du_partialSetoid_2018 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → T_PartialSetoid_10 Source #

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

du_refl_2020 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → AgdaAny → AgdaAny Source #