Code

FunExt implies WeakFunExt#74

Code

Merged

emilyriehl merged 8 commits intorzk-lang:mainrzk-lang/sHoTT:mainfrom MatthiasHu:weakfunext-vs-funextMatthiasHu/sHoTT:weakfunext-vs-funextCopy head branch name to clipboardOct 3, 2023

+22-14

Commits

Commits on Sep 28, 2023

• delete this, as suggested by Emily

  MatthiasHu

  committed
  f638c5a

• weakfunext-funext

  MatthiasHu

  committed
  8419403

• name idea

  MatthiasHu

  committed
  2b38f90

Commits on Sep 29, 2023

• polish

  MatthiasHu

  committed
  4132c1b

• clean up

  MatthiasHu

  committed
  c4405ed

• remove unusual annotation

  MatthiasHu

  committed
  77fc08d

Commits on Oct 2, 2023

• improve naming

  MatthiasHu

  committed
  7f20903

• Merge branch 'main' into weakfunext-vs-funext

  jonweinb

  authored
  8e7717d