This note corresponds to Ch. 3 in the HoTT book
This chapter is dedicated to the study of HSet (sets, the
Notation Contr := (IsTrunc minus_two).
Notation IsHProp := (IsTrunc minus_two.+1).
Notation IsHSet := (IsTrunc minus_two.+2).
focusing on the logic of mere propositions and the notion of propositional truncation.
Sets and types
A type
Sets in homotopy type theory are not like sets in ZF set theory, in that there is no global "membership predicate"
Global Instance hprop_Empty : IsHProp Empty.
Proof. intro x. destruct x. Defined.
Corollary hset_nat : IsHSet nat.
Proof.
exact _.
Defined.
Moreover, if
Similarly, if
Given
But for
So since
Global Instance trunc_forall `{P : A > Type} `{forall a, IsTrunc n (P a)}
: IsTrunc n (forall a, P a)  100.
Sets are just the first rung of the ladder of
Notation Is1Type := IsTrunc 1.
A type
If
(** Truncation levels are cumulative. *)
Global Instance trunc_succ `{IsTrunc n A}
: IsTrunc n.+1 A  1000.
Proof.
generalize dependent A.
simple_induction n n IH; simpl; intros A H x y.
 apply contr_paths_contr.
 apply IH, H.
Qed.
Another fact to keep in mind is that this stratification of types is not degenerate; in particular, not all types are sets. For instance, universe
Definition not_hset_Type : ~ (IsHSet Type).
Proof.
intro HT.
apply true_ne_false.
pose (r := path_ishprop (path_universe equiv_negb) 1).
refine (_ @ (ap (fun q => transport idmap q false) r)).
symmetry; apply transport_path_universe.
Defined.
Propositions as types?
Our previous straightforward interpretation of "propositions as types" do not work anymore. The statements of double negation and law of excluded middle do not function as they do in classical type theory; in particular, they are incompatible with the univalence axiom.
For
For
Mere propositions
Propositionsastypes have good and bad properties. Both have a common cause: when types are viewed as propositions, they contain more information than mere truth or falsity, and all "logical" constructions on them must respect this additional information. This suggests that we could obtain a more conventional logic by restricting attention to types that do not contain any more information than the truth value, and only regarding these as logical propositions.
Indeed, if
Type
For
Thus, to assert that
If
(** If an hprop is inhabited, then it is equivalent to [Unit]. *)
Lemma if_hprop_then_equiv_Unit (hprop : Type) `{IsHProp hprop} : hprop > hprop <~> Unit.
Proof.
intro p.
apply equiv_iff_hprop.
 exact (fun _ => tt).
 exact (fun _ => p).
Defined.
If
(** Two propositions are equivalent as soon as there are maps in both directions. *)
Definition isequiv_iff_hprop `{IsHProp A} `{IsHProp B}
(f : A > B) (g : B > A)
: IsEquiv f.
Proof.
apply (isequiv_adjointify f g);
intros ?; apply path_ishprop.
Defined.
A space that is homotopy equivalent to
Note that a type
Every mere proposition is a set.
For any type
(** Truncatedness is an hprop. *)
Global Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
: IsHProp (IsTrunc n A)  0.
Classical versus intuitionistic logic
With the notion of mere proposition, we can now give a proper formulation of LEM and double negation:
These are seen as being logically equivalent to each other. Renaming for clarity:

A type
is decidable if . 
A type family
is decidable if . 
has decidable equality if .
Class Decidable (A : Type) :=
dec : A + (~ A).
Class DecidablePaths (A : Type) :=
dec_paths : forall (x y : A), Decidable (x = y).
Subsets and propositional resizing
Suppose
Suppose
(** ** Subtypes (sigma types whose second components are hprops) *)
(** To prove equality in a subtype, we only need equality of the first component. *)
Definition path_sigma_hprop {A : Type} {P : A > Type}
`{forall x, IsHProp (P x)}
(u v : sigT P)
: u.1 = v.1 > u = v
:= path_sigma_uncurried P u v o pr1^1.
For instance, recall that we defined
where each type
As further examples of subtypes, we may define the "subuniverses" of sets and propositions in
Recall that for any two universes
However, the former cannot be an equivalence, as making it so would remind us of paradoxes in Cantorian set theory. However, the latter could be an equivalence, and we consier adding the propositional resizing axiom:
The map
It essentially says that any mere proposition in universe
In practice, however, what we want is a slightly different statement, that a universe
In the absence of propositional resizing, the definition of power set depends on the choice of
which is then independent of
The logic of mere propositions
In many cases, logical connectives and quantifiers can be represented in this logic by simply restricting the typeformer to mere propositions; this, of course, requires us to know whether the type former in question preserve mere propositions.
If
If
Definition PiType_isMereProp `{Funext} (A : Type) (B : A > Type)
:= trunc_forall _ A B (1).
In particular, If
On the other hand, even if
Propositional truncation
The propositional truncation, also called
More precisely, given type

For any
, we have . 
For any
, we have .
The first constructor means that if
The recursion principle of
In other words, any mere proposition that follows from
With propositional truncation, we can extend the "logic of mere propositions" to cover disjunction and existential quantification. Specifically,
The recursion principle of truncation implies that we can still do a case analysis on
Similarly, or a type family
The axiom of choice
assume type
and moreover that:

is a set. 
is a set for all . 
is a mere proposition for all and .
The axiom of choice asserts that under these assumptions,
Note, in particular, that propositional truncation appears twice. The truncation in the domain means we assume that for every
AC is equivalent to the statement that for any set
this corresponds to a wellknown equivalent form of the classical AC, namely "the cartesian product of a family of nonempty sets is nonempty".
These two statements of AC are not a consequence of out basic type theory, but they may be consistently assumed as axioms. Note that the latter can be shown equivalent to asking for an equivalence:
This illustrates a common pitfall: although dependent function types preserve mere propositions, they do not commute with truncation. AC says that the equivalence holds for sets, but fails in general.
The principle of unique choice
If
Definition isequiv_to_O_inO (T : Type) `{In O T} : IsEquiv (to O T).
Definition p_simeq_trun_p := isequiv_to_O_inO (Tr (1)).
It has the following important consequence:
Principle of unique choice. Suppose

For each
, the type is a mere proposition. 
For each
we have .
Then we have
Lemma unique_choice {X Y} (R:X>Y>Type) :
(forall x y, IsHProp (R x y)) > (forall x, (hunique (R x)))
> {f : X > Y & forall x, (R x (f x))}.
When are mere propositions truncated?
In a nutshell, we shall use untruncated logic as the default convention, and qualify the truncated versions by "mere", for the following reason: mere propositions aren't a fundamental part of type theory; they are only the second rung on the
Contractability
A mere proposition which is inhabited must be equivalent to
Type A is contractible or a singleton, if there is an
We can pronounce this as "
For type

is contractible. 
is a mere proposition, and there is a point . 
is equivalent to .𝟙
(* The Unit type is contractible *)
(** Because [Contr] is a notation, and [Contr_internal] is the record, we need to iota expand to fool Coq's typeclass machinery into accepting supposedly "mismatched" contexts. *)
Global Instance contr_unit : Contr Unit  0 := let x := {
center := tt;
contr := fun t : Unit => match t with tt => 1 end
} in x.
For any type
Global Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
: IsHProp (IsTrunc n A)  0.
If
Global Instance contr_contr `{Funext} (A : Type) `{Contr A}
: Contr (Contr A)  100.
If
Global Instance trunc_forall `{P : A > Type} `{forall a, IsTrunc n (P a)}
: IsTrunc n (forall a, P a)  100.
If
For any
Global Instance contr_basedpaths {X : Type} (x : X) : Contr {y : X & x = y}  100.
Let

If each
is contractible, then is equivalent to . 
If
is contractible with center , then is equivalent to .
Definition equiv_sigma_contr {A : Type} (P : A > Type)
`{forall a, Contr (P a)}
: sigT P <~> A
:= Build_Equiv _ _ pr1 _.
Definition equiv_contr_sigma {A : Type} (P : A > Type) `{Contr A}
: { x : A & P x } <~> P (center A).
Type
(** Any two points in an hprop are connected by a path. *)
Theorem path_ishprop `{H : IsHProp A}
: forall x y : A, x = y.
Proof.
apply H.
Defined.
Theorem hprop_allpath (A : Type)
: (forall (x y : A), x = y) > IsHProp A.
intros H x y.
pose (C := Build_Contr A x (H x)).
apply contr_paths_contr.
Defined.