Safe HaskellNone

MAlonzo.Code.Relation.Binary.Morphism.Structures

Documentation

d_Homomorphic'8322'_18 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

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

newtype T_IsRelHomomorphism_42 Source #

Constructors

C_IsRelHomomorphism'46'constructor_371 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

d_cong_52 :: T_IsRelHomomorphism_42 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

data T_IsRelMonomorphism_64 Source #

Constructors

C_IsRelMonomorphism'46'constructor_1081 T_IsRelHomomorphism_42 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

d_isHomomorphism_76 :: T_IsRelMonomorphism_64 -> T_IsRelHomomorphism_42 Source #

d_injective_78 :: T_IsRelMonomorphism_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_82 :: T_IsRelMonomorphism_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

data T_IsRelIsomorphism_94 Source #

Constructors

C_IsRelIsomorphism'46'constructor_2169 T_IsRelMonomorphism_64 (AgdaAny -> T_Σ_14) 

d_isMonomorphism_106 :: T_IsRelIsomorphism_94 -> T_IsRelMonomorphism_64 Source #

d_surjective_108 :: T_IsRelIsomorphism_94 -> AgdaAny -> T_Σ_14 Source #

d_cong_112 :: T_IsRelIsomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_114 :: T_IsRelIsomorphism_94 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isHomomorphism_116 :: T_IsRelIsomorphism_94 -> T_IsRelHomomorphism_42 Source #

d_bijective_118 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsRelIsomorphism_94 -> T_Σ_14 Source #

du_bijective_118 :: T_IsRelIsomorphism_94 -> T_Σ_14 Source #

d_IsOrderHomomorphism_138 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> p12 -> p13 -> () Source #

data T_IsOrderHomomorphism_138 Source #

Constructors

C_IsOrderHomomorphism'46'constructor_4003 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

d_cong_154 :: T_IsOrderHomomorphism_138 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_mono_156 :: T_IsOrderHomomorphism_138 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_160 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42 Source #

du_isRelHomomorphism_160 :: T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42 Source #

d_isRelHomomorphism_162 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42 Source #

du_isRelHomomorphism_162 :: T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42 Source #

d_IsOrderMonomorphism_182 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> p12 -> p13 -> () Source #

data T_IsOrderMonomorphism_182 Source #

Constructors

C_IsOrderMonomorphism'46'constructor_6709 T_IsOrderHomomorphism_138 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) 

d_isOrderHomomorphism_200 :: T_IsOrderMonomorphism_182 -> T_IsOrderHomomorphism_138 Source #

d_injective_202 :: T_IsOrderMonomorphism_182 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cancel_204 :: T_IsOrderMonomorphism_182 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_208 :: T_IsOrderMonomorphism_182 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelHomomorphism_210 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderMonomorphism_182 -> T_IsRelHomomorphism_42 Source #

du_isRelHomomorphism_210 :: T_IsOrderMonomorphism_182 -> T_IsRelHomomorphism_42 Source #

d_mono_212 :: T_IsOrderMonomorphism_182 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelMonomorphism_216 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_216 :: T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64 Source #

d_isRelMonomorphism_218 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_218 :: T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64 Source #

d_IsOrderIsomorphism_238 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> p12 -> p13 -> () Source #

data T_IsOrderIsomorphism_238 Source #

Constructors

C_IsOrderIsomorphism'46'constructor_10541 T_IsOrderMonomorphism_182 (AgdaAny -> T_Σ_14) 

d_isOrderMonomorphism_254 :: T_IsOrderIsomorphism_238 -> T_IsOrderMonomorphism_182 Source #

d_surjective_256 :: T_IsOrderIsomorphism_238 -> AgdaAny -> T_Σ_14 Source #

d_cancel_260 :: T_IsOrderIsomorphism_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_cong_262 :: T_IsOrderIsomorphism_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_264 :: T_IsOrderIsomorphism_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isOrderHomomorphism_266 :: T_IsOrderIsomorphism_238 -> T_IsOrderHomomorphism_138 Source #

d_isRelHomomorphism_268 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderIsomorphism_238 -> T_IsRelHomomorphism_42 Source #

du_isRelHomomorphism_268 :: T_IsOrderIsomorphism_238 -> T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_270 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderIsomorphism_238 -> T_IsRelMonomorphism_64 Source #

du_isRelMonomorphism_270 :: T_IsOrderIsomorphism_238 -> T_IsRelMonomorphism_64 Source #

d_mono_272 :: T_IsOrderIsomorphism_238 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isRelIsomorphism_276 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderIsomorphism_238 -> T_IsRelIsomorphism_94 Source #

du_isRelIsomorphism_276 :: T_IsOrderIsomorphism_238 -> T_IsRelIsomorphism_94 Source #