Fix commented code and minor issues from thesis-pr - Githubissues

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.

GNU General Public License v3.0

228 stars 42 forks source link

Fix commented code and minor issues from thesis-pr #273

Closed tnttodda closed 4 months ago

tnttodda commented 4 months ago

A sizable portion of code was accidentally commented out, something I only noticed today! I also fixed most of the issues from https://github.com/martinescardo/TypeTopology/pull/172.

I still need to:

Use projections less throughout, for the sake of readability
Use variations of Π-is-prop that apply it multiple times, in order to get more concise and readable proofs
Remove any code that already exists in TypeTopology, and use the version that already exists (this is most true in the files Escardo-Simpson-LICS2001 and Chapter5/IntervalObject that are almost the same

martinescardo commented 4 months ago

Great!