Code

Sequential limits#839

Code

Merged

EgbertRijke merged 47 commits intoUniMath:masterUniMath/agda-unimath:masterfrom fredrik-bakke:towerfredrik-bakke/agda-unimath:towerCopy head branch name to clipboardOct 16, 2023

+2,494-868

Commits

Commits on Oct 13, 2023

• towers

  fredrik-bakke

  committed
  85dac52

  Copy full SHA for 85dac52

Commits on Oct 14, 2023

• universal property of limits of towers

  fredrik-bakke

  committed
  1177563

  Copy full SHA for 1177563

• patch file generation MAlonzo

  fredrik-bakke

  committed
  7d83c9c

  Copy full SHA for 7d83c9c

• more additions universal-property-limits-of-towers

  fredrik-bakke

  committed
  aec13d6

  Copy full SHA for aec13d6

• rename canonical-pullback -> standard-pullback

  fredrik-bakke

  committed
  93bfbe7

  Copy full SHA for 93bfbe7

• touch-up foundation-core.pullbacks

  fredrik-bakke

  committed
  efef160

  Copy full SHA for efef160

• a little touch-up foundation.pullbacks

  fredrik-bakke

  committed
  f75ba9b

  Copy full SHA for f75ba9b

• more fixes

  fredrik-bakke

  committed
  81ead26

  Copy full SHA for 81ead26

• shifting towers

  fredrik-bakke

  committed
  06843c4

  Copy full SHA for 06843c4

• commuting squares of homotopies

  fredrik-bakke

  committed
  386eb78

  Copy full SHA for 386eb78

• maps of towers

  fredrik-bakke

  committed
  04996cd

  Copy full SHA for 04996cd

• standard limits of towers

  fredrik-bakke

  committed
  2fc0216

  Copy full SHA for 2fc0216

• transfinite composition of maps

  fredrik-bakke

  committed
  1fdae05

  Copy full SHA for 1fdae05

• remove unused imports

  fredrik-bakke

  committed
  feec07c

  Copy full SHA for feec07c

• Merge branch 'master' into tower

  fredrik-bakke

  authored
  ed26dd8

  Copy full SHA for ed26dd8

• mistaken renaming

  fredrik-bakke

  committed
  315a084

  Copy full SHA for 315a084

• fix links

  fredrik-bakke

  committed
  62dccbd

  Copy full SHA for 62dccbd

• characterize equality of towers, and fix some namings

  fredrik-bakke

  committed
  1e64fb5

  Copy full SHA for 1e64fb5

• revert MAlonzo patch

  fredrik-bakke

  committed
  d88916b

  Copy full SHA for d88916b

• towers and sequential-limits

  fredrik-bakke

  committed
  391238d

  Copy full SHA for 391238d

• comp-hom-tower

  fredrik-bakke

  committed
  52dc593

  Copy full SHA for 52dc593

• Merge branch 'master' into tower

  fredrik-bakke

  authored
  a42c703

  Copy full SHA for a42c703

• Characterization of equality of maps of towers

  fredrik-bakke

  committed
  8062e4d

  Copy full SHA for 8062e4d

• cleanup

  fredrik-bakke

  committed
  76ef045

  Copy full SHA for 76ef045

• self-review 1

  fredrik-bakke

  committed
  a5efd8c

  Copy full SHA for a5efd8c

• coherence-htpy-triangle-maps

  fredrik-bakke

  committed
  947e5ad

  Copy full SHA for 947e5ad

• more small fixes

  fredrik-bakke

  committed
  f2e0c80

  Copy full SHA for f2e0c80

• a typo

  fredrik-bakke

  committed
  a5bb9df

  Copy full SHA for a5bb9df

Commits on Oct 15, 2023

• review 1

  fredrik-bakke

  committed
  031dfba

  Copy full SHA for 031dfba

• post-pre-commit

  fredrik-bakke

  committed
  65b54a0

  Copy full SHA for 65b54a0

• remove duplicate def

  fredrik-bakke

  committed
  48583fd

  Copy full SHA for 48583fd

• idea universal-property-sequential-limits

  fredrik-bakke

  committed
  c199b44

  Copy full SHA for c199b44

• typo

  fredrik-bakke

  committed
  470e3a4

  Copy full SHA for 470e3a4

• refactor functoriality

  fredrik-bakke

  committed
  2e7c60c

  Copy full SHA for 2e7c60c

• Precomposing cones over X with a map

  fredrik-bakke

  committed
  1dc1d35

  Copy full SHA for 1dc1d35

• The property of being a ...

  fredrik-bakke

  committed
  fff7c89

  Copy full SHA for fff7c89

• table of pullback files

  fredrik-bakke

  committed
  a04c54d

  Copy full SHA for a04c54d

• table of fibers of maps files

  fredrik-bakke

  committed
  547517a

  Copy full SHA for 547517a

• table of sequential limits files

  fredrik-bakke

  committed
  6f1400c

  Copy full SHA for 6f1400c

• reorder table entries

  fredrik-bakke

  committed
  43ed912

  Copy full SHA for 43ed912

• remove unused imports and revert fibers of maps of finite types renaming

  fredrik-bakke

  committed
  e7a47b1

  Copy full SHA for e7a47b1

• fix link

  fredrik-bakke

  committed
  04a739d

  Copy full SHA for 04a739d

• Update tables/sequential-limits.md

  Show description for 0d5a8b0
  

  fredrik-bakke

  and

  EgbertRijke

  authored
  0d5a8b0

  Copy full SHA for 0d5a8b0

• The universal property of X _at a universe level_

  fredrik-bakke

  committed
  972dace

  Copy full SHA for 972dace

• move map-universal-property-*

  fredrik-bakke

  committed
  3bb70bc

  Copy full SHA for 3bb70bc

• fix boldface

  fredrik-bakke

  committed
  eede4dc

  Copy full SHA for eede4dc

• comments

  fredrik-bakke

  committed
  6400bce

  Copy full SHA for 6400bce