Skip to content

Commit d2d2a4f

Browse files
Update README.adoc
1 parent f11cc29 commit d2d2a4f

1 file changed

Lines changed: 19 additions & 0 deletions

File tree

README.adoc

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -93,3 +93,22 @@ It should not be placed between Kategoria/Katagoria and TypeLL as a required dep
9393
QTT overestimates wall-clock time; tropical grades give the tighter bound.
9494

9595
See `docs/ARCHITECTURE.adoc`, `docs/PIPELINE.adoc`, and `ROADMAP.adoc` for full detail.
96+
97+
TypeFix Zero is a proposed standalone calibration calculus for the type-theory pipeline.
98+
99+
It is not a production language and not a replacement for TypeLL. Its role is to mark the lower bound of the estate’s “typed but Turing-complete” design space:
100+
101+
stratified universes / metasets: Type i : Type (i + 1)
102+
ordinary function types: A -> B
103+
natural numbers as the minimal observable data type
104+
lambda abstraction and application
105+
one explicit fixed-point primitive: fix : (A -> A) -> A
106+
107+
The key distinction is that TF0 separates:
108+
109+
a total mathematical fragment suitable for proof-like reasoning
110+
an explicitly partial fragment introduced only through fix
111+
112+
This makes TF0 useful as a test object for TypeLL, Kategoria/Katagoria, and typed-Wasm discussions: it exposes exactly where Turing completeness enters and exactly where proof-theoretic totality stops.
113+
114+
Status: proposed standalone repository; design-stage.

0 commit comments

Comments
 (0)