Anders Mörtberg

Will the Coq `now` tactic also go away? That would be great because then we know that if someone uses `now` then it is the simple one from MoreFoundations.Tactics

Just so you know, I switched off type-in-type just to see where building UniMath breaks a while ago. It breaks already in PartA: ``` COQC UniMath/Foundations/PartA.v File "./UniMath/Foundations/PartA.v", line 971,...

Re: "all of PartA should be strictly about what would be, in a type theory with good universe management, about types in a single universe." Ok, I think PartA was...

If we are going to switch off type-in-type from parts of UniMath it might be useful to look at the following code from the HoTT library: https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v#L87 https://github.com/HoTT/HoTT/blob/master/theories/Basics/UniverseLevel.v Side remark:...

Even if we polish it up we're using an `Inductive` (https://github.com/unimath2019-tt/UniMath/pull/1/files#diff-452b433f08e8e74d6437469aa8fde510c75068ffb77a815cb2aa0ce3006c183aR185) in the core definition. So unless the UniMath policy on inductive types has changed I'm afraid that preparing the...

Or is there some construction of W types in UniMath that I'm not aware of? I have a vague recollection that another group at the same school worked on this...

I prefer `eqtohomot`, not so much because of the name but because it has the right number of implicit arguments.

No, this seems like an oversight of the developer. In fact it happens often to me that I cannot apply a lemma because the lemma expects something in hProp, but...

For W-sets I think many of the results are already present in https://github.com/UniMath/UniMath/tree/master/UniMath/CategoryTheory/Chains. With this we can do many concrete inductive types (see https://github.com/UniMath/UniMath/tree/master/UniMath/CategoryTheory/Inductives), but I didn't think too hard...

@siddharthist : Nice! Have all of your results been merged into UniMath? I haven't really been keeping track of UniMath developments lately. If they are all there I don't think...