Exploring equality via homotopy and proof assistants - Day 3 - Inductive types and their equalities

This file contains the exercises for Day 3. Some are explicitly marked as "Homework"; the rest can be done either in class or for homework. If the Macs in the computer lab do not have CoqIDE installed, you can go to https://coq.inria.fr/coq-85, download CoqIDE_8.5beta2.dmg, open it, and run CoqIDE directly, without installing it. When doing exercises on your own, feel free to skip around; there are some interesting puzzles near the bottom. If you feel like you know exactly how a proof will go, but find it painful and tedious to write out the proof terms explicitly, come find me. Coq has a lot of support for automation and taking care of things that are easy and verbose, so you don't have to. Proving should feel like a game. If it doesn't, I can probably help you with that. The following are placeholders; admit indicates that something should be filled in later.

Compatibility between Coq 8.5 and 8.4

Guiding Puzzles

There are three guiding questions for today: 1. What are (inductive) types? 2. What does it mean to say that two inhabitants of a given type are equal? 3. Where is equality under-specified, and how can we extend the patterns we see to fill in these areas?

Puzzle 1: contractibility of based path spaces

We use the notation { x : T | P x } to denote the type of pairs (x; p) which consist of an inhabitant x : T and a proof p : P x.

A type is called contractible if there is a (continuous!) function showing that all inhabitants are equal to a particular one.

Puzzle: The following theorem is provable. Prove it.

Note that x = y :> T means x : T, y : T, and x = y. It is the notation for @eq T x y. It is how we write x =_T y in Coq. Since equals are inter-substitutable, we should be able to prove:

But it turns out that we can't prove this. Why not? Give both a formal, type theoretic reason (what terms don't typecheck?), and a topological reason.

Puzzle 2: understanding the encode-decode method

Here is a concrete puzzle for the second question: To classify the equality of a given type, we give a "code" for each pair of elements. We must say how to "encode" equality proofs, and how to "decode" codes into equality proofs. We want this to be an isomorphism, i.e., encode ∘ decode and decode ∘ encode should both be the identity function. It turns out that we don't need to know anything about encode or decode other than their existance to ensure this; we can always adjust decode to create an inverse to encode, as long as a particular property holds of code. What is that property? More concretely, the puzzle is to fill in the following holes.

We assume we are given a type, a code, an encode, and a decode. We introduce the assumptions as we get to definitions that should need them.

For this last one, we'll need the correctness property on codes.

The following sanity check on the classification should be provable:

x = y should be a valid code

If you didn't choose a silly correctness property like code = (fun x y ⇒ x = y), then your proof should generalize to the following: Suppose we are given a valid encoding.

Then it should satisfy your validity principle.

Puzzle 3

Classify the equalities of types. That is, fill in the following:

The following are unprovable in Coq, currently. They are collectively known as the "univalence axiom".

This was all very abstract. Let's drill down with some exmples.

Inductive Types

First, we must understand the types which we are classifying the path-spaces of. An inductive type is specified by introduction and elimination rules; introduction rules tell you how to create inhabitants (elements) of a type, and elimination rules tell you how to use such inhabitants. Coq generate eliminations rules automatically, but we will try to come up with the first few without peeking.

Coq has special syntax for nat, so we don't overwrite it. Inductive nat' : Type := ... Inductive Empty_set : Type := ... Anecdote: Proving unit → Empty_set (i.e., True → False) by recursion on unit, if we assume that True = (False → False) Any that we don't do in class are homework

A notational helper.

Inductive prod (A B : Type) : Type := ... Some notational helpers

Arguments pair {A B} _ _.

Add Printing Let prod.

Notation "x * y" := (prod x y) : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.

Example prod_1 := (1, 1) : nat * nat.
Example prod_2 := (1, 2) : nat * nat.
Example prod_3 := (true, true) : bool * bool.
Example prod_4 := (1, true) : nat * bool.

(** We use curlie braces so that we don't have to pass the arguments explicitly all the time. 

sum A B, written A + B, is the disjoint sum of A and B Inductive sum (A B : Type) : Type := ... Notational helpers

Notation "x + y" := (sum x y) : type_scope.

Arguments inl {A B} _ , [A] B _.
Arguments inr {A B} _ , A [B] _.

Inductive sigT A (B : A -> Type) : Type := ... Notational helpers

Arguments sigT {A} B.
Arguments existT {A} B _ _.
Notation "{ a : A  & B }" := (sigT (A:=A) (fun a => B)) : type_scope.

The projections

Definition projT1
: forall {A B}, { a : A | B a } -> A
  := admit.

Definition projT2
: forall {A B} (x : { a : A | B a}), B (projT1 x)
  := admit.

Notational helpers for the projections

Inductive option (A : Type) : Type := ... Inductive list (A : Type) : Type := ... Function types also have intro and elim rules, though they don't have syntactic forms. Can you describe them? Note well: J is the eliminator for the equality type.

Provable equalities

What equalities of types are provable?

Provable inequalities

What equalities of types are provably absurd? More generally, when are two types provably different?

Isomorphisms

We can define a notion of isomorphism:

Let us use an object of type Isomorphic as a function:

Tell Coq that the function associated to an Isomorphic object is always an isomorphism.

We can prove the standard properties about isomorphisms:

We would like to prove the last corresponding law:

But it's not provable! Here's a counter-example: Recall the taboo from earlier; we can't prove equality of two identical types defined separately. But if we could prove Isomorphic_ap, then we could prove this!

Ooops! We'll be coming back to this soon. More practice: You can prove the higher groupoid laws about isomorphisms, but it's a bit of a pain. Before dealing with the taboo above, let's classify the equality space of isomorphisms.

Equality classification

We can classify the equality types. For each type, we come up with a simpler type that represents ("codes for") its equality type. Then we prove that this type is isomorphic to the given equality type. The exercises here are all to help understand how the encode-decode method works, to build up to function extensionality and univalence, and, for sigma types, to solve the first puzzle. We'll do them as needed to explain the method; the rest are (optional) homework. There are more exercises at the bottom of the file.

unit

We use curlie braces to not have to pass the x and y around all the time.

bool

Empty_set

arrow types

The rest aren't currently provable in Coq; it's the axiom of functional extensionality.

Pi types (dependent function types)

The rest aren't currently provable in Coq; it's the axiom of functional extensionality.

sigma (dependent pairs)

Homework

Back to isomorphisms.

Ooops. Turns out this isn't provable. Challenge: Figure out why.

Equivalences

We can define a slight variation on isomorphisms, called "contractible fibers", which generalizes the notion of injective+surjective. If you're interested in the various ways of formulating equivalences, Chapter 4 of the HoTT Book (http://homotopytypetheory.org/book/) is an excellent resource.

Let us use an object of type Equiv as a function:

Tell Coq that the function associated to an Equiv object is always an equivalence.

We can prove that an equivalence gives us an isomorphism very easily.

We can go the other way with more work. Optional Homework: Complete this proof.

Now, we prove the following helper lemma, which lets us get the right codes for Equiv. We again assume functional extensionality.

Now that we have a "good" type of isomorphism/equivalence (one with the right equality type), we can go back to the question of Isomorphic_ap; Recall that we want to prove:

Definition Isomorphic_ap : forall (f : Type -> Type) {A B}, A ≅ B -> f A ≅ f B.

We can prove this by axiomatizing the codes for types:

The following are unprovable in Coq, currently. They are collectively known as the "univalence axiom".

Homework: Playing with univalence

Using univalence, we can prove some things.

Challenge: Show, without axioms, that univalence implies functional extensionality:

Exercise 2.17 from the HoTT Book (http://homotopytypetheory.org/book/ - don't worry about reading the book): Show that if A ≃ A' and B ≃ B', then (A × B) ≃ (A' × B') in two ways: once using univalence, and once without assuming it.

Now prove that these two ways are equal

prod

sum

nat

Warmup:

Hint for the above: Use J.

option

list

Homework: mere propositions

Homework; challenging problem Recall the definition of contractibility above. The reason that we can safely call this contractible is that all of the higher structure collapses. That is, if all inhabitants of A are (continuously) equal, then all inhabitants of x = y for x : A and y : A are also equal. Prove this, as follows. First we define what it means for a type to be a "mere proposition", or to satisfy the uniqueness of identity proofs.

We classify the equality type of propositions.

If you find this proof hard, and can't figure out why, think about the proof of dec_deencode. If you're still having trouble, look a bit further down for a hint.

Hint: you may need to rewrite your prop_decode function. The following lemmas may prove helpful. Try to write an "adjuster" for is_prop that will always return something equal to refl (provably) when handed two judgmentally equal things.

Now move these lemmas above prop_decode and try re-writing the codes so that you expect prop_deencode to work.

decidable types

Homework; challenging problem More generally, we can do this for any type with decidable equality. First we define what it means for a type to have decidable equality: it means that we have a (continuous!) function from pairs of inhabitants to proofs that either they are equal, or that their equality is absurd.

If you find this proof hard, and can't figure out why, look a bit further down for a hint.

Hint: you may need to rewrite your dec_decode, dec_code, and dec_encode functions, just as you did with prop_decode. The following lemmas may prove helpful. Try to write an "adjuster" for decidable equality that will always return something equal to refl (provably) when handed two equal things.

Now move these lemmas above dec_code and try re-writing the codes so that you expect dec_deencode to work.

Pushing Further

Homework: Generalize the above two proofs to solve "Puzzle 2" far above. (Don't forget to also do puzzle 1 while you're at it.) Homework: Using the solution to Puzzle 2, show that it is sufficient to assume function_decode an axiom; the endecode and deencode proofs follow from puzzle 2.