Safe HaskellNone

MAlonzo.Code.Function.Inverse

Documentation

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

data T__InverseOf__20 Source #

Constructors

C__InverseOf_'46'constructor_1525 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) 

d_left'45'inverse'45'of_42 :: T__InverseOf__20 -> AgdaAny -> AgdaAny Source #

d_right'45'inverse'45'of_44 :: T__InverseOf__20 -> AgdaAny -> AgdaAny Source #

d_Inverse_58 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_Inverse_58 Source #

Constructors

C_Inverse'46'constructor_2615 T_Π_16 T_Π_16 T__InverseOf__20 

d_to_78 :: T_Inverse_58 -> T_Π_16 Source #

d_from_80 :: T_Inverse_58 -> T_Π_16 Source #

d_inverse'45'of_82 :: T_Inverse_58 -> T__InverseOf__20 Source #

d_left'45'inverse'45'of_86 :: T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d_right'45'inverse'45'of_88 :: T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d_left'45'inverse_90 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_LeftInverse_82 Source #

du_left'45'inverse_90 :: T_Inverse_58 -> T_LeftInverse_82 Source #

d_injection_94 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Injection_88 Source #

du_injection_94 :: T_Setoid_44 -> T_Inverse_58 -> T_Injection_88 Source #

d_injective_96 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_injective_96 :: T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_bijection_98 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64 Source #

du_bijection_98 :: T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64 Source #

d_equivalence_102 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Equivalence_16 Source #

du_equivalence_102 :: T_Setoid_44 -> T_Inverse_58 -> T_Equivalence_16 Source #

d_to'45'from_104 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_to'45'from_104 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_right'45'inverse_106 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_LeftInverse_82 Source #

du_right'45'inverse_106 :: T_Setoid_44 -> T_Inverse_58 -> T_LeftInverse_82 Source #

d_surjection_108 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Surjection_54 Source #

du_surjection_108 :: T_Setoid_44 -> T_Inverse_58 -> T_Surjection_54 Source #

d_surjective_110 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Surjective_18 Source #

du_surjective_110 :: T_Setoid_44 -> T_Inverse_58 -> T_Surjective_18 Source #

d_to'45'from_112 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_to'45'from_112 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8596'__118 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d__'8596''775'__132 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> () Source #

d_inverse_156 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> (AgdaAny -> T__'8801'__12) -> T_Inverse_58 Source #

du_inverse_156 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> (AgdaAny -> T__'8801'__12) -> T_Inverse_58 Source #

d_fromBijection_178 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> T_Inverse_58 Source #

du_fromBijection_178 :: T_Bijection_64 -> T_Inverse_58 Source #

d_id_186 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Inverse_58 Source #

du_id_186 :: T_Setoid_44 -> T_Inverse_58 Source #

d_id'8242'_194 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_LeftInverse_82 Source #

du_id'8242'_194 :: T_Setoid_44 -> T_LeftInverse_82 Source #

d__'8728'__208 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58 Source #

du__'8728'__208 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58 Source #

d_sym_226 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 Source #

du_sym_226 :: T_Inverse_58 -> T_Inverse_58 Source #

d_bijection_236 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64 Source #

du_bijection_236 :: T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64 Source #

d_equivalence_238 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Equivalence_16 Source #

du_equivalence_238 :: T_Setoid_44 -> T_Inverse_58 -> T_Equivalence_16 Source #

d_from_240 :: T_Inverse_58 -> T_Π_16 Source #

d_to'45'from_242 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_to'45'from_242 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injection_244 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Injection_88 Source #

du_injection_244 :: T_Setoid_44 -> T_Inverse_58 -> T_Injection_88 Source #

d_injective_246 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_injective_246 :: T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse'45'of_248 :: T_Inverse_58 -> T__InverseOf__20 Source #

d_left'45'inverse_250 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_LeftInverse_82 Source #

du_left'45'inverse_250 :: T_Inverse_58 -> T_LeftInverse_82 Source #

d_left'45'inverse'45'of_252 :: T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d_right'45'inverse_254 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_LeftInverse_82 Source #

du_right'45'inverse_254 :: T_Setoid_44 -> T_Inverse_58 -> T_LeftInverse_82 Source #

d_right'45'inverse'45'of_256 :: T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d_surjection_258 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Surjection_54 Source #

du_surjection_258 :: T_Setoid_44 -> T_Inverse_58 -> T_Surjection_54 Source #

d_surjective_260 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> T_Surjective_18 Source #

du_surjective_260 :: T_Setoid_44 -> T_Inverse_58 -> T_Surjective_18 Source #

d_to_262 :: T_Inverse_58 -> T_Π_16 Source #

d_to'45'from_264 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_to'45'from_264 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_map_298 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_Inverse_58 Source #

du_map_298 :: (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_Inverse_58 Source #

d_bijection_314 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_Bijection_64 Source #

du_bijection_314 :: T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64 Source #

d_equivalence_316 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_Equivalence_16 Source #

du_equivalence_316 :: T_Setoid_44 -> T_Inverse_58 -> T_Equivalence_16 Source #

d_from_318 :: T_Inverse_58 -> T_Π_16 Source #

d_to'45'from_320 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_to'45'from_320 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injection_322 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_Injection_88 Source #

du_injection_322 :: T_Setoid_44 -> T_Inverse_58 -> T_Injection_88 Source #

d_injective_324 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_injective_324 :: T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_inverse'45'of_326 :: T_Inverse_58 -> T__InverseOf__20 Source #

d_left'45'inverse_328 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_LeftInverse_82 Source #

du_left'45'inverse_328 :: T_Inverse_58 -> T_LeftInverse_82 Source #

d_left'45'inverse'45'of_330 :: T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d_right'45'inverse_332 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_LeftInverse_82 Source #

du_right'45'inverse_332 :: T_Setoid_44 -> T_Inverse_58 -> T_LeftInverse_82 Source #

d_right'45'inverse'45'of_334 :: T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d_surjection_336 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_Surjection_54 Source #

du_surjection_336 :: T_Setoid_44 -> T_Inverse_58 -> T_Surjection_54 Source #

d_surjective_338 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_Surjective_18 Source #

du_surjective_338 :: T_Setoid_44 -> T_Inverse_58 -> T_Surjective_18 Source #

d_to_340 :: T_Inverse_58 -> T_Π_16 Source #

d_to'45'from_342 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_to'45'from_342 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_58 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_zip_392 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> (T_Π_16 -> T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58 Source #

du_zip_392 :: (T_Π_16 -> T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T_Π_16) -> (T_Π_16 -> T_Π_16 -> T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T__InverseOf__20 -> T__InverseOf__20) -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58 Source #