TypeTheory
TypeTheory copied to clipboard
UniMath
The mathematical study of type theories, in univalent foundations
After merging #234 two files still unfortunately imports `Coq.Init.Logic`: - Initiality/Interpretation.v - TypeCat/General.v It's currently unclear to me if it's easy to fix or requires a more involved patch, so...
As argued by @nmvdw in the discussion about [PR 1582 of UniMath](https://github.com/UniMath/UniMath/pull/1582), the inclusion of material from PAdics is not even needed.
Great work was done by @peterlefanulumsdaine in #202 regarding organization of auxiliary material in `Auxiliary`. Question: would some of the material from `Auxiliary` fit well into UniMath/UniMath? The advantages of...
File https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v contains admitted statements: - https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v#L44 - https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v#L90 - https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v#L91 Fragments or complete proofs are there, but do not type-check in a reasonable amount of time, or at all....
Some Benchmark for the CwF and SplTC equivalence, that contain mostly the common part of the two structure and some additional constructions : - The Ty presheaf - context extension...
see https://github.com/UniMath/UniMath/issues/362#issuecomment-225556634
explain that - location of Coq binaries needs to be given manually (by PATH or locally) - UniMath files are found automatically after `make install` if using the right Coq...
Before making public, would be good to have a rough quality/cleanup pass over all files (at least all of ALV1). Doesn’t need to be too thorough, but should at least:...
In Fibrations.v, it reads "We make the cloven version the default, so is_fibration etc are the cloven notions, and call the mere-existence versions un-cloven." So `is_fibration` is actually a structure,...