インスティチューションは、さまざまな型理論を統一的に扱うための便利な枠組みになります。与えられたインスティチューションをインデックス付き圏（indexed category）とみなして、グロタンディーク構成を行うことは有効なテクニックです。このテクニック…