Code

Equality in iterated Sigma types#899

Code

Merged

fredrik-bakke merged 7 commits intoUniMath:masterUniMath/agda-unimath:masterfrom maybemabeline:equality-iterated-sum-typesmaybemabeline/agda-unimath:equality-iterated-sum-typesCopy head branch name to clipboardNov 9, 2023

+115-7

Commits

Commits on Nov 2, 2023

• Compute equalities

  maybemabeline

  committed
  1bd7e40

  Copy full SHA for 1bd7e40

• pre-commit

  maybemabeline

  committed
  ebd5af7

  Copy full SHA for ebd5af7

Commits on Nov 3, 2023

• Renaming and cleanup

  maybemabeline

  committed
  3ec095f

  Copy full SHA for 3ec095f

• Interchange law

  maybemabeline

  committed
  d4a3373

  Copy full SHA for d4a3373

• Formatting and quadruples

  maybemabeline

  committed
  a9d3b66

  Copy full SHA for a9d3b66

Commits on Nov 8, 2023

• Merge branch 'master' into equality-iterated-sum-types

  maybemabeline

  authored
  756e788

  Copy full SHA for 756e788

Commits on Nov 9, 2023

• Merge branch 'master' into equality-iterated-sum-types

  fredrik-bakke

  authored
  be0bd8a

  Copy full SHA for be0bd8a