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_constructor_94 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) T_IsEquivalence_28 T_IsEquivalence_28

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

d_isEquivalence'8321'_34 ∷ T_IsCongruent_22 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_36 ∷ T_IsCongruent_22 → T_IsEquivalence_28 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_46 Source #

du_setoid_40 ∷ T_IsCongruent_22 → T_Setoid_46 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_28 Source #

du_isEquivalence_50 ∷ T_IsCongruent_22 → T_IsEquivalence_28 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_rawSetoid_56 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_RawSetoid_12 Source #

d_refl_58 ∷ 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_58 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny Source #

d_reflexive_60 ∷ 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_60 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

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

du_sym_62 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_64 ∷ 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_64 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_setoid_68 ∷ T_IsCongruent_22 → T_Setoid_46 Source #

d__'8776'__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__'8777'__74 ∷ 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_76 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → () Source #

d_isEquivalence_78 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsEquivalence_28 Source #

du_isEquivalence_78 ∷ T_IsCongruent_22 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_80 ∷ 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_80 ∷ T_IsCongruent_22 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_82 ∷ 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_82 ∷ T_IsCongruent_22 → T_PartialSetoid_10 Source #

d_rawSetoid_84 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_RawSetoid_12 Source #

d_refl_86 ∷ 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_86 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny Source #

d_reflexive_88 ∷ 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_88 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_sym_90 ∷ 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_90 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_92 ∷ 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_92 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsInjection_98 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsInjection_98 Source #

Constructors

C_constructor_170 T_IsCongruent_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isCongruent_106 ∷ T_IsInjection_98 → T_IsCongruent_22 Source #

d_injective_108 ∷ T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_112 ∷ T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_114 ∷ T_IsInjection_98 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_116 ∷ T_IsInjection_98 → T_IsEquivalence_28 Source #

d__'8776'__120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny → () Source #

d__'8777'__122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny → () Source #

d_Carrier_124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → () Source #

d_isEquivalence_126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_IsEquivalence_28 Source #

du_isEquivalence_126 ∷ T_IsInjection_98 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_128 ∷ T_IsInjection_98 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_130 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_PartialSetoid_10 Source #

du_partialSetoid_130 ∷ T_IsInjection_98 → T_PartialSetoid_10 Source #

d_rawSetoid_132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_RawSetoid_12 Source #

d_refl_134 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny Source #

du_refl_134 ∷ T_IsInjection_98 → AgdaAny → AgdaAny Source #

d_reflexive_136 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_136 ∷ T_IsInjection_98 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_Setoid_46 Source #

du_setoid_138 ∷ T_IsInjection_98 → T_Setoid_46 Source #

d_sym_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_140 ∷ T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_142 ∷ T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny → () Source #

d__'8777'__148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny → () Source #

d_Carrier_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → () Source #

d_isEquivalence_152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_IsEquivalence_28 Source #

du_isEquivalence_152 ∷ T_IsInjection_98 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_154 ∷ T_IsInjection_98 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_PartialSetoid_10 Source #

du_partialSetoid_156 ∷ T_IsInjection_98 → T_PartialSetoid_10 Source #

d_rawSetoid_158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_RawSetoid_12 Source #

d_refl_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny Source #

du_refl_160 ∷ T_IsInjection_98 → AgdaAny → AgdaAny Source #

d_reflexive_162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_162 ∷ T_IsInjection_98 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_Setoid_46 Source #

du_setoid_164 ∷ T_IsInjection_98 → T_Setoid_46 Source #

d_sym_166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_166 ∷ T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_168 ∷ T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSurjection_174 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsSurjection_174 Source #

Constructors

C_constructor_252 T_IsCongruent_22 (AgdaAny → T_Σ_14)

d_isCongruent_182 ∷ T_IsSurjection_174 → T_IsCongruent_22 Source #

d_surjective_184 ∷ T_IsSurjection_174 → AgdaAny → T_Σ_14 Source #

d_cong_188 ∷ T_IsSurjection_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_190 ∷ T_IsSurjection_174 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_192 ∷ T_IsSurjection_174 → T_IsEquivalence_28 Source #

d__'8776'__196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny → () Source #

d__'8777'__198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny → () Source #

d_Carrier_200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → () Source #

d_isEquivalence_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_IsEquivalence_28 Source #

du_isEquivalence_202 ∷ T_IsSurjection_174 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_204 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_204 ∷ T_IsSurjection_174 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_206 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_PartialSetoid_10 Source #

du_partialSetoid_206 ∷ T_IsSurjection_174 → T_PartialSetoid_10 Source #

d_rawSetoid_208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_RawSetoid_12 Source #

d_refl_210 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny Source #

du_refl_210 ∷ T_IsSurjection_174 → AgdaAny → AgdaAny Source #

d_reflexive_212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_212 ∷ T_IsSurjection_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_Setoid_46 Source #

du_setoid_214 ∷ T_IsSurjection_174 → T_Setoid_46 Source #

d_sym_216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_216 ∷ T_IsSurjection_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_218 ∷ T_IsSurjection_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny → () Source #

d__'8777'__224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny → () Source #

d_Carrier_226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → () Source #

d_isEquivalence_228 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_IsEquivalence_28 Source #

du_isEquivalence_228 ∷ T_IsSurjection_174 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_230 ∷ T_IsSurjection_174 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_232 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_PartialSetoid_10 Source #

du_partialSetoid_232 ∷ T_IsSurjection_174 → T_PartialSetoid_10 Source #

d_rawSetoid_234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_RawSetoid_12 Source #

d_refl_236 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny Source #

du_refl_236 ∷ T_IsSurjection_174 → AgdaAny → AgdaAny Source #

d_reflexive_238 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_238 ∷ T_IsSurjection_174 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_240 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_Setoid_46 Source #

du_setoid_240 ∷ T_IsSurjection_174 → T_Setoid_46 Source #

d_sym_242 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_242 ∷ T_IsSurjection_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_244 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_244 ∷ T_IsSurjection_174 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

du_strictlySurjective_246 ∷ T_IsSurjection_174 → AgdaAny → T_Σ_14 Source #

d_IsBijection_256 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsBijection_256 Source #

Constructors

C_constructor_340 T_IsInjection_98 (AgdaAny → T_Σ_14)

d_isInjection_264 ∷ T_IsBijection_256 → T_IsInjection_98 Source #

d_surjective_266 ∷ T_IsBijection_256 → AgdaAny → T_Σ_14 Source #

d_cong_270 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_272 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_274 ∷ T_IsBijection_256 → T_IsCongruent_22 Source #

d_isEquivalence'8321'_276 ∷ T_IsBijection_256 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_278 ∷ T_IsBijection_256 → T_IsEquivalence_28 Source #

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

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

d_Carrier_286 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → () Source #

d_isEquivalence_288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsEquivalence_28 Source #

du_isEquivalence_288 ∷ T_IsBijection_256 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_290 ∷ T_IsBijection_256 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_PartialSetoid_10 Source #

du_partialSetoid_292 ∷ T_IsBijection_256 → T_PartialSetoid_10 Source #

d_rawSetoid_294 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_RawSetoid_12 Source #

d_refl_296 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny Source #

du_refl_296 ∷ T_IsBijection_256 → AgdaAny → AgdaAny Source #

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

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

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

du_setoid_300 ∷ T_IsBijection_256 → T_Setoid_46 Source #

d_sym_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_302 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_304 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_Carrier_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → () Source #

d_isEquivalence_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsEquivalence_28 Source #

du_isEquivalence_314 ∷ T_IsBijection_256 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_316 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_316 ∷ T_IsBijection_256 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_318 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_PartialSetoid_10 Source #

du_partialSetoid_318 ∷ T_IsBijection_256 → T_PartialSetoid_10 Source #

d_rawSetoid_320 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_RawSetoid_12 Source #

d_refl_322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny Source #

du_refl_322 ∷ T_IsBijection_256 → AgdaAny → AgdaAny Source #

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

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

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

du_setoid_326 ∷ T_IsBijection_256 → T_Setoid_46 Source #

d_sym_328 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_328 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_330 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_330 ∷ T_IsBijection_256 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_bijective_332 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_Σ_14 Source #

du_bijective_332 ∷ T_IsBijection_256 → T_Σ_14 Source #

d_isSurjection_334 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsSurjection_174 Source #

du_isSurjection_334 ∷ T_IsBijection_256 → T_IsSurjection_174 Source #

d_strictlySurjective_338 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → T_Σ_14 Source #

du_strictlySurjective_338 ∷ T_IsBijection_256 → AgdaAny → T_Σ_14 Source #

d_IsLeftInverse_346 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsLeftInverse_346 Source #

Constructors

C_constructor_432 T_IsCongruent_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isCongruent_358 ∷ T_IsLeftInverse_346 → T_IsCongruent_22 Source #

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

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

d_isEquivalence'8321'_366 ∷ T_IsLeftInverse_346 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_368 ∷ T_IsLeftInverse_346 → T_IsEquivalence_28 Source #

d_cong_370 ∷ T_IsLeftInverse_346 → 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_346 → 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_346 → 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_346 → () 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_346 → T_IsEquivalence_28 Source #

du_isEquivalence_380 ∷ T_IsLeftInverse_346 → T_IsEquivalence_28 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_346 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_382 ∷ T_IsLeftInverse_346 → 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_346 → T_PartialSetoid_10 Source #

du_partialSetoid_384 ∷ T_IsLeftInverse_346 → T_PartialSetoid_10 Source #

d_rawSetoid_386 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_RawSetoid_12 Source #

d_refl_388 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny Source #

du_refl_388 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny Source #

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

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

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

du_setoid_392 ∷ T_IsLeftInverse_346 → T_Setoid_46 Source #

d_sym_394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_394 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_396 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_396 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_Carrier_404 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → () Source #

d_isEquivalence_406 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsEquivalence_28 Source #

du_isEquivalence_406 ∷ T_IsLeftInverse_346 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_408 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_408 ∷ T_IsLeftInverse_346 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_410 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_PartialSetoid_10 Source #

du_partialSetoid_410 ∷ T_IsLeftInverse_346 → T_PartialSetoid_10 Source #

d_rawSetoid_412 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_RawSetoid_12 Source #

d_refl_414 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny Source #

du_refl_414 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny Source #

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

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

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

du_setoid_418 ∷ T_IsLeftInverse_346 → T_Setoid_46 Source #

d_sym_420 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_420 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_422 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_422 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_isSurjection_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsSurjection_174 Source #

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

d_IsRightInverse_438 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsRightInverse_438 Source #

Constructors

C_constructor_520 T_IsCongruent_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isCongruent_450 ∷ T_IsRightInverse_438 → T_IsCongruent_22 Source #

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

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

d_isEquivalence'8321'_458 ∷ T_IsRightInverse_438 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_460 ∷ T_IsRightInverse_438 → T_IsEquivalence_28 Source #

d_cong_462 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_Carrier_470 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → () Source #

d_isEquivalence_472 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsEquivalence_28 Source #

du_isEquivalence_472 ∷ T_IsRightInverse_438 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_474 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_474 ∷ T_IsRightInverse_438 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_476 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_PartialSetoid_10 Source #

du_partialSetoid_476 ∷ T_IsRightInverse_438 → T_PartialSetoid_10 Source #

d_rawSetoid_478 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_RawSetoid_12 Source #

d_refl_480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny Source #

du_refl_480 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny Source #

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

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

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

du_setoid_484 ∷ T_IsRightInverse_438 → T_Setoid_46 Source #

d_sym_486 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_486 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_488 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_488 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_Carrier_496 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → () Source #

d_isEquivalence_498 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsEquivalence_28 Source #

du_isEquivalence_498 ∷ T_IsRightInverse_438 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_500 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_500 ∷ T_IsRightInverse_438 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_502 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_PartialSetoid_10 Source #

du_partialSetoid_502 ∷ T_IsRightInverse_438 → T_PartialSetoid_10 Source #

d_rawSetoid_504 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_RawSetoid_12 Source #

d_refl_506 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny Source #

du_refl_506 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny Source #

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

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

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

du_setoid_510 ∷ T_IsRightInverse_438 → T_Setoid_46 Source #

d_sym_512 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_512 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_514 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_514 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_IsInverse_526 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsInverse_526 Source #

Constructors

C_constructor_618 T_IsLeftInverse_346 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isLeftInverse_536 ∷ T_IsInverse_526 → T_IsLeftInverse_346 Source #

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

d_from'45'cong_542 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_544 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_546 ∷ T_IsInverse_526 → T_IsCongruent_22 Source #

d_isEquivalence'8321'_548 ∷ T_IsInverse_526 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_550 ∷ T_IsInverse_526 → T_IsEquivalence_28 Source #

d_isSurjection_552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsSurjection_174 Source #

du_isSurjection_552 ∷ (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsSurjection_174 Source #

d_strictlyInverse'737'_554 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny Source #

du_strictlyInverse'737'_554 ∷ (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny Source #

d_cong_556 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_Carrier_564 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → () Source #

d_isEquivalence_566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsEquivalence_28 Source #

du_isEquivalence_566 ∷ T_IsInverse_526 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_568 ∷ T_IsInverse_526 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_PartialSetoid_10 Source #

du_partialSetoid_570 ∷ T_IsInverse_526 → T_PartialSetoid_10 Source #

d_rawSetoid_572 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_RawSetoid_12 Source #

d_refl_574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny Source #

du_refl_574 ∷ T_IsInverse_526 → AgdaAny → AgdaAny Source #

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

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

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

du_setoid_578 ∷ T_IsInverse_526 → T_Setoid_46 Source #

d_sym_580 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_580 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_582 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_Carrier_590 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → () Source #

d_isEquivalence_592 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsEquivalence_28 Source #

du_isEquivalence_592 ∷ T_IsInverse_526 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_594 ∷ T_IsInverse_526 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_596 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_PartialSetoid_10 Source #

du_partialSetoid_596 ∷ T_IsInverse_526 → T_PartialSetoid_10 Source #

d_rawSetoid_598 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_RawSetoid_12 Source #

d_refl_600 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny Source #

du_refl_600 ∷ T_IsInverse_526 → AgdaAny → AgdaAny Source #

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

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

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

du_setoid_604 ∷ T_IsInverse_526 → T_Setoid_46 Source #

d_sym_606 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_606 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_608 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_608 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRightInverse_610 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsRightInverse_438 Source #

du_isRightInverse_610 ∷ T_IsInverse_526 → T_IsRightInverse_438 Source #

d_strictlyInverse'691'_614 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny Source #

du_strictlyInverse'691'_614 ∷ (AgdaAny → AgdaAny) → T_IsInverse_526 → AgdaAny → AgdaAny Source #

d_inverse_616 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_Σ_14 Source #

du_inverse_616 ∷ T_IsInverse_526 → T_Σ_14 Source #

d_IsBiEquivalence_626 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsBiEquivalence_626 Source #

Constructors

C_constructor_706 T_IsCongruent_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_to'45'isCongruent_640 ∷ T_IsBiEquivalence_626 → T_IsCongruent_22 Source #

d_from'8321''45'cong_642 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_from'8322''45'cong_644 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_648 ∷ T_IsBiEquivalence_626 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_650 ∷ T_IsBiEquivalence_626 → T_IsEquivalence_28 Source #

d_cong_652 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__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_626 → AgdaAny → AgdaAny → () Source #

d__'8777'__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_626 → AgdaAny → AgdaAny → () Source #

d_Carrier_660 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → () Source #

d_isEquivalence_662 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → T_IsEquivalence_28 Source #

du_isEquivalence_662 ∷ T_IsBiEquivalence_626 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_664 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_664 ∷ T_IsBiEquivalence_626 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_666 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → T_PartialSetoid_10 Source #

du_partialSetoid_666 ∷ T_IsBiEquivalence_626 → T_PartialSetoid_10 Source #

d_rawSetoid_668 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → T_RawSetoid_12 Source #

d_refl_670 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → AgdaAny → AgdaAny Source #

du_refl_670 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny Source #

d_reflexive_672 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_672 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_674 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → T_Setoid_46 Source #

du_setoid_674 ∷ T_IsBiEquivalence_626 → T_Setoid_46 Source #

d_sym_676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_676 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_678 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_678 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → AgdaAny → AgdaAny → () Source #

d__'8777'__684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → AgdaAny → AgdaAny → () Source #

d_Carrier_686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → () Source #

d_isEquivalence_688 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → T_IsEquivalence_28 Source #

du_isEquivalence_688 ∷ T_IsBiEquivalence_626 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_690 ∷ T_IsBiEquivalence_626 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_692 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → T_PartialSetoid_10 Source #

du_partialSetoid_692 ∷ T_IsBiEquivalence_626 → T_PartialSetoid_10 Source #

d_rawSetoid_694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → T_RawSetoid_12 Source #

d_refl_696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → AgdaAny → AgdaAny Source #

du_refl_696 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny Source #

d_reflexive_698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_698 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → T_Setoid_46 Source #

du_setoid_700 ∷ T_IsBiEquivalence_626 → T_Setoid_46 Source #

d_sym_702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_702 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_704 ∷ T_IsBiEquivalence_626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBiInverse_714 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsBiInverse_714 Source #

Constructors

C_constructor_802 T_IsCongruent_22 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_to'45'isCongruent_732 ∷ T_IsBiInverse_714 → T_IsCongruent_22 Source #

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

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

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

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

d_isEquivalence'8321'_744 ∷ T_IsBiInverse_714 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_746 ∷ T_IsBiInverse_714 → T_IsEquivalence_28 Source #

d_cong_748 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__752 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny → () Source #

d__'8777'__754 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny → () Source #

d_Carrier_756 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → () Source #

d_isEquivalence_758 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → T_IsEquivalence_28 Source #

du_isEquivalence_758 ∷ T_IsBiInverse_714 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_760 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_760 ∷ T_IsBiInverse_714 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_762 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → T_PartialSetoid_10 Source #

du_partialSetoid_762 ∷ T_IsBiInverse_714 → T_PartialSetoid_10 Source #

d_rawSetoid_764 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → T_RawSetoid_12 Source #

d_refl_766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny Source #

du_refl_766 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny Source #

d_reflexive_768 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_768 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_770 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → T_Setoid_46 Source #

du_setoid_770 ∷ T_IsBiInverse_714 → T_Setoid_46 Source #

d_sym_772 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_772 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_774 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_774 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__778 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny → () Source #

d__'8777'__780 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny → () Source #

d_Carrier_782 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → () Source #

d_isEquivalence_784 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → T_IsEquivalence_28 Source #

du_isEquivalence_784 ∷ T_IsBiInverse_714 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_786 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_786 ∷ T_IsBiInverse_714 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_788 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → T_PartialSetoid_10 Source #

du_partialSetoid_788 ∷ T_IsBiInverse_714 → T_PartialSetoid_10 Source #

d_rawSetoid_790 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → T_RawSetoid_12 Source #

d_refl_792 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny Source #

du_refl_792 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny Source #

d_reflexive_794 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_794 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_796 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → T_Setoid_46 Source #

du_setoid_796 ∷ T_IsBiInverse_714 → T_Setoid_46 Source #

d_sym_798 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_798 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_800 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_800 ∷ T_IsBiInverse_714 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsSplitSurjection_806 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsSplitSurjection_806 Source #

Constructors

C_constructor_888 (AgdaAny → AgdaAny) T_IsLeftInverse_346

d_from_814 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny Source #

d_isLeftInverse_816 ∷ T_IsSplitSurjection_806 → T_IsLeftInverse_346 Source #

d_from'45'cong_820 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_822 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_824 ∷ T_IsSplitSurjection_806 → T_IsCongruent_22 Source #

d_isEquivalence'8321'_826 ∷ T_IsSplitSurjection_806 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_828 ∷ T_IsSplitSurjection_806 → T_IsEquivalence_28 Source #

d_isSurjection_830 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_IsSurjection_174 Source #

du_isSurjection_830 ∷ T_IsSplitSurjection_806 → T_IsSurjection_174 Source #

d_strictlyInverse'737'_832 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny Source #

du_strictlyInverse'737'_832 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny Source #

d_cong_834 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny → () Source #

d__'8777'__840 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny → () Source #

d_Carrier_842 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → () Source #

d_isEquivalence_844 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_IsEquivalence_28 Source #

du_isEquivalence_844 ∷ T_IsSplitSurjection_806 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_846 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_846 ∷ T_IsSplitSurjection_806 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_848 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_PartialSetoid_10 Source #

du_partialSetoid_848 ∷ T_IsSplitSurjection_806 → T_PartialSetoid_10 Source #

d_rawSetoid_850 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_RawSetoid_12 Source #

d_refl_852 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny Source #

du_refl_852 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny Source #

d_reflexive_854 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_854 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_856 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_Setoid_46 Source #

du_setoid_856 ∷ T_IsSplitSurjection_806 → T_Setoid_46 Source #

d_sym_858 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_858 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_860 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_860 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

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

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

d_Carrier_868 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → () Source #

d_isEquivalence_870 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_IsEquivalence_28 Source #

du_isEquivalence_870 ∷ T_IsSplitSurjection_806 → T_IsEquivalence_28 Source #

d_isPartialEquivalence_872 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_872 ∷ T_IsSplitSurjection_806 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_874 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_PartialSetoid_10 Source #

du_partialSetoid_874 ∷ T_IsSplitSurjection_806 → T_PartialSetoid_10 Source #

d_rawSetoid_876 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_RawSetoid_12 Source #

d_refl_878 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny Source #

du_refl_878 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny Source #

d_reflexive_880 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_880 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_882 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → T_Setoid_46 Source #

du_setoid_882 ∷ T_IsSplitSurjection_806 → T_Setoid_46 Source #

d_sym_884 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_884 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_886 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_886 ∷ T_IsSplitSurjection_806 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #