Code

Opaque FreeCommAlgebra#1089

Code

Draft

MatthiasHu wants to merge 11 commits intoagda:masteragda/cubical:masterfrom MatthiasHu:opaque-FreeCommAlgebraMatthiasHu/cubical:opaque-FreeCommAlgebraCopy head branch name to clipboard

Commits

Commits on Jul 23, 2024

• fix auto-univalence

  felixwellen

  committed
  d7f2b5d

  Copy full SHA for d7f2b5d

• fix FreeCommAlg

  felixwellen

  committed
  89345fb

  Copy full SHA for 89345fb

• fix subalgebra

  felixwellen

  committed
  24f2ab7

  Copy full SHA for 24f2ab7

• fix FPAlgebra

  felixwellen

  committed
  2878b76

  Copy full SHA for 2878b76

• copy Evans approach for Groups

  felixwellen

  committed
  9c3a53e

  Copy full SHA for 9c3a53e

Commits on Jul 24, 2024

• (wip) opaque FreeCommAlgebra

  

  MatthiasHu

  authored and

  felixwellen

  committed
  e9712a7

  Copy full SHA for e9712a7

• strengthen makeCommAlgebraHom

  

  MatthiasHu

  authored and

  felixwellen

  committed
  4540f70

  Copy full SHA for 4540f70

• (wip) experiment redoing OnCoproduct

  

  MatthiasHu

  authored and

  felixwellen

  committed
  cf402df

  Copy full SHA for cf402df

• WIP

  felixwellen

  committed
  efc76c4

  Copy full SHA for efc76c4

• still allow definitional commutativity with projecting to the carrier

  felixwellen

  committed
  815d8c2

  Copy full SHA for 815d8c2

• start with other universal property of free comm alg

  felixwellen

  committed
  16e3338

  Copy full SHA for 16e3338