Code

a recursive view of Fin n#1923

Code

Merged

MatthewDaggitt merged 43 commits intoagda:masteragda/agda-stdlib:masterfrom jamesmckinna:top-viewjamesmckinna/agda-stdlib:top-viewCopy head branch name to clipboardSep 18, 2023

Commits

Commits on May 12, 2023

• a view of Fin (suc n)

  jamesmckinna

  committed
  75fa9d0

  Copy full SHA for 75fa9d0

• documentation

  jamesmckinna

  committed
  629b415

  Copy full SHA for 629b415

• theory of opposite also

  jamesmckinna

  committed
  c6a9994

  Copy full SHA for c6a9994

• tweak

  jamesmckinna

  committed
  d6e7b9c

  Copy full SHA for d6e7b9c

• first of Jacques' review changes

  jamesmckinna

  committed
  d2173fb

  Copy full SHA for d2173fb

• refactored according to Jacques' prescriptions; renamed the inverse

  jamesmckinna

  committed
  6e0c4be

  Copy full SHA for 6e0c4be

• fix whitespace

  jamesmckinna

  committed
  1021deb

  Copy full SHA for 1021deb

• tightened imports

  jamesmckinna

  committed
  a870d69

  Copy full SHA for a870d69

• tightened imports

  jamesmckinna

  committed
  c766cc7

  Copy full SHA for c766cc7

• tightened imports

  jamesmckinna

  committed
  f43a21f

  Copy full SHA for f43a21f

• cosmetics

  jamesmckinna

  committed
  66bc0c7

  Copy full SHA for 66bc0c7

• rmeoved redundant

  jamesmckinna

  committed
  8eff5d6

  Copy full SHA for 8eff5d6

• made Instances not public

  jamesmckinna

  committed
  6576fe5

  Copy full SHA for 6576fe5

• slight refactor

  jamesmckinna

  committed
  c18173c

  Copy full SHA for c18173c

• symmetry typo

  jamesmckinna

  committed
  d4069e9

  Copy full SHA for d4069e9

• imports

  jamesmckinna

  committed
  6d4cc58

  Copy full SHA for 6d4cc58

• other use of lower₁ in Data.Fin.Induction

  jamesmckinna

  committed
  0e6db5e

  Copy full SHA for 0e6db5e

• previously uncommitted comment on the View itself

  jamesmckinna

  committed
  fa28f4c

  Copy full SHA for fa28f4c

• tidied up imports for Top view

  jamesmckinna

  committed
  c51dd63

  Copy full SHA for c51dd63

• made --cubical-compatible

  jamesmckinna

  committed
  904fdbe

  Copy full SHA for 904fdbe

• better use of variables

  jamesmckinna

  committed
  f3550ad

  Copy full SHA for f3550ad

Commits on May 14, 2023

• (vertical) whitespace)

  jamesmckinna

  committed
  9a0d6ad

  Copy full SHA for 9a0d6ad

Commits on Sep 12, 2023

• made the view recursive; with simplifications

  jamesmckinna

  committed
  1dd382e

  Copy full SHA for 1dd382e

• final tweaks; use of variable {n} still needed in places

  jamesmckinna

  committed
  f10cb3f

  Copy full SHA for f10cb3f

• streamlined use of instances

  jamesmckinna

  committed
  d878b2c

  Copy full SHA for d878b2c

• revised names, as per discusison

  jamesmckinna

  committed
  c0d5651

  Copy full SHA for c0d5651

• factored out Instances; revised README and CHANGELOG

  jamesmckinna

  committed
  2c94427

  Copy full SHA for 2c94427

• followed Matthew's suggestion better; added uniqueness proof for the view; cosmetic tweaks

  jamesmckinna

  committed
  9bce07e

  Copy full SHA for 9bce07e

• typo

  jamesmckinna

  committed
  9012225

  Copy full SHA for 9012225

• revised Instances

  jamesmckinna

  committed
  c7e7c9e

  Copy full SHA for c7e7c9e

• fresh round of variable review comments

  jamesmckinna

  committed
  1f1f9f3

  Copy full SHA for 1f1f9f3

• sharpened use of instances in response to review comments

  jamesmckinna

  committed
  a88d39c

  Copy full SHA for a88d39c

• reordering

  jamesmckinna

  committed
  c962e14

  Copy full SHA for c962e14

• fromℕ≢inject₁ now takes implicit argument

  jamesmckinna

  committed
  6ba18be

  Copy full SHA for 6ba18be

• CHANGELOG!

  jamesmckinna

  committed
  c7b3acf

  Copy full SHA for c7b3acf

Commits on Sep 14, 2023

• tidy up comments and binders

  jamesmckinna

  committed
  eae3f83

  Copy full SHA for eae3f83

Commits on Sep 15, 2023

• Change to use i rather than j in Top

  MatthewDaggitt

  committed
  4a4a4e2

  Copy full SHA for 4a4a4e2

• uniform naming scheme

  jamesmckinna

  committed
  c8451d7

  Copy full SHA for c8451d7

• Merge branch 'top-view' of github.com:jamesmckinna/agda-stdlib into top-view

  Show description for 6d8979d
  jamesmckinna

  committed
  6d8979d

  Copy full SHA for 6d8979d

Commits on Sep 17, 2023

• removed Instances

  jamesmckinna

  committed
  21500e9

  Copy full SHA for 21500e9

• removed inject₁⁻¹

  jamesmckinna

  committed
  c5ed38f

  Copy full SHA for c5ed38f

• removed Top.Instances

  jamesmckinna

  committed
  cb3eb95

  Copy full SHA for cb3eb95

• drastic import simplification

  jamesmckinna

  committed
  7207c6e

  Copy full SHA for 7207c6e