simplicial model of type theory

HoTT

絵が多いので、こっち↓の方に書いた。xyjaxを使いたかっただけというわけではない
http://formalgroup.tumblr.com/post/96778113120/simplicial-model-of-type-theory


cubical modelのことを書こうと思ったけど、数学の世界では、simplicial setの方が、cubical setより、ずっとメジャーで勉強しやすい(教科書も多い)。基本的なところは似ているので、まずはsimplicial setから理解するのが結局近道な気がする
cf.A model of type theory in cubical sets

http://www.cse.chalmers.se/~coquand/mod1.pdf