「C-システム、分裂ディスプレイクラス、カートメルツリー」より：
ヴォエヴォドスキー〈Vladimir Voevodsky〉は、型理論の理論〈theory of type theories〉の基礎としてカートメル〈John Cartmell〉のコンテキスト圏〈contextual category〉を採用しました。が、呼び名はC-システム〈C-system〉に変更しています。
ヴォエヴォドスキーがコンテキスト圏を「圏」と呼びたくない理由は、おおよそ「あれはホンマモンの圏じゃないからな」ということです。
では、ホンマモンの圏〈genuine category〉とは何でしょうか？ プレーンな圏であれ、構造が載った圏（例： モノイド圏）であれ、圏同値で移りあえる2つの圏は同一視可能です。しかし、「圏は小さい」とか「モノイド積は厳密」とかの条件を付けてしまうと、圏同値で移りあえても同一視はできません。違うモノとして扱う必要があります。
ヴォエヴォドスキーは、圏の同一視可能性（同じとみなしてよい基準）は、（構造があれば構造を保存するような）圏同値で移りあえることだと考えているようです。なので、圏の上に、圏同値で保存できない（破られる／壊れてしまう）構造や法則を載せたものは、ホンマモンの圏ではない、ということになります。
偶発的に〈accidentally〉圏として定義はされているが、ホンマモンではない圏を、ヴォエヴォドスキーは「集合レベルの圏〈set-level category〉」とか「プレ圏〈pre-category〉」と呼んでいます。厳密圏〈strict category〉と呼ぶ人もいますが、厳密モノイド圏などの用法と食い違うのであまりよろしくないかと。
集合レベルの圏は、それを構成している集合レベルの同型がないと、（構造を含めた）同一視ができない構造物です。そういったモノは「システム」と呼んだほうがいいだろう、ということです。よって、ヴォエヴォドスキーの型理論では、C-システム、C0-システム、B-システムなどが出てきます。
僕は「圏」よりむしろ、「圏」の前につく形容詞があまりにも一般的過ぎる言葉で「使いにくいなぁ」とは思ってました。カートメル〈John Cartmell〉のコンテキスト圏〈contextual category〉、ジェイコブス〈Bart Jacobs〉の包括圏〈comprehension category〉 ピッツ〈Andrew M Pitts〉の型圏〈type category〉など。
型理論に出てくる圏は、偶発的に圏として定式化されたパチモンの圏が多いのは確からしいです。それらの“システム”を差別的(?)に扱う、というよりは、扱う際に「圏論のお作法や道徳に必ずしも従う必要はない」と捉えればいいと思います。
圏同値で保存されないような概念・構造・法則は良くない〈evil〉という発想があります。nLab: principle of equivalence より：
Floating around the web (and maybe the 𝑛Lab) is the idea of half-jokingly referring to a breaking of equivalence invariance as “evil”.
ウェブ上で（𝑛Lab でも）広まっている考え方は、冗談半分ではありますが、同値不変性を破る／壊すことは「悪」とみなそう、ということです。
“システム”に関しては、同値不変性を破っても悪じゃないと思えば、気が楽になります。
