Elektrine lite

← Feed

Trebor

trebor@types.pl

<p>PhD student at IUB interested in type theory and music and stuff</p>

Posts

  • View post

    Cartesian cubical groups aren&amp;#39;t even Kan

  • View post

    I understand why homotopy theorists don&amp;#39;t do cubical sets often now. Nothing ever works with cubical sets!

  • View post

    Are inference rules figures or equations?

  • View post

    What&amp;#39;s the free cartesian closed category with an applicative functor like

  • View post

    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

  • View post

    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.