Code

Reflective global subuniverses#1228

Code

Open

fredrik-bakke wants to merge 17 commits intoUniMath:masterUniMath/agda-unimath:masterfrom fredrik-bakke:global-localizationsfredrik-bakke/agda-unimath:global-localizationsCopy head branch name to clipboard

+3,481-192

Commits

Commits on Nov 26, 2024

• edits

  fredrik-bakke

  committed
  e38af6f

• the type of equivalences as a pullback

  fredrik-bakke

  committed
  0aa5327

• extensions of types in subuniverses

  fredrik-bakke

  committed
  f6da36a

• some additions and edits local types

  fredrik-bakke

  committed
  c49b731

• edits

  fredrik-bakke

  committed
  f8213da

• reflective global subuniverses

  fredrik-bakke

  committed
  99c0204

Commits on Nov 27, 2024

• retracts localizations global subuniverses

  fredrik-bakke

  committed
  6f22515

• Null types are closed under dependent sums

  fredrik-bakke

  committed
  d9a85a2

Commits on Nov 28, 2024

• an informal proof fiber condition orthogonal maps

  fredrik-bakke

  committed
  76007fa

• work

  fredrik-bakke

  committed
  62ea2f9

• fixes

  fredrik-bakke

  committed
  6c78efa

• fixes

  fredrik-bakke

  committed
  46413d9

• prose reflective global subuniverses

  fredrik-bakke

  committed
  7a3537d

• fix citation

  fredrik-bakke

  committed
  99e95fc

Commits on Dec 3, 2024

• fix links

  fredrik-bakke

  committed
  e07dc4e

• fix links

  fredrik-bakke

  committed
  d34cd1c

Commits on Dec 4, 2024

• Merge branch 'master' into global-localizations

  fredrik-bakke

  authored
  0044690