Code

Splitting idempotents#1105

Code

Merged

EgbertRijke merged 55 commits intoUniMath:masterUniMath/agda-unimath:masterfrom fredrik-bakke:idempotentsfredrik-bakke/agda-unimath:idempotentsCopy head branch name to clipboardApr 17, 2024

+2,548-300

Commits

Commits on Mar 30, 2024

• work on idempotents

  fredrik-bakke

  committed
  da04247

• pre-commit

  fredrik-bakke

  committed
  9b11cf1

• revert global subuniverses

  fredrik-bakke

  committed
  b640a94

• typos split idempotent maps

  fredrik-bakke

  committed
  6afb27a

• prose fixes

  fredrik-bakke

  committed
  e96ba01

Commits on Mar 31, 2024

• fixes

  fredrik-bakke

  committed
  8540d4e

• more fixes

  fredrik-bakke

  committed
  f286f0f

• Characterizing equality of the total type of retracts

  fredrik-bakke

  committed
  2b136b6

• quasiidempotents split!

  fredrik-bakke

  committed
  de7f089

• cleanup

  fredrik-bakke

  committed
  10db717

• renaming is-split-idempotent-is-quasiidempotent -> splitting-type-is-quasiidempotent

  fredrik-bakke

  committed
  5b98e7b

• "We record these same facts for the bundled data of a quasiidempotent map on A."

  fredrik-bakke

  committed
  0c8db94

• KECA17

  fredrik-bakke

  committed
  3ca6301

• characterizing equality of split idempotence structures

  fredrik-bakke

  committed
  b38400b

• optimize imports

  fredrik-bakke

  committed
  ce39cb2

• Small types are closed under retracts

  fredrik-bakke

  committed
  35f9606

• remove unused id algebra

  fredrik-bakke

  committed
  aa246bd

• keep second order inverse laws

  fredrik-bakke

  committed
  b9b978a

• more fixes

  fredrik-bakke

  committed
  0085a04

• fix link

  fredrik-bakke

  committed
  592deeb

• fix link again

  fredrik-bakke

  committed
  bd7e46d

Commits on Apr 4, 2024

• is-small-retract

  fredrik-bakke

  committed
  6dfcab7

• fix citation labels

  fredrik-bakke

  committed
  79bdc74

• sort references

  fredrik-bakke

  committed
  09e4379

Commits on Apr 9, 2024

• preidempotent -> idempotent

  fredrik-bakke

  committed
  d93fb41

• explain "idempotent map" terminology

  fredrik-bakke

  committed
  433ed0d

• quasiidempotent -> quasicoherently-idempotent

  fredrik-bakke

  committed
  1bc9bdc

• explain terminology "quasicoherently idempotent maps"

  fredrik-bakke

  committed
  7d79cd2

• If a map is split idempotent at any universe level, it is split idempotent at its own universe level

  fredrik-bakke

  committed
  28bb323

• The type of split idempotent maps on A is equivalent to retracts of A

  fredrik-bakke

  committed
  10872d6

• omit redundant -map suffix

  fredrik-bakke

  committed
  217e9d7

• fix link

  fredrik-bakke

  committed
  5ab1779

• self-review

  fredrik-bakke

  committed
  9974178

• Merge branch 'master' into idempotents

  fredrik-bakke

  authored
  6ffd058

Commits on Apr 10, 2024

• homotopy reasoning coherence-is-quasicoherently-idempotent-htpy

  fredrik-bakke

  committed
  f987aef

• some explanations

  fredrik-bakke

  committed
  15e69fc

• a word

  fredrik-bakke

  committed
  f8f80a8

• Merge branch 'master' into idempotents

  fredrik-bakke

  authored
  2d5be6b

• align diagram

  fredrik-bakke

  committed
  9f72b4c

Commits on Apr 11, 2024

• Merge branch 'master' into idempotents

  fredrik-bakke

  authored
  07bfa65

• pre-commit

  fredrik-bakke

  committed
  f887eaa

Commits on Apr 14, 2024

• Update src/foundation/idempotent-maps.lagda.md

  Show description for 8fd2a4c
  

  fredrik-bakke

  and

  EgbertRijke

  authored
  8fd2a4c

• Update src/foundation/split-idempotent-maps.lagda.md

  Show description for be236d9
  

  fredrik-bakke

  and

  EgbertRijke

  authored
  be236d9

• Update src/foundation/split-idempotent-maps.lagda.md

  Show description for 6149161
  

  fredrik-bakke

  and

  EgbertRijke

  authored
  6149161

• some review comments

  fredrik-bakke

  committed
  788a10a

• nitpick

  fredrik-bakke

  committed
  c72f777

Commits on Apr 15, 2024

• fix some citations and references

  fredrik-bakke

  committed
  34c5514

• remark on "Quasicoherent idempotence is preserved by homotopies"

  fredrik-bakke

  committed
  7bcdac4

• Explanation "Not every idempotent map is quasicoherently idempotent"

  fredrik-bakke

  committed
  d05502a

• is-small-map-retract

  fredrik-bakke

  committed
  971f289

• clarify "Not every idempotent map is quasicoherently idempotent"

  fredrik-bakke

  committed
  72aa99c

• Being quasicoherently idempotent is generally not a property

  fredrik-bakke

  committed
  485fd5f

• pre-commit

  fredrik-bakke

  committed
  eb0460e

• Merge branch 'master' into idempotents

  fredrik-bakke

  authored
  b615029

Commits on Apr 17, 2024

• Merge branch 'master' into idempotents

  fredrik-bakke

  authored
  49c6b83