Formalizing the graph model of type theory, part 3

In the induction principle for the graph quotient $latex \mathsf{colim}(\Gamma)$, we have seen that terms of a type family $latex P : \mathsf{colim}(\Gamma)\to\mathsf{Type}$ are equivalently described by terms of the transposed family $latex \Delta(P)\circ\eta$ of graphs over $latex \Gamma$. This family is no ordinary family, and in this post I'd like to discuss its special … Continue reading Formalizing the graph model of type theory, part 3

Advertisements

Formalizing the graph model of type theory, part 2

The most basic construction of higher inductive types can be formulated as a 'left adjoint' to the canonical homomorphism of models $latex \Delta : U \to \mathsf{Graph}$, and my interest in formalizing the graph model originates from this idea. Also, looking at the higher inductive types in this type theoretical framework has helped me prove … Continue reading Formalizing the graph model of type theory, part 2

Formalizing the graph model of type theory, part 1

This semester I'm doing a formalization project with┬áJeremy Avigad, based on work that I did mostly with Bas Spitters, back when I was a research assistant in Nijmegen. The goal of my project is to formalize several aspects of the graph model of type theory, using the Lean proof assistant. In this series of blog … Continue reading Formalizing the graph model of type theory, part 1