Equality

The source code for this module: PartI/Equality.ard
The source code for the exercises: PartI/EqualityEx.ard

In the previous modules we treated the identity type = in a rather hand-wavy manner as in most of the cases we needed just reflexivity idp {A : \Type} {a : A} : a = a. Here we will get into details of the definition of the identity type and explain some key aspects of it, which will be important for writing more advanced proofs. Along the way we introduce the interval type I, whose properties are essentially determined by the function coe, playing the role of eliminator for I. In order to clarify this we briefly recall the general concept of eliminator.

Symmetry, transitivity, Leibniz principle

First of all, we show that the identity type satisfies some basic properties of equality: it is an equivalence relation and it satisfies the Leibniz principle.

The Leibniz principle says that if a and a’ satisfy the same properties, then they are equal. It can be easily proven that = satisfies this principle:

\func Leibniz {A : \Type} {a a' : A}
  (f : \Pi (P : A -> \Type) -> \Sigma (P a -> P a') (P a' -> P a)) : a = a'
  => (f (\lam x => a = x)).1 idp

The inverse Leibniz principle (which we will call merely Leibniz principle as well) says that if a = a’, then a and a’ satisfy the same properties, that is if P a is true, then P a’ is true. The proof of this is easy, but requires some constructs that will be introduced very shortly further in this module:

\func transport {A : \Type} (B : A -> \Type) {a a' : A} (p : a = a') (b : B a) : B a'
    => coe (\lam i => B (p @ i)) b right

Using this latter Leibniz principle, it is easy to prove that = satisfies (almost) all the properties of equality. For example, the following properties:

-- symmetry
\func inv {A : \Type} {a a' : A} (p : a = a') : a' = a
    => transport (\lam x => x = a) p idp

-- transitivity
\func trans {A : \Type} {a a' a'' : A} (p : a = a') (q : a' = a'') : a = a''
    => transport (\lam x => a = x) q p

-- congruence
\func pmap {A B : \Type} (f : A -> B) {a a' : A} (p : a = a') : f a = f a'
    => transport (\lam x => f a = f x) p idp

Exercise 1: Define congruence for functions with two arguments via transport. It is allowed to use any functions defined via transport.

Exercise 2: Prove that transport can be defined via pmap and repl and vice versa. The function repl says that if two types are equal then there exists a function between them.

Definition of =

The central ingredient of the definition of the identity type is the interval type I contained in Prelude. The type I looks like a two-element data type with constructors left and right, but actually it is not: these constructors are made equal (by means of coe). Of course, pattern matching on I is prohibited since it can be used to derive Empty = Unit.

The equality left = right implies that some a : A and a’ : A are equal if and only if there exists a function f : I -> A such that f left ==> a and f right ==> a’ (where ==> denotes computational equality). The type a = {A} a’ is defined simply as the type of all functions f : I -> A satisfying this property. The constructor path (f : I -> A) : f left = f right allows to construct equality proofs out of such functions and the function @ (p : a = a’) (i : I) : A does the inverse operation:

path f @ i ==> f i -- beta-equivalence
path (\lam i => p @ i) ==> p -- eta-equivalence

In order to prove reflexivity idp we can simply take the constant function \lam _ => a : I -> A:

\func idp {A : \Type} {a : A} : a = a => path (\lam _ => a)

Exercise 3: Prove that left = right without using transport or coe.

If f : A -> B and g : I -> A, then g determines a proof of the equality g left = g right and the congruence pmap can be interpreted as simply the composition of f and g. This observation suggests an alternative definition of pmap:

\func pmap {A B : \Type} (f : A -> B) {a a' : A} (p : a = a') : f a = f a'
    => path (\lam i => f (p @ i))

This definition of pmap behaves better than others with respect to computational properties. For example, pmap id is computationally the same as id and pmap (f . g) is computationally the same as pmap f . pmap g, where (.) is the composition:

\func pmap-idp {A : \Type} {a a' : A} (p : a = a') : pmap {A} (\lam x => x) p = p
    => idp

Exercise 4: Prove that a = {A} a’ and b = {B} b’ implies (a,b) = {\Sigma A B} (a’,b’) without using transport.

Exercise 5: Prove that p = {\Sigma (x : A) (B x)} p’ implies p.1 = {A} p’.1 without using transport.

Functional extensionality

Function extensionality is a principle saying that if two functions f and g are equal pointwise, then they are equal functions. Our definition of equality allows us to prove this principle very easily:

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

This useful principle is unprovable in many other intensional dependently typed theories. In such theories function extensionality can be introduced as an axiom, that is as a function without implementation, however adding new axioms worsens computational properties of the theory. For example, if we add the axiom of excluded middle lem, then we can define a constant ugly_num : Nat that does not evaluate to any concrete natural number:

\func lem : \Pi (X : \Type) -> Either X (X -> Empty) => {?}
\func ugly_num : Nat => \case lem Nat \with { | Left => 0 | Right => 1 }

Exercise 6: Prove that (\lam x => not (not x)) = (\lam x => x).

Eliminators

Elimination principles for a data type D specify what kind of data should be provided in order to define a function from D to a non-dependent or dependent type. And, essentially, these principles say that it is enough to show how “generators” (that is constructors) of D are mapped to a type A and that that would uniquely determine a function D -> A. For example, eliminators for Nat and Bool:

-- Dependent eliminator for Nat (induction).
\func Nat-elim (P : Nat -> \Type)
               (z : P zero)
               (s : \Pi (n : Nat) -> P n -> P (suc n))
               (x : Nat) : P x \elim x
  | zero => z
  | suc n => s n (Nat-elim P z s n)

-- Non-dependent eliminator for Nat (recursion).
\func Nat-rec (P : \Type)
              (z : P)
              (s : Nat -> P -> P)
              (x : Nat) : P \elim x
  | zero => z
  | suc n => s n (Nat-rec P z s n)

-- Dependent eliminator for Bool (recursor for Bool is just 'if').
\func Bool-elim (P : Bool -> \Type)
                (t : P true)
                (f : P false)
                (x : Bool) : P x \elim x
  | true => t
  | false => f

Exercise 7: Define factorial via Nat-rec (i.e., without recursion and pattern matching).

Exercise 8: Prove associativity of Nat.+ via Nat-elim (i.e., without recursion and pattern matching).

Exercise 9: Define recursor and eliminator for \data D | con1 Nat | con2 D D | con3 (Nat -> D).

Exercise 10: Define recursor and eliminator for List.

The function coe thus defines dependent eliminator for I, it says that in order to define f : \Pi (i : I) -> P i for some P : I -> \Type it is enough to specify f left:

\func coe (P : I -> \Type)
          (a : P left)
          (i : I) : P i \elim i
  | left => a

Exercise 11: We defined transport via coe. It is possible to define a special case of coe via transport. Define coe0 (A : I -> \Type) (a : A left) : A right via transport. Is it possible to define transport via coe0?

Exercise 12: Define a function B right -> B left.

left = right

With the use of the function coe, we now prove that I has one element:

\func left=i (i : I) : left = i
  -- | left => idp
  => coe (\lam i => left = i) idp i

-- In particular left = right.
\func left=right : left = right => left=i right

coe and transport

Functions coe and transport are closely related. Recall the definition of transport given earlier in this module:

\func transport {A : \Type} (B : A -> \Type) {a a' : A} (p : a = a') (b : B a) : B a'
     => coe (\lam i => B (p @ i)) b right

Denote \lam i => B (p @ i) as B’. Then B’ : I -> \Type, B’ left ==> B a, B’ right ==> B a’ and \lam x => coe B’ x right : B’ left -> B’ right.

Proofs of non-equalities

In order to prove that true is not equal to false it is enough to define a function T : Bool -> \Type such that T true is the unit type and T false is the empty type. Then the contradiction can be easily derived from true = false by means of transport:

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

Note that it is not possible to prove that left is not equal to right since such T cannot be defined neither recursively nor inductively:

-- This function does not typecheck!
\func TI (b : I)
  | left => \Sigma
  | right => Empty

Exercise 13: Prove that 0 does not equal to suc x.

Exercise 14: Prove that fac does not equal to suc.