Erik Palmgren: Progress report on formalizing categories with attributes in type theory, part 2
Tid: On 2015-09-02 kl 10.00 - 11.45
Plats: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm University
Medverkande: 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.