Podcasts Technology Iowa Type Theory Commute Reassembling datatypes from functors using a fixed-point

Reassembling datatypes from functors using a fixed-point

Published: July 11, 2021, 3 a.m.

b'

Last episode we discussed how functors can describe a single level of a datatype.\\xa0 In this episode, we discuss how to put these functors back together into a datatype, using disjoint unions of functors and a fixed-point datatype.\\xa0 The latter expresses the idea that inductive data is built in any finite number of layers, where each layer is described by the functor for the datatype.

'