Hello, I'm working on creating a dependently typed programming language that stores code as raw syntax trees for deduplication purposes (kinda like unison). I joined this server because I was wondering if anyone knew any good resources about how I might go about implementing a dependently typed programming language, (i.e. PI operator, type inference & checking, hierarchy of universes & inductive types)

Are you familiar with the little typer? https://mitpress.mit.edu/books/little-typer

I am, I've seen the talk on youtube and read a few pages from the book, but i'm better at watching videos than reading, so i've been putting it off.

Personally, I’m not sure if a better resource exists. If you are looking for videos though, Edwin Brady’s lectures on Idris 2 are probably a good start

I am creating something similar to Unison too, but as well as Envision and Lamdu, I store every node of the AST in json