Taskboard for MFPS submission

vikraman / 2DTypes

Collaborative work on reversible computing

17 stars 1 forks source link

Taskboard for MFPS submission #3

Closed vikraman closed 7 years ago

vikraman commented 7 years ago

[x] Sec 1
[x] Sec 2
[x] Sec 3 ( @vikraman )
- [x] Univalent fibrations
- [x] Propositional Truncation
- [x] Univalent sub-universes
- [x] U[2] is univalent
[x] Sec 4 ( @DreamLinuxer )
- [x] Write down the proofs in literate agda?

JacquesCarette commented 7 years ago

Are there specific things that still need to be done in sections 1 or 2 (other than editing for style)?

Also, what do we want after section 4?

I can work on this on Wednesday-Thursday of this week, and then in bits and pieces Tuesday-Thursday next week (when I will, strictly speaking, be on vacation).

vikraman commented 7 years ago

We finished it!