Code

Make IsTrunc an inductive type#1806

Code

Merged

jdchristensen merged 16 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom jdchristensen:inductive-istruncjdchristensen/HoTT:inductive-istruncCopy head branch name to clipboardJan 16, 2024

+389-335

Commits

Commits on Jan 14, 2024

• WIP: Make IsTrunc an inductive type

  jdchristensen

  committed
  fbdb824

• Overture: add a Coercion istrunc_fun : IsTrunc >-> Funclass

  jdchristensen

  committed
  82c8143

• Convert more files to Inductive IsTrunc

  jdchristensen

  committed
  eb45a5e

• Simplify proof of ishprop_istrunc, by moving istrunc_forall to Trunc.v

  Show description for 0fa6a7c
  jdchristensen

  committed
  0fa6a7c

• Minor changes in response to review

  jdchristensen

  committed
  9c977fa

• Make library build with inductive IsTrunc

  jdchristensen

  committed
  129e6f1

• Make compatible with Coq 8.17

  jdchristensen

  committed
  53127ff

• HoTTBookExercises: fix universe error in Book_4_6_iii

  jdchristensen

  committed
  f8b444c

• Speed up Algebra/Universal/Algebra and Modalities/Fracture a bit

  jdchristensen

  committed
  2af8511

Commits on Jan 15, 2024

• Sets/Hartogs: remove two of the three admits

  jdchristensen

  committed
  e534868

• Sets/Powers: make hset_power have same signature as before

  jdchristensen

  committed
  8632305

• Sets/Ordinals: remove redundant Instance, simplify another

  jdchristensen

  committed
  45961a1

• Sets/Hartogs: remove last admit.

  jdchristensen

  committed
  9a87e4f

• Overture: update comments, and remove redundant Cumulative modifier

  jdchristensen

  committed
  1b4bc68

• Equivalences: make make_equiv work with Contr

  jdchristensen

  committed
  df81fec

• Move Contr_ind to Contractible, and prove it with a match

  jdchristensen

  committed
  1f28fac