Contents

# Contents

## Idea

In type theory the type of propositions $Prop$ corresponds roughly under categorical semantics to the subobject classifier. (To be precise, depending on the type theoretic rules and axioms this may not be quite true: one needs propositional resizing, propositional extensionality, and — in some type theories where “proposition” is not defined as an h-proposition, such as the calculus of constructions — the principle of unique choice?.)

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

## References

Detailed discussion of the type of propositions in Coq is in

Last revised on December 1, 2016 at 12:39:59. See the history of this page for a list of all contributions to it.