Code

Equivalence injective type families#1009

Code

Merged

EgbertRijke merged 7 commits intoUniMath:masterUniMath/agda-unimath:masterfrom fredrik-bakke:injectivefredrik-bakke/agda-unimath:injectiveCopy head branch name to clipboardJan 28, 2024

+184-41

Commits

Commits on Jan 25, 2024

• equivalence injective type families

  fredrik-bakke

  committed
  6196a04

  Copy full SHA for 6196a04

Commits on Jan 26, 2024

• review

  fredrik-bakke

  committed
  7ef885f

  Copy full SHA for 7ef885f

• fix import

  fredrik-bakke

  committed
  07d34f7

  Copy full SHA for 07d34f7

Commits on Jan 27, 2024

• wip prose

  fredrik-bakke

  committed
  a4fda14

  Copy full SHA for a4fda14

Commits on Jan 28, 2024

• add note about injective types

  fredrik-bakke

  committed
  c348a2f

  Copy full SHA for c348a2f

• fix headers

  fredrik-bakke

  committed
  cf542b4

  Copy full SHA for cf542b4

• Merge branch 'master' into injective

  fredrik-bakke

  authored
  4bbf1dd

  Copy full SHA for 4bbf1dd