The slogan “Hask is a subcategory of ” is inaccurate. A programming type does not denote a set of values but a pointed CPO, a partial order that is complete under directed suprema and carries a least element for nontermination, with programs interpreted as Scott-continuous maps preserving directed joins. The order records how defined a value is, and makes general recursion meaningful as a least fixed point . Types are domains, not sets.
Even the pointed-CPO reading is only approximately the category one wants. The operator seq, which forces a value to weak head normal form, breaks faithfulness. Under seq a term can distinguish from , so the two are no longer denotationally equal, and the categorical laws degrade. With seq present the product fails its universal property, since can observe the definedness of a pair independently of its projections, so no mediating map is unique.
The categories that actually model this are , the ω-complete pointed CPOs with strict continuous maps, or the SFP / bifinite domains, closed under the constructions one needs and cartesian closed on the non-strict maps. Recursion at the type level demands algebraic compactness, an endofunctor whose initial algebra and final coalgebra coincide, so that a recursive type equation has a canonical solution. This is where F-algebras meet the domain theory. Achieving it in general requires the two-layer structure of axiomatic domain theory. This structure pairs a cartesian closed category for the total and higher-order maps with a strict subcategory of partial, -preserving maps in which limit–colimit coincidence and the compactness hold.
“Categorical proof assistant” conflates two independent axes. One axis is whether the syntax corresponds strictly to an internal language. Cubical Agda realizes the internal language of an -topos, with univalence holding as a computation rule rather than merely asserted. The other axis is whether the design is category-derived without being an internal language. Charity programs with initial algebras and final coalgebras directly, whereas the compiling-to-categories approach elaborates a term into arrows of a cartesian closed category. A system can sit on either axis alone.
Lean sits on neither. Its foundation is the Calculus of Inductive Constructions extended with quotient types as primitive, a proof-irrelevant impredicative Prop, universe polymorphism, and exactly three axioms, namely propext, Quot.sound, and Classical.choice. Together these force any model to be a well-pointed boolean topos with choice, which collapses essentially to . Consequently Lean cannot serve as the internal language of a nontrivial topos such as a sheaf topos , whose internal logic is intuitionistic and not well-pointed.
Simplicial type theory, implemented in Rzk, is by contrast a genuinely new theory rather than a repackaging. Segal types and extension types make higher-coherence bookkeeping automatic, to the point that the Yoneda lemma is provable in a few pages of formalization. Its cost is practical. It remains a research prototype, with slow type-checking, no tactic layer, and univalence still taken axiomatically rather than computed.
References
Dana Scott, “Outline of a Mathematical Theory of Computation” (1970) / Scott & Strachey, CPOs, Scott-continuity, least-fixed-point recursion
Peter Freyd, “Algebraically Complete Categories”, in Como Category Theory (LNM 1488, 1991), algebraic compactness / initial-algebra = final-coalgebra
Emily Riehl & Michael Shulman, “A type theory for synthetic ∞-categories”, Higher Structures 1 (2017), Segal/extension types, the simplicial type theory implemented in Rzk