References
 
Extentionality
Altenkirch, Thorsten. Extensional Equality in Intensional Type Theory. [Link]
Hofmann, Martin. Conservativity of Equality Reflection over Intensional Type Theory. 1996. [Link]
Altenkirch, Thorsten McBride, Conor Swierstra, Wouter. Observational Equality, Now! [Link]http://www.cs.nott.ac.uk/~txa/publ/lics99.pdfhttp://www.springerlink.com/content/y26jp374t0147505/fulltext.pdfhttp://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdfshapeimage_2_link_0shapeimage_2_link_1shapeimage_2_link_2
Identity Types
Dybjer, Peter. (What I Know about) the History of the Identity Type. [Link]http://www.cse.chalmers.se/~peterd/papers/historyidentitytype.pdfshapeimage_3_link_0
Homotopy Type Theory
Kraus, Nicolai. Equality in the Dependently Typed Lambda Calculus: An Introduction to Homotopy Type Theory. [Link]
Licata, Dan. Just Kidding: Understanding Identity Elimination in Homotopy Type Theory. [Link]
http://www.cs.nott.ac.uk/~ngk/karlsruhe.pdfhttp://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/shapeimage_4_link_0shapeimage_4_link_1
Writing tips:
How to write a literature reviewhttp://wilderdom.com/OEcourses/PROFLIT/Class3LiteratureReview.htmshapeimage_5_link_0