1999/11/11 by Kosta Došen, Kosta Dosen, Dosen, Kosta +3 · 1 citation
Computer Science · Mathematics · #18A15 (Secondary) #18D15 (Primary) 03B40 #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #math.CT #math.LO #msc:03B40 #msc:18A15 #msc:18D15
paper · pdf · doi:10.48550/arxiv.math/9911073
21 pages, published in Publications de l'Institut Mathematique, note with additional reference added in September 2012
openalex publication_date 1999/11/11 · arxiv created 2012/09/25 · arxiv updated 2012/09/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
From the analogue of Boehm's Theorem proved for the typed lambda calculus, without product types and with them, it is inferred that every cartesian closed category that satisfies an equality between arrows not satisfied in free cartesian closed categories must be a preorder. A new proof is given here of these results, which were obtained previously by Richard Statman and Alex K. Simpson.