Jason (jcreed) wrote,

I've been trying to extract some understanding out of Michael Warren's approach to directed homotopy type theory. It's rough going because although I have a pretty definite intuition for equality types as an inductive type, the notion of "transformation type" or "hom type" or whatever that you'd want for a directed theory doesn't seem to have any similarly obvious characterization.

Warren does nonetheless propose a characterization in terms of introduction and elim rules, but it sets of red flashing klaxony alarms in my brain because it has the same introduction rule as equality: just refl. Experience has taught me repeatedly that something deeply weird is going on (not necessarily wrong, just weird) when two propositional connectives have the same intro rules but different elim rules, or vice-versa.

That being said, I'm definitely sympathetic to the goal of finding a characterization of roughly this shape. It would be awesome to have. The stuff Bob Harper and Dan Licata worked out at dimension 2 ("2-Dimensional directed dependent type theory", which is cited and linked over here) is really cool and all, but it seems to require a lot of clever and delicate axiom-inventing. It took me a lot of staring and mumbling before I believed that all of the polarities assigned in the rules for dependent product types had to be the way they were.
Tags: hott, math

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded