Jason (jcreed) wrote,

Have been reading around in the Homotopy Type Theory Book and it's really great stuff.

So, higher-dimensional category theory, right? It's amazing and awesome and beautiful, and has this flavor that is at once computational and topological and algebraic, and yet the thing about it that itches and itches and itches unrelentingly is where the heck do all the coherence conditions come from? How am I supposed to know how to define equivalence? There seem to be a million different definitions of strict this and weak that and pseudo-quasi-lax-whatever. But I know that someone I need them to prevent "evil" constructions that depend too much on too-exact equalities.

HoTT seems to break free of this itch because it doesn't ham-fistedly define what a weak ω-groupoid is, doesn't say in detail what fiddly axioms it's supposed to satisfy. It instead arranges a type theory where (if I understand this right) only non-evil constructions exist. The fiddly axioms that they satisfy fall out of beautiful and simple things like the inductive definition of equality types and the univalence axiom.

I have a type A in my hands: it is actually secretly a huge, ramified, complex thing swirling with paths between its elements and 2-paths between those paths, and turtles between turtles and so on. But I don't need to know that to use it. I hypothesize a variable of type A, construct some term of type B, and I have a function. But it's actually a functor, well, it's actually also an appropriately weak quasi-lax-whatever-5-pseudofunctor.
Tags: 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