Safe HaskellNone

MAlonzo.Code.Function.Structures

Documentation

d_IsCongruent_22 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_IsCongruent_22 Source #

Constructors

C_IsCongruent'46'constructor_597 (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__46 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_48 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> () Source #

d_isEquivalence_50 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__72 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_74 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> () Source #

d_isEquivalence_76 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_IsInjection_92 Source #

Constructors

C_IsInjection'46'constructor_3223 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__116 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_118 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> () Source #

d_isEquivalence_120 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__140 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_142 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> () Source #

d_isEquivalence_144 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_IsSurjection_162 Source #

Constructors

C_IsSurjection'46'constructor_5483 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__186 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_188 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> () Source #

d_isEquivalence_190 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__210 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_212 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> () Source #

d_isEquivalence_214 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_IsBijection_232 Source #

Constructors

C_IsBijection'46'constructor_7739 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__260 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_262 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> () Source #

d_isEquivalence_264 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__284 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_286 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> () Source #

d_isEquivalence_288 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> () Source #

data T_IsLeftInverse_312 Source #

Constructors

C_IsLeftInverse'46'constructor_11245 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_312 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__342 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_312 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_344 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_312 -> () Source #

d_isEquivalence_346 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_312 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__366 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_312 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_368 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_312 -> () Source #

d_isEquivalence_370 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> () Source #

data T_IsRightInverse_390 Source #

Constructors

C_IsRightInverse'46'constructor_14103 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_390 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__420 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_390 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_422 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_390 -> () Source #

d_isEquivalence_424 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_390 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__444 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_390 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_446 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_390 -> () Source #

d_isEquivalence_448 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> () Source #

data T_IsInverse_468 Source #

Constructors

C_IsInverse'46'constructor_16657 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__500 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_502 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> () Source #

d_isEquivalence_504 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__524 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_526 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> () Source #

d_isEquivalence_528 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> () Source #

data T_IsBiEquivalence_554 Source #

Constructors

C_IsBiEquivalence'46'constructor_20621 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_554 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__586 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_554 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_588 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_554 -> () Source #

d_isEquivalence_590 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_554 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__610 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_554 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_612 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_554 -> () Source #

d_isEquivalence_614 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> () Source #

data T_IsBiInverse_636 Source #

Constructors

C_IsBiInverse'46'constructor_24463 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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_636 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__676 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_636 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_678 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_636 -> () Source #

d_isEquivalence_680 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_636 -> AgdaAny -> AgdaAny -> () Source #

d__'8777'__700 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_636 -> AgdaAny -> AgdaAny -> () Source #

d_Carrier_702 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_636 -> () Source #

d_isEquivalence_704 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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 #