Code

Closed Modality#970

Code

Merged

ecavallo merged 5 commits intoagda:masteragda/cubical:masterfrom markrd-williams:mastermarkrd-williams/cubical:masterCopy head branch name to clipboardJan 14, 2023

+49

Commits

Commits on Jan 10, 2023

• Add left unit law for join

  markrd-williams

  committed
  5cf36fd

• Implement closed modality

  markrd-williams

  committed
  62a43ce

• Remove extra imports and comment

  markrd-williams

  committed
  553342f

Commits on Jan 13, 2023

• Merge branch 'agda:master' into master

  markrd-williams

  authored
  7cde03a

Commits on Jan 14, 2023

• Simplify closed elim rule and rename join annihilation law

  markrd-williams

  committed
  7db9d9b