Right now the the new file 04a on right orthogonality does not appear in the web directory. This is an easy fix but at the same time I propose we renumber them to get rid of the a.
One easy to implement change would be to move 03-simplicial-type-theory to 02-simplicial-type-theory and 04-extension-types to 03-extension-types and 04a-right-orthogonality to 04-right-orthogonality. This could be implemented immediately as it should not create conflicts with the open pull requests.
This also leaves the numbers 00 and 01 open for later similar moves. What do we think @jonweinb and @fizruk and @TashiWalde?
Right now the the new file 04a on right orthogonality does not appear in the web directory. This is an easy fix but at the same time I propose we renumber them to get rid of the a.
One easy to implement change would be to move 03-simplicial-type-theory to 02-simplicial-type-theory and 04-extension-types to 03-extension-types and 04a-right-orthogonality to 04-right-orthogonality. This could be implemented immediately as it should not create conflicts with the open pull requests.
This also leaves the numbers 00 and 01 open for later similar moves. What do we think @jonweinb and @fizruk and @TashiWalde?