# 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

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