Andrej Bauer: Cell types

Abstract: cell types are a special kind of higher-inductive types which do not involve any recursion. They roughly correspond to gluing constructions a la CW complexes in ordinary topology. We shall look at their formalization in HoTT.

Vabljeni!