Safe Haskell	Safe-Inferred
Language	Haskell2010

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_constructor_54 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

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

d_IsRelMonomorphism_66 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsRelMonomorphism_66 Source #

Constructors

C_constructor_86 T_IsRelHomomorphism_42 (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isHomomorphism_78 ∷ T_IsRelMonomorphism_66 → T_IsRelHomomorphism_42 Source #

d_injective_80 ∷ T_IsRelMonomorphism_66 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_84 ∷ T_IsRelMonomorphism_66 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_IsRelIsomorphism_98 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T_IsRelIsomorphism_98 Source #

Constructors

C_constructor_124 T_IsRelMonomorphism_66 (AgdaAny → T_Σ_14)

d_isMonomorphism_110 ∷ T_IsRelIsomorphism_98 → T_IsRelMonomorphism_66 Source #

d_surjective_112 ∷ T_IsRelIsomorphism_98 → AgdaAny → T_Σ_14 Source #

d_cong_116 ∷ T_IsRelIsomorphism_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_118 ∷ T_IsRelIsomorphism_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isHomomorphism_120 ∷ T_IsRelIsomorphism_98 → T_IsRelHomomorphism_42 Source #

d_bijective_122 ∷ T_Level_18 → T_Level_18 → () → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsRelIsomorphism_98 → T_Σ_14 Source #

du_bijective_122 ∷ T_IsRelIsomorphism_98 → T_Σ_14 Source #

d_IsOrderHomomorphism_144 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsOrderHomomorphism_144 Source #

Constructors

C_constructor_170 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_cong_160 ∷ T_IsOrderHomomorphism_144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_mono_162 ∷ T_IsOrderHomomorphism_144 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_166 ∷ 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_144 → T_IsRelHomomorphism_42 Source #

du_isRelHomomorphism_166 ∷ T_IsOrderHomomorphism_144 → T_IsRelHomomorphism_42 Source #

d_isRelHomomorphism_168 ∷ 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_144 → T_IsRelHomomorphism_42 Source #

du_isRelHomomorphism_168 ∷ T_IsOrderHomomorphism_144 → T_IsRelHomomorphism_42 Source #

d_IsOrderMonomorphism_190 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsOrderMonomorphism_190 Source #

Constructors

C_constructor_228 T_IsOrderHomomorphism_144 (AgdaAny → AgdaAny → AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny)

d_isOrderHomomorphism_208 ∷ T_IsOrderMonomorphism_190 → T_IsOrderHomomorphism_144 Source #

d_injective_210 ∷ T_IsOrderMonomorphism_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cancel_212 ∷ T_IsOrderMonomorphism_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_216 ∷ T_IsOrderMonomorphism_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelHomomorphism_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_190 → T_IsRelHomomorphism_42 Source #

du_isRelHomomorphism_218 ∷ T_IsOrderMonomorphism_190 → T_IsRelHomomorphism_42 Source #

d_mono_220 ∷ T_IsOrderMonomorphism_190 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelMonomorphism_224 ∷ 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_190 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_224 ∷ T_IsOrderMonomorphism_190 → T_IsRelMonomorphism_66 Source #

d_isRelMonomorphism_226 ∷ 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_190 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_226 ∷ T_IsOrderMonomorphism_190 → T_IsRelMonomorphism_66 Source #

d_IsOrderIsomorphism_248 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsOrderIsomorphism_248 Source #

Constructors

C_constructor_288 T_IsOrderMonomorphism_190 (AgdaAny → T_Σ_14)

d_isOrderMonomorphism_264 ∷ T_IsOrderIsomorphism_248 → T_IsOrderMonomorphism_190 Source #

d_surjective_266 ∷ T_IsOrderIsomorphism_248 → AgdaAny → T_Σ_14 Source #

d_cancel_270 ∷ T_IsOrderIsomorphism_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_cong_272 ∷ T_IsOrderIsomorphism_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injective_274 ∷ T_IsOrderIsomorphism_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isOrderHomomorphism_276 ∷ T_IsOrderIsomorphism_248 → T_IsOrderHomomorphism_144 Source #

d_isRelHomomorphism_278 ∷ 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_248 → T_IsRelHomomorphism_42 Source #

du_isRelHomomorphism_278 ∷ T_IsOrderIsomorphism_248 → T_IsRelHomomorphism_42 Source #

d_isRelMonomorphism_280 ∷ 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_248 → T_IsRelMonomorphism_66 Source #

du_isRelMonomorphism_280 ∷ T_IsOrderIsomorphism_248 → T_IsRelMonomorphism_66 Source #

d_mono_282 ∷ T_IsOrderIsomorphism_248 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isRelIsomorphism_286 ∷ 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_248 → T_IsRelIsomorphism_98 Source #

du_isRelIsomorphism_286 ∷ T_IsOrderIsomorphism_248 → T_IsRelIsomorphism_98 Source #