Code

opposite of a Ring#1900

Code

Closed

jamesmckinna wants to merge 21 commits intoagda:masteragda/agda-stdlib:masterfrom

jamesmckinna:ring-opjamesmckinna/agda-stdlib:ring-opCopy head branch name to clipboard

Commits

Commits on Jan 5, 2023

• construction of the opposite of a ring: `IsRing` proofs

  jamesmckinna

  committed
  09f7409

  Copy full SHA for 09f7409

• `CHANGELOG`

  jamesmckinna

  committed
  a681dc7

  Copy full SHA for a681dc7

• bundle

  jamesmckinna

  committed
  2b93bbf

  Copy full SHA for 2b93bbf

Commits on Jan 7, 2023

• refactored `Algebra.Construct.Zero` into `Initial` and `Terminal`

  jamesmckinna

  committed
  69d0dff

  Copy full SHA for 69d0dff

• added `Algebra.Construct.Initial` and `Terminal`

  jamesmckinna

  committed
  92305c2

  Copy full SHA for 92305c2

• refactored `Zero` for modules

  jamesmckinna

  committed
  0d2a36d

  Copy full SHA for 0d2a36d

• consistency between sources

  jamesmckinna

  committed
  22b5b22

  Copy full SHA for 22b5b22

• `CHANGELOG`

  jamesmckinna

  committed
  e54f2a7

  Copy full SHA for e54f2a7

Commits on Jan 8, 2023

• removed unnecessary imports from `Data.Unit`

  jamesmckinna

  committed
  3891c16

  Copy full SHA for 3891c16

Commits on Jan 9, 2023

• Matthew's feedback

  jamesmckinna

  committed
  7c592c1

  Copy full SHA for 7c592c1

• capitalise comments

  jamesmckinna

  committed
  83cb803

  Copy full SHA for 83cb803

• reorder declarations in `𝕆ne`

  jamesmckinna

  committed
  46aa741

  Copy full SHA for 46aa741

• Matthew's simplifications

  jamesmckinna

  committed
  0575c70

  Copy full SHA for 0575c70

• making things 'a little nicer'

  jamesmckinna

  committed
  a0f96d8

  Copy full SHA for a0f96d8

• fix-whitespace

  jamesmckinna

  committed
  3b0923c

  Copy full SHA for 3b0923c

• Merge branch 'ring-op' of https://github.com/jamesmckinna/agda-stdlib into ring-op

  jamesmckinna

  committed
  d23bc6f

  Copy full SHA for d23bc6f

Commits on Jan 10, 2023

• added `CommutativeRing` to the tally

  jamesmckinna

  committed
  5baffde

  Copy full SHA for 5baffde

• Bogus commits have entered the picture.

  Show description for 1fbffab
  jamesmckinna

  committed
  1fbffab

  Copy full SHA for 1fbffab

• Going back to before the spurious commits form #1902 entered this branch/PR

  Show description for a0d1107
  jamesmckinna

  committed
  a0d1107

  Copy full SHA for a0d1107

• restored `Algebra.Construct.Zero`

  jamesmckinna

  committed
  08cdea6

  Copy full SHA for 08cdea6

• re-added `Ring` bundle... now begin again with the review changes

  jamesmckinna

  committed
  64fb403

  Copy full SHA for 64fb403