HoTT III: Sets and Logic

This note corresponds to Ch. 3 in the HoTT book

This chapter is dedicated to the study of HSet (sets, the -type), HProp (mere propositions, the -type), and Contr (contractible types, the -type):

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 is a set if forall and , we have . The proposition is defined to be the type:

Sets in homotopy type theory are not like sets in ZF set theory, in that there is no global "membership predicate" . To provide some examples of sets, $𝟙$ , $𝟘$ and are sets.

Global Instance hprop_Empty : IsHProp Empty.
Proof. intro x. destruct x. Defined.

Corollary hset_nat : IsHSet nat.
Proof.
  exact _.
Defined.

Moreover, if and are sets, then so is . For given and , we have and . But since is a set, and , since is a set; hence .

Similarly, if is a set, and such that is a set, then is a set

Given , is a set. For suppose and for . By functional extensionality,

But for , we have

So since is a set, we have . Now, using funext again, the dependent functions and are equal, and hence, applying , so are and .

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 -types, and may also be called the -type; its defining property is that it has no non-trivial paths. Similarly, the -type can be has no non-trivial paths between paths.

Notation Is1Type := IsTrunc 1.

A type is a -type if for all , and , , we have . We can similarly define -types, -types, and so on.

If is a set, that is, is inhabitated, then is a -type.

(** 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 is not a set.

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 , we do not have .

Mere propositions

Propositions-as-types 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 will be "true" if it is inhabitated, and false if its inhabit yields a contradiction (i.e. $𝟘$ ). Now, for example, if we're given an element of $𝟚$ , it contains one bit of additional information: which element of $𝟚$ we are given. By contrast, when we're given an element of $𝟙$ (i.e. ), we receive no more information than the mere fact that $𝟙$ contains an element, since any two elements of $𝟙$ are equal to each other. This suggests the following definition:

Type is a mere proposition if forall , we have .

For ,

Thus, to assert that is a mere proposition means to exhibit an inhabitant of , which is a dependent function connecting any two elements of by a path. The continuity/naturality of this function implies not only that any two elements of are equal, but also that contains no higher homotopies either.

If is a mere proposition, and , then $𝟙$ .

(** 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 and are mere propositions such that and , then .

(** 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 $𝟙$ is said to be contractible. Thus, any mere proposition that is inhabitated is contractible. On the other hand, the uninhabited type $𝟘$ is also vacuously a mere proposition.

Note that a type is a set if and only if, for , the identity type is a mere proposition.

Every mere proposition is a set.

For any type , types and are mere propositions.

(** 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 is a type family with each type regarded as a proposition. Then itself is a predicate on , or a property of elements of . What we regard as in set theory can be regarded as in type theory. For a general element , has more than one distinct proof; but if is a mere proposition, this cannot happen.

Suppose is a type famiy such that is a mere proposition for all . If are such that , then .

(** ** 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 was supposed to be a mere proposition. It follows that if two equivalences have equal underlying functions, then they are equal as equivalences. In , can be thought of as a subtype of . We may write to refer to the mere proposition . If it holds, we say that is a member of . Similarly, can be written as .

As further examples of subtypes, we may define the "subuniverses" of sets and propositions in :

Recall that for any two universes and , if , then . For sets and mere propositions, we therefore have maps:

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 is an equivalence.

It essentially says that any mere proposition in universe can be resized to an equivalent one in . It follows automatically if satisfies LEM. This is a form of impredicativity for mere propositions, and by avoiding its use, our type theory will remain predicative.

In practice, however, what we want is a slightly different statement, that a universe under consideration contains a type which "classifies all mere propositions". In other words, we want a type together with an -indexed family of mere propositions, which contains every mere proposition, upto equivalence. This follows from the propositional resizing axiom, if is not the smallest universe , then we can define .

In the absence of propositional resizing, the definition of power set depends on the choice of . In its presence, however, one can define the power set to be:

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 type-former to mere propositions; this, of course, requires us to know whether the type former in question preserve mere propositions.

If and are mere propositions, so is .

If is such that for all , B(x) is a mere proposition, then is a mere proposition.

Definition PiType_isMereProp `{Funext} (A : Type) (B : A -> Type)
  := trunc_forall _ A B (-1).

In particular, If is a mere proposition, then so is regardless of what is. Since $𝟘$ is a mere proposition, so is $𝟘$ . Thus the connectives "implies", "not", and "forall" preserve mere propositions.

On the other hand, even if and are mere propositions, will not, in general, be one. For instance, $𝟙$ is a mere proposition, but $𝟚 𝟙 𝟙$ is not. Logically speaking, is a "purely constructive" sort of "or": a witness of it contains which disjunct is true. However, if we need a more classical sort of "or" that preserves mere propositions, we need a way to "truncate" this type into a mere proposition by forgetting the additional information. The same issue arises with .

Propositional truncation

The propositional truncation, also called -truncation, bracket type, or squash type, is an additional type former wich "truncates" a type down to a mere proposition, forgetting all information contained in inhabitants of that type other than their existence.

More precisely, given type , there is a type with two constructors:

For any , we have .
For any , we have .

The first constructor means that if is inhabited, so is . The second ensures that is a mere proposition; usually we leave the witness of this fact nameless.

The recursion principle of says that: if is a mere proposition, and we have , then there is an induced such that for all .

In other words, any mere proposition that follows from already follows from . Thus, , as a mere proposition, contains no more information than the inhabitedness of .

With propositional truncation, we can extend the "logic of mere propositions" to cover disjunction and existential quantification. Specifically, is a mere propositional version of "A or B", which does not remember which disjunct is true.

The recursion principle of truncation implies that we can still do a case analysis on when attempting to prove a mere proposition. That is, suppose we have an assumption , and we are trying to prove a mere proposition . In other words, we are trying to define an element . Since is a mere proposition, by recursion principle for propositional truncation, it suffices to construct a function . But now we can do case analysis on .

Similarly, or a type family , we can consider to be the mere propositional version of "there exists an such that ". If we have an assumption of type , we may introduce new assumptions and when attempting to prove a mere proposition. In other words, if we know that there exists some such that , but we don't have a particular such at hand, then we are free to make use of such an as long as we aren't trying to construct anything which might depend on the particular value of .

The axiom of choice

assume type and type families

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 , there exists some such that , but that these values are not chosen or specified in any known way. The truncation in the codomain means we conclude that there exists some function , but this function is not determined or specified in any known way.

AC is equivalent to the statement that for any set and map such that each is a set, we have

this corresponds to a well-known 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 is a mere proposition, then .

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 such that:

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 -ladder of types, and there are many other modalities not lying on this ladder at all.

Contractability

A mere proposition which is inhabited must be equivalent to $𝟙$ , and the converse also holds. A type with this property is called contractible.

Type A is contractible or a singleton, if there is an , called the center of contraction, such tht for all . We denote the specified path by . In other words,

We can pronounce this as " contains an element, and every other element of is equal to that element". To the classical ear, this could sound as a definition of connectedness, rather than contractability.

For type , the following are logically equivalent:

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 , the type is a mere proposition.

Global Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
  : IsHProp (IsTrunc n A) | 0.

If is contractible, so is .

Global Instance contr_contr `{Funext} (A : Type) `{Contr A}
  : Contr (Contr A) | 100.

If is a type family such that is contractible, then is contractible.

Global Instance trunc_forall `{P : A -> Type} `{forall a, IsTrunc n (P a)}
  : IsTrunc n (forall a, P a) | 100.

If is a retract of , and is contractible, then so is .

For any and any , the type is contractible.

Global Instance contr_basedpaths {X : Type} (x : X) : Contr {y : X & x = y} | 100.

Let be a type family.

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 is a mere proposition if and only if for all , the type is contractible.

(** 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.