Code

Add initial commutative algebra#664

Code

Merged

mortberg merged 6 commits intoagda:masteragda/cubical:masterfrom felixwellen:initial-algebrafelixwellen/cubical:initial-algebraCopy head branch name to clipboardDec 17, 2021

+126

Commits

Commits on Dec 13, 2021

• make-function for CommAlgebraHoms

  felixwellen

  committed
  c01e5a0

  Copy full SHA for c01e5a0

• show that IsCommAlgebraHom is a Prop

  felixwellen

  committed
  ceb9cc7

  Copy full SHA for ceb9cc7

• Construct initial commutative R-Algebra

  felixwellen

  committed
  42871ee

  Copy full SHA for 42871ee

Commits on Dec 15, 2021

• Fixes for Anders' comments

  felixwellen

  committed
  8cc16cc

  Copy full SHA for 8cc16cc

• Whitespace

  felixwellen

  committed
  c2c0609

  Copy full SHA for c2c0609

Commits on Dec 16, 2021

• Whitespace

  felixwellen

  committed
  6dc2161

  Copy full SHA for 6dc2161