Propositions and Sets

The source code for this module: PartII/PropsSets.ard
The source code for the exercises: PartII/PropsSetsEx.ard

Recall that under Curry-Howard correspondence there is no difference between propositions and types: all types are propositions and vice versa. In this module we discuss and justify an alternative view, according to which propositions are only some types, namely those types, all elements of which are equal. These types are called mere propositions since they have at most one element, which, if it exists, usually does not contain any data and is merely a proof of the proposition. It is standard in homotopy type theory to use the term “proposition” for mere propositions.

Subsequently we discuss another important subclass of types, consisting of those types that can be identified with sets.

Subsets, injective functions

In set theory if A is a set and P is a predicate on A, then we can define the subset { x : A | P x } of elements of A satisfying P, and the elements of the subset will also be elements of A.

In type theory we cannot talk about subtypes in this way. Instead, we say that a subtype B of type A is just any type together with an injective function B -> A. For example, the subset above corresponds to the type \Sigma (x : A) (P x), which is realized as a subtype of A by means of the function:

\lam t => t.1 : \Sigma (x : A) (P x) -> A

as long as this function is an injection. As we will see further in this module, this function is always an injection if the range of P is restricted to a certain class of types. This class is precisely the class of all mere propositions.

Consider an example: the subtype of Nat consisting of even natural numbers.

\func isEven (n : Nat) : Bool
  | 0 => true
  | 1 => false
  | suc (suc n) => isEven n

-- { n : Nat | T (isEven n) } -- set-theoretic notation 
\func Even => \Sigma (n : Nat) (T (isEven n)) -- subtype of even numbers

-- Embedding of even numbers into the type of all natural numbers
\func Even-inc (e : Even) => e.1

Let us show that Even-inc is an injection, namely that it satisfies the predicate isInj:

\func isInj {A B : \Type} (f : A -> B) =>
   \Pi (x y : A) -> f x = f y -> x = y
-- This is equivalent to the predicate below only in
-- presence of the excluded middle:
-- \Pi (x y : A) -> Not (x = y) -> Not (f x = f y)

This requires proving equalities between pairs. For non-dependent pairs this is completely straightforward and reduces to proving equalities between components:

\func prodEq {A B : \Type} (t1 t2 : \Sigma A B) (p : t1.1 = t2.1) (q : t1.2 = t2.2)
  : t1 = t2
  => path (\lam i => (p @ i, q @ i))

In case of dependent pairs, we cannot talk about equalities of second components since they have different types. In order to prove equality of such pairs we need to have a proof of equality between their first components and a proof of equality between the second component of one of the pairs and transported second component of the other pair:

\func sigmaEq {A : \Type} (B : A -> \Type) (t1 t2 : \Sigma (x : A) (B x))
  -- t1.2 : B t1.1
  -- t2.2 : B t2.1
              (p : t1.1 = t2.1) (q : transport B p t1.2 = t2.2)
  : t1 = t2
  {-
  \elim t1,t2,p,q
  | (a1,b1), (a2,b2), idp, idp => idp
  -}
  => J (\lam a' p' => 
          \Pi (b' : B a') (q' : transport B p' t1.2 = b') -> t1 = (a',b'))
       (\lam b' q' => pmap (\lam b'' => ((t1.1,b'') : \Sigma (x : A) (B x))) q')
       p t2.2 q

Note that any two elements of T b are equal. This allows us to prove that Even-inc is injective:

\func T-lem {b : Bool} {x y : T b} : x = y
  | {true} => idp

\func Even-inc-isInj : isInj Even-inc =>
  \lam x y p => sigmaEq (\lam n => T (isEven n)) x y p T-lem

Exercise 1: Let f : A -> B and g : B -> C be some functions. Prove that if f and g are injective, then g o f is also injective. Prove that if g o f is injective, then f is also injective.

Consider one more example. Define functions computing residuals modulo 3 and 5 and define the type of all natural numbers that are divisible by 3 or 5:

\func mod3 (n : Nat) : Nat
  | 0 => 0
  | 1 => 1
  | 2 => 2
  | suc (suc (suc n)) => mod3 n

\func mod5 (n : Nat) : Nat
  | 0 => 0
  | 1 => 1
  | 2 => 2
  | 3 => 3
  | 4 => 4
  | suc (suc (suc (suc (suc n)))) => mod5 n

\func MultipleOf3Or5 => \Sigma (n : Nat) ((mod3 n = 0) `Either` (mod5 n = 0))

In contrast to the previous example, the function that maps elements of MultipleOf3Or5 to Nat is not an injection:

\func Mul-inc (m : MultipleOf3Or5) => m.1

-- One can prove that Mul-inc is not injective
\func not-Mul-inc-isInj (p : isInj Mul-inc) : Empty => {?}

This is so because for some n, namely for those that are divisible by both 3 and 5, there are several non-equal proofs of (mod3 n = 0) Either (mod5 n = 0). Thus MultipleOf3Or5 is not a subtype of Nat.

Exercise 2: Define the predicate “divisible by 3 or by 5” in such a way that it becomes a proposition. Prove that MultipleOf3Or5 embeds in Nat.

Mere propositions

As the two examples above illustrate, a predicate defining a subtype should have the range consisting of types, all elements of which are equal. The types satisfying these conditions are called mere propositions or just propositions.

\func isProp (A : \Type) => \Pi (x y : A) -> x = y

For example, according to this definition Bool is not a proposition.

\func BoolIsNotProp (p : isProp Bool) : Empty => transport T (p true false) ()

Exercise 3: We say that a type A is trivial if there exists an element in A such that it is equal to any other element in A. Prove that A is trivial iff A is proposition and there is an element in A.

Propositions can be formed using logical operations ⊤, ⊥, ∧, →, ∀ the same as in the Curry-Howard correspondence. Operations ∨, ∃ and the predicate = can, of course, also be defined, but in general require additional language constructs, which we introduce later. One can use recursion and induction to define predicates in this logic as usual.

Consider several examples. The unit type Unit corresponds to the proposition “True”:

\func Unit => \Sigma

\func Unit-isProp : isProp Unit => \lam x y => idp

The empty type Empty is the proposition “False”:

\func Empty-isProp : isProp Empty => \lam x y => absurd x

The product (conjunction) of propositions is proposition:

\func Sigma-isProp {A B : \Type} (pA : isProp A) (pB : isProp B)
  : isProp (\Sigma A B) => \lam p q => prodEq p q (pA p.1 q.1) (pB p.2 q.2)

The function type (implication) between propositions is proposition:

\func funcExt {A : \Type} (B : A -> \Type) (f g : \Pi (x : A) -> B x)
              (p : \Pi (x : A) -> f x = g x) : f = g =>
  path (\lam i x => p x @ i)


\func Impl-isProp {A B : \Type} {- (pA : isProp A) -} (pB : isProp B) : isProp (A -> B)
  => \lam f g =>
      -- path (\lam i x => pB (f x) (g x) @ i)
      funcExt (\lam _ => B) f g (\lam x => pB (f x) (g x))

Propositions are closed under Pi-types (universal quantification):

\func forall-isProp {A : \Type} (B : A -> \Type) (pB : \Pi (x : A) -> isProp (B x))
  : isProp (\Pi (x : A) -> B x)
  => \lam f g => funcExt B f g (\lam x => pB x (f x) (g x))

However, the logic of propositions is not closed in general under sum types Either A B (Curry-Howard disjunctions), sigma types \Sigma (x : A) (B x) (Curry-Howard existential quantifier) and the equality type.

\func Either-isProp {A B : \Type} (pA : isProp A) (pB : isProp B)
   : isProp (Either A B) =>
   {?}

\func exists-isProp {A : \Type} (B : A -> \Type)
                    (pB : \Pi (x : A) -> isProp (B x))
  : isProp (\Sigma (x : A) (B x)) =>
  {?}

\func equality-isProp {A : \Type} (a a' : A) : isProp (a = a') => {?}

Exercise 4: Prove that Either is not a proposition in general.

Exercise 5: Prove that \Sigma (x : A) (B x) preserves propositions.

For now we cannot define disjunctions, existential quantifiers and equality. But later we will introduce a way to project appropriately any type A to the class of propositions, and this projection will be applied to the types above to get corresponding logical operations.

We now make several remarks on definitions of predicates.

A recursive definition defines a predicate valued in propositions if all its clauses are propositions. For example, the following defines a predicate in the logic of mere propositions if expressions E-zero and E-suc are propositions:

\func pred (n : Nat) : \Type
  | 0 => E-zero
  | suc n => E-suc

Inductive definitions can be also used to define predicates. One should be careful with inductive definitions since a predicate can often have several inductive definitions, some of which are valued in propositions and some of which are not. For example:

-- Defines predicate valued in propositions
\data \infix 4 <= (n m : Nat) \with
  | 0, _ => zero<=_
  | suc n, suc m => suc<=suc (n <= m)

-- Does not define a predicate valued in propositions
\data \infix 4 <=' (n m : Nat) \elim m
  | m => <=-refl (n = m)
  | 1 => zero<=one (n = 0)
  | suc m => <=-step (n <=' m)

Exercise 6: Prove that <= and <=’’ are predicates. It is allowed to use the fact that Nat is a set without a proof.

\data <='' (n m : Nat) : \Set0 \elim m
  | suc m => <=-step (<='' n m)
  | m => <=-refl (n = m)

Exercise 7: Prove that ReflClosure <= is not a predicate, but ReflClosure (\lam x y => T (x < y)) is a predicate.

\func \infix 4 < (n m : Nat) : Bool
  | _, 0 => false
  | 0, suc _ => true
  | suc n, suc m => n < m

\data ReflClosure (R : Nat -> Nat -> \Type) (x y : Nat)
  | refl (x = y)
  | inc (R x y)

Exercise 8: Prove that if A embeds in B and B is a proposition, then A is proposition.

Sets

Although, as we have just seen, equality of elements of a type A is not a proposition in general, it holds for many types A. Such types are called sets.

\func isSet (A : \Type) => \Pi (a a' : A) -> isProp (a = a')

-- By definition equality is mere proposition for sets
\func equality-isProp {A : \Type} (p : isSet A) (a a' : A) : isProp (a = a') => p a a'

This can be interated further: we may consider types A such that a=a’ are sets for all a a’ : A and so on. Define the homotopy level of a type inductively as follows:

• Mere propositions are of homotopy level -1.
• A type A has homotopy level suc n iff a=a’ is of homotopy level n.

The predicate hasLevel A suc-l, saying that A has homotopy level suc-l - 1, can be defined as follows:

\func hasLevel (A : \Type) (suc-l : Nat) : \Type \elim suc-l
  | 0 => isProp A
  | suc suc-l => \Pi (x y : A) -> (x = y) `hasLevel` suc-l

The sets are thus precisely all the types of homotopy level 0. This is a large class of types, which includes, for example, Nat, Unit, Bool, lists of sets and so on. All set-theoretic reasoning can be done entirely in the levels of sets and propositions.

Let us consider several types and prove that they are sets. First of all, the empty type is trivially a set:

\func Empty-isSet : isSet Empty => \lam x y _ _ => \case x \with {}

Let us prove that the unit type is a set. We will need a lemma saying that if B is a proposition and A is a retract of B, then A is also a proposition. Recall that A is called a retract of B if there exist functions f : A -> B and g : B -> A such that the composition g o f is identity.

\func retract-isProp {A B : \Type} (pB : isProp B) (f : A -> B) (g : B -> A)
  (h : \Pi (x : A) -> g (f x) = x)
  : isProp A
  => \lam x y => sym (h x) *> pmap g (pB (f x) (f y)) *> h y

By this lemma we reduce proving that isProp (x=y) for all x y : Unit to proving that x=y is a retract of \Sigma and using Unit-isProp:

\data Unit | unit

\func Unit-isProp (x y : Unit) : x = y
  | unit, unit => idp

\func Unit-isSet : isSet Unit => \lam x y => retract-isProp {x = y} Unit-isProp
  (\lam _ => unit) (\lam _ => Unit-isProp x y)
  (\lam p => \case \elim x, \elim y, \elim p \with { | unit, _, idp => idp })

Consider another example: the type \Sigma (x : A) (B x) of dependent pairs is a set if A is a set and B x is a set for all x. We need two lemmas to prove this: the first one is the same statement with the word “set” replaced with “proposition”, and the second one is another variant of the retract lemma:

\func Sigma-isProp {A : \Type} (B : A -> \Type)
                    (pA : isProp A) (pB : \Pi (x : A) -> isProp (B x))
  : isProp (\Sigma (x : A) (B x)) => \lam p q => sigmaEq B p q (pA _ _) (pB _ _ _)

\func retract'-isProp {A B : \Type} (pB : isProp B) (g : B -> A)
                      (H : \Pi (x : A) -> \Sigma (y : B) (g y = x))
  : isProp A
  => \lam x y => sym (H x).2 *> pmap g (pB (H x).1 (H y).1) *> (H y).2

We can now prove that dependent pairs of sets is a set as follows:

\func Sigma-isSet {A : \Type} (B : A -> \Type)
                  (pA : isSet A) (pB : \Pi (x : A) -> isSet (B x))
  : isSet (\Sigma (x : A) (B x))
  => \lam t t' => retract'-isProp
      {t = t'}
      {\Sigma (p : t.1 = t'.1) (transport B p t.2 = t'.2)}
      (Sigma-isProp (\lam p => transport B p t.2 = t'.2) (pA _ _) (\lam _ => pB _ _ _))
      (\lam s => sigmaEq B t t' s.1 s.2)
      (\lam p => \case \elim t', \elim p \with { | _, idp => ((idp,idp),idp) })

Exercise 9: Prove that a type with decidable equality is a set. Note that this implies that Nat is a set since we have already proved that Nat has decidable equality.

Exercise 10: Prove that if A and B are sets, then A Or B is also a set.

Exercise 11: Prove that if B x is a set, then \Pi (x : A) -> B x is a set.

Exercise 12: Prove that if A is a set, then List A is a set.

Groupoid structure on types

We conclude with description of a structure that characterizes types of higher homotopy levels. The types of homotopy level 1, or 1-types for short, have structure of what is called a groupoid:

\func isGpd (A : \Type) => \Pi (x y : A) -> isSet (x = y)

A groupoid is a categorical generalization of the notion of a group: it is a category, where every morphism is invertible. In particular, all endomorphisms of any object in a groupoid is a group with composition as the group operation. In the groupoid of a 1-type A the set of morphisms between objects x y : A is given by elements of x=y. The identity morphism is idp and the composition is given by transitivity *> of equality, which turns out to be in this case a nontrivial function rather than mere implication:

\func \infixr 5 *> {A : \Type} {a a' a'' : A} (p : a = a') (q : a' = a'') : a = a''
  \elim q
  | idp => p

For example, the universe \Set of sets is 1-type and *> in this case defines the composition of bijections between sets.

We can prove that *> and idp satisfy the required properties:

-- 'idp' is left and right identity
\func idp-right {A : \Type} {x y : A} (p : x = y) : p *> idp = p => idp

\func idp-left {A : \Type} {x y : A} (p : x = y) : idp *> p = p \elim p
  | idp => idp

-- * is associative
\func *-assoc {A : \Type} {x y z w : A} (p : x = y) (q : y = z) (r : z = w)
  : (p *> q) *> r = p *> (q *> r) \elim r
  | idp => idp

-- 'sym' is inverse 
\func sym-left {A : \Type} {x y : A} (p : x = y) : sym p *> p = idp
  \elim p
  | idp => idp

\func sym-right {A : \Type} {x y : A} (p : x = y) : p *> sym p = idp
  \elim p
  | idp => idp

The function *> is thus similar to a group operation. For example, we can prove the left cancellation property for it:

\func cancelLeft {A : \Type} {x y z : A}
                 (p : x = y) (q r : y = z) (s : p *> q = p *> r) : q = r
  \elim p, r
  | idp, idp => sym (idp-left q) *> s

We can generalize this structure and define inductively n-groupoid as a category, where morphisms form (n-1)-groupoid. This is precisely the structure corresponding to homotopy level n, where n>=-1 is an integer. The types with infinite homotopy level correspond to infinity-groupoids, which are not necessarily merely limits of n-groupoids and should be defined in a special way.

Exercise 13: Prove that n-types are closed under \Pi-types. Hint: Proof by induction. For the induction step ‘suc n’ one should prove that if f,g : \Pi (x : A) -> B x, then f = g is equivalent to \Pi (x : A) -> f x = g x.