Issues

• TypeTheory does no longer compile with the development version of Rocq

  UniMath/TypeTheory#254 · Filter by author rmatthes opened on Apr 2, 2026

• configuration for ProofGeneral with a Dune build of UniMath and this satellite

  UniMath/TypeTheory#253 · Filter by author rmatthes opened on Feb 17, 2026

• Remove two Time commands

  UniMath/TypeTheory#249 · Filter by author arnoudvanderleer opened on Dec 20, 2024

• does not compile with Coq 8.20 release candidate 1

  UniMath/TypeTheory#245 · Filter by author rmatthes opened on Jul 1, 2024

• Remove dependency on Coq.Init.Logic

  UniMath/TypeTheory#235 · Filter by author m-lindgren opened on Mar 7, 2023
  2

• PR#224 not yet fully satisfying

  UniMath/TypeTheory#225 · Filter by author rmatthes opened on Oct 27, 2022

• Slow type-checking: replace admitted by proof

  UniMath/TypeTheory#204 · Filter by author benediktahrens opened on Jan 13, 2022

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

  UniMath/TypeTheory#203 · Filter by author benediktahrens opened on Jan 13, 2022
  1

• Put notations in scope or make them local

  UniMath/TypeTheory#109 · Filter by author benediktahrens opened on Jun 15, 2017
  1

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

  UniMath/TypeTheory#102 · Filter by author benediktahrens opened on May 4, 2017
  

• Improve compilation instructions in README

  UniMath/TypeTheory#57 · Filter by author benediktahrens opened on Mar 11, 2017

• Naming: structure vs property

  UniMath/TypeTheory#22 · Filter by author benediktahrens opened on Oct 10, 2016

• Make code quality/cleaning pass over files

  UniMath/TypeTheory#16 · Filter by author peterlefanulumsdaine opened on Oct 5, 2016

• Add careful refs for definitions in OtherDefs files

  UniMath/TypeTheory#9 · Filter by author peterlefanulumsdaine opened on Oct 4, 2016

• Provide export wrapper file

  UniMath/TypeTheory#5 · Filter by author peterlefanulumsdaine opened on Oct 4, 2016
  1