Started proof of main theorem of composition.tex

Also added proposition that arrow objects have internal category
structures in wfs.tex