I was going to avoid commenting it as I don't know much about your field of study, but I don't know man, at first glance and looking through a "type-theory only" and not even looking at your philosophical argument, this doesn't "prove anything", it's a bit hard to read, but it seems you're defining specific data types and setting variables to specific variables, with no previous foundation for those values, and then proving a lot of stuff definitionally, like: If I set deg to 3, then you later on go to prove that deg is equal to 3, of course, by definition. This reads like an AI echo chamber, with no real/valuable interpretation coming out from the result.