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_3991 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_6577 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_IsBijection_232 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsBijection_232 Source #

Constructors

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

d_isInjection_240 ∷ T_IsBijection_232 → T_IsInjection_92 Source #

d_surjective_242 ∷ T_IsBijection_232 → AgdaAny → T_Σ_14 Source #

d_cong_246 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_248 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_250 ∷ T_IsBijection_232 → T_IsCongruent_22 Source #

d_isEquivalence'8321'_252 ∷ T_IsBijection_232 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_254 ∷ T_IsBijection_232 → T_IsEquivalence_26 Source #

d__'8776'__258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → () Source #

d__'8777'__260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → () Source #

d_Carrier_262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → () Source #

d_isEquivalence_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_IsEquivalence_26 Source #

du_isEquivalence_264 ∷ T_IsBijection_232 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_266 ∷ T_IsBijection_232 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_PartialSetoid_10 Source #

du_partialSetoid_268 ∷ T_IsBijection_232 → T_PartialSetoid_10 Source #

d_refl_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny Source #

du_refl_270 ∷ T_IsBijection_232 → AgdaAny → AgdaAny Source #

d_reflexive_272 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_272 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_Setoid_44 Source #

du_setoid_274 ∷ T_IsBijection_232 → T_Setoid_44 Source #

d_sym_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_276 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_278 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__282 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → 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_232 → 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_232 → () Source #

d_isEquivalence_288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_IsEquivalence_26 Source #

du_isEquivalence_288 ∷ T_IsBijection_232 → T_IsEquivalence_26 Source #

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

du_isPartialEquivalence_290 ∷ T_IsBijection_232 → 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_232 → T_PartialSetoid_10 Source #

du_partialSetoid_292 ∷ T_IsBijection_232 → T_PartialSetoid_10 Source #

d_refl_294 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny Source #

du_refl_294 ∷ T_IsBijection_232 → AgdaAny → AgdaAny Source #

d_reflexive_296 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_296 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_298 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_Setoid_44 Source #

du_setoid_298 ∷ T_IsBijection_232 → T_Setoid_44 Source #

d_sym_300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_300 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_302 ∷ T_IsBijection_232 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_bijective_304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_Σ_14 Source #

du_bijective_304 ∷ T_IsBijection_232 → T_Σ_14 Source #

d_isSurjection_306 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_232 → T_IsSurjection_162 Source #

du_isSurjection_306 ∷ T_IsBijection_232 → T_IsSurjection_162 Source #

d_IsLeftInverse_312 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsLeftInverse_312 Source #

Constructors

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

d_isCongruent_324 ∷ T_IsLeftInverse_312 → T_IsCongruent_22 Source #

d_cong'8322'_326 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_328 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny Source #

d_cong_332 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_334 ∷ T_IsLeftInverse_312 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_336 ∷ T_IsLeftInverse_312 → T_IsEquivalence_26 Source #

d__'8776'__340 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny → () Source #

d__'8777'__342 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny → () Source #

d_Carrier_344 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → () Source #

d_isEquivalence_346 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → T_IsEquivalence_26 Source #

du_isEquivalence_346 ∷ T_IsLeftInverse_312 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_348 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_348 ∷ T_IsLeftInverse_312 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_350 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → T_PartialSetoid_10 Source #

du_partialSetoid_350 ∷ T_IsLeftInverse_312 → T_PartialSetoid_10 Source #

d_refl_352 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny Source #

du_refl_352 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny Source #

d_reflexive_354 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_354 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_356 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → T_Setoid_44 Source #

du_setoid_356 ∷ T_IsLeftInverse_312 → T_Setoid_44 Source #

d_sym_358 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_358 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_360 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_360 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__364 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny → () Source #

d__'8777'__366 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny → () Source #

d_Carrier_368 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → () Source #

d_isEquivalence_370 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → T_IsEquivalence_26 Source #

du_isEquivalence_370 ∷ T_IsLeftInverse_312 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_372 ∷ T_IsLeftInverse_312 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_374 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → T_PartialSetoid_10 Source #

du_partialSetoid_374 ∷ T_IsLeftInverse_312 → T_PartialSetoid_10 Source #

d_refl_376 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny Source #

du_refl_376 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny Source #

d_reflexive_378 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_378 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_380 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → T_Setoid_44 Source #

du_setoid_380 ∷ T_IsLeftInverse_312 → T_Setoid_44 Source #

d_sym_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_382 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_384 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_384 ∷ T_IsLeftInverse_312 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsRightInverse_390 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsRightInverse_390 Source #

Constructors

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

d_isCongruent_402 ∷ T_IsRightInverse_390 → T_IsCongruent_22 Source #

d_cong'8322'_404 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_406 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny Source #

d_cong_410 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_412 ∷ T_IsRightInverse_390 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_414 ∷ T_IsRightInverse_390 → T_IsEquivalence_26 Source #

d__'8776'__418 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny → () Source #

d__'8777'__420 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny → () Source #

d_Carrier_422 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → () Source #

d_isEquivalence_424 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → T_IsEquivalence_26 Source #

du_isEquivalence_424 ∷ T_IsRightInverse_390 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_426 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_426 ∷ T_IsRightInverse_390 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → T_PartialSetoid_10 Source #

du_partialSetoid_428 ∷ T_IsRightInverse_390 → T_PartialSetoid_10 Source #

d_refl_430 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny Source #

du_refl_430 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny Source #

d_reflexive_432 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_432 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_434 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → T_Setoid_44 Source #

du_setoid_434 ∷ T_IsRightInverse_390 → T_Setoid_44 Source #

d_sym_436 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_436 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_438 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_438 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny → () Source #

d__'8777'__444 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny → () Source #

d_Carrier_446 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → () Source #

d_isEquivalence_448 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → T_IsEquivalence_26 Source #

du_isEquivalence_448 ∷ T_IsRightInverse_390 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_450 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_450 ∷ T_IsRightInverse_390 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_452 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → T_PartialSetoid_10 Source #

du_partialSetoid_452 ∷ T_IsRightInverse_390 → T_PartialSetoid_10 Source #

d_refl_454 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny Source #

du_refl_454 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny Source #

d_reflexive_456 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_456 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → T_Setoid_44 Source #

du_setoid_458 ∷ T_IsRightInverse_390 → T_Setoid_44 Source #

d_sym_460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_460 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_390 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_462 ∷ T_IsRightInverse_390 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsInverse_468 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsInverse_468 Source #

Constructors

C_IsInverse'46'constructor_19781 T_IsLeftInverse_312 (AgdaAny → AgdaAny)

d_isLeftInverse_478 ∷ T_IsInverse_468 → T_IsLeftInverse_312 Source #

d_inverse'691'_480 ∷ T_IsInverse_468 → AgdaAny → AgdaAny Source #

d_cong_484 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8322'_486 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_488 ∷ T_IsInverse_468 → AgdaAny → AgdaAny Source #

d_isCongruent_490 ∷ T_IsInverse_468 → T_IsCongruent_22 Source #

d_isEquivalence'8321'_492 ∷ T_IsInverse_468 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_494 ∷ T_IsInverse_468 → T_IsEquivalence_26 Source #

d__'8776'__498 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → () Source #

d__'8777'__500 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → () Source #

d_Carrier_502 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → () Source #

d_isEquivalence_504 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_IsEquivalence_26 Source #

du_isEquivalence_504 ∷ T_IsInverse_468 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_506 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_506 ∷ T_IsInverse_468 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_508 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_PartialSetoid_10 Source #

du_partialSetoid_508 ∷ T_IsInverse_468 → T_PartialSetoid_10 Source #

d_refl_510 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny Source #

du_refl_510 ∷ T_IsInverse_468 → AgdaAny → AgdaAny Source #

d_reflexive_512 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_512 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_514 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_Setoid_44 Source #

du_setoid_514 ∷ T_IsInverse_468 → T_Setoid_44 Source #

d_sym_516 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_516 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_518 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_518 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__522 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → () Source #

d__'8777'__524 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → () Source #

d_Carrier_526 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → () Source #

d_isEquivalence_528 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_IsEquivalence_26 Source #

du_isEquivalence_528 ∷ T_IsInverse_468 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_530 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_530 ∷ T_IsInverse_468 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_PartialSetoid_10 Source #

du_partialSetoid_532 ∷ T_IsInverse_468 → T_PartialSetoid_10 Source #

d_refl_534 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny Source #

du_refl_534 ∷ T_IsInverse_468 → AgdaAny → AgdaAny Source #

d_reflexive_536 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_536 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_538 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_Setoid_44 Source #

du_setoid_538 ∷ T_IsInverse_468 → T_Setoid_44 Source #

d_sym_540 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_540 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_542 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_542 ∷ T_IsInverse_468 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRightInverse_544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_IsRightInverse_390 Source #

du_isRightInverse_544 ∷ T_IsInverse_468 → T_IsRightInverse_390 Source #

d_inverse_546 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_468 → T_Σ_14 Source #

du_inverse_546 ∷ T_IsInverse_468 → T_Σ_14 Source #

d_IsBiEquivalence_554 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsBiEquivalence_554 Source #

Constructors

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

d_f'45'isCongruent_568 ∷ T_IsBiEquivalence_554 → T_IsCongruent_22 Source #

d_cong'8322'_570 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8323'_572 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_576 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_578 ∷ T_IsBiEquivalence_554 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_580 ∷ T_IsBiEquivalence_554 → T_IsEquivalence_26 Source #

d__'8776'__584 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → AgdaAny → AgdaAny → () Source #

d__'8777'__586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → AgdaAny → AgdaAny → () Source #

d_Carrier_588 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → () Source #

d_isEquivalence_590 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → T_IsEquivalence_26 Source #

du_isEquivalence_590 ∷ T_IsBiEquivalence_554 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_592 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_592 ∷ T_IsBiEquivalence_554 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → T_PartialSetoid_10 Source #

du_partialSetoid_594 ∷ T_IsBiEquivalence_554 → T_PartialSetoid_10 Source #

d_refl_596 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → AgdaAny → AgdaAny Source #

du_refl_596 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny Source #

d_reflexive_598 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_598 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_600 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → T_Setoid_44 Source #

du_setoid_600 ∷ T_IsBiEquivalence_554 → T_Setoid_44 Source #

d_sym_602 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_602 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_604 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_604 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__608 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → AgdaAny → AgdaAny → () Source #

d__'8777'__610 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → AgdaAny → AgdaAny → () Source #

d_Carrier_612 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiEquivalence_554 → () Source #

d_isEquivalence_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_554 → T_IsEquivalence_26 Source #

du_isEquivalence_614 ∷ T_IsBiEquivalence_554 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_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_554 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_616 ∷ T_IsBiEquivalence_554 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_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_554 → T_PartialSetoid_10 Source #

du_partialSetoid_618 ∷ T_IsBiEquivalence_554 → T_PartialSetoid_10 Source #

d_refl_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_554 → AgdaAny → AgdaAny Source #

du_refl_620 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny Source #

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

du_reflexive_622 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_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_554 → T_Setoid_44 Source #

du_setoid_624 ∷ T_IsBiEquivalence_554 → T_Setoid_44 Source #

d_sym_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_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_626 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_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_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_628 ∷ T_IsBiEquivalence_554 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsBiInverse_636 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsBiInverse_636 Source #

Constructors

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

d_f'45'isCongruent_654 ∷ T_IsBiInverse_636 → T_IsCongruent_22 Source #

d_cong'8322'_656 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_658 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny Source #

d_cong'8323'_660 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_662 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny Source #

d_cong_666 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_668 ∷ T_IsBiInverse_636 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_670 ∷ T_IsBiInverse_636 → T_IsEquivalence_26 Source #

d__'8776'__674 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → AgdaAny → AgdaAny → () Source #

d__'8777'__676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → AgdaAny → AgdaAny → () Source #

d_Carrier_678 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → () Source #

d_isEquivalence_680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → T_IsEquivalence_26 Source #

du_isEquivalence_680 ∷ T_IsBiInverse_636 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_682 ∷ T_IsBiInverse_636 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → T_PartialSetoid_10 Source #

du_partialSetoid_684 ∷ T_IsBiInverse_636 → T_PartialSetoid_10 Source #

d_refl_686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → AgdaAny → AgdaAny Source #

du_refl_686 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny Source #

d_reflexive_688 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_reflexive_688 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → T_Setoid_44 Source #

du_setoid_690 ∷ T_IsBiInverse_636 → T_Setoid_44 Source #

d_sym_692 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_692 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_694 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'8776'__698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → AgdaAny → AgdaAny → () Source #

d__'8777'__700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → AgdaAny → AgdaAny → () Source #

d_Carrier_702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBiInverse_636 → () Source #

d_isEquivalence_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_636 → T_IsEquivalence_26 Source #

du_isEquivalence_704 ∷ T_IsBiInverse_636 → T_IsEquivalence_26 Source #

d_isPartialEquivalence_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_636 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_706 ∷ T_IsBiInverse_636 → T_IsPartialEquivalence_16 Source #

d_partialSetoid_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_636 → T_PartialSetoid_10 Source #

du_partialSetoid_708 ∷ T_IsBiInverse_636 → T_PartialSetoid_10 Source #

d_refl_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_636 → AgdaAny → AgdaAny Source #

du_refl_710 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny Source #

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

du_reflexive_712 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_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_636 → T_Setoid_44 Source #

du_setoid_714 ∷ T_IsBiInverse_636 → T_Setoid_44 Source #

d_sym_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_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_sym_716 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_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_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_trans_718 ∷ T_IsBiInverse_636 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #