Code

Refactoring pointed types#1056

Code

Merged

VojtechStep merged 55 commits intoUniMath:masterUniMath/agda-unimath:masterfrom EgbertRijke:pointedEgbertRijke/agda-unimath:pointedCopy head branch name to clipboardMar 13, 2024

+6,722-815

Commits

Commits on Mar 5, 2024

• pulling changes from spans

  EgbertRijke

  committed
  626e354

• making changes compatible with rest of library, up to synthetic hott

  EgbertRijke

  committed
  1a7562b

• moving files

  EgbertRijke

  committed
  05bdc81

• some repairs in synthetic homotopy theory

  EgbertRijke

  committed
  cc07eb7

• null

  EgbertRijke

  committed
  262572b

Commits on Mar 6, 2024

• fixing smash products

  EgbertRijke

  committed
  22e58c3

• everything compiles

  EgbertRijke

  committed
  c59bf6e

• make pre-commit

  EgbertRijke

  committed
  375d16d

• adding file about pointed equivalences to fix missing link error

  EgbertRijke

  committed
  b9eee83

• adding file about pointed equivalences to fix missing link error

  EgbertRijke

  committed
  780ee8e

• make pre-commit

  EgbertRijke

  committed
  bad9f16

• name change for pointed type of cocones under pointed span diagrams

  EgbertRijke

  committed
  66f71a6

• adding new file on morphisms of twisted pointed arrows in order to fix missing link

  EgbertRijke

  committed
  0ce4ad5

• factor out opposite pointed spans

  EgbertRijke

  committed
  02c8dbf

• create new file on transposition pointed span diagrams in order to fix missing link error

  EgbertRijke

  committed
  a2346ab

• make pre-commit

  EgbertRijke

  committed
  931a98f

• adding Agda entries to concept macros

  EgbertRijke

  committed
  d14273e

• fix broken entries in concept macros

  EgbertRijke

  committed
  2c55621

Commits on Mar 7, 2024

• work

  EgbertRijke

  committed
  3ce12ab

• whiskering of pointed 2-homotopies with respect to concatenation

  EgbertRijke

  committed
  ac225b4

• the reflexive homotopy of morphisms of pointed arrows

  EgbertRijke

  committed
  b8ccae0

• review comments

  EgbertRijke

  committed
  7544d3c

Commits on Mar 8, 2024

• review comments on pointed homotopies

  EgbertRijke

  committed
  85c97f0

• make pre-commit

  EgbertRijke

  committed
  678dc82

• fix Cavallo's trick

  EgbertRijke

  committed
  d63be88

• fix broken links

  EgbertRijke

  committed
  f981069

• Merge branch 'master' of github.com:UniMath/agda-unimath into pointed

  EgbertRijke

  committed
  caed77b

• really fix broken links

  EgbertRijke

  committed
  e82eb9e

• factoring out uniform pointed homotopies and pointed 2-homotopies

  EgbertRijke

  committed
  294f9cd

• fix missing Agda entry in concept macro

  EgbertRijke

  committed
  734963f

• concatenation of pointed homotopies is a binary equivalence

  EgbertRijke

  committed
  a888f56

• shortening a lengthy coherence proof

  EgbertRijke

  committed
  c80a035

Commits on Mar 9, 2024

• concatenation of pointed 2-homotopies is a binary equivalence

  EgbertRijke

  committed
  25627ff

• torsoriality of homotopies of morphisms of pointed arrows

  EgbertRijke

  committed
  1022b00

• cut off unfinished work

  EgbertRijke

  committed
  92df156

• refactoring long construction of the base point coherence of the right unit law of concatenation of pointed homotopies

  EgbertRijke

  committed
  a2cb069

• using span diagrams in null cocones

  EgbertRijke

  committed
  cfe3204

• review comments

  EgbertRijke

  committed
  1858236

• review comments

  EgbertRijke

  committed
  bb76498

• revised all review comments

  EgbertRijke

  committed
  4d1ebcd

• refactoring pointed isos

  EgbertRijke

  committed
  b0b482d

• comma

  EgbertRijke

  committed
  d84cc36

• revised wording

  EgbertRijke

  committed
  b215898

• review comments

  EgbertRijke

  committed
  432c6db

• make pre-commit

  EgbertRijke

  committed
  d154d60

Commits on Mar 10, 2024

• Merge branch 'master' of github.com:UniMath/agda-unimath into pointed

  EgbertRijke

  committed
  7ba9e27

Commits on Mar 11, 2024

• Merge branch 'master' of github.com:UniMath/agda-unimath into pointed

  EgbertRijke

  committed
  cf05eb9

• addressing last comments

  EgbertRijke

  committed
  c60e6e3

• make pre-commit

  EgbertRijke

  committed
  04a3f6d

• make pre-commit

  EgbertRijke

  committed
  a724639

• fix link

  EgbertRijke

  committed
  ce905ad

• Merge branch 'master' of github.com:UniMath/agda-unimath into pointed

  EgbertRijke

  committed
  c63634c

• Merge branch 'pointed' of github.com:EgbertRijke/agda-unimath into pointed

  EgbertRijke

  committed
  073f7c0

Commits on Mar 13, 2024

• review comments

  EgbertRijke

  committed
  c9c1dca

• merge conflict

  EgbertRijke

  committed
  1166932