Induction and coinduction schemes in category theory

This thesis studies induction and coinduction schemes from the point of view of category theory. We start from the account of inductive and coinductive types given by initial algebra semantics and final coalgebra semantics, respectively. We then use fibrations as a generic setting describing a logic for a type theory to study induction and coinduction. As our starting point we consider the seminal work of Hermida and Jacobs [Her93, HJ98], who pioneered the fibrational approach. We extend their induction and coinduction schemes to give provably sound generic induction and coinduction schemes for arbitrary inductive and coinductive types. To achieve this we introduce the notion of a quotient category with equality (QCE) which i) abstracts the standard notion of a fibration of relations constructed from a given fibration and ii) gives us the correct structure to compare induction and coinduction from a categorical perspective. This allows us to broaden the applications of the coinduction scheme, as well as present the duality between coinduction and induction in a systematic way. Finally, we consider induction and coinduction schemes in the more general setting of fibred fibrations which is used to give sound, generic indexed induction and coinduction schemes for indexed inductive and coinductive types.

Resource Type

DOI

Date Created

Former identifier

Relations

Thumbnail	Title	Date Uploaded	Visibility	Actions
	PDF for thesis 13203	2021-07-02	Public	Download