From 00978587e5f601ab3b3337f6ff20eb3cc1bc97ec Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Sun, 6 Mar 2016 13:23:30 -0500
Subject: [PATCH] update README

---
 README.md | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/README.md b/README.md
index e1732ce..9e4c302 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,8 @@
 # Spectral Sequences
 
-Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence. 
+Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
 
-#### Participants 
+#### Participants
 Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.
 
 ## Resources
@@ -20,7 +20,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
 - some basic theory: product, tensor, hom, projective,
 - categories of algebras, [abelian categories](http://ncatlab.org/nlab/show/abelian+category),
 - exact sequences, short and long
-- [snake lemma](http://ncatlab.org/nlab/show/snake+lemma) 
+- [snake lemma](http://ncatlab.org/nlab/show/snake+lemma)
 - [5-lemma](http://ncatlab.org/nlab/show/five+lemma)
 - [chain complexes](http://ncatlab.org/nlab/show/chain+complex) and [homology](http://ncatlab.org/nlab/show/homology)
 - [exact couples](http://ncatlab.org/nlab/show/exact+couple), probably just of Z-graded objects, and derived exact couples
@@ -28,8 +28,8 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
 - [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences)
 
 ### Topology To Do:
-- HoTT Book chapter 8
-- fiber and cofiber sequences (is this in the library already?)
+- HoTT Book sections 8.7, 8.8.
+- cofiber sequences
 - [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension
 - [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification)
 - [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), parametrized smash and hom between types and spectra
@@ -40,6 +40,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
 - exact couple of a tower of spectra
 
 ### Already Done:
-- pointed types
-- definition of algebraic structures such as groups, rings, fields, 
-- some algebra: quotient, product, free.
+- Most things in the HoTT Book up to Section 8.6 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md))
+- pointed types, maps, homotopies and equivalences
+- definition of algebraic structures such as groups, rings, fields
+- some algebra: quotient, product, free groups.
\ No newline at end of file