In this lab, we are going to define the basic functions for working with identity types. The names for the functions have been chosen so that we are mostly compatible with the cubical Agda library, even though we are not using it for now. You should work in the same directory as for previous lab. In particular, it should contain the Prelude.agda file. The labs will be following each other starting from now: it is important for you to work regularly! Many of the functions have similar proofs, so that the proofs are not always fascinating, but the functions will still turn out to be very useful in the following.

0.1 Prelude

TODO: read Prelude……………..

1 Prelude

Create a file Path.agda. Start your file with

{-# OPTIONS --without-K #-}

which indicates that we want to use the variant of the pattern matching algorithm which does not enforce uniqueness of identity proofs (more details here). Then write

open import Prelude

in order to import all the functions from the Prelude module. Finally, write

private variable
  ℓ ℓ' ℓ'' : Level

In order to have Agda automatically, generate implicit arguments for universe level variables ℓ (typed \ell).

2 The ∞-groupoid structure of types

2.1 Symmetry

Show that equality is symmetric by defining a function

sym : {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x

In the course, we sometimes write \(p^-\) for sym p.

2.2 J

Define the eliminator

J : {A : Type ℓ} {x : A} (P : (y : A) → x ≡ y → Type ℓ') → P x refl → {y : A} (p : x ≡ y) → P y p

Use it in order to define again symmetry (without using pattern matching)

sym' : {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x

2.3 Transitivity

Show that equality is transitive

trans : {A : Type ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z

We can then define the usual notation for path composition as

infixr 30 _∙_
_∙_ = trans

where the point “∙” is typed \..

2.4 Left unitality

Show that path composition admits refl as neutral element on the left

lUnit : {A : Type ℓ} {x y : A} (p : x ≡ y) → p ≡ refl ∙ p

2.5 Right unitality

Show that path composition admits refl as neutral element on the right

rUnit : {A : Type ℓ} {x y : A} (p : x ≡ y) → p ≡ p ∙ refl

2.6 Cancelativity

Show that path composition is cancelative on the left

lCancel : {A : Type ℓ} {x y : A} (p : x ≡ y) → sym p ∙ p ≡ refl

and on the right

rCancel : {A : Type ℓ} {x y : A} (p : x ≡ y) → p ∙ sym p ≡ refl

2.7 Associativity

Show that path composition is associative

assoc : {A : Type ℓ} {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r

2.8 Symmetry is involutive

Show that symmetry

symInvo : {A : Type ℓ} {x y : A} (p : x ≡ y) → p ≡ sym (sym p)

3 Functoriality

3.1 Congruence

Show that equality is a congruence / that all functions are functorial, by proving

cong : {A : Type ℓ} {B : Type ℓ'} (f : A → B) {x y : A} (p : x ≡ y) → f x ≡ f y

Note that cong is noted ap in the course.

3.2 Path components

Show that we can extract the components of a path:

≡× : {A : Type ℓ} {B : Type ℓ'} {x x' : A} {y y' : B} → (x , y) ≡ (x' , y') → (x ≡ x') × (y ≡ y')

You are not allowed to perform pattern matching in the above definition.

3.3 Constant application

Show that applying a constant function to a path gives refl:

congConst : {A : Type ℓ} {B : Type ℓ'} {x' : B} {x y : A} (p : x ≡ y) → cong (λ _ → x') p ≡ refl

3.4 More properties

Define the following functions

• congComposite: applying a function to a composite of paths is the composite of their application
• congSym: applying a function to the symmetric of a path is the symmetric of the application
• congId: applying the identity (id) to a path leaves the path unchanged
• cong∘: applying the composite of two functions to a paths amounts to successively apply the two functions
• cong₂: we can apply a function taking two arguments to two paths simultaneously

Above, “∘” is typed \circ and “₂” is typed \_2.

3.5 A small lemma

Using the previous functions, show the following lemma

rotate∙≡ : {A : Type ℓ} {x y y' : A} (p : x ≡ y) (q : y ≡ y') (p' : x ≡ y') → p ∙ q ≡ p' → sym p ∙ p' ≡ q

We advise you to use the notation for equational reasoning and begin with

rotate∙≡ p q p' α =
  sym p ∙ p' ≡⟨ ? ⟩
  q ∎

You can then insert lines of the form

  ? ≡⟨ ? ⟩

in the middle in order to add intermediate steps.

4 Transport

4.1 Substitutivity

Define a function

subst : {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → B x → B y

which shows that equality is substitutive. This function is called transport in the course.

4.2 True is not false

Show that true is not false:

true≢false : ¬ true ≡ false

Change your proof in order to use subst instead of pattern matching.

4.3 Transport

Define a function

transport : {A B : Type ℓ} → A ≡ B → A → B

which corresponds to coe in the course. If you used pattern matching, modify your definition in order not to.

4.4 Substitutivity from transport

Above, you have defined transport from subst. Show that we could do the converse by defining

subst' : {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → B x → B y

without using pattern matching.

4.5 Properties of transport

Show that

• transporting along composite paths corresponds to successively substituting

  substComposite : {A : Type ℓ} (B : A → Type ℓ) {x y z : A} (p : x ≡ y) (q : y ≡ z) (x' : B x) → subst B (p ∙ q) x' ≡ subst B q (subst B p x')

• transporting a path along its right end amounts to composition

  substInPathsL : {A : Type ℓ} {x y y' : A} (p : x ≡ y) (q : y ≡ y') → subst (λ y → x ≡ y) q p ≡ p ∙ q

• transporting a path along its left end amounts to reverse composition

  substInPathsR : {A : Type ℓ} {x x' y : A} (p : x ≡ x') (q : x ≡ y) → subst (λ x → x ≡ y) p q ≡ sym p ∙ q

• the following generalization of the two previous lemmas

  substInPaths : {A : Type ℓ} {B : Type ℓ'}  {x y : A} (f g : A → B) (p : x ≡ y) (q : f x ≡ g x) → subst (λ x → f x ≡ g x) p q ≡ sym (cong f p) ∙ q ∙ cong g p

5 Paths over

Define the type of paths in a type family over another path as

PathOver : {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) (x' : B x) (y' : B y) → Type ℓ'
PathOver B p x' y' = subst B p x' ≡ y'

5.1 Paths in products

Show that we can construct paths in a product type as a pair of paths:

×≡ : {A : Type ℓ} {B : Type ℓ'} {x x' : A} {y y' : B} → (p : x ≡ x') (q : y ≡ y') → (x , y) ≡ (x' , y')

Generalize the previous definition to dependent sums:

Σ≡ : {A : Type ℓ} {B : A → Type ℓ'} {x x' : A} (p : x ≡ x') {y : B x} {y' : B x'} → PathOver B p y y' → (x , y) ≡ (x' , y')

5.2 Dependent application

Define the following generalization of application of cong

congP : {A : Type ℓ} (B : A → Type ℓ') (f : (x : A) → B x) {x y : A} (p : x ≡ y) → PathOver B p (f x) (f y)

This function is called apd in the course.

5.3 Transporting functions

Show the following results about the transport of functions:

• transporting the target of a function:

  funTypeTranspR : {A : Type ℓ} {B B' : Type ℓ'} (p : B ≡ B') (f : A → B) → subst (λ X → A → X) p f ≡ transport p ∘ f

• transporting the source of a function:

  funTypeTranspL : {A A' : Type ℓ} {B : Type ℓ'} (p : A ≡ A') (f : A → B) → subst (λ X → X → B) p f ≡ f ∘ transport (sym p)

• transporting both the source and target of a function:

  funTypeTransp : {A : Type ℓ} (B : A → Type ℓ') (C : A → Type ℓ'') {x y : A} (p : x ≡ y) (f : B x → C x) → PathOver (λ x → B x → C x) p f (subst C p ∘ f ∘ subst B (sym p))

6 Uniqueness of identity proofs

The goal here is to show the equivalence between the various formulations of uniqueness of identity proofs.

6.1 Logical principles

Define the following logical principles:

• uniqueness of identity proofs:

  UIP : Type₁
  UIP = {A : Type} {x y : A} (p q : x ≡ y) → p ≡ q

• uniqueness of reflexivity proofs:

  URP : Type₁
  URP = {A : Set} {x : A} (p : x ≡ x) → p ≡ refl

• Streicher’s axiom K

  K : Type₁
  K = {A : Type} {x : A} (P : (x ≡ x) → Set) → P refl → (p : x ≡ x) → P p

6.2 Equivalence

Show that they are logically equivalent by proving the following implications

UIP→URP : UIP → URP

URP→UIP : URP → UIP

URP→K : URP → K

K→URP : K → URP

7 Optional: Leibniz equality

7.1 Leibniz equality

Define Leibniz equality as

_==_ : {ℓ : Level} {A : Type ℓ} → A → A → Type _
_==_ {ℓ} {A} x y = (P : A → Type ℓ) → P x → P y

7.2 Properties

Show that Leibniz equality is reflexive

Lrefl : {A : Type ℓ} {x : A} → x == x

symmetric

Lsym : {A : Type ℓ} {x y : A} → x == y → y == x

and transitive

Ltrans : {A : Type ℓ} {x y z : A} → x == y → y == z → x == z

7.3 Logical equivalence with identity types

Show that we can convert Leibniz equalities to identity types

Lto≡ : {A : Type ℓ} {x y : A} → x == y → x ≡ y

and the converse

≡toL : {A : Type ℓ} {x y : A} → x ≡ y → x == y

Show that those functions form a section retraction pair:

≡to≡ : {A : Type ℓ} {x y : A} (p : x ≡ y) → Lto≡ (≡toL p) ≡ p

8 Optional: Eckmann-Hilton

Show the Eckmann-Hilton property: composition is commutative for paths between refl.

EH : {A : Type ℓ} {x : A} (α β : refl {x = x} ≡ refl) → α ∙ β ≡ β ∙ α

The general idea is to show the following sequence of equalities:

This requires intermediate lemmas, and you might want to have a look at Theorem 2.1.6 in the HoTT book.