Documentation

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

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

d_IsBijection_50 ∷ p → p → p → p → p → p → p → () Source #

d_IsCongruent_54 ∷ p → p → p → p → p → p → p → () Source #

d_IsInjection_58 ∷ p → p → p → p → p → p → p → () Source #

d_IsSurjection_78 ∷ p → p → p → p → p → p → p → () Source #

d_isInjection_232 ∷ T_IsBijection_256 → T_IsInjection_98 Source #

d_surjective_238 ∷ T_IsBijection_256 → AgdaAny → T_Σ_14 Source #

d__'8776'__242 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → () Source #

d__'8777'__244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → () Source #

d_Carrier_246 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → () Source #

d_isEquivalence_248 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsEquivalence_28 Source #

du_isEquivalence_248 ∷ T_IsBijection_256 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_250 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_250 ∷ T_IsBijection_256 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_252 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_PartialSetoid_10 Source #

du_partialSetoid_252 ∷ T_IsBijection_256 → T_PartialSetoid_10 Source #

d_rawSetoid_254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_RawSetoid_12 Source #

d_refl_256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny Source #

du_refl_256 ∷ T_IsBijection_256 → AgdaAny → AgdaAny Source #

d_reflexive_258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_258 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_Setoid_46 Source #

du_setoid_260 ∷ T_IsBijection_256 → T_Setoid_46 Source #

d_sym_262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_262 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_264 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → () Source #

d__'8777'__270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → () Source #

d_Carrier_272 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → () Source #

d_isEquivalence_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsEquivalence_28 Source #

du_isEquivalence_274 ∷ T_IsBijection_256 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_276 ∷ T_IsBijection_256 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_PartialSetoid_10 Source #

du_partialSetoid_278 ∷ T_IsBijection_256 → T_PartialSetoid_10 Source #

d_rawSetoid_280 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_RawSetoid_12 Source #

d_refl_282 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny Source #

du_refl_282 ∷ T_IsBijection_256 → AgdaAny → AgdaAny Source #

d_reflexive_284 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_286 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_Setoid_46 Source #

du_setoid_286 ∷ T_IsBijection_256 → T_Setoid_46 Source #

d_sym_288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_288 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_290 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_294 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_296 ∷ T_IsCongruent_22 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_298 ∷ T_IsCongruent_22 → T_IsEquivalence_28 Source #

d__'8776'__302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → () Source #

d__'8777'__304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → () Source #

d_Carrier_306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → () Source #

d_isEquivalence_308 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsEquivalence_28 Source #

du_isEquivalence_308 ∷ T_IsCongruent_22 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_310 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_310 ∷ T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_PartialSetoid_10 Source #

du_partialSetoid_312 ∷ T_IsCongruent_22 → T_PartialSetoid_10 Source #

d_rawSetoid_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_RawSetoid_12 Source #

d_refl_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny Source #

du_refl_316 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny Source #

d_reflexive_318 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_320 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_Setoid_46 Source #

du_setoid_320 ∷ (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_Setoid_46 Source #

d_sym_322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_322 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_324 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_324 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → () Source #

d__'8777'__330 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → () Source #

d_Carrier_332 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → () Source #

d_isEquivalence_334 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsEquivalence_28 Source #

du_isEquivalence_334 ∷ T_IsCongruent_22 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_336 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_336 ∷ T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_338 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_PartialSetoid_10 Source #

du_partialSetoid_338 ∷ T_IsCongruent_22 → T_PartialSetoid_10 Source #

d_rawSetoid_340 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_RawSetoid_12 Source #

d_refl_342 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny Source #

du_refl_342 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny Source #

d_reflexive_344 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_346 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_Setoid_46 Source #

du_setoid_346 ∷ (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_Setoid_46 Source #

d_sym_348 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_348 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_350 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_350 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_356 ∷ T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_358 ∷ T_IsInjection_98 → T_IsCongruent_22 Source #

d_isCongruent_712 ∷ T_IsSurjection_174 → T_IsCongruent_22 Source #

d_strictlySurjective_718 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → T_Σ_14 Source #

du_strictlySurjective_718 ∷ (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → T_Σ_14 Source #

d_surjective_720 ∷ T_IsSurjection_174 → AgdaAny → T_Σ_14 Source #

d_Func_774 ∷ p → p → p → p → p → p → () Source #

data T_Func_774 Source #

d_to_780 ∷ T_Func_774 → AgdaAny → AgdaAny Source #

d_cong_782 ∷ T_Func_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_784 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_IsCongruent_22 Source #

du_isCongruent_784 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_IsCongruent_22 Source #

d__'8776'__790 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → () Source #

d__'8777'__792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → () Source #

d_Carrier_794 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → () Source #

d_isEquivalence_796 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_IsEquivalence_28 Source #

du_isEquivalence_796 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_798 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_798 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_800 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_PartialSetoid_10 Source #

du_partialSetoid_800 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_PartialSetoid_10 Source #

d_rawSetoid_802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_RawSetoid_12 Source #

d_refl_804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny Source #

du_refl_804 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny Source #

d_reflexive_806 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_806 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_Setoid_46 Source #

du_setoid_808 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_Setoid_46 Source #

d_sym_810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_810 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_812 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → () Source #

d__'8777'__818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → () Source #

d_Carrier_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → () Source #

d_isEquivalence_822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_IsEquivalence_28 Source #

du_isEquivalence_822 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_824 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_824 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_PartialSetoid_10 Source #

du_partialSetoid_826 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_PartialSetoid_10 Source #

d_rawSetoid_828 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_RawSetoid_12 Source #

d_refl_830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny Source #

du_refl_830 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny Source #

d_reflexive_832 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_832 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_834 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_Setoid_46 Source #

du_setoid_834 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_Setoid_46 Source #

d_sym_836 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_836 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_838 ∷ T_Setoid_46 → T_Setoid_46 → T_Func_774 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_Injection_842 ∷ p → p → p → p → p → p → () Source #

data T_Injection_842 Source #

d_to_850 ∷ T_Injection_842 → AgdaAny → AgdaAny Source #

d_cong_852 ∷ T_Injection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_854 ∷ T_Injection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_function_856 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_Func_774 Source #

du_function_856 ∷ T_Injection_842 → T_Func_774 Source #

d_isCongruent_860 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsCongruent_22 Source #

du_isCongruent_860 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsCongruent_22 Source #

d__'8776'__864 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → () Source #

d__'8777'__866 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → () Source #

d_Carrier_868 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → () Source #

d_isEquivalence_870 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsEquivalence_28 Source #

du_isEquivalence_870 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_872 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_872 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_874 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_PartialSetoid_10 Source #

du_partialSetoid_874 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_PartialSetoid_10 Source #

d_rawSetoid_876 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_RawSetoid_12 Source #

d_refl_878 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny Source #

du_refl_878 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny Source #

d_reflexive_880 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_880 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_882 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_Setoid_46 Source #

du_setoid_882 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_Setoid_46 Source #

d_sym_884 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_884 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_886 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_886 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__890 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → () Source #

d__'8777'__892 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → () Source #

d_Carrier_894 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → () Source #

d_isEquivalence_896 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsEquivalence_28 Source #

du_isEquivalence_896 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_898 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_898 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_900 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_PartialSetoid_10 Source #

du_partialSetoid_900 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_PartialSetoid_10 Source #

d_rawSetoid_902 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_RawSetoid_12 Source #

d_refl_904 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny Source #

du_refl_904 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny Source #

d_reflexive_906 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_906 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_908 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_Setoid_46 Source #

du_setoid_908 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_Setoid_46 Source #

d_sym_910 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_910 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_912 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_912 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isInjection_914 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsInjection_98 Source #

du_isInjection_914 ∷ T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_IsInjection_98 Source #

d_Surjection_918 ∷ p → p → p → p → p → p → () Source #

data T_Surjection_918 Source #

d_to_926 ∷ T_Surjection_918 → AgdaAny → AgdaAny Source #

d_cong_928 ∷ T_Surjection_918 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_surjective_930 ∷ T_Surjection_918 → AgdaAny → T_Σ_14 Source #

d_function_932 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_Func_774 Source #

du_function_932 ∷ T_Surjection_918 → T_Func_774 Source #

d_isCongruent_936 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsCongruent_22 Source #

du_isCongruent_936 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsCongruent_22 Source #

d__'8776'__940 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → () Source #

d__'8777'__942 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → () Source #

d_Carrier_944 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → () Source #

d_isEquivalence_946 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsEquivalence_28 Source #

du_isEquivalence_946 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_948 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_948 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_950 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_PartialSetoid_10 Source #

du_partialSetoid_950 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_PartialSetoid_10 Source #

d_rawSetoid_952 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_RawSetoid_12 Source #

d_refl_954 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny Source #

du_refl_954 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny Source #

d_reflexive_956 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_956 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_Setoid_46 Source #

du_setoid_958 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_Setoid_46 Source #

d_sym_960 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_960 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_962 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_962 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → () Source #

d__'8777'__968 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → () Source #

d_Carrier_970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → () Source #

d_isEquivalence_972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsEquivalence_28 Source #

du_isEquivalence_972 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_974 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_974 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_PartialSetoid_10 Source #

du_partialSetoid_976 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_PartialSetoid_10 Source #

d_rawSetoid_978 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_RawSetoid_12 Source #

d_refl_980 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny Source #

du_refl_980 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny Source #

d_reflexive_982 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_982 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_Setoid_46 Source #

du_setoid_984 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_Setoid_46 Source #

d_sym_986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_986 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_988 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_988 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isSurjection_990 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsSurjection_174 Source #

du_isSurjection_990 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_IsSurjection_174 Source #

d_strictlySurjective_994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → T_Σ_14 Source #

du_strictlySurjective_994 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → T_Σ_14 Source #

d_to'8315'_996 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny Source #

du_to'8315'_996 ∷ T_Surjection_918 → AgdaAny → AgdaAny Source #

d_to'8728'to'8315'_1000 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny Source #

du_to'8728'to'8315'_1000 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → AgdaAny → AgdaAny Source #

d_Bijection_1004 ∷ p → p → p → p → p → p → () Source #

data T_Bijection_1004 Source #

d_to_1012 ∷ T_Bijection_1004 → AgdaAny → AgdaAny Source #

d_cong_1014 ∷ T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_bijective_1016 ∷ T_Bijection_1004 → T_Σ_14 Source #

d_injective_1018 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_injective_1018 ∷ T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_surjective_1020 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → T_Σ_14 Source #

du_surjective_1020 ∷ T_Bijection_1004 → AgdaAny → T_Σ_14 Source #

d_injection_1022 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_Injection_842 Source #

du_injection_1022 ∷ T_Bijection_1004 → T_Injection_842 Source #

d_surjection_1024 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_Surjection_918 Source #

du_surjection_1024 ∷ T_Bijection_1004 → T_Surjection_918 Source #

d_isInjection_1028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsInjection_98 Source #

du_isInjection_1028 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsInjection_98 Source #

d_isSurjection_1032 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsSurjection_174 Source #

du_isSurjection_1032 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsSurjection_174 Source #

d_strictlySurjective_1034 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → T_Σ_14 Source #

du_strictlySurjective_1034 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → T_Σ_14 Source #

d_to'8315'_1036 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny Source #

du_to'8315'_1036 ∷ T_Bijection_1004 → AgdaAny → AgdaAny Source #

d_isBijection_1038 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsBijection_256 Source #

du_isBijection_1038 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsBijection_256 Source #

d__'8776'__1044 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → () Source #

d__'8777'__1046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → () Source #

d_Carrier_1048 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → () Source #

d_isEquivalence_1050 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsEquivalence_28 Source #

du_isEquivalence_1050 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1052 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1052 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1054 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_PartialSetoid_10 Source #

du_partialSetoid_1054 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_PartialSetoid_10 Source #

d_rawSetoid_1056 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_RawSetoid_12 Source #

d_refl_1058 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny Source #

du_refl_1058 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny Source #

d_reflexive_1060 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1060 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1062 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_Setoid_46 Source #

du_setoid_1062 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_Setoid_46 Source #

d_sym_1064 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1064 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1066 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1066 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1070 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → () Source #

d__'8777'__1072 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → () Source #

d_Carrier_1074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → () Source #

d_isEquivalence_1076 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsEquivalence_28 Source #

du_isEquivalence_1076 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1078 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1078 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1080 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_PartialSetoid_10 Source #

du_partialSetoid_1080 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_PartialSetoid_10 Source #

d_rawSetoid_1082 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_RawSetoid_12 Source #

d_refl_1084 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny Source #

du_refl_1084 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny Source #

d_reflexive_1086 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1086 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1088 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_Setoid_46 Source #

du_setoid_1088 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_Setoid_46 Source #

d_sym_1090 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1090 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1092 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1092 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → AgdaAny → () Source #

d_Carrier_1116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → () Source #

d_IsBiInverse_1130 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_IsCongruent_1138 ∷ p → p → p → p → p → p → p → () Source #

d_IsInverse_1146 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsLeftInverse_1150 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsRightInverse_1154 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSplitSurjection_1158 ∷ p → p → p → p → p → p → p → () Source #

d_from'8321''45'cong_1234 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'8322''45'cong_1236 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_1238 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_1240 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_to'45'isCongruent_1248 ∷ T_IsBiInverse_714 → T_IsCongruent_22 Source #

d_cong_1378 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_1380 ∷ T_IsCongruent_22 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_1382 ∷ T_IsCongruent_22 → T_IsEquivalence_28 Source #

d_inverse'691'_1506 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isLeftInverse_1516 ∷ T_IsInverse_526 → T_IsLeftInverse_346 Source #

d__'8776'__1530 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → () Source #

d__'8777'__1532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → () Source #

d_Carrier_1534 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → () Source #

d_isEquivalence_1536 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsEquivalence_28 Source #

du_isEquivalence_1536 ∷ T_IsInverse_526 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1538 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1538 ∷ T_IsInverse_526 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1540 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_PartialSetoid_10 Source #

du_partialSetoid_1540 ∷ T_IsInverse_526 → T_PartialSetoid_10 Source #

d_rawSetoid_1542 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_RawSetoid_12 Source #

d_refl_1544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny Source #

du_refl_1544 ∷ T_IsInverse_526 → AgdaAny → AgdaAny Source #

d_reflexive_1546 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1546 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_Setoid_46 Source #

du_setoid_1548 ∷ T_IsInverse_526 → T_Setoid_46 Source #

d_sym_1550 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1550 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1552 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1556 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → () Source #

d__'8777'__1558 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → () Source #

d_Carrier_1560 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → () Source #

d_isEquivalence_1562 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsEquivalence_28 Source #

du_isEquivalence_1562 ∷ T_IsInverse_526 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1564 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1564 ∷ T_IsInverse_526 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_PartialSetoid_10 Source #

du_partialSetoid_1566 ∷ T_IsInverse_526 → T_PartialSetoid_10 Source #

d_rawSetoid_1568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_RawSetoid_12 Source #

d_refl_1570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny Source #

du_refl_1570 ∷ T_IsInverse_526 → AgdaAny → AgdaAny Source #

d_reflexive_1572 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1572 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_Setoid_46 Source #

du_setoid_1574 ∷ T_IsInverse_526 → T_Setoid_46 Source #

d_sym_1576 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1576 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1578 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1578 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_1582 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_1584 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_1586 ∷ T_IsLeftInverse_346 → T_IsCongruent_22 Source #

d_isSurjection_1592 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsSurjection_174 Source #

du_isSurjection_1592 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsSurjection_174 Source #

d_strictlyInverse'737'_1594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny Source #

du_strictlyInverse'737'_1594 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny Source #

d__'8776'__1600 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → () Source #

d__'8777'__1602 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → () Source #

d_Carrier_1604 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → () Source #

d_isEquivalence_1606 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsEquivalence_28 Source #

du_isEquivalence_1606 ∷ T_IsLeftInverse_346 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1608 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1608 ∷ T_IsLeftInverse_346 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1610 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_PartialSetoid_10 Source #

du_partialSetoid_1610 ∷ T_IsLeftInverse_346 → T_PartialSetoid_10 Source #

d_rawSetoid_1612 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_RawSetoid_12 Source #

d_refl_1614 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny Source #

du_refl_1614 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny Source #

d_reflexive_1616 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1616 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1618 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_Setoid_46 Source #

du_setoid_1618 ∷ T_IsLeftInverse_346 → T_Setoid_46 Source #

d_sym_1620 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1620 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1622 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1622 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1626 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → () Source #

d__'8777'__1628 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → () Source #

d_Carrier_1630 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → () Source #

d_isEquivalence_1632 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsEquivalence_28 Source #

du_isEquivalence_1632 ∷ T_IsLeftInverse_346 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1634 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1634 ∷ T_IsLeftInverse_346 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1636 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_PartialSetoid_10 Source #

du_partialSetoid_1636 ∷ T_IsLeftInverse_346 → T_PartialSetoid_10 Source #

d_rawSetoid_1638 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_RawSetoid_12 Source #

d_refl_1640 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny Source #

du_refl_1640 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny Source #

d_reflexive_1642 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1642 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1644 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_Setoid_46 Source #

du_setoid_1644 ∷ T_IsLeftInverse_346 → T_Setoid_46 Source #

d_sym_1646 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1646 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1648 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1648 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_1652 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_1654 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_1656 ∷ T_IsRightInverse_438 → T_IsCongruent_22 Source #

d_strictlyInverse'691'_1662 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny Source #

du_strictlyInverse'691'_1662 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny Source #

d__'8776'__1668 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → () Source #

d__'8777'__1670 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → () Source #

d_Carrier_1672 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → () Source #

d_isEquivalence_1674 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsEquivalence_28 Source #

du_isEquivalence_1674 ∷ T_IsRightInverse_438 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1676 ∷ T_IsRightInverse_438 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1678 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_PartialSetoid_10 Source #

du_partialSetoid_1678 ∷ T_IsRightInverse_438 → T_PartialSetoid_10 Source #

d_rawSetoid_1680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_RawSetoid_12 Source #

d_refl_1682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny Source #

du_refl_1682 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny Source #

d_reflexive_1684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1684 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_Setoid_46 Source #

du_setoid_1686 ∷ T_IsRightInverse_438 → T_Setoid_46 Source #

d_sym_1688 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1688 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1690 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → () Source #

d__'8777'__1696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → () Source #

d_Carrier_1698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → () Source #

d_isEquivalence_1700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsEquivalence_28 Source #

du_isEquivalence_1700 ∷ T_IsRightInverse_438 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1702 ∷ T_IsRightInverse_438 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_PartialSetoid_10 Source #

du_partialSetoid_1704 ∷ T_IsRightInverse_438 → T_PartialSetoid_10 Source #

d_rawSetoid_1706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_RawSetoid_12 Source #

d_refl_1708 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny Source #

du_refl_1708 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny Source #

d_reflexive_1710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1710 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_Setoid_46 Source #

du_setoid_1712 ∷ T_IsRightInverse_438 → T_Setoid_46 Source #

d_sym_1714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1714 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1716 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from_1720 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny Source #

d_isLeftInverse_1732 ∷ T_IsSplitSurjection_806 → T_IsLeftInverse_346 Source #

d_Equivalence_1858 ∷ p → p → p → p → p → p → () Source #

data T_Equivalence_1858 Source #

d_to_1868 ∷ T_Equivalence_1858 → AgdaAny → AgdaAny Source #

d_from_1870 ∷ T_Equivalence_1858 → AgdaAny → AgdaAny Source #

d_to'45'cong_1872 ∷ T_Equivalence_1858 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_1874 ∷ T_Equivalence_1858 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_toFunction_1876 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_Func_774 Source #

du_toFunction_1876 ∷ T_Equivalence_1858 → T_Func_774 Source #

d_isCongruent_1880 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsCongruent_22 Source #

du_isCongruent_1880 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsCongruent_22 Source #

d__'8776'__1884 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → () Source #

d__'8777'__1886 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → () Source #

d_Carrier_1888 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → () Source #

d_isEquivalence_1890 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsEquivalence_28 Source #

du_isEquivalence_1890 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1892 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1892 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1894 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_PartialSetoid_10 Source #

du_partialSetoid_1894 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_PartialSetoid_10 Source #

d_rawSetoid_1896 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_RawSetoid_12 Source #

d_refl_1898 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny Source #

du_refl_1898 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny Source #

d_reflexive_1900 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1900 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1902 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_Setoid_46 Source #

du_setoid_1902 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_Setoid_46 Source #

d_sym_1904 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1904 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1906 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1906 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__1910 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → () Source #

d__'8777'__1912 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → () Source #

d_Carrier_1914 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → () Source #

d_isEquivalence_1916 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsEquivalence_28 Source #

du_isEquivalence_1916 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1918 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1918 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1920 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_PartialSetoid_10 Source #

du_partialSetoid_1920 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_PartialSetoid_10 Source #

d_rawSetoid_1922 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_RawSetoid_12 Source #

d_refl_1924 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny Source #

du_refl_1924 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny Source #

d_reflexive_1926 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1926 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1928 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_Setoid_46 Source #

du_setoid_1928 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_Setoid_46 Source #

d_sym_1930 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1930 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1932 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1932 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_fromFunction_1934 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_Func_774 Source #

du_fromFunction_1934 ∷ T_Equivalence_1858 → T_Func_774 Source #

d_isCongruent_1938 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsCongruent_22 Source #

du_isCongruent_1938 ∷ T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_IsCongruent_22 Source #

d_LeftInverse_1942 ∷ p → p → p → p → p → p → () Source #

data T_LeftInverse_1942 Source #

d_to_1954 ∷ T_LeftInverse_1942 → AgdaAny → AgdaAny Source #

d_from_1956 ∷ T_LeftInverse_1942 → AgdaAny → AgdaAny Source #

d_to'45'cong_1958 ∷ T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_1960 ∷ T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_1962 ∷ T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_1964 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsCongruent_22 Source #

du_isCongruent_1964 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsCongruent_22 Source #

d_isLeftInverse_1966 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsLeftInverse_346 Source #

du_isLeftInverse_1966 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsLeftInverse_346 Source #

d_isSurjection_1970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsSurjection_174 Source #

du_isSurjection_1970 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsSurjection_174 Source #

d_strictlyInverse'737'_1972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny Source #

du_strictlyInverse'737'_1972 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny Source #

d__'8776'__1976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → () Source #

d__'8777'__1978 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → () Source #

d_Carrier_1980 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → () Source #

d_isEquivalence_1982 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsEquivalence_28 Source #

du_isEquivalence_1982 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_1984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1984 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_1986 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_PartialSetoid_10 Source #

du_partialSetoid_1986 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_PartialSetoid_10 Source #

d_rawSetoid_1988 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_RawSetoid_12 Source #

d_refl_1990 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny Source #

du_refl_1990 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny Source #

d_reflexive_1992 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_1992 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_1994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_Setoid_46 Source #

du_setoid_1994 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_Setoid_46 Source #

d_sym_1996 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_1996 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_1998 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_1998 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__2002 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → () Source #

d__'8777'__2004 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → () Source #

d_Carrier_2006 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → () Source #

d_isEquivalence_2008 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsEquivalence_28 Source #

du_isEquivalence_2008 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_2010 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2010 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_2012 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_PartialSetoid_10 Source #

du_partialSetoid_2012 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_PartialSetoid_10 Source #

d_rawSetoid_2014 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_RawSetoid_12 Source #

d_refl_2016 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny Source #

du_refl_2016 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny Source #

d_reflexive_2018 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2018 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2020 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_Setoid_46 Source #

du_setoid_2020 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_Setoid_46 Source #

d_sym_2022 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2022 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2024 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2024 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_equivalence_2026 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_Equivalence_1858 Source #

du_equivalence_2026 ∷ T_LeftInverse_1942 → T_Equivalence_1858 Source #

d_isSplitSurjection_2028 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsSplitSurjection_806 Source #

du_isSplitSurjection_2028 ∷ T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_IsSplitSurjection_806 Source #

d_surjection_2030 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_Surjection_918 Source #

du_surjection_2030 ∷ T_LeftInverse_1942 → T_Surjection_918 Source #

d_RightInverse_2036 ∷ p → p → p → p → p → p → () Source #

data T_RightInverse_2036 Source #

d_to_2048 ∷ T_RightInverse_2036 → AgdaAny → AgdaAny Source #

d_from_2050 ∷ T_RightInverse_2036 → AgdaAny → AgdaAny Source #

d_to'45'cong_2052 ∷ T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_2054 ∷ T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_2056 ∷ T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_2058 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsCongruent_22 Source #

du_isCongruent_2058 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsCongruent_22 Source #

d_isRightInverse_2060 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsRightInverse_438 Source #

du_isRightInverse_2060 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsRightInverse_438 Source #

d_strictlyInverse'691'_2064 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny Source #

du_strictlyInverse'691'_2064 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny Source #

d__'8776'__2068 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → () Source #

d__'8777'__2070 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → () Source #

d_Carrier_2072 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → () Source #

d_isEquivalence_2074 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsEquivalence_28 Source #

du_isEquivalence_2074 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_2076 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2076 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_2078 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_PartialSetoid_10 Source #

du_partialSetoid_2078 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_PartialSetoid_10 Source #

d_rawSetoid_2080 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_RawSetoid_12 Source #

d_refl_2082 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny Source #

du_refl_2082 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny Source #

d_reflexive_2084 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2084 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2086 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_Setoid_46 Source #

du_setoid_2086 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_Setoid_46 Source #

d_sym_2088 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2088 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2090 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2090 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__2094 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → () Source #

d__'8777'__2096 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → () Source #

d_Carrier_2098 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → () Source #

d_isEquivalence_2100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsEquivalence_28 Source #

du_isEquivalence_2100 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_2102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_2102 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_2104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_PartialSetoid_10 Source #

du_partialSetoid_2104 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_PartialSetoid_10 Source #

d_rawSetoid_2106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_RawSetoid_12 Source #

d_refl_2108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny Source #

du_refl_2108 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny Source #

d_reflexive_2110 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_2110 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2112 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_Setoid_46 Source #

du_setoid_2112 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_Setoid_46 Source #

d_sym_2114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_2114 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_2116 ∷ T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_equivalence_2118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_Equivalence_1858 Source #

du_equivalence_2118 ∷ T_RightInverse_2036 → T_Equivalence_1858 Source #

d_Inverse_2122 ∷ p → p → p → p → p → p → () Source #

data T_Inverse_2122 Source #

d_to_2134 ∷ T_Inverse_2122 → AgdaAny → AgdaAny Source #

d_from_2136 ∷ T_Inverse_2122 → AgdaAny → AgdaAny Source #

d_to'45'cong_2138 ∷ T_Inverse_2122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'45'cong_2140 ∷ T_Inverse_2122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #