2.22.10-13

[marcbezem]

There is a mismatch between 2.22.10-12 where A is assumed to be a set, and 2.22.13, where A is a type. This has consequences for the notation, in particular in the 5th line of Remark 2.22.13. What are the types of x and y there, given that the left hand side of the equivalence is a proposition? NB notations are not updated, since this depends on the outcome of the discussion.

To me it seems a good solution to add an exercise that the image of any function A -> S, for any type A and set S, is a set. Then it follows that A/R is always a set, since A/R is the image of R : A -> (A -> Prop).

BTW (not for the book) if one replaces the set S by a groupoid G, and the type of R by A -> (A -> Set), don't we get that A/R is a groupoid, even if we replace the ( -1)-image by the 0-image? And perhaps we then get the 1-truncation of A by quotienting with Rxy := || x=y ||_0 ?

[UlrikBuchholtz]

There was a typo on that line (l. 5) in Rem. 2.22.13, where the propositional truncation was missing on the right. (I fixed this.)

But we should probably generalize 2.22.10 to allow for general carriers. (TBD)

I like your exercise, and yes, the (n+1)-truncation is the image of the n-truncated identity type A -> (A -> n-Type).

[marcbezem]

We also decided to change Lemma 2.22.1. Please take a look at e7ab442. I added a \cast: there, but I don't like it. Why not allowing to leave out elements of types that are not propositions if they play no essential role in the argument, for example when proving a proposition? For me that would also justify the use of "we have T" when T is a type that is not a prop.

[marcbezem]

@UlrikBuchholtz a few lines below your change there was another x=y with x,y in A that I put back to your original \Trunc{x \eqto y}, plus "g(x)=g(y)" since S is a set. I put other possible changes (A a type from the beginning, explanation or exercise that A/R is a set, several \eqto ---> = between propositions/predicates) on hold in view of #166.

[bidundas]

This seems dangerous to me. Could we discuss it Monday?

Bjorn

On 10 Dec 2022, at 19:12, Marc Bezem @.***> wrote:



We also decided to change Lemma 2.22.1. Please take a look at e7ab442https://github.com/UniMath/SymmetryBook/commit/e7ab44219f29e9890815b9bd48094bd80ed2fa67. I added a \cast: there, but I don't like it. Why not allowing to leave out elements of types that are not propositions if they play no essential role in the argument, for example when proving a proposition? For me that would also justify the use of "we have T" when T is a type that is not a prop.

— Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/163#issuecomment-1345352690, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SK6J6KGV22VNOEQGC63WMTBYRANCNFSM6AAAAAASX6UBTA. You are receiving this because you are subscribed to this thread.Message ID: @.***>

[UlrikBuchholtz]

Resolved.