Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Function.Structures

Documentation

d_IsCongruent_22 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsCongruent_22 #

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 #

d_isEquivalence'8321'_34 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_36 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

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 #

du_setoid_40 :: T_IsCongruent_22 -> T_Setoid_44 #

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 -> () #

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 -> () #

d_Carrier_48 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> () #

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 #

du_isEquivalence_50 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

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 #

du_isPartialEquivalence_52 :: T_IsCongruent_22 -> T_IsPartialEquivalence_16 #

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 #

du_partialSetoid_54 :: T_IsCongruent_22 -> T_PartialSetoid_10 #

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 #

du_refl_56 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_58 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

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 #

du_sym_60 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_trans_62 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_setoid_66 :: T_IsCongruent_22 -> T_Setoid_44 #

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 -> () #

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 -> () #

d_Carrier_74 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> () #

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 #

du_isEquivalence_76 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

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 #

du_isPartialEquivalence_78 :: T_IsCongruent_22 -> T_IsPartialEquivalence_16 #

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 #

du_partialSetoid_80 :: T_IsCongruent_22 -> T_PartialSetoid_10 #

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 #

du_refl_82 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_84 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

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 #

du_sym_86 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_trans_88 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsInjection_92 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsInjection_92 #

Constructors

C_IsInjection'46'constructor_3997 T_IsCongruent_22 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isCongruent_100 :: T_IsInjection_92 -> T_IsCongruent_22 #

d_injective_102 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_cong_106 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence'8321'_108 :: T_IsInjection_92 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_110 :: T_IsInjection_92 -> T_IsEquivalence_26 #

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 -> () #

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 -> () #

d_Carrier_118 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> () #

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 #

du_isEquivalence_120 :: T_IsInjection_92 -> T_IsEquivalence_26 #

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 #

du_isPartialEquivalence_122 :: T_IsInjection_92 -> T_IsPartialEquivalence_16 #

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 #

du_partialSetoid_124 :: T_IsInjection_92 -> T_PartialSetoid_10 #

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 #

du_refl_126 :: T_IsInjection_92 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_128 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

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 #

du_setoid_130 :: T_IsInjection_92 -> T_Setoid_44 #

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 #

du_sym_132 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_trans_134 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 -> () #

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 -> () #

d_Carrier_142 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> () #

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 #

du_isEquivalence_144 :: T_IsInjection_92 -> T_IsEquivalence_26 #

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 #

du_isPartialEquivalence_146 :: T_IsInjection_92 -> T_IsPartialEquivalence_16 #

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 #

du_partialSetoid_148 :: T_IsInjection_92 -> T_PartialSetoid_10 #

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 #

du_refl_150 :: T_IsInjection_92 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_152 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

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 #

du_setoid_154 :: T_IsInjection_92 -> T_Setoid_44 #

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 #

du_sym_156 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_trans_158 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsSurjection_162 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsSurjection_162 #

Constructors

C_IsSurjection'46'constructor_6463 T_IsCongruent_22 (AgdaAny -> T_Σ_14)

d_isCongruent_170 :: T_IsSurjection_162 -> T_IsCongruent_22 #

d_surjective_172 :: T_IsSurjection_162 -> AgdaAny -> T_Σ_14 #

d_cong_176 :: T_IsSurjection_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence'8321'_178 :: T_IsSurjection_162 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_180 :: T_IsSurjection_162 -> T_IsEquivalence_26 #

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 -> () #

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 -> () #

d_Carrier_188 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> () #

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 #

du_isEquivalence_190 :: T_IsSurjection_162 -> T_IsEquivalence_26 #

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 #

du_isPartialEquivalence_192 :: T_IsSurjection_162 -> T_IsPartialEquivalence_16 #

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 #

du_partialSetoid_194 :: T_IsSurjection_162 -> T_PartialSetoid_10 #

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 #

du_refl_196 :: T_IsSurjection_162 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_198 :: T_IsSurjection_162 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

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 #

du_setoid_200 :: T_IsSurjection_162 -> T_Setoid_44 #

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 #

du_sym_202 :: T_IsSurjection_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_trans_204 :: T_IsSurjection_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 -> () #

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 -> () #

d_Carrier_212 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> () #

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 #

du_isEquivalence_214 :: T_IsSurjection_162 -> T_IsEquivalence_26 #

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 #

du_isPartialEquivalence_216 :: T_IsSurjection_162 -> T_IsPartialEquivalence_16 #

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 #

du_partialSetoid_218 :: T_IsSurjection_162 -> T_PartialSetoid_10 #

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 #

du_refl_220 :: T_IsSurjection_162 -> AgdaAny -> AgdaAny #

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 #

du_reflexive_222 :: T_IsSurjection_162 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

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 #

du_setoid_224 :: T_IsSurjection_162 -> T_Setoid_44 #

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 #

du_sym_226 :: T_IsSurjection_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

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 #

du_trans_228 :: T_IsSurjection_162 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_strictlySurjective_230 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> AgdaAny -> T_Σ_14 #

du_strictlySurjective_230 :: T_IsSurjection_162 -> AgdaAny -> T_Σ_14 #

d_IsBijection_238 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsBijection_238 #

Constructors

C_IsBijection'46'constructor_10113 T_IsInjection_92 (AgdaAny -> T_Σ_14)

d_isInjection_246 :: T_IsBijection_238 -> T_IsInjection_92 #

d_surjective_248 :: T_IsBijection_238 -> AgdaAny -> T_Σ_14 #

d_cong_252 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_254 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_256 :: T_IsBijection_238 -> T_IsCongruent_22 #

d_isEquivalence'8321'_258 :: T_IsBijection_238 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_260 :: T_IsBijection_238 -> T_IsEquivalence_26 #

d__'8776'__264 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> () #

d__'8777'__266 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> () #

d_Carrier_268 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> () #

d_isEquivalence_270 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsEquivalence_26 #

du_isEquivalence_270 :: T_IsBijection_238 -> T_IsEquivalence_26 #

d_isPartialEquivalence_272 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_272 :: T_IsBijection_238 -> T_IsPartialEquivalence_16 #

d_partialSetoid_274 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_PartialSetoid_10 #

du_partialSetoid_274 :: T_IsBijection_238 -> T_PartialSetoid_10 #

d_refl_276 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny #

du_refl_276 :: T_IsBijection_238 -> AgdaAny -> AgdaAny #

d_reflexive_278 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_278 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_280 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_Setoid_44 #

du_setoid_280 :: T_IsBijection_238 -> T_Setoid_44 #

d_sym_282 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_282 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_284 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_284 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__288 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> () #

d__'8777'__290 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> () #

d_Carrier_292 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> () #

d_isEquivalence_294 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsEquivalence_26 #

du_isEquivalence_294 :: T_IsBijection_238 -> T_IsEquivalence_26 #

d_isPartialEquivalence_296 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_296 :: T_IsBijection_238 -> T_IsPartialEquivalence_16 #

d_partialSetoid_298 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_PartialSetoid_10 #

du_partialSetoid_298 :: T_IsBijection_238 -> T_PartialSetoid_10 #

d_refl_300 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny #

du_refl_300 :: T_IsBijection_238 -> AgdaAny -> AgdaAny #

d_reflexive_302 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_302 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_304 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_Setoid_44 #

du_setoid_304 :: T_IsBijection_238 -> T_Setoid_44 #

d_sym_306 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_306 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_308 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_308 :: T_IsBijection_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_bijective_310 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_Σ_14 #

du_bijective_310 :: T_IsBijection_238 -> T_Σ_14 #

d_isSurjection_312 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsSurjection_162 #

du_isSurjection_312 :: T_IsBijection_238 -> T_IsSurjection_162 #

d_strictlySurjective_316 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> AgdaAny -> T_Σ_14 #

du_strictlySurjective_316 :: T_IsBijection_238 -> AgdaAny -> T_Σ_14 #

d_IsLeftInverse_322 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsLeftInverse_322 #

Constructors

C_IsLeftInverse'46'constructor_14363 T_IsCongruent_22 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isCongruent_334 :: T_IsLeftInverse_322 -> T_IsCongruent_22 #

d_from'45'cong_336 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'737'_338 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence'8321'_342 :: T_IsLeftInverse_322 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_344 :: T_IsLeftInverse_322 -> T_IsEquivalence_26 #

d_cong_346 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__350 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> () #

d__'8777'__352 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> () #

d_Carrier_354 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> () #

d_isEquivalence_356 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsEquivalence_26 #

du_isEquivalence_356 :: T_IsLeftInverse_322 -> T_IsEquivalence_26 #

d_isPartialEquivalence_358 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_358 :: T_IsLeftInverse_322 -> T_IsPartialEquivalence_16 #

d_partialSetoid_360 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_PartialSetoid_10 #

du_partialSetoid_360 :: T_IsLeftInverse_322 -> T_PartialSetoid_10 #

d_refl_362 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

du_refl_362 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

d_reflexive_364 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_364 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_366 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_Setoid_44 #

du_setoid_366 :: T_IsLeftInverse_322 -> T_Setoid_44 #

d_sym_368 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_368 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_370 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_370 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__374 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> () #

d__'8777'__376 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> () #

d_Carrier_378 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> () #

d_isEquivalence_380 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsEquivalence_26 #

du_isEquivalence_380 :: T_IsLeftInverse_322 -> T_IsEquivalence_26 #

d_isPartialEquivalence_382 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_382 :: T_IsLeftInverse_322 -> T_IsPartialEquivalence_16 #

d_partialSetoid_384 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_PartialSetoid_10 #

du_partialSetoid_384 :: T_IsLeftInverse_322 -> T_PartialSetoid_10 #

d_refl_386 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

du_refl_386 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

d_reflexive_388 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_388 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_390 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_Setoid_44 #

du_setoid_390 :: T_IsLeftInverse_322 -> T_Setoid_44 #

d_sym_392 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_392 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_394 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_394 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_strictlyInverse'737'_396 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

du_strictlyInverse'737'_396 :: (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> AgdaAny -> AgdaAny #

d_isSurjection_400 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsSurjection_162 #

du_isSurjection_400 :: (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsSurjection_162 #

d_IsRightInverse_408 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsRightInverse_408 #

Constructors

C_IsRightInverse'46'constructor_18837 T_IsCongruent_22 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isCongruent_420 :: T_IsRightInverse_408 -> T_IsCongruent_22 #

d_from'45'cong_422 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'691'_424 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence'8321'_428 :: T_IsRightInverse_408 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_430 :: T_IsRightInverse_408 -> T_IsEquivalence_26 #

d_cong_432 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__436 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> () #

d__'8777'__438 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> () #

d_Carrier_440 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> () #

d_isEquivalence_442 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_IsEquivalence_26 #

du_isEquivalence_442 :: T_IsRightInverse_408 -> T_IsEquivalence_26 #

d_isPartialEquivalence_444 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_444 :: T_IsRightInverse_408 -> T_IsPartialEquivalence_16 #

d_partialSetoid_446 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_PartialSetoid_10 #

du_partialSetoid_446 :: T_IsRightInverse_408 -> T_PartialSetoid_10 #

d_refl_448 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

du_refl_448 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

d_reflexive_450 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_450 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_452 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_Setoid_44 #

du_setoid_452 :: T_IsRightInverse_408 -> T_Setoid_44 #

d_sym_454 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_454 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_456 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_456 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__460 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> () #

d__'8777'__462 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> () #

d_Carrier_464 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> () #

d_isEquivalence_466 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_IsEquivalence_26 #

du_isEquivalence_466 :: T_IsRightInverse_408 -> T_IsEquivalence_26 #

d_isPartialEquivalence_468 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_468 :: T_IsRightInverse_408 -> T_IsPartialEquivalence_16 #

d_partialSetoid_470 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_PartialSetoid_10 #

du_partialSetoid_470 :: T_IsRightInverse_408 -> T_PartialSetoid_10 #

d_refl_472 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

du_refl_472 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

d_reflexive_474 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_474 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_476 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_Setoid_44 #

du_setoid_476 :: T_IsRightInverse_408 -> T_Setoid_44 #

d_sym_478 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_478 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_480 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_480 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_strictlyInverse'691'_482 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

du_strictlyInverse'691'_482 :: (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny #

d_IsInverse_490 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsInverse_490 #

Constructors

C_IsInverse'46'constructor_22449 T_IsLeftInverse_322 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isLeftInverse_500 :: T_IsInverse_490 -> T_IsLeftInverse_322 #

d_inverse'691'_502 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'45'cong_506 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'737'_508 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_510 :: T_IsInverse_490 -> T_IsCongruent_22 #

d_isEquivalence'8321'_512 :: T_IsInverse_490 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_514 :: T_IsInverse_490 -> T_IsEquivalence_26 #

d_isSurjection_516 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsSurjection_162 #

du_isSurjection_516 :: (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsSurjection_162 #

d_strictlyInverse'737'_518 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny #

du_strictlyInverse'737'_518 :: (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny #

d_cong_520 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__524 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> () #

d__'8777'__526 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> () #

d_Carrier_528 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> () #

d_isEquivalence_530 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsEquivalence_26 #

du_isEquivalence_530 :: T_IsInverse_490 -> T_IsEquivalence_26 #

d_isPartialEquivalence_532 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_532 :: T_IsInverse_490 -> T_IsPartialEquivalence_16 #

d_partialSetoid_534 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_PartialSetoid_10 #

du_partialSetoid_534 :: T_IsInverse_490 -> T_PartialSetoid_10 #

d_refl_536 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny #

du_refl_536 :: T_IsInverse_490 -> AgdaAny -> AgdaAny #

d_reflexive_538 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_538 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_540 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_Setoid_44 #

du_setoid_540 :: T_IsInverse_490 -> T_Setoid_44 #

d_sym_542 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_542 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_544 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_544 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__548 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> () #

d__'8777'__550 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> () #

d_Carrier_552 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> () #

d_isEquivalence_554 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsEquivalence_26 #

du_isEquivalence_554 :: T_IsInverse_490 -> T_IsEquivalence_26 #

d_isPartialEquivalence_556 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_556 :: T_IsInverse_490 -> T_IsPartialEquivalence_16 #

d_partialSetoid_558 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_PartialSetoid_10 #

du_partialSetoid_558 :: T_IsInverse_490 -> T_PartialSetoid_10 #

d_refl_560 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny #

du_refl_560 :: T_IsInverse_490 -> AgdaAny -> AgdaAny #

d_reflexive_562 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_562 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_564 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_Setoid_44 #

du_setoid_564 :: T_IsInverse_490 -> T_Setoid_44 #

d_sym_566 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_566 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_568 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_568 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isRightInverse_570 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsRightInverse_408 #

du_isRightInverse_570 :: T_IsInverse_490 -> T_IsRightInverse_408 #

d_strictlyInverse'691'_574 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny #

du_strictlyInverse'691'_574 :: (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> AgdaAny -> AgdaAny #

d_inverse_576 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_Σ_14 #

du_inverse_576 :: T_IsInverse_490 -> T_Σ_14 #

d_IsBiEquivalence_584 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsBiEquivalence_584 #

Constructors

C_IsBiEquivalence'46'constructor_28009 T_IsCongruent_22 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_to'45'isCongruent_598 :: T_IsBiEquivalence_584 -> T_IsCongruent_22 #

d_from'8321''45'cong_600 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'8322''45'cong_602 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence'8321'_606 :: T_IsBiEquivalence_584 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_608 :: T_IsBiEquivalence_584 -> T_IsEquivalence_26 #

d_cong_610 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__614 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> () #

d__'8777'__616 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> () #

d_Carrier_618 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> () #

d_isEquivalence_620 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> T_IsEquivalence_26 #

du_isEquivalence_620 :: T_IsBiEquivalence_584 -> T_IsEquivalence_26 #

d_isPartialEquivalence_622 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_622 :: T_IsBiEquivalence_584 -> T_IsPartialEquivalence_16 #

d_partialSetoid_624 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> T_PartialSetoid_10 #

du_partialSetoid_624 :: T_IsBiEquivalence_584 -> T_PartialSetoid_10 #

d_refl_626 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny #

du_refl_626 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny #

d_reflexive_628 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_628 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_630 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> T_Setoid_44 #

du_setoid_630 :: T_IsBiEquivalence_584 -> T_Setoid_44 #

d_sym_632 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_632 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_634 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_634 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__638 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> () #

d__'8777'__640 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> () #

d_Carrier_642 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> () #

d_isEquivalence_644 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> T_IsEquivalence_26 #

du_isEquivalence_644 :: T_IsBiEquivalence_584 -> T_IsEquivalence_26 #

d_isPartialEquivalence_646 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_646 :: T_IsBiEquivalence_584 -> T_IsPartialEquivalence_16 #

d_partialSetoid_648 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> T_PartialSetoid_10 #

du_partialSetoid_648 :: T_IsBiEquivalence_584 -> T_PartialSetoid_10 #

d_refl_650 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny #

du_refl_650 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny #

d_reflexive_652 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_652 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_654 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> T_Setoid_44 #

du_setoid_654 :: T_IsBiEquivalence_584 -> T_Setoid_44 #

d_sym_656 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_656 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_658 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_658 :: T_IsBiEquivalence_584 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsBiInverse_666 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsBiInverse_666 #

Constructors

C_IsBiInverse'46'constructor_32731 T_IsCongruent_22 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_to'45'isCongruent_684 :: T_IsBiInverse_666 -> T_IsCongruent_22 #

d_from'8321''45'cong_686 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_from'8322''45'cong_688 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'737'_690 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'691'_692 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence'8321'_696 :: T_IsBiInverse_666 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_698 :: T_IsBiInverse_666 -> T_IsEquivalence_26 #

d_cong_700 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__704 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> () #

d__'8777'__706 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> () #

d_Carrier_708 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> () #

d_isEquivalence_710 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> T_IsEquivalence_26 #

du_isEquivalence_710 :: T_IsBiInverse_666 -> T_IsEquivalence_26 #

d_isPartialEquivalence_712 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_712 :: T_IsBiInverse_666 -> T_IsPartialEquivalence_16 #

d_partialSetoid_714 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> T_PartialSetoid_10 #

du_partialSetoid_714 :: T_IsBiInverse_666 -> T_PartialSetoid_10 #

d_refl_716 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny #

du_refl_716 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny #

d_reflexive_718 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_718 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_720 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> T_Setoid_44 #

du_setoid_720 :: T_IsBiInverse_666 -> T_Setoid_44 #

d_sym_722 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_722 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_724 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_724 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__728 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> () #

d__'8777'__730 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> () #

d_Carrier_732 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> () #

d_isEquivalence_734 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> T_IsEquivalence_26 #

du_isEquivalence_734 :: T_IsBiInverse_666 -> T_IsEquivalence_26 #

d_isPartialEquivalence_736 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_736 :: T_IsBiInverse_666 -> T_IsPartialEquivalence_16 #

d_partialSetoid_738 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> T_PartialSetoid_10 #

du_partialSetoid_738 :: T_IsBiInverse_666 -> T_PartialSetoid_10 #

d_refl_740 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny #

du_refl_740 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny #

d_reflexive_742 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_742 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_744 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> T_Setoid_44 #

du_setoid_744 :: T_IsBiInverse_666 -> T_Setoid_44 #

d_sym_746 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_746 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_748 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_748 :: T_IsBiInverse_666 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsSplitSurjection_752 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsSplitSurjection_752 #

Constructors

C_IsSplitSurjection'46'constructor_35501 (AgdaAny -> AgdaAny) T_IsLeftInverse_322

d_from_760 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny #

d_isLeftInverse_762 :: T_IsSplitSurjection_752 -> T_IsLeftInverse_322 #

d_from'45'cong_766 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'737'_768 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_770 :: T_IsSplitSurjection_752 -> T_IsCongruent_22 #

d_isEquivalence'8321'_772 :: T_IsSplitSurjection_752 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_774 :: T_IsSplitSurjection_752 -> T_IsEquivalence_26 #

d_isSurjection_776 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> T_IsSurjection_162 #

du_isSurjection_776 :: T_IsSplitSurjection_752 -> T_IsSurjection_162 #

d_strictlyInverse'737'_778 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny #

du_strictlyInverse'737'_778 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny #

d_cong_780 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__784 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> () #

d__'8777'__786 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> () #

d_Carrier_788 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> () #

d_isEquivalence_790 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> T_IsEquivalence_26 #

du_isEquivalence_790 :: T_IsSplitSurjection_752 -> T_IsEquivalence_26 #

d_isPartialEquivalence_792 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_792 :: T_IsSplitSurjection_752 -> T_IsPartialEquivalence_16 #

d_partialSetoid_794 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> T_PartialSetoid_10 #

du_partialSetoid_794 :: T_IsSplitSurjection_752 -> T_PartialSetoid_10 #

d_refl_796 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny #

du_refl_796 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny #

d_reflexive_798 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_798 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_800 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> T_Setoid_44 #

du_setoid_800 :: T_IsSplitSurjection_752 -> T_Setoid_44 #

d_sym_802 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_802 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_804 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_804 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d__'8776'__808 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> () #

d__'8777'__810 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> () #

d_Carrier_812 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> () #

d_isEquivalence_814 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> T_IsEquivalence_26 #

du_isEquivalence_814 :: T_IsSplitSurjection_752 -> T_IsEquivalence_26 #

d_isPartialEquivalence_816 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> T_IsPartialEquivalence_16 #

du_isPartialEquivalence_816 :: T_IsSplitSurjection_752 -> T_IsPartialEquivalence_16 #

d_partialSetoid_818 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> T_PartialSetoid_10 #

du_partialSetoid_818 :: T_IsSplitSurjection_752 -> T_PartialSetoid_10 #

d_refl_820 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny #

du_refl_820 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny #

d_reflexive_822 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

du_reflexive_822 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny #

d_setoid_824 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> T_Setoid_44 #

du_setoid_824 :: T_IsSplitSurjection_752 -> T_Setoid_44 #

d_sym_826 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_sym_826 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_trans_828 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_trans_828 :: T_IsSplitSurjection_752 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #