"In Lean, types are terms, too, and so they have types, as we have already seen. So what is the type of 1 = 1. It’s Prop."
I believe a question mark would work better for the "So what is the type of 1=1" sentence, like so: "In Lean, types are terms, too, and so they have types, as we have already seen. So what is the type of 1 = 1? It’s Prop."
"We we have the following picture of the type hierarchy for the terms we’ve just constructed."
One of the "we" should be deleted.
"In Lean, types are terms, too, and so they have types, as we have already seen. So what is the type of 1 = 1. It’s Prop."
I believe a question mark would work better for the "So what is the type of 1=1" sentence, like so: "In Lean, types are terms, too, and so they have types, as we have already seen. So what is the type of 1 = 1? It’s Prop."
"We we have the following picture of the type hierarchy for the terms we’ve just constructed." One of the "we" should be deleted.