plutus-metatheory-1.60.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

MAlonzo.Code.Relation.Binary.Morphism.Structures

Documentation

d_Homomorphic'8322'_18 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () #

d_IsRelHomomorphism_42 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

newtype T_IsRelHomomorphism_42 #

Constructors

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

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

d_IsRelMonomorphism_64 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsRelMonomorphism_64 #

Constructors

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

d_isHomomorphism_76 :: T_IsRelMonomorphism_64 -> T_IsRelHomomorphism_42 #

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

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

d_IsRelIsomorphism_94 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsRelIsomorphism_94 #

Constructors

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

d_isMonomorphism_106 :: T_IsRelIsomorphism_94 -> T_IsRelMonomorphism_64 #

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

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

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

d_isHomomorphism_116 :: T_IsRelIsomorphism_94 -> T_IsRelHomomorphism_42 #

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

du_bijective_118 :: T_IsRelIsomorphism_94 -> T_Σ_14 #

d_IsOrderHomomorphism_138 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsOrderHomomorphism_138 #

Constructors

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

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

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

d_isRelHomomorphism_160 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42 #

du_isRelHomomorphism_160 :: T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42 #

d_isRelHomomorphism_162 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42 #

du_isRelHomomorphism_162 :: T_IsOrderHomomorphism_138 -> T_IsRelHomomorphism_42 #

d_IsOrderMonomorphism_182 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsOrderMonomorphism_182 #

Constructors

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

d_isOrderHomomorphism_200 :: T_IsOrderMonomorphism_182 -> T_IsOrderHomomorphism_138 #

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

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

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

d_isRelHomomorphism_210 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderMonomorphism_182 -> T_IsRelHomomorphism_42 #

du_isRelHomomorphism_210 :: T_IsOrderMonomorphism_182 -> T_IsRelHomomorphism_42 #

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

d_isRelMonomorphism_216 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_216 :: T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64 #

d_isRelMonomorphism_218 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_218 :: T_IsOrderMonomorphism_182 -> T_IsRelMonomorphism_64 #

d_IsOrderIsomorphism_238 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T_IsOrderIsomorphism_238 #

Constructors

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

d_isOrderMonomorphism_254 :: T_IsOrderIsomorphism_238 -> T_IsOrderMonomorphism_182 #

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

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

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

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

d_isOrderHomomorphism_266 :: T_IsOrderIsomorphism_238 -> T_IsOrderHomomorphism_138 #

d_isRelHomomorphism_268 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderIsomorphism_238 -> T_IsRelHomomorphism_42 #

du_isRelHomomorphism_268 :: T_IsOrderIsomorphism_238 -> T_IsRelHomomorphism_42 #

d_isRelMonomorphism_270 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderIsomorphism_238 -> T_IsRelMonomorphism_64 #

du_isRelMonomorphism_270 :: T_IsOrderIsomorphism_238 -> T_IsRelMonomorphism_64 #

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

d_isRelIsomorphism_276 :: T_Level_18 -> T_Level_18 -> () -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsOrderIsomorphism_238 -> T_IsRelIsomorphism_94 #

du_isRelIsomorphism_276 :: T_IsOrderIsomorphism_238 -> T_IsRelIsomorphism_94 #