Code

Universal property of smash products#865

Code

Merged

fredrik-bakke merged 22 commits intoUniMath:masterUniMath/agda-unimath:masterfrom maybemabeline:universal-property-of-smash-productsmaybemabeline/agda-unimath:universal-property-of-smash-productsCopy head branch name to clipboardOct 31, 2023

+450-38

Commits

Commits on Oct 19, 2023

• Preliminary work

  maybemabeline

  committed
  e857921

  Copy full SHA for e857921

• Remove notes

  maybemabeline

  committed
  66592cc

  Copy full SHA for 66592cc

• Remove remaining notes

  maybemabeline

  committed
  bf255b0

  Copy full SHA for bf255b0

Commits on Oct 20, 2023

• Reformat

  maybemabeline

  committed
  86096d4

  Copy full SHA for 86096d4

Commits on Oct 22, 2023

• Compute coherences

  maybemabeline

  committed
  329668e

  Copy full SHA for 329668e

• Add titles

  maybemabeline

  committed
  c69d6c2

  Copy full SHA for c69d6c2

• Change prefixes

  maybemabeline

  committed
  b6ed7e7

  Copy full SHA for b6ed7e7

• Merge branch 'master' into universal-property-of-smash-products

  maybemabeline

  authored
  b9e98f0

  Copy full SHA for b9e98f0

• Compute one side of universal property

  maybemabeline

  committed
  4904a5d

  Copy full SHA for 4904a5d

Commits on Oct 23, 2023

• Dependent pair type accessors

  maybemabeline

  committed
  8bd0f99

  Copy full SHA for 8bd0f99

Commits on Oct 29, 2023

• Renaming

  maybemabeline

  committed
  4874385

  Copy full SHA for 4874385

• Merge branch 'master' into universal-property-of-smash-products

  maybemabeline

  authored
  a7cbe35

  Copy full SHA for a7cbe35

• Apply suggestions from code review

  Show description for f2ef33c
  

  maybemabeline

  and

  fredrik-bakke

  authored
  f2ef33c

  Copy full SHA for f2ef33c

• Reformat homotopies and rebracket commuting-square

  maybemabeline

  committed
  52d7e93

  Copy full SHA for 52d7e93

Commits on Oct 30, 2023

• Rework coherence proof

  maybemabeline

  committed
  5d73e9c

  Copy full SHA for 5d73e9c

• pre-commit

  maybemabeline

  committed
  43f12ee

  Copy full SHA for 43f12ee

• Indentation

  maybemabeline

  committed
  8a0e75c

  Copy full SHA for 8a0e75c

• Precedence of pointed homotopies

  maybemabeline

  committed
  a72b2c5

  Copy full SHA for a72b2c5

• Explanatory text

  maybemabeline

  committed
  428eb00

  Copy full SHA for 428eb00

• Renaming equalities

  maybemabeline

  committed
  deff983

  Copy full SHA for deff983

Commits on Oct 31, 2023

• Renaming and fix indentation

  maybemabeline

  committed
  37dba43

  Copy full SHA for 37dba43

• Merge branch 'master' into universal-property-of-smash-products

  maybemabeline

  authored
  c6c713c

  Copy full SHA for c6c713c