← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Algebra/RingSolver/AlmostCommutativeRing.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra/RingSolver/AlmostCommutativeRing.agda
99
99
  }
100
100
  where open AlmostCommutativeRing R
101
101
 
 
102
-- A homomorphism induces a notion of equivalence on the raw ring.
 
103
 
 
104
Induced-equivalence :
 
105
  ∀ {c₁ c₂ ℓ} {Coeff : RawRing c₁} {R : AlmostCommutativeRing c₂ ℓ} →
 
106
  Coeff -Raw-AlmostCommutative⟶ R → Rel (RawRing.Carrier Coeff) ℓ
 
107
Induced-equivalence {R = R} morphism a b = ⟦ a ⟧ ≈ ⟦ b ⟧
 
108
  where
 
109
  open AlmostCommutativeRing R
 
110
  open _-Raw-AlmostCommutative⟶_ morphism
 
111
 
102
112
------------------------------------------------------------------------
103
113
-- Conversions
104
114