Connections between Size, Truncation and Connectedness

[IanRay11]

I am now pushing the file on on Size, Truncation and Connectedness that was split off from the original PR. One of the main things I need to revisit here are the naming schemes; both of the results from Dan's paper and in my where blocks. I spent some time thinking about renaming results other than Prop-2-2 (for example) but describing the result is typically a mouth full so I wanted to get some feedback. @tomdjong.

By the way I checked for unused imports (by hand lol) and I referenced Dan's paper correctly (these where things suggested in the original PR before the split).

[IanRay11]

@martinescardo if you'd like to take a look.

[martinescardo]

I request minor changes only. Thanks for formalizing this.

It would be nice to formalize the join construction in a future pull request. :-)

[IanRay11]

Thanks @martinescardo! I would still like @tomdjong to take a look when he gets a chance.

[tomdjong]

I also only had minor comments. Thanks @IanRay11!

[tomdjong]

Another small comment: could you rename the file from SizeTruncationandConnectedness.lagda to Size-TruncatedConnected.lagda?

[tomdjong]

Also, could you please record the following corollary/example of Theorem 2.6: the set truncation of the universe is large (i.e. cannot be small). Thanks!

[martinescardo]

Also, could you please record the following corollary/example of Theorem 2.6: the set truncation of the universe is large (i.e. cannot be small). Thanks!

In fact, this was the initial motivation for asking somebody on mathstodon to formalize Dan's result, and you volunteered.

[IanRay11]

Also, could you please record the following corollary/example of Theorem 2.6: the set truncation of the universe is large (i.e. cannot be small). Thanks!

In fact, this was the initial motivation for asking somebody on mathstodon to formalize Dan's result, and you volunteered.

Right... sorry. It's been awhile and I lost track.

[IanRay11]

@tomdjong ready for further review

[tomdjong]

Some more minor comments.

[IanRay11]

Okay, hopefully the comment before Thm 2.6. is better now. @tomdjong

[tomdjong]

@martinescardo Do you wish to take one last look?

[martinescardo]

Thanks a lot, @IanRay11 .

[martinescardo]

@martinescardo Do you wish to take one last look?

Done. I am happy for you to merge whenever you are ready.