Benedikt Ahrens

The CI error comes from one of the "sanity" checks: ``` --- checking the ordering prescribed by the files UniMath/*/.packages/files --- error: *** UniMath/CategoryTheory/Enriched/ChangeOfBase.vo should not require UniMath/CategoryTheory/Enriched/BicatOfEnrichedCat.vo error: ***...

> The sanity checks passed, but the build script failed with the message "Error: Universe inconsistency." I don't think I did anything strange. No error occurs when I run `make`...

@rmatthes : have your change requests been addressed?

Your proposal leads to "longer" projections down to the carrier set, which could lead to bad performance. Of course, Vladimir wrote the code before primitive projections were introduced... I think...

@DanGrayson : I think you recently changed something that is related to this issue. Could you link to the change from here?

@rmatthes : thanks a lot for giving these examples; they illustrate some issues with `Let` very clearly. I currently think (but am very happy to have my opinion changed) that...

On 07/03/2016 02:07 PM, Daniel R. Grayson wrote: > My main motivation was to reduce duplication of proofs. In this > case, uniqueness of universal constructions up to isomorphism is...

On 07/04/2016 05:21 PM, Vladimir Voevodsky wrote: > Then I suggest the following modified version of the rule: > > "Formalizing a result or a group of results one should...

On 07/07/2016 01:15 PM, Ralph Matthes wrote: > I am sorry for this rather administrative remark, but it seems to me > that the style guide in UniMath/UniMath/README.md is not...

I think that this issue is not really one. Can we close it?