を階数とする。型を次のレコード型と定義する。
- -対象(object)の型
- -射(morphism)の型の族
- -恒等射(identity)
- -射の合成(composition)
- -
- -
- -
- -
を階数とする。型を次のレコード型と定義する。
射の型は集合であると要請される。これは、群の定義([004W])においては集合としたのと同様である。対して、は集合とは限らない。
を階数、を前圏とする。がの対象であることをの代わりに単にと書く。対象に対して、の代わりに単にと書く。と書いた時点での前圏の構造が暗黙に了解されるのでこの表記で曖昧性はない。同様に、対象に対して、の代わりに単にと書く。合成は二項演算子を使ってと書く。
を階数、を前圏とする。前圏を次のように定義する。
前圏の対象の間には、同一視型の他に同型という同一視の概念が考えらる。
を階数、を前圏、を対象、を射とする。
を階数、を前圏、を対象、を射とすると、型は命題である。
を階数、を前圏、を対象とする。型をと定義する。
同型の基本性質は次のようにまとめられる。
圏とは、前圏であって対象の間の同型の型と同一視型が同値になるようなものである。
を階数とする。
を圏とすると、恒等射は同型なので[001S]を適用できて、同値
圏の典型例として、 ([006H])が圏であることを見る。
[004K]による。
関数外延性と一価性を仮定する。を階数とすると、は圏である。