Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Algebra.Consequences.Setoid

Documentation

d__DistributesOver'691'__40 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'737'__42 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_AlmostLeftCancellative_50 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_AlmostRightCancellative_52 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Associative_54 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Commutative_58 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Congruent'8322'_62 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Identity_70 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftCancellative_78 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftIdentity_84 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftInverse_86 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftZero_88 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightCancellative_90 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightIdentity_96 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightInverse_98 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightZero_100 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_comm'43'cancel'737''8658'cancel'691'_138 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_comm'43'cancel'737''8658'cancel'691'_138 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm'43'cancel'691''8658'cancel'737'_150 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_comm'43'cancel'691''8658'cancel'737'_150 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm'43'id'737''8658'id'691'_172 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'id'737''8658'id'691'_172 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'id'691''8658'id'737'_178 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'id'691''8658'id'737'_178 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'ze'737''8658'ze'691'_184 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'ze'737''8658'ze'691'_184 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'ze'691''8658'ze'737'_190 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'ze'691''8658'ze'737'_190 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'almostCancel'737''8658'almostCancel'691'_196 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny Source #

du_comm'43'almostCancel'737''8658'almostCancel'691'_196 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny Source #

d_comm'43'almostCancel'691''8658'almostCancel'737'_210 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny Source #

du_comm'43'almostCancel'691''8658'almostCancel'737'_210 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny Source #

d_comm'43'inv'737''8658'inv'691'_236 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'inv'737''8658'inv'691'_236 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'inv'691''8658'inv'737'_242 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'inv'691''8658'inv'737'_242 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_assoc'43'id'43'inv'691''8658'inv'737''45'unique_264 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc'43'id'43'inv'691''8658'inv'737''45'unique_264 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc'43'id'43'inv'737''8658'inv'691''45'unique_284 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_assoc'43'id'43'inv'737''8658'inv'691''45'unique_284 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm'43'distr'737''8658'distr'691'_312 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_comm'43'distr'737''8658'distr'691'_312 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm'43'distr'691''8658'distr'737'_322 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_comm'43'distr'691''8658'distr'737'_322 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm'8658'sym'91'distrib'737''93'_338 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_comm'8658'sym'91'distrib'737''93'_338 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_subst'43'comm'8658'sym_406 ∷ T_Setoid_44 → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_subst'43'comm'8658'sym_406 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_wlog_420 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

du_wlog_420 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #