I read one of those popular papers on cubical type theory, but no wonder I could only see formulas and diagrams without being able to recognize them at all.

So here's what I want. I want a deep enough explanation of what composition, Kan filling and gluing have to do with homotopy type theory. I don't expect there could be an ELI (insert age) for it but instead define the word dummy in the title as someone having some basic understanding of HoTT and category theory (perhaps, but not necessarily optionally).

  • 6
    $\begingroup$ Dan Licata's talk on Cubical Infinite-dimensional type theory is probably a good intuitive introduction with a reasonable amount of type theory given it's a talk. (Licata is definitely in the type theory camp of the HoTT community.) $\endgroup$ Commented Jun 6, 2017 at 14:21
  • $\begingroup$ I watched the whole thing. It was pretty easy until the Kan filling part ... It seems the strategy in the paper (defining Kan filling in terms of composition) is much simpler, or is it? And it seems the whole technique of gluing was'nt developed at the time the video was recorded. Perhaps I could understand the paper after watching it, though. $\endgroup$
    – 盛安安
    Commented Jun 6, 2017 at 16:40

1 Answer 1


A year after and I'm writing one myself.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.