UniMath/TypeTheory

Issues

• does not compile with Coq 8.20 release candidate 1

  #245 opened 3 months ago by rmatthes
  0

• Fix typo to re-establish compatibility with UniMath/UniMath

  #239 opened a year ago by benediktahrens
  0

• Remove dependency on Coq.Init.Logic

  #235 opened 2 years ago by m-lindgren
  2

• Build fails with Coq 8.16.0

  #230 opened a year ago by m-lindgren
  5

• File `Bsystems/lBsystems_work` unlisted, stale, and very unclear status — salvage, delete, …?

  #213 opened 2 years ago by peterlefanulumsdaine
  2

• PR#224 not yet fully satisfying

  #225 opened 2 years ago by rmatthes
  0

• CI: Build instructions for Coq and UniMath need to be updated

  #222 opened 2 years ago by benediktahrens
  0

• Reorganise library structure: consistently use topic-based packages, not project-based?

  #205 opened 2 years ago by peterlefanulumsdaine
  3

• Refactor definition of the codomain displayed cat

  #79 opened 3 years ago by peterlefanulumsdaine
  1

• Upstreaming some of the material in `Auxiliary` to UniMath/UniMath?

  #203 opened 3 years ago by benediktahrens
  1

• Slow type-checking: replace `admitted` by proof

  #204 opened 3 years ago by benediktahrens
  0

• CI broken, due to recent package dependencies in UniMath

  #199 opened 3 years ago by peterlefanulumsdaine
  0

• CI broken due to missing system packages for OPAM

  #197 opened 3 years ago by peterlefanulumsdaine
  2

• Travis build failure

  #186 opened 3 years ago by benediktahrens
  1

• Build system (opam) seems to require changes

  #184 opened 4 years ago by benediktahrens
  4

• Anomaly detected during compilation

  #182 opened 4 years ago by rmatthes
  6

• Compilation error after updating Coq version

  #168 opened 5 years ago by benediktahrens
  1

• TypeTheory does not compile with current UniMath

  #155 opened 5 years ago by benediktahrens
  1

• TypeTheory does not compile with Coq 8.10

  #162 opened 5 years ago by rmatthes
  4

• Compilation broken due to changes in UniMath/UniMath

  #144 opened 6 years ago by benediktahrens
  2

• Remove material that has been upstreamed to UniMath/UniMath

  #145 opened 6 years ago by benediktahrens
  1

• Replace all uses of `cancel_postcomposition` by `maponpaths_2`

  #132 opened 7 years ago by benediktahrens
  0

• Compilation Failure with coq 8.7

  #125 opened 7 years ago by amblafont
  1

• Adapt Travis configuration to new version of Coq

  #129 opened 7 years ago by benediktahrens
  1

• Put notations in scope or make them local

  #109 opened 7 years ago by benediktahrens
  1

• Change name and of arguments in `functor_over`, `nat_trans_over`, etc

  #82 opened 7 years ago by peterlefanulumsdaine
  1

• Implement mechanism to conveniently specify full subcategories as displayed categories

  #86 opened 7 years ago by benediktahrens
  1

• Rename identifiers for categories to adhere to convention suggested by VV

  #102 opened 7 years ago by benediktahrens
  0

• Add algebras for a functor + a monad as example of displayed cats

  #80 opened 7 years ago by peterlefanulumsdaine
  1

• Add lemma: any disp cat over a univalent cat is an isofibration

  #88 opened 7 years ago by peterlefanulumsdaine
  1

• Topological spaces as an example of displayed cats

  #81 opened 7 years ago by peterlefanulumsdaine
  1

• Improve compilation instructions in README

  #57 opened 8 years ago by benediktahrens
  0

• Move the repository into the UniMath organization

  #15 opened 8 years ago by benediktahrens
  1

• Make code quality/cleaning pass over files

  #16 opened 8 years ago by peterlefanulumsdaine
  0

• Naming: structure vs property

  #22 opened 8 years ago by benediktahrens
  0

• Consistentise terminology: cartesian generators, qq-morphisms, etc.

  #2 opened 8 years ago by peterlefanulumsdaine
  14

• Attribution for def of rel univ strux

  #8 opened 8 years ago by peterlefanulumsdaine
  0

• Add careful refs for definitions in `OtherDefs` files

  #9 opened 8 years ago by peterlefanulumsdaine
  0

• Provide summary/overview file

  #4 opened 8 years ago by peterlefanulumsdaine
  1

• Consolidate notations

  #1 opened 8 years ago by peterlefanulumsdaine
  1

• Provide export wrapper file

  #5 opened 8 years ago by peterlefanulumsdaine
  1

• Remove duplicate definition `CwF_structure`

  #10 opened 8 years ago by benediktahrens
  0

• Consolidate CategoryTheory imports

  #6 opened 8 years ago by peterlefanulumsdaine
  1

• Document `CwF_SplitTypeCat_Defs` better

  #3 opened 8 years ago by peterlefanulumsdaine
  1

• Clarify referencing/attributions of main defs of CwF’s, split type cats

  #7 opened 8 years ago by peterlefanulumsdaine
  1