Unless I am mistaken, there are two lingering commands which don't belong anymore https://github.com/UniMath/TypeTheory/blob/41adfeccb8f25ca00323c7aa5a14fb871b37daee/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Maps.v#L453 https://github.com/UniMath/TypeTheory/blob/41adfeccb8f25ca00323c7aa5a14fb871b37daee/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Maps.v#L533
Unless I am mistaken, there are two lingering commands which don't belong anymore
TypeTheory/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Maps.v
Line 453 in 41adfec
TypeTheory/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Maps.v
Line 533 in 41adfec