Code

Computational identity types#1015

Code

Merged

EgbertRijke merged 41 commits intoUniMath:masterUniMath/agda-unimath:masterfrom fredrik-bakke:compute-Idfredrik-bakke/agda-unimath:compute-IdCopy head branch name to clipboardFeb 8, 2024

+2,428-43

Commits

Commits on Jan 31, 2024

• Judgmentally involutive identity types

  fredrik-bakke

  committed
  70559c6

  Copy full SHA for 70559c6

• fixes

  fredrik-bakke

  committed
  00feefb

  Copy full SHA for 00feefb

• swap superscript i for superscript -

  fredrik-bakke

  committed
  3eacf4b

  Copy full SHA for 3eacf4b

• add _∙ᵣ_

  fredrik-bakke

  committed
  c6922b8

  Copy full SHA for c6922b8

• The judgmentally right unital concatenation operation on identifications

  fredrik-bakke

  committed
  3def29f

  Copy full SHA for 3def29f

• judgmental left unit law for _∙⁻_

  fredrik-bakke

  committed
  d0f41aa

  Copy full SHA for d0f41aa

• Merge branch 'master' into compute-Id

  fredrik-bakke

  authored
  28d4a4b

  Copy full SHA for 28d4a4b

• pre-commit

  fredrik-bakke

  committed
  43a71e3

  Copy full SHA for 43a71e3

• merge

  fredrik-bakke

  committed
  1a9d35c

  Copy full SHA for 1a9d35c

Commits on Feb 1, 2024

• naming fixes judgmentally involutive identity types

  fredrik-bakke

  committed
  c5a6004

  Copy full SHA for c5a6004

• Judgmentally compositional identity types

  fredrik-bakke

  committed
  58dfbfc

  Copy full SHA for 58dfbfc

• vscode code snippets for equational reasoning

  fredrik-bakke

  committed
  a588ece

  Copy full SHA for a588ece

• The inversion operation on the judgmentally compositional identity types defined by the judgmentally right unital concatenation operation on identifications

  fredrik-bakke

  committed
  9d12fbf

  Copy full SHA for 9d12fbf

• The judgmentally right unital concatenation operation on the judgmentally involutive identity types

  fredrik-bakke

  committed
  3653073

  Copy full SHA for 3653073

• rconcat -> concatr

  fredrik-bakke

  committed
  9ffa4ca

  Copy full SHA for 9ffa4ca

• wip computational identity types

  fredrik-bakke

  committed
  5d43534

  Copy full SHA for 5d43534

• checks

  fredrik-bakke

  committed
  e181181

  Copy full SHA for e181181

• remove wrong text

  fredrik-bakke

  committed
  fcee669

  Copy full SHA for fcee669

Commits on Feb 2, 2024

• finish work?

  fredrik-bakke

  committed
  470df2f

  Copy full SHA for 470df2f

• remove unused imports

  fredrik-bakke

  committed
  332929c

  Copy full SHA for 332929c

• part of review

  fredrik-bakke

  committed
  9541610

  Copy full SHA for 9541610

• judgmental non-dependent eliminator

  fredrik-bakke

  committed
  14f99fa

  Copy full SHA for 14f99fa

Commits on Feb 6, 2024

• wip compute id

  fredrik-bakke

  committed
  5503c12

  Copy full SHA for 5503c12

Commits on Feb 7, 2024

• work yoneda identity types

  fredrik-bakke

  committed
  50a779c

  Copy full SHA for 50a779c

• explanations for judgmentally involutive identity types

  fredrik-bakke

  committed
  ab3ab47

  Copy full SHA for ab3ab47

• Headers are nice

  fredrik-bakke

  committed
  a93cc82

  Copy full SHA for a93cc82

• explanations computational identity types

  fredrik-bakke

  committed
  019b5bd

  Copy full SHA for 019b5bd

• Merge branch 'master' into compute-Id

  fredrik-bakke

  authored
  c12a6a1

  Copy full SHA for c12a6a1

• fix merge conflicts

  fredrik-bakke

  committed
  051e804

  Copy full SHA for 051e804

• rename judgmentally compositional ids to yoneda ids

  fredrik-bakke

  committed
  502a40f

  Copy full SHA for 502a40f

• change judgmental to something else in many places

  fredrik-bakke

  committed
  aac9d2c

  Copy full SHA for aac9d2c

• update identity-types table

  fredrik-bakke

  committed
  27234ae

  Copy full SHA for 27234ae

• common operations on computational identifications

  fredrik-bakke

  committed
  b9dfac0

  Copy full SHA for b9dfac0

• an unused import

  fredrik-bakke

  committed
  2eda7ff

  Copy full SHA for 2eda7ff

• self-review

  fredrik-bakke

  committed
  1d295b5

  Copy full SHA for 1d295b5

• fix link

  fredrik-bakke

  committed
  92e35b5

  Copy full SHA for 92e35b5

• review

  fredrik-bakke

  committed
  f39c8a5

  Copy full SHA for f39c8a5

• remainder of review

  fredrik-bakke

  committed
  7687894

  Copy full SHA for 7687894

• finishing touches

  fredrik-bakke

  committed
  1a2694d

  Copy full SHA for 1a2694d

• fix mistakes

  fredrik-bakke

  committed
  b1cd48a

  Copy full SHA for b1cd48a

• line break

  fredrik-bakke

  committed
  565137d

  Copy full SHA for 565137d