Stratified Universes and Univalence

The source code for this module: PartII/HomUniverses.ard
The source code for the exercises: PartII/HomUniversesEx.ard

In this module we introduce additional universes and explain the principles that allow us to prove non-trivial equalities between elements of universes, that is between types.

Firstly, we show that the stratification of types according to their homotopy level is reflected in the structure of universes. Apart from the universe \Type of all types there are more specific universes: the universe \Prop of all propositions, the universe \Set of all sets and more generally the universe \n-Type of all types of homotopy level n.

Secondly, we introduce the univalence axiom saying that equalities between types are precisely the equivalences between them.

The universe \Prop

The universe \Prop consists of all propositions, that is of all types A : \Type satisfying the predicate isProp:

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

This means that there exist functions in both directions between \Prop and the subuniverse \Sigma (A : \Type) (isProp A) of \Type, consisting of all propositions in \Type. We denote the latter universe as PropInType.

By definition \Prop embeds into PropInType. Firstly, \Prop is a subuniverse of \Type, that is P : \Prop implies P : \Type. Secondly, every P : \Prop is a proposition by an axiom Path.inProp P located in Prelude.

The construction of a function in the opposite direction from PropInType to \Prop is also simple, but requires an additional language construct \use \level.

The \use \level construct allows to place a data definition D A_1 … A_n in the universe \Prop as long as there is a proof of \Pi (a_1 : A_1) … (a_n : A_n) -> isProp (D a_1 … a_n). In order to do that one should write a function with corresponding result type in the \where-block of D and with \use \level keywords instead of \func.

\data PropInType-to-Prop (A : \Type) (p : isProp A)
  | inc A
  \where {
    -- Here we prove that 'PropInType-to-Prop' satisfies 'isProp'.
    -- This results in 'PropInType-to-Prop A p : \Prop' for all 'A' and 'p'.
    -- Without '\use \level' 'PropInType-to-Prop A p' would not be in '\Prop'
    --   unless 'A' is in '\Prop'.
    \use \level dataIsProp {A : \Type} {p : isProp A} 
                     (d1 d2 : PropInType-to-Prop A p) : d1 = d2 \elim d1, d2
      | inc a1, inc a2 => pmap inc (p a1 a2)
  }

As we will discuss below, there are universes \Set of all sets and, in general, \n-Type of all types of homotopy level n. The \use \level construct can be used similarly in these cases, see Language Reference for details.

Exercise 1: The type Dec A below is by default placed in \Set0. Place it in \Prop by means of \use \level.

\data Dec (A : \Prop)
  | yes A
  | no (A -> Empty)

The embedding of \Prop into PropInType is inverse to the map PropInType-to-Prop, but we have not yet introduced all the tools necessary to prove that.

The universe \Set

Recall that in the previous module we noted that the equality x=y is not always a proposition and defined sets as those types A, for which equality a=a’ between any two elements a a’ : A is a proposition:

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

There is a universe \Set of all sets. Just as the universe \Type is not a single universe, but a hierarchy of universes \Type n parameterized by the predicative level n, \Set is also a predicative hierarchy \Set n.

The universe \Set n is equivalent to the subuniverse \Sigma (A : \Type n) (isSet A) of \Type n. Denote \Sigma (A : \Type) (isSet A) as SetInType.

Let us construct a function from \Set to SetInType. Such a construction relies on the following property of the universe \Set: for every set A in \Set its equality type lies in the universe \Prop. We can thus use Path.inProp to prove isSet A for sets in \Set:

\func Set-to-SetInType (A : \Set \lp) : \Sigma (A : \Type \lp) (isSet A) =>
       (A, \lam x y => Path.inProp {x = y})

The inverse function can be constructed with the use of \use \level in the similar way as the function PropInType-to-Prop.

Universes \n-Type

Universes \Prop and \Set are particular instances of universes of all types of a given homotopy level. In general, we have a hierarchy \n-Type of universes parameterized by homotopy level n. The homotopy level can be specified as the second argument to \Type (after predicative level) or before Type:

\func bak => \Type 30 66
\func bak' => \66-Type 30
-- With predicative level omitted.
\func bak'' => \66-Type

There are two equivalent ways to refer to the universe of sets: as \Set or as \0-Type. For every predicative level n the universe \Set n is the same as \0-Type n. The universe of propositions, however, can only be referred to as \Prop, it is not allowed to write \(-1)-Type. The universe \Prop is slightly aside since it is impredicative, that is it does not have predicative level.

The universes form a hierarchy according to the following rule: A : \Type n m implies A : \Type (n+1) (m+1). In particular, A : \Prop implies A : \Type n m.

Recall the definition of hasLevel from the previous module:

-- The predicate saying "A has level suc-l - 1"
\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

For any natural number n>0, the equivalence between \(n-1)-Type and the subuniverse \Sigma (A : \Type) (A hasLevel n) can be constructed in the same way as for \Set.

The computation of homotopy levels of types is in many respects similar to the computation of predicative levels. However, there are two important distinctions of homotopy levels. Firstly, the level of \Pi is equal to the level of its codomain: if A : \Type n m and B : A -> \Type n’ m’, then (\Pi (x : A) -> B x) : \Type (\max n n’) m’. Secondly, if A : \(n+1)-Type, then a=a’ : \n-Type for all a a’ : A.

Truncated data, propositional truncation

As we have seen, by means of \use \level a data definition D can be placed in the universe of homotopy level n in case D can be proven to be of homotopy level n. A data definition can be also enforced to be in the universe of a given homotopy level by using the keyword \truncated. In that case the universe of the data definition must, of course, be specified explicitly. For example, the projection of types to propositions, which is called propositional truncation, is a truncated data:

-- Proposition 'Trunc A' says "A is nonempty".
\truncated \data Trunc (A : \Type) : \Prop
  | trunc A

-- Example: 'Trunc Nat'.
\func truncNat : trunc 0 = trunc 1 => Path.inProp (trunc 0) (trunc 1)

-- We can prove the negation of "Empty is nonempty".
\func Trunc-Empty (t : Trunc Empty) : Empty \elim t
  | trunc a => a

Truncating a data has one crucial consequence: any function defined by recursion over a truncated data must have the codomain lying in the universe of the data. For example, the following function does not typecheck:

-- This does not typecheck!
\func ex1 (t : Trunc Nat) : Nat
  | trunc n => n

-- But we can define 'ex2' since 0 = 0 is in \Prop.
\func ex2 (t : Trunc Nat) : 0 = 0
  | trunc n => idp

Elimination principle for Trunc A is restricted to propositions. It says that if B is a proposition and there is a function A -> B, then Trunc A implies B:

\func Trunc-elim {A : \Type} {B : \Prop} (f : A -> B) (a : Trunc A) : B \elim a
  | trunc a => f a
-- The eliminator computes on constructor:
-- Trunc-elim f (trunc a) ===> f a

Exercise 2: Prove that if A : \Prop, then Trunc A is equivalent to A.

Note that we can alternatively define the propositional truncation as a function reflecting this elimination principle. Recall, that in this way we can define, say, Church-style natural numbers:

\func Nat-church => \Pi (X : \Type) -> (X -> X) -> X -> X

\func zero-church : Nat-church => \lam X f x => x
\func one-church : Nat-church => \lam X f x => f x
-- ...

In case of the propositional translation we have the following:

\func Trunc' (A : \Type) : \Prop => \Pi (X : \Prop) -> (A -> X) -> X

\func trunc' {A : \Type} (a : A) : Trunc' A => \lam X f => f a

\func Trunc'-elim {A : \Type} {B : \Prop} (f : A -> B) (a : Trunc' A) : B
  => a B f

In some simple cases there is no need to truncate the data or to use \use \level since the data is placed in the universe automatically. For example, a data is placed in \Prop if it has at most one constructor and types of all the parameters of the constructor are in \Prop:

\data T (b : Bool) \with
   | true => tt

\func T-test (b : Bool) : \Prop => T b

For functions defined by pattern matching the minimal appropriate universe is inferred:

\func T' (b : Bool) : \Type
  | true => \Sigma
  | false => Empty

\func T'-test (b : Bool) : \Prop => T' b

Propositions ∨ and ∃

We are now ready to define propositional operations “or” and “exists”, which were left undefined in the previous module. Types Either and \Sigma, the Curry-Howard “or” and “exists” respectively, are not propositions even if they are applied to propositions, but we can fix it by applying propositional truncation. “or” can be equivalently defined either as a truncation of Either or as a \truncated \data:

\data Either (A B : \Type) | inl A | inr B

\truncated \data \fixr 2 Or (A B : \Type) : \Prop
  | inl A
  | inr B

\func \fixr 2 Or' (A B : \Type) : \Prop => Trunc (Either A B)

It is easy to see that Or satisfies the required properties: A -> A Or B (constructor inl), B -> A Or B (constructor inr) and for any proposition C and all types A, B if A -> C and B -> C, then A Or B -> C. The latter is the recursor for Or:

\func Or-rec {A B C : \Prop} (f : A -> C) (g : B -> C) (p : A `Or` B) : C \elim p
  | inl a => f a
  | inr b => g b

Exercise 3: Prove the following de Morgan’s law:

\func deMorgan (A B C : \Prop) : (\Sigma A (B `Or` C)) <-> ((\Sigma A B) `Or` (\Sigma A C)) => {?}

Exercise 4: Define eliminator for Or via Or-rec not using pattern matching on Or.

Similarly, “exists” is the propositional truncation of \Sigma:

\func exists (A : \Type) (B : A -> \Prop) => Trunc (\Sigma (x : A) (B x))

Note that the predicate “A is nonempty” defined via exists as exists A (\lam _ => Unit) (“there exists a : A such that True is true”) is equivalent to Trunc A.

We can use this definition of “exists”, for example, to give a proper definition of the image of a function:

\func image {A B : \Type} (f : A -> B) => \Sigma (b : B) (Trunc (\Sigma (a : A) (f a = b)))

Note that the definition if the image without truncation is not correct:

\func image' {A B : \Type} (f : A -> B) => \Sigma (b : B) (\Sigma (a : A) (f a = b))

-- image {Nat} {\Sigma} (\lam _ => ()) == \Sigma
-- image' {Nat} {\Sigma} (\lam _ => ()) == Nat

Exercise 5: A type C is called cogenerator if for every sets A and B and all functions f,g : A -> B whenever h o f = h o g holds for all h : B -> C, then f = g. Prove that \Prop is cogenerator.

Equality of types, ‘iso’

Consider the following question: given any type, when are its elements equal? We have already seen, say, that two pairs are equal iff their components are equal, two functions are equal iff they are equal pointwise and so on. By now we can offer such a characterization of equality for almost all the types. The only exception is the type \Type and other universes: we do not have any mechanism to prove structural equalities between types.

Consider several examples of equalities between types:

\func eq1 : Maybe Unit = Bool => {?}
\func eq2 : (\Sigma Nat Nat) = Nat => {?}
\func eq3 : Bool = Nat => {?}

In the first two cases we can prove neither the equalities eq1 and eq2 nor their negations. However, the last equality eq3 can certainly be disproved: Bool = Nat implies that there is a bijection between Bool and Nat, the assertion which is clearly refutable.

Thus we can prove negations of equalities for non-isomorphic types, and yet we can prove no interesting equalities between types. This suggests to fill the gap by making the assertion that two types are equal iff there exists a bijection between them. We will typically use the term “bijection” only for sets and use the term “equivalence” instead while talking about arbitrary types.

\func Equiv (A B : \Type) => \Sigma (f : A -> B)
                                    (g : B -> A)
                                    (\Pi (x : A) -> g (f x) = x)
                                    (\Pi (y : B) -> f (g y) = y)

We can easily prove that if two types are equal, then they are equivalent:

\func equality=>equivalence (A B : \Type) (p : A = B) : Equiv A B =>
  transport (Equiv A) p (\lam x => x, \lam x => x, \lam x => idp, \lam x => idp)

The function iso postulated in Prelude says that the converse is also true:

\func equivalence=>equality (A B : \Type) (e : Equiv A B) : A = B =>
  path (iso e.1 e.2 e.3 e.4)

Note that if f : A -> B is equivalence, then we can define the function f’ : A -> B using iso and coe:

\let f' : A -> B => \lam a => coe (iso f g p q) a right

We have the rule coe (iso f g p q) a right ==> f a, which implies that f’ is the same function as f. Therefore the following equality holds by reflexivity:

\func test (A B : \Type) (e : Equiv A B)
  : transport (\lam X => X) (equivalence=>equality A B e) = e.1
  => idp

The property equivalence=>equality does not still fully characterize equalities between types: the type A = B should be equivalent to the type Equiv A B. The computational rule for iso mentioned above allows to prove that the composition of equivalence=>equality and equality=>equivalence equals the identity on Equiv A B. It is also possible to prove, although a bit less straightforwardly, that the opposite composition of the maps gives the identity on A = B. This principle is called the univalence axiom or just univalence. We simply assume it as an axiom, although it is possible to prove it:

\func UA (A B : \Set) : Equiv (A = B) (Equiv A B) => (equality=>equivalence A B, equivalence=>equality A B, LRL A B, RLR A B)
  \where {
    \func LRL (A B : \Set) (p : A = B) : equivalence=>equality A B (equality=>equivalence A B p) = p => {?}
    \func RLR (A B : \Set) (e : Equiv A B) : equality=>equivalence A B (equivalence=>equality A B e) = e => {?}
  }

An example of application of univalence

Let P : (A -> B) -> \Type be a predicate on functions. Assume f g : A -> B are two functions, which are equal pointwise. Because of function extensionality we know that such functions are equal and therefore whenever if we prove P f we will obtain also a proof of P g for free.

Because of the univalence the analogous property holds for types: if we prove that a proposition holds for some type, we will automatically get proofs of this proposition for all equivalent types. For example, we know that equality of Nat is decidable. By univalence we immediately conclude that all countable sets are also decidable.

\data Dec (E : \Type)
  | yes E
  | no (Not E)

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

-- We proved this earlier.
\func NatDecEq : DecEq Nat => {?} 

\func isCountable (X : \Type) => Equiv Nat X

\func countableDecEq (X : \Type) (p : isCountable X) : DecEq X =>
  transport DecEq (equivalence=>equality Nat X p) NatDecEq

In this particular case there exist alternative proofs without univalence, however any such proof is much more complex. There are also examples of properties of types, which are provable for a type A, but not provable without univalence for some B equivalent to A.

Implications of univalence for \Prop and \Set

One of the consequences of univalence is extensionality for propositions: whenever two propositions A and B are logically equivalent (A -> B and B -> A) they are equal.

\func propExt {A B : \Prop} (f : A -> B) (g : B -> A) : A = B =>
  equivalence=>equality A B (f, g, \lam x => Path.inProp _ _, \lam y => Path.inProp _ _)

Another consequence of univalence is that the universe \Prop is a set.

Exercise 6: Prove that \Prop is a set.

Quite expectedly, \Set is not a set, but a 1-type. The universe \Set is provably not a set only in presence of univalence.

Let us show how to prove that \Set is not a set using univalence. Recall that univalence says that equalities between two sets are precisely bijections between them. Thus the claim would follow if we prove that there exists a set with two different automorphisms. The simplest example is the set Bool and the automorphisms id and not:

\func not-not (b : Bool) : not (not b) = b
  | true => idp
  | false => idp

\func true/=false (p : true = false) : Empty => absurd (transport T p ())

\func Set-isNotSet (p : isSet \Set) : Empty =>
  \let 
  -- We first prove equality between 'idp' and 
  -- the equality, corresponding to 'not'.
       | idp=not => 
          p Bool Bool
          idp -- : Bool = Bool
          (equivalence=>equality Bool Bool (not, not, not-not, not-not)) -- : Bool = Bool
  -- Now we can prove the equality between the two bijections 
  -- corresponding to 'idp' and 'not', that is that 'id'
  -- equals 'not'.
       | id=not : (\lam x => x) = not => pmap (transport (\lam X => X)) idp=not
  -- The contradiction follows easily.
  \in true/=false (pmap (\lam f => f true) id=not)

Exercise 7: Prove that (Bool = Bool) = Bool.

Exercise 8: Prove that (n+m)-element set is a disjoint union of n- and m-element sets.

Exercise 9: We say that a type X is injective if for any function f : A -> X and any injection i : A -> B there exists a function l : B -> X such that l o i = f. Prove that \Prop is injective.