Trebor
trebor@types.pl
<p>PhD student at IUB interested in type theory and music and stuff</p>
Posts
-
Post #2142736
Cartesian cubical groups aren&#39;t even Kan
-
Post #2142735
I understand why homotopy theorists don&#39;t do cubical sets often now. Nothing ever works with cubical sets!
-
Post #2142734
Are inference rules figures or equations?
-
Post #2142732
What&#39;s the free cartesian closed category with an applicative functor like
-
Post #2142731
The problem with implementing cubical is that we have so many variables of the same type, so really nothing saves us from making scope errors, not even dependent types and intrinsic scopes
-
Post #2142730
Today I finally finished formalizing the proof that a term is typable in intersection type theory if and only if it is strongly normalizing! Intersection type theory is simply typed λ-calculus with a binary intersection type (and no subtyping relation or anything fancy). A term has an intersection type iff the same term inhabits both types.