2013/06/16 by Michał R. Przybyłek, Michal R. Przybylek, Przybylek, Michal R.
Computer Science · Mathematics · #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic, programming, and type systems #math.CT
paper · pdf · doi:10.48550/arxiv.1306.3703
openalex publication_date 2013/06/16 · arxiv created 2014/10/15 · arxiv updated 2014/10/16 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
This paper shows how internal models for polymorphic lambda calculi arise in any 2-category with a notion of discreteness. We generalise to a 2-categorical setting the famous theorem of Peter Freyd saying that there are no sufficiently (co)complete non-degenerate categories. As a simple corollary, we obtain a variant of Freyd theorem for categories internal to any tensored category. Also, with help of introduced concept of an associated category, we prove a representation theorem relating our internal models with well-studied fibrational models for polymorphism.