Erik Palmgren: Progress report on formalizing categories with attributes in type theory, part 2
Time: Wed 2015-09-02 10.00 - 11.45
Location: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm University
Participating: Erik Palmgren
This talk is a follow up of the talks, by Peter Lumsdaine and myself respectively, last term on this subject. A complete formalization in Coq of bounded categories with attributes and structures for type theory with one universe, has since then been achieved. We indicate how a setoid model of type theory is constructed via the use of a formalized model of CZF.