Code

Flattening lemma for pushouts#764

Code

Merged

EgbertRijke merged 9 commits intoUniMath:masterUniMath/agda-unimath:masterfrom VojtechStep:feature/flattening-lemmaVojtechStep/agda-unimath:feature/flattening-lemmaCopy head branch name to clipboardSep 13, 2023

Commits

Commits on Sep 13, 2023

• Various computation lemmas

  VojtechStep

  committed
  474f3e4

  Copy full SHA for 474f3e4

• Proof of the flattening lemma for pushouts

  VojtechStep

  committed
  92456f1

  Copy full SHA for 92456f1

• UwUps

  VojtechStep

  committed
  b415cb9

  Copy full SHA for b415cb9

• Fix rebase moving stuff

  VojtechStep

  committed
  f56e6e9

  Copy full SHA for f56e6e9

• Formatting

  VojtechStep

  committed
  ec24749

  Copy full SHA for ec24749

• Add section title

  VojtechStep

  committed
  7f0c440

  Copy full SHA for 7f0c440

• Cosmetic change

  VojtechStep

  committed
  ed362d1

  Copy full SHA for ed362d1

• Elaborate on pre/postcomposition lemmas

  VojtechStep

  committed
  a855562

  Copy full SHA for a855562

• Pesky grammar

  VojtechStep

  committed
  d684cbb

  Copy full SHA for d684cbb