Start / Iowa Type Theory Commute / Reassembling datatypes from functors using a fixed point

Iowa Type Theory Commute

Reassembling datatypes from functors using a fixed-point

10 min • 11 juli 2021

Last episode we discussed how functors can describe a single level of a datatype.  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.  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.

Senaste avsnitt

Correction: the Correct Author of the Proof from Last Episode, and an AI flop

12 maj | 7 min

Krivine's Proof of FD, Using Intersection Types

5 maj | 22 min

A Measure-Based Proof of Finite Developments

16 april | 23 min

Introduction to the Finite Developments Theorem

27 mars | 16 min

Nominal Isabelle/HOL

31 januari | 16 min
Vad är en podd?

En liten tjänst av I'm With Friends. Finns även på engelska.

Podcastbild

00:00 -00:00
00:00 -00:00