Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Function.Structures

Documentation

d_IsCongruent_22 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsCongruent_22 Source #

Constructors

C_IsCongruent'46'constructor_985 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) T_IsEquivalence_26 T_IsEquivalence_26

d_cong_32 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_34 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_36 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

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

du_setoid_40 ∷ T_IsCongruent_22 → T_Setoid_44 Source #

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

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

d_Carrier_48 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → () Source #

d_isEquivalence_50 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsEquivalence_26 Source #

du_isEquivalence_50 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_52 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_52 ∷ T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_54 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_PartialSetoid_10 Source #

du_partialSetoid_54 ∷ T_IsCongruent_22 → T_PartialSetoid_10 Source #

d_refl_56 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny Source #

du_refl_56 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny Source #

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

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

d_sym_60 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_60 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_62 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_62 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_setoid_66 ∷ T_IsCongruent_22 → T_Setoid_44 Source #

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

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

d_Carrier_74 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → () Source #

d_isEquivalence_76 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsEquivalence_26 Source #

du_isEquivalence_76 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_78 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_78 ∷ T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_80 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_PartialSetoid_10 Source #

du_partialSetoid_80 ∷ T_IsCongruent_22 → T_PartialSetoid_10 Source #

d_refl_82 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny Source #

du_refl_82 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny Source #

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

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

d_sym_86 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_86 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_88 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_88 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsInjection_92 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsInjection_92 Source #

Constructors

C_IsInjection'46'constructor_3997 T_IsCongruent_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isCongruent_100 ∷ T_IsInjection_92 → T_IsCongruent_22 Source #

d_injective_102 ∷ T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_106 ∷ T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_108 ∷ T_IsInjection_92 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_110 ∷ T_IsInjection_92 → T_IsEquivalence_26 Source #

d__'8776'__114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny → () Source #

d__'8777'__116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny → () Source #

d_Carrier_118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → () Source #

d_isEquivalence_120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → T_IsEquivalence_26 Source #

du_isEquivalence_120 ∷ T_IsInjection_92 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_122 ∷ T_IsInjection_92 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → T_PartialSetoid_10 Source #

du_partialSetoid_124 ∷ T_IsInjection_92 → T_PartialSetoid_10 Source #

d_refl_126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny Source #

du_refl_126 ∷ T_IsInjection_92 → AgdaAny → AgdaAny Source #

d_reflexive_128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_128 ∷ T_IsInjection_92 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_130 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → T_Setoid_44 Source #

du_setoid_130 ∷ T_IsInjection_92 → T_Setoid_44 Source #

d_sym_132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_132 ∷ T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_134 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_134 ∷ T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny → () Source #

d__'8777'__140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny → () Source #

d_Carrier_142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → () Source #

d_isEquivalence_144 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → T_IsEquivalence_26 Source #

du_isEquivalence_144 ∷ T_IsInjection_92 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_146 ∷ T_IsInjection_92 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → T_PartialSetoid_10 Source #

du_partialSetoid_148 ∷ T_IsInjection_92 → T_PartialSetoid_10 Source #

d_refl_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny Source #

du_refl_150 ∷ T_IsInjection_92 → AgdaAny → AgdaAny Source #

d_reflexive_152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_152 ∷ T_IsInjection_92 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → T_Setoid_44 Source #

du_setoid_154 ∷ T_IsInjection_92 → T_Setoid_44 Source #

d_sym_156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_156 ∷ T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_158 ∷ T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSurjection_162 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsSurjection_162 Source #

Constructors

C_IsSurjection'46'constructor_6463 T_IsCongruent_22 (AgdaAny → T_Σ_14)

d_isCongruent_170 ∷ T_IsSurjection_162 → T_IsCongruent_22 Source #

d_surjective_172 ∷ T_IsSurjection_162 → AgdaAny → T_Σ_14 Source #

d_cong_176 ∷ T_IsSurjection_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_178 ∷ T_IsSurjection_162 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_180 ∷ T_IsSurjection_162 → T_IsEquivalence_26 Source #

d__'8776'__184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny → () Source #

d__'8777'__186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny → () Source #

d_Carrier_188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → () Source #

d_isEquivalence_190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → T_IsEquivalence_26 Source #

du_isEquivalence_190 ∷ T_IsSurjection_162 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_192 ∷ T_IsSurjection_162 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → T_PartialSetoid_10 Source #

du_partialSetoid_194 ∷ T_IsSurjection_162 → T_PartialSetoid_10 Source #

d_refl_196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny Source #

du_refl_196 ∷ T_IsSurjection_162 → AgdaAny → AgdaAny Source #

d_reflexive_198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_198 ∷ T_IsSurjection_162 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → T_Setoid_44 Source #

du_setoid_200 ∷ T_IsSurjection_162 → T_Setoid_44 Source #

d_sym_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_202 ∷ T_IsSurjection_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_204 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_204 ∷ T_IsSurjection_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny → () Source #

d__'8777'__210 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny → () Source #

d_Carrier_212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → () Source #

d_isEquivalence_214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → T_IsEquivalence_26 Source #

du_isEquivalence_214 ∷ T_IsSurjection_162 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_216 ∷ T_IsSurjection_162 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → T_PartialSetoid_10 Source #

du_partialSetoid_218 ∷ T_IsSurjection_162 → T_PartialSetoid_10 Source #

d_refl_220 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny Source #

du_refl_220 ∷ T_IsSurjection_162 → AgdaAny → AgdaAny Source #

d_reflexive_222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_222 ∷ T_IsSurjection_162 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → T_Setoid_44 Source #

du_setoid_224 ∷ T_IsSurjection_162 → T_Setoid_44 Source #

d_sym_226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_226 ∷ T_IsSurjection_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_228 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_228 ∷ T_IsSurjection_162 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_strictlySurjective_230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_162 → AgdaAny → T_Σ_14 Source #

du_strictlySurjective_230 ∷ T_IsSurjection_162 → AgdaAny → T_Σ_14 Source #

d_IsBijection_238 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsBijection_238 Source #

Constructors

C_IsBijection'46'constructor_10113 T_IsInjection_92 (AgdaAny → T_Σ_14)

d_isInjection_246 ∷ T_IsBijection_238 → T_IsInjection_92 Source #

d_surjective_248 ∷ T_IsBijection_238 → AgdaAny → T_Σ_14 Source #

d_cong_252 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_254 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_256 ∷ T_IsBijection_238 → T_IsCongruent_22 Source #

d_isEquivalence'8321'_258 ∷ T_IsBijection_238 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_260 ∷ T_IsBijection_238 → T_IsEquivalence_26 Source #

d__'8776'__264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny → () Source #

d__'8777'__266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny → () Source #

d_Carrier_268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → () Source #

d_isEquivalence_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_IsEquivalence_26 Source #

du_isEquivalence_270 ∷ T_IsBijection_238 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_272 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_272 ∷ T_IsBijection_238 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_PartialSetoid_10 Source #

du_partialSetoid_274 ∷ T_IsBijection_238 → T_PartialSetoid_10 Source #

d_refl_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny Source #

du_refl_276 ∷ T_IsBijection_238 → AgdaAny → AgdaAny Source #

d_reflexive_278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_280 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_Setoid_44 Source #

du_setoid_280 ∷ T_IsBijection_238 → T_Setoid_44 Source #

d_sym_282 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_282 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_284 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_284 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny → () Source #

d__'8777'__290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny → () Source #

d_Carrier_292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → () Source #

d_isEquivalence_294 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_IsEquivalence_26 Source #

du_isEquivalence_294 ∷ T_IsBijection_238 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_296 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_296 ∷ T_IsBijection_238 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_PartialSetoid_10 Source #

du_partialSetoid_298 ∷ T_IsBijection_238 → T_PartialSetoid_10 Source #

d_refl_300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny Source #

du_refl_300 ∷ T_IsBijection_238 → AgdaAny → AgdaAny Source #

d_reflexive_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_Setoid_44 Source #

du_setoid_304 ∷ T_IsBijection_238 → T_Setoid_44 Source #

d_sym_306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_306 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_308 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_308 ∷ T_IsBijection_238 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_bijective_310 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_Σ_14 Source #

du_bijective_310 ∷ T_IsBijection_238 → T_Σ_14 Source #

d_isSurjection_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_IsSurjection_162 Source #

du_isSurjection_312 ∷ T_IsBijection_238 → T_IsSurjection_162 Source #

d_strictlySurjective_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → T_Σ_14 Source #

du_strictlySurjective_316 ∷ T_IsBijection_238 → AgdaAny → T_Σ_14 Source #

d_IsLeftInverse_322 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsLeftInverse_322 Source #

Constructors

C_IsLeftInverse'46'constructor_14363 T_IsCongruent_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isCongruent_334 ∷ T_IsLeftInverse_322 → T_IsCongruent_22 Source #

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

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

d_isEquivalence'8321'_342 ∷ T_IsLeftInverse_322 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_344 ∷ T_IsLeftInverse_322 → T_IsEquivalence_26 Source #

d_cong_346 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__350 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny → () Source #

d__'8777'__352 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny → () Source #

d_Carrier_354 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → () Source #

d_isEquivalence_356 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_IsEquivalence_26 Source #

du_isEquivalence_356 ∷ T_IsLeftInverse_322 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_358 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_358 ∷ T_IsLeftInverse_322 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_360 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_PartialSetoid_10 Source #

du_partialSetoid_360 ∷ T_IsLeftInverse_322 → T_PartialSetoid_10 Source #

d_refl_362 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny Source #

du_refl_362 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny Source #

d_reflexive_364 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_366 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_Setoid_44 Source #

du_setoid_366 ∷ T_IsLeftInverse_322 → T_Setoid_44 Source #

d_sym_368 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_368 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_370 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_370 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__374 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny → () Source #

d__'8777'__376 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny → () Source #

d_Carrier_378 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → () Source #

d_isEquivalence_380 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_IsEquivalence_26 Source #

du_isEquivalence_380 ∷ T_IsLeftInverse_322 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_382 ∷ T_IsLeftInverse_322 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_384 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_PartialSetoid_10 Source #

du_partialSetoid_384 ∷ T_IsLeftInverse_322 → T_PartialSetoid_10 Source #

d_refl_386 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny Source #

du_refl_386 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny Source #

d_reflexive_388 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_390 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_Setoid_44 Source #

du_setoid_390 ∷ T_IsLeftInverse_322 → T_Setoid_44 Source #

d_sym_392 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_392 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_394 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_strictlyInverse'737'_396 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → AgdaAny → AgdaAny Source #

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

d_isSurjection_400 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_IsSurjection_162 Source #

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

d_IsRightInverse_408 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsRightInverse_408 Source #

Constructors

C_IsRightInverse'46'constructor_18837 T_IsCongruent_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isCongruent_420 ∷ T_IsRightInverse_408 → T_IsCongruent_22 Source #

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

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

d_isEquivalence'8321'_428 ∷ T_IsRightInverse_408 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_430 ∷ T_IsRightInverse_408 → T_IsEquivalence_26 Source #

d_cong_432 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_Carrier_440 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → () Source #

d_isEquivalence_442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → T_IsEquivalence_26 Source #

du_isEquivalence_442 ∷ T_IsRightInverse_408 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_444 ∷ T_IsRightInverse_408 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_446 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → T_PartialSetoid_10 Source #

du_partialSetoid_446 ∷ T_IsRightInverse_408 → T_PartialSetoid_10 Source #

d_refl_448 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny Source #

du_refl_448 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny Source #

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

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

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

du_setoid_452 ∷ T_IsRightInverse_408 → T_Setoid_44 Source #

d_sym_454 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_454 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_456 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_456 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny → () Source #

d__'8777'__462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny → () Source #

d_Carrier_464 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → () Source #

d_isEquivalence_466 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → T_IsEquivalence_26 Source #

du_isEquivalence_466 ∷ T_IsRightInverse_408 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_468 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_468 ∷ T_IsRightInverse_408 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_470 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → T_PartialSetoid_10 Source #

du_partialSetoid_470 ∷ T_IsRightInverse_408 → T_PartialSetoid_10 Source #

d_refl_472 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny Source #

du_refl_472 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny Source #

d_reflexive_474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_476 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → T_Setoid_44 Source #

du_setoid_476 ∷ T_IsRightInverse_408 → T_Setoid_44 Source #

d_sym_478 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_478 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_480 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_strictlyInverse'691'_482 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → AgdaAny → AgdaAny Source #

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

d_IsInverse_490 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsInverse_490 Source #

Constructors

C_IsInverse'46'constructor_22449 T_IsLeftInverse_322 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isLeftInverse_500 ∷ T_IsInverse_490 → T_IsLeftInverse_322 Source #

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

d_from'45'cong_506 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_508 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_510 ∷ T_IsInverse_490 → T_IsCongruent_22 Source #

d_isEquivalence'8321'_512 ∷ T_IsInverse_490 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_514 ∷ T_IsInverse_490 → T_IsEquivalence_26 Source #

d_isSurjection_516 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_IsSurjection_162 Source #

du_isSurjection_516 ∷ (AgdaAny → AgdaAny) → T_IsInverse_490 → T_IsSurjection_162 Source #

d_strictlyInverse'737'_518 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny Source #

du_strictlyInverse'737'_518 ∷ (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny Source #

d_cong_520 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__524 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny → () Source #

d__'8777'__526 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny → () Source #

d_Carrier_528 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → () Source #

d_isEquivalence_530 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_IsEquivalence_26 Source #

du_isEquivalence_530 ∷ T_IsInverse_490 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_532 ∷ T_IsInverse_490 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_534 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_PartialSetoid_10 Source #

du_partialSetoid_534 ∷ T_IsInverse_490 → T_PartialSetoid_10 Source #

d_refl_536 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny Source #

du_refl_536 ∷ T_IsInverse_490 → AgdaAny → AgdaAny Source #

d_reflexive_538 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_540 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_Setoid_44 Source #

du_setoid_540 ∷ T_IsInverse_490 → T_Setoid_44 Source #

d_sym_542 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_542 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_544 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny → () Source #

d__'8777'__550 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny → () Source #

d_Carrier_552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → () Source #

d_isEquivalence_554 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_IsEquivalence_26 Source #

du_isEquivalence_554 ∷ T_IsInverse_490 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_556 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_556 ∷ T_IsInverse_490 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_558 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_PartialSetoid_10 Source #

du_partialSetoid_558 ∷ T_IsInverse_490 → T_PartialSetoid_10 Source #

d_refl_560 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny Source #

du_refl_560 ∷ T_IsInverse_490 → AgdaAny → AgdaAny Source #

d_reflexive_562 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

d_setoid_564 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_Setoid_44 Source #

du_setoid_564 ∷ T_IsInverse_490 → T_Setoid_44 Source #

d_sym_566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_566 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_568 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRightInverse_570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_IsRightInverse_408 Source #

du_isRightInverse_570 ∷ T_IsInverse_490 → T_IsRightInverse_408 Source #

d_strictlyInverse'691'_574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny Source #

du_strictlyInverse'691'_574 ∷ (AgdaAny → AgdaAny) → T_IsInverse_490 → AgdaAny → AgdaAny Source #

d_inverse_576 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_Σ_14 Source #

du_inverse_576 ∷ T_IsInverse_490 → T_Σ_14 Source #

d_IsBiEquivalence_584 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsBiEquivalence_584 Source #

Constructors

C_IsBiEquivalence'46'constructor_28009 T_IsCongruent_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_to'45'isCongruent_598 ∷ T_IsBiEquivalence_584 → T_IsCongruent_22 Source #

d_from'8321''45'cong_600 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'8322''45'cong_602 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_606 ∷ T_IsBiEquivalence_584 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_608 ∷ T_IsBiEquivalence_584 → T_IsEquivalence_26 Source #

d_cong_610 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__614 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny → () Source #

d__'8777'__616 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny → () Source #

d_Carrier_618 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → () Source #

d_isEquivalence_620 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → T_IsEquivalence_26 Source #

du_isEquivalence_620 ∷ T_IsBiEquivalence_584 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_622 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_622 ∷ T_IsBiEquivalence_584 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_624 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → T_PartialSetoid_10 Source #

du_partialSetoid_624 ∷ T_IsBiEquivalence_584 → T_PartialSetoid_10 Source #

d_refl_626 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny Source #

du_refl_626 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny Source #

d_reflexive_628 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_628 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_630 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → T_Setoid_44 Source #

du_setoid_630 ∷ T_IsBiEquivalence_584 → T_Setoid_44 Source #

d_sym_632 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_632 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_634 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_634 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__638 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny → () Source #

d__'8777'__640 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny → () Source #

d_Carrier_642 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → () Source #

d_isEquivalence_644 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → T_IsEquivalence_26 Source #

du_isEquivalence_644 ∷ T_IsBiEquivalence_584 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_646 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_646 ∷ T_IsBiEquivalence_584 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_648 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → T_PartialSetoid_10 Source #

du_partialSetoid_648 ∷ T_IsBiEquivalence_584 → T_PartialSetoid_10 Source #

d_refl_650 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny Source #

du_refl_650 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny Source #

d_reflexive_652 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_652 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_654 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → T_Setoid_44 Source #

du_setoid_654 ∷ T_IsBiEquivalence_584 → T_Setoid_44 Source #

d_sym_656 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_656 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_658 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_658 ∷ T_IsBiEquivalence_584 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBiInverse_666 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsBiInverse_666 Source #

Constructors

C_IsBiInverse'46'constructor_32731 T_IsCongruent_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_to'45'isCongruent_684 ∷ T_IsBiInverse_666 → T_IsCongruent_22 Source #

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

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

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

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

d_isEquivalence'8321'_696 ∷ T_IsBiInverse_666 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_698 ∷ T_IsBiInverse_666 → T_IsEquivalence_26 Source #

d_cong_700 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny → () Source #

d__'8777'__706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny → () Source #

d_Carrier_708 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → () Source #

d_isEquivalence_710 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → T_IsEquivalence_26 Source #

du_isEquivalence_710 ∷ T_IsBiInverse_666 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_712 ∷ T_IsBiInverse_666 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → T_PartialSetoid_10 Source #

du_partialSetoid_714 ∷ T_IsBiInverse_666 → T_PartialSetoid_10 Source #

d_refl_716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny Source #

du_refl_716 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny Source #

d_reflexive_718 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_718 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → T_Setoid_44 Source #

du_setoid_720 ∷ T_IsBiInverse_666 → T_Setoid_44 Source #

d_sym_722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_722 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_724 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_724 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny → () Source #

d__'8777'__730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny → () Source #

d_Carrier_732 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → () Source #

d_isEquivalence_734 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → T_IsEquivalence_26 Source #

du_isEquivalence_734 ∷ T_IsBiInverse_666 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_736 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_736 ∷ T_IsBiInverse_666 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_738 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → T_PartialSetoid_10 Source #

du_partialSetoid_738 ∷ T_IsBiInverse_666 → T_PartialSetoid_10 Source #

d_refl_740 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny Source #

du_refl_740 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny Source #

d_reflexive_742 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_742 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_744 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → T_Setoid_44 Source #

du_setoid_744 ∷ T_IsBiInverse_666 → T_Setoid_44 Source #

d_sym_746 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_746 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_748 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_748 ∷ T_IsBiInverse_666 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSplitSurjection_752 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsSplitSurjection_752 Source #

Constructors

C_IsSplitSurjection'46'constructor_35501 (AgdaAny → AgdaAny) T_IsLeftInverse_322

d_from_760 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny Source #

d_isLeftInverse_762 ∷ T_IsSplitSurjection_752 → T_IsLeftInverse_322 Source #

d_from'45'cong_766 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_768 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_770 ∷ T_IsSplitSurjection_752 → T_IsCongruent_22 Source #

d_isEquivalence'8321'_772 ∷ T_IsSplitSurjection_752 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_774 ∷ T_IsSplitSurjection_752 → T_IsEquivalence_26 Source #

d_isSurjection_776 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → T_IsSurjection_162 Source #

du_isSurjection_776 ∷ T_IsSplitSurjection_752 → T_IsSurjection_162 Source #

d_strictlyInverse'737'_778 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny Source #

du_strictlyInverse'737'_778 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny Source #

d_cong_780 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__784 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny → () Source #

d__'8777'__786 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny → () Source #

d_Carrier_788 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → () Source #

d_isEquivalence_790 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → T_IsEquivalence_26 Source #

du_isEquivalence_790 ∷ T_IsSplitSurjection_752 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_792 ∷ T_IsSplitSurjection_752 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_794 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → T_PartialSetoid_10 Source #

du_partialSetoid_794 ∷ T_IsSplitSurjection_752 → T_PartialSetoid_10 Source #

d_refl_796 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny Source #

du_refl_796 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny Source #

d_reflexive_798 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_798 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_800 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → T_Setoid_44 Source #

du_setoid_800 ∷ T_IsSplitSurjection_752 → T_Setoid_44 Source #

d_sym_802 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_802 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_804 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny → () Source #

d__'8777'__810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny → () Source #

d_Carrier_812 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → () Source #

d_isEquivalence_814 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → T_IsEquivalence_26 Source #

du_isEquivalence_814 ∷ T_IsSplitSurjection_752 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_816 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_816 ∷ T_IsSplitSurjection_752 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_818 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → T_PartialSetoid_10 Source #

du_partialSetoid_818 ∷ T_IsSplitSurjection_752 → T_PartialSetoid_10 Source #

d_refl_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny Source #

du_refl_820 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny Source #

d_reflexive_822 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_822 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_824 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → T_Setoid_44 Source #

du_setoid_824 ∷ T_IsSplitSurjection_752 → T_Setoid_44 Source #

d_sym_826 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_826 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_828 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_828 ∷ T_IsSplitSurjection_752 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #