Contains a formal proof of the theorem that countable choice implies postnikov effectiveness in HoTT
This is based on the proofs of lemmas 3.1 and 3.4 in Choice axioms and Postnikov completeness by Mathieu Anel and Reid Barton.
Main theorem is contained in "ChoicePostnikov.agda"
"Preliminary.agda" is independent of the rest of the code and contains an early outline of the proof
"Everything.agda" serves to import the foundations folder, I should change this
TODO: general cleaning up, especially in Limits and DiagramSigma files; add some ascii diagrams; deal with "Everything.agda"; delete Preliminary.agda?