Set-truncation in Lemma 10.3.22
jdchristensen opened this issue · 8 comments
In the statement of Lemma 10.3.22, should X be assumed to be a set? If not, then in the proof, B is defined as a quotient of the (non-set) Sigma_{x : X} Fx, so there should probably be an explicit set-truncation. If X is assumed to be a set, should the proof say "set quotient" instead of "quotient"?
(Is the material on ordinals formalized anywhere?)
The "set-quotient" introduced in 6.10 is introduced in a context where the ambient type is indeed a set.
I formalized ordinals in Agda here: https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.html (this is an index to various files).
This contains almost everything in the HoTT Book (sometimes with different proofs) plus unpublished work presented at Types2019 (https://www.cs.bham.ac.uk/~mhe/papers/compact-ordinals-Types-2019-abstract.pdf). In the definition of ordinal, I don't assume that the underlying type is a set, because this follows from the other axioms.
Yes, I suppose given the way set-quotients were defined, we ought to set-truncate this type before taking its quotient. Or else observe to start with that F factors through the set-truncation of X, since Ord is a set. Anyone want to submit a correction?
What about changing the beginning of the proof to: "Let B be the set- quotient (see Remark 6.10.1) of the equivalence relation ..." In other words: add paths according to the given relation, and then set-truncate. This is equivalent to the two options that Mike described, but involves only one set-truncation at the end instead of two in total (one explicit and one implicit in the meaning of set-quotient). In the HoTT/Coq library, quotients are defined in this generality, and with those extra words in the proof, I wouldn't have thought twice about it.
That's reasonable in principle, but if so, I would also want to change section 6.10 where set-quotients are defined, which starts out with "let A be a set", and then we'd want to be careful about whether there are any results about set-quotients that do depend on the underlying type being a set.
I don't want to change section 6.10, but thought that extending it (as mentioned in Remark 6.10.1) internally to this proof would be reasonable, since all that is being used is that a certain relation extends to the quotient. Adding some explicit truncation before taking the set quotient is also reasonable, but isn't how it would be formalized, and it leads to an extra step where you have to mention that the relation ~ factors through this first set-quotient. Anyway, this is all minor and I'm fine with either approach.
I suppose that's fair; I'd forgotten about Remark 6.10.1. Feel free to submit a pull request doing it your way.