A few notes, because this is obviously vibe coded, and does not work in many ways.
1. Yon's documentation mentions "Homotopy type theory:"
> the runnable HoTT fragment is refl/pair/fst/snd
These are basic features of martin-lof type theory, not homotopy type theory. The documentation makes no reference of an interval type, which is generally the way to go for decidable type-checking in HoTT without univalence as an opaque axiom.
Pi types are mentioned, but Yon does not have dependent types. From what I can tell, they are polymorphic, maybe even just simply-typed (except for identity types under Pi). See here in the repo: https://github.com/yon-language/yon/blob/523e363a4a00e8da1410a2521b1d7d1309d360ce/frontend/ast.ml#L37
The datatype Ty only refers to other Ty's. Thus, it is not dependent. Terms cannot appear in types. Pi is explicitly indexed by a type defining its domain and codomain. A pi type is not a pi type if its codomain cannot depend on its domain.
2. Normalization can fail in Yon.
Yon's docs say that its universe of propositions has booleans (
https://yon-lang.org/book/heyting-core?_highlight=prop). It also says its logic is intuitionistic (AKA, constructive). However, it also says the logical connectives on booleans are CLASSICAL. This implies law of excluded middle, which is NOT constructive without careful sandboxing (e.g., Linear logic).
Yon dangerously allows propositions to be lifted to booleans. If I am interpreting correctly (docs are very vague), this means propositions can be lifted to terms. This causes an obvious failure of normalization due to assumed proof irrelevance (otherwise Prop would not be distinguished) (also see Coquand's paper on this https://arxiv.org/abs/1911.08174).
3. Yon's type definitional equality does not actually reduce types.
See here. This is the function used by the type-checker to check if types are equal.
https://github.com/yon-language/yon/blob/523e363a4a00e8da141...
No reduction actually occurs, conveniently because none of the types actually contain terms (that is, it is simply typed).
Yon claims to be dependently-typed. See this in the repo: https://github.com/yon-language/yon/blob/523e363a4a00e8da1410a2521b1d7d1309d360ce/frontend/ast.ml#L21
> Types in Yon Core kernel — the small dependent type theory used for the operational semantics.
Suppose I'm reading the source code wrong. Conveniently, the comment one line below reveals, once again, that the "type theory" is simply-typed:
> * T, U ::= Type_n universe of level n
> * | Pi(x:T). U dependent function
Pi types eliminate into a FIXED type that does not depend on x. This means there is also no purpose for having a universe hierarchy.
To confirm, I scoured the docs a bit for any examples using Pi types or Sigma types. I searched the docs, and could not find any, besides this example:
> world W { Code is X }
> place Account in W { balance number }
> fun takes_sub(s: { a : Account where Pi(x: Account). Pi(y: Account). Id(Account, x, y) }): number { return 0 }
> fun main(): number { return 0 }
Notably, the identity is the only constructor for Ty indexed by a term. That is, Pi types can ONLY eliminate into the identity. What if I want my Pi type to eliminate into anything else living in Prop? e.g., an existential like \forall (x : Nat), \exists (y : Nat), x This project is clearly produced by AI, and clearly dangerously incorrect. Do not use this for anything serious.