Documentation

d_inj'8321''8347'_52 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Func_714 #

du_inj'8321''8347'_52 :: T_Func_714 #

d_inj'8322''8347'_54 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Func_714 #

du_inj'8322''8347'_54 :: T_Func_714 #

d_'91'_'44'_'93''8347'_56 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Func_714 -> T_Func_714 -> T_Func_714 #

du_'91'_'44'_'93''8347'_56 :: T_Func_714 -> T_Func_714 -> T_Func_714 #

d_'46'extendedlambda0_66 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Func_714 -> T_Func_714 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> AgdaAny #

du_'46'extendedlambda0_66 :: T_Func_714 -> T_Func_714 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> AgdaAny #

d_swap'8347'_72 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Func_714 #

du_swap'8347'_72 :: T_Func_714 #

d_'8846''45'injective_78 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'8846''45'injective_78 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

d_'8846''45'strictlySurjective_104 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14 #

du_'8846''45'strictlySurjective_104 :: (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14 #

d_'8846''45'surjective_114 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14 #

du_'8846''45'surjective_114 :: (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> T__'8846'__30 -> T_Σ_14 #

d_'46'extendedlambda0_120 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'46'extendedlambda0_120 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

d_'46'extendedlambda1_126 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'46'extendedlambda1_126 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

d__'8846''45'function__132 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Func_714 -> T_Func_714 -> T_Func_714 #

du__'8846''45'function__132 :: T_Func_714 -> T_Func_714 -> T_Func_714 #

d__'8846''45'equivalence__142 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714 #

du__'8846''45'equivalence__142 :: T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714 #

d__'8846''45'injection__152 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Injection_776 -> T_Injection_776 -> T_Injection_776 #

du__'8846''45'injection__152 :: T_Injection_776 -> T_Injection_776 -> T_Injection_776 #

d__'8846''45'surjection__162 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846 #

du__'8846''45'surjection__162 :: T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846 #

d__'8846''45'bijection__172 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926 #

du__'8846''45'bijection__172 :: T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926 #

d__'8846''45'leftInverse__182 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792 #

du__'8846''45'leftInverse__182 :: T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792 #

d_'46'extendedlambda2_192 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_LeftInverse_1792 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'46'extendedlambda2_192 :: T_LeftInverse_1792 -> T_LeftInverse_1792 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

d__'8846''45'rightInverse__198 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880 #

du__'8846''45'rightInverse__198 :: T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880 #

d_'46'extendedlambda2_208 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_RightInverse_1880 -> T_RightInverse_1880 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'46'extendedlambda2_208 :: T_RightInverse_1880 -> T_RightInverse_1880 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

d__'8846''45'inverse__214 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #

du__'8846''45'inverse__214 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #

d_'46'extendedlambda2_224 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Inverse_1960 -> T_Inverse_1960 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'46'extendedlambda2_224 :: T_Inverse_1960 -> T_Inverse_1960 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

d_'46'extendedlambda3_230 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Inverse_1960 -> T_Inverse_1960 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

du_'46'extendedlambda3_230 :: T_Inverse_1960 -> T_Inverse_1960 -> T__'8846'__30 -> T__'8846'__30 -> T_Pointwise_70 -> T_Pointwise_70 #

d__'8846''45'left'45'inverse__236 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792 #