Types as Categories Using Simplicial Sets

Abstract

This thesis will provide an alternative type theory that is based on simplicial sets to view types as categories. The hope being that this perspective will allow a more accessible and simpler type system that more people could use to prove results in computation. Given how category theory has only gotten more popular due to more consciousness of its usefulness in verification, particularly in functional programming, the hope of this project is so that more people will be able to use the semantics of category theory to elide some of the more technical proofs that are often involved in proving computational properties. Nevertheless, the paper will not comment upon the usefulness of said theory but will show the theory necessary to establish the type system to get to how a computer could interpret types as categories.