Univalence, Foundations and Philosophy: With a Sheaf-Shaped Appendix