クランやC-システムは、型理論の構文構造の定式化のために案出されたものです。構文構造の定式化には、大きい集合は出てこないので、クランやC-システムは原則的に小さい圏です。しかし、具体例を考える場合には、むしろ大きな圏まで含めたほうが例を作りや…