introit

Our standard library is here! https://github.com/yatima-inc/introit

I would dearly love to make Yatima a usable theorem prover, and Lean has been a huge inspiration particularly regarding syntax. But building a usable theorem prover is a huge project, and at minimum will require substantial work on our theory, on type-inference (which is fairly minimal right now) and on advanced features like quotient types or univalence. On that point, we've done a little exploration on encoding the Path types from Cubical Type Theory as self-types, and I think there's some promising work to be done there. But I know my limits and while I feel very comfortable building a useful programming language that can do a little bit of basic theorem proving, I know that doing a proper job on a real theorem is going to require larger scale resources. As far as the link from the Self-Types paper, our theory is similar to their Syste

Some random questions to the developers regarding the motivation that "math is more fun when you have a computer to take care of the detail-work" [0]: 1. Do you have plans to make Yatima a usable theorem prover? 2. If so, how will people typically quotient things (e.g. does it have quotient types)? 3. How far does the type theory depart from classical mathematics? 4. The paper you've linked [1] suggests that the standard definition of contradiction is "too strong" in its theory, but that appears to be the definition of Empty [2]. What am I missing? [0]: https://github.com/yatima-inc/yatima#motivation [1]: https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta... [2]: https://github.com/yatima-inc/introit/blob/main/Empty.ya

Sure, thanks for the feedback. Our standard library is here: https://github.com/yatima-inc/introit, I'll edit the README to make that more prominent As far as docs and tutorials, we weren't planning on doing a public release for another month or two, so there isn't anything yet. The language is still pre-alpha, so our focus has been on getting the core working correctly before smoothing the on-ramp. Also, tbh, I'm not 100% settled on what the user-facing syntax should be. Right now we have a simple lisp-like core syntax, but I'm thinking about implementing something like Racket's #lang declaration to allow the user to define and import frontends to that core syntax.

> types are very complex expressions and they're expressed with the same machinery as arithmetic expressions (femtolisp). This is how it works in Yatima. Since we use self-types and lambda-encodings for our datatypes, all type expressions are built up via some combination of self types, pi types and a few type-level constants (like primitives). For example, the type of booleans can be expressed as: def Bool : Type = @self ∀ (0 P : ∀ (Bool) -> Type) (& true : P (data λ P t f => t)) (& false : P (data λ P t f => f)) -> P self def true : Bool = data λ P t f => t def false : Bool = data λ P t f => f from https://github.com/yatima-inc/introit/blob/main/Pure/Bool.ya

Their explanation is reductive, but it looks like more than that. For example, in the standard library [0] the definition of the Map type is a function of other types. [0]: https://github.com/yatima-inc/introit/blob/main/Map.ya#L10