Code

Solve exercise 3.15 and 3.17#1678

Code

Open

HyunggyuJang wants to merge 4 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom HyunggyuJang:ex-3.15&3.17HyunggyuJang/HoTT:ex-3.15&3.17Copy head branch name to clipboard

+40-1

Commits

Commits on Nov 4, 2022

• Solve exercise 3.15 and 3.17

  HyunggyuJang

  committed
  da9b309

Commits on Nov 30, 2022

• Reflect reviews

  HyunggyuJang

  committed
  0910287

• Reflect review

  HyunggyuJang

  committed
  fea4f10

Commits on Dec 2, 2022

• Make propositional resizing assumption explicit

  HyunggyuJang

  committed
  2b657ab