# Contents

## Idea

In type theory the type of propositions is what in the categorical semantics becomes the subobject classifier.

Its generalization from propositions to general types is the type of types in homotopy type theory.

## References

Detailed discussion of the type of propositions in Coq is in

Revised on October 3, 2012 02:01:13 by Urs Schreiber (82.169.65.155)