I couldn't find some basic facts about propositions, so I added them:
1) Every contractible type is a proposition.
2) All parallel paths in a proposition are equal.
3) Proposition induction
4) Given a family over a proposition, the total type is a proposition iff each fiber is a proposition
5) Propositions are closed under retracts and equivalences
6) Added a few "shortcuts" to go directly between some characterizations of propositions which were only linked by a chain of implication.
I couldn't find some basic facts about propositions, so I added them:
1) Every contractible type is a proposition. 2) All parallel paths in a proposition are equal. 3) Proposition induction 4) Given a family over a proposition, the total type is a proposition iff each fiber is a proposition 5) Propositions are closed under retracts and equivalences 6) Added a few "shortcuts" to go directly between some characterizations of propositions which were only linked by a chain of implication.