plutus-metatheory-0.1.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) → () Source #

d_IsRelHomomorphism_42 ∷ p → p → p → p → p → p → p → p → p → () Source #

newtype T_IsRelHomomorphism_42 Source #

Constructors

C_IsRelHomomorphism'46'constructor_587 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) 

d_cong_52 ∷ T_IsRelHomomorphism_42 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsRelMonomorphism_64 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsRelMonomorphism_64 Source #

Constructors

C_IsRelMonomorphism'46'constructor_1563 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 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsRelIsomorphism_94 Source #

Constructors

C_IsRelIsomorphism'46'constructor_3019 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_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsRelIsomorphism_94 → T_Σ_14 Source #

du_bijective_118 ∷ T_IsRelIsomorphism_94 → T_Σ_14 Source #

d_IsOrderHomomorphism_138 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsOrderHomomorphism_138 Source #

Constructors

C_IsOrderHomomorphism'46'constructor_5435 (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_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 Source #

du_isRelHomomorphism_160 ∷ T_IsOrderHomomorphism_138 → T_IsRelHomomorphism_42 Source #

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 Source #

du_isRelHomomorphism_162 ∷ T_IsOrderHomomorphism_138 → T_IsRelHomomorphism_42 Source #

d_IsOrderMonomorphism_182 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsOrderMonomorphism_182 Source #

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 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_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 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_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 Source #

du_isRelMonomorphism_216 ∷ T_IsOrderMonomorphism_182 → T_IsRelMonomorphism_64 Source #

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 Source #

du_isRelMonomorphism_218 ∷ T_IsOrderMonomorphism_182 → T_IsRelMonomorphism_64 Source #

d_IsOrderIsomorphism_238 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsOrderIsomorphism_238 Source #

Constructors

C_IsOrderIsomorphism'46'constructor_14201 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_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 Source #

du_isRelHomomorphism_268 ∷ T_IsOrderIsomorphism_238 → T_IsRelHomomorphism_42 Source #

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 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_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 Source #

du_isRelIsomorphism_276 ∷ T_IsOrderIsomorphism_238 → T_IsRelIsomorphism_94 Source #