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.

  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).

  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:

> 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 < y. Unfortunately impossible in Yon.

This project is clearly produced by AI, and clearly dangerously incorrect. Do not use this for anything serious.

> Slots are stable for the life of the process; the heap grows with distinct content only.

So how is a program supposed to handle lots of unique content? Like a web server handling user requests?

So if you want to define a world, I expect you to tell me how to supply objects + morphisms + the composition law + the site structure. I don't know what a "semantic site" is, just what a "site" is. You'd need to define it. Anyway, we then get to our first examples of declaring worlds:

  world Currency { Code is EUR, USD }
  world Status { State is on, off }

  world Sub subset of Currency  

So now I think, "OK, maybe you just declare part of the structure and fill it in later, before you actually use it..."

But then your example disproves that notion! You have

  world Shop { Code is X }

  place Account in Shop {
    balance number
    owner String
  }

  fun main(): number {
    be a holds new Account { balance 40 owner "ada" }
    be _p holds String.print(a.owner)
    return a.balance + 2
  }

I think a "topos inspired programming language" would be kind of cool if you could pull it off, but I think you really need to figure out how to sell it in the docs to at least one of the two communities above.

> Yon allocates into xleech2, a content-addressed heap whose geometry is the Leech lattice Λ24: exactly 196,560 slots per heap.

What is the computational complexity of memory allocation into this Leech lattice? What applications did you have in mind where making allocation a maths problem in order to save time on comparisons makes sense? What is going to happen when a program exhausts your little heap?