A short proof that lists form a set

ListHLevels.lagda.md

A short, self-contained proof that List A has UIP if A has UIP

First, we enable the --without-K flag, which removes UIP as an axiom. We also import Agda.Primitive, which gives us access to the Level type, though this isn't strictly required. We also add a variable block so we don't need to constantly abstract over types and levels.

{-# OPTIONS --without-K --safe #-}
module ListHLevels where

open import Agda.Primitive

private variable
  ℓ : Level
  A B C : Set ℓ

Before we get to the proof, we need to define the equality type. This is all standard.

data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x

infix 4 _≡_

cong : ∀ {a a'} → (f : A → B) → a ≡ a' → f a ≡ f a'
cong f refl = refl

cong₂ : ∀ {a a' b b'} → (f : A → B → C) → a ≡ a' → b ≡ b' → f a b ≡ f a' b'
cong₂ f refl refl = refl

sym : ∀ {x y : A} → x ≡ y → y ≡ x
sym refl = refl

_∙_ : ∀ {x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl ∙ refl = refl

infixr 5 _∙_

Propositions

We say a type A is a proposition if all of it's elements can be identified.

is-prop : ∀ {ℓ} → Set ℓ → Set ℓ
is-prop A = ∀ (x y : A) → x ≡ y

Furthermore, we say a type has UIP if it's identity type is a proposition for all elements. Explicitly, this means that for all x y : A and all p q : x ≡ y, we have p ≡ q.¹

has-uip : ∀ {ℓ} → Set ℓ → Set ℓ
has-uip A = ∀ (x y : A) → is-prop (x ≡ y)

Now, for our crucial lemma: is-prop is closed under retractions.

retract→is-prop
  : (f : A → B) → (g : B → A)
  → (∀ x → f (g x) ≡ x)
  → is-prop A
  → is-prop B
retract→is-prop f g retract A-prop x y =
  sym (retract x) ∙ cong f (A-prop (g x) (g y)) ∙ retract y

Lists and Pointwise Equality

Next, we define lists, and pointwise equality of lists.

data List {ℓ} (A : Set ℓ) : Set ℓ where
  [] : List A
  _∷_ : A → List A → List A

data Pointwise {ℓ} {A : Set ℓ} : List A → List A → Set ℓ where
  [] : Pointwise [] []
  _∷_ : ∀ {x y xs ys} → x ≡ y → Pointwise xs ys → Pointwise (x ∷ xs) (y ∷ ys)

We can show that pointwise equality is a proposition when A has UIP by a straightforward induction.

Pointwise-is-prop : ∀ {xs ys : List A} → has-uip A → is-prop (Pointwise xs ys)
Pointwise-is-prop A-uip [] [] = refl
Pointwise-is-prop A-uip (p ∷ ps) (q ∷ qs) =
  cong₂ _∷_ (A-uip _ _ p q) (Pointwise-is-prop A-uip ps qs)

Pointwise Equality and Equality

Given xs ≡ ys, we can deduce that xs and ys are equal pointwise.

encode : ∀ {xs ys : List A} → xs ≡ ys → Pointwise xs ys
encode {xs = []} {ys = []} p = []
encode {xs = x ∷ xs} {ys = .x ∷ .xs} refl = refl ∷ (encode refl)

Likewise, if xs and ys are pointwise equal, then they are equal.

decode : ∀ {xs ys : List A} → Pointwise xs ys → xs ≡ ys
decode [] = refl
decode {xs = x ∷ xs} {ys = .x ∷ ys} (refl ∷ ps) = cong (x ∷_) (decode ps)

Crucially, decode and encode form a retraction.

decode-encode : ∀ {xs ys : List A} (p : xs ≡ ys) → decode (encode p) ≡ p
decode-encode {xs = []} {ys = []} refl = refl
decode-encode {xs = x ∷ xs} {ys = .x ∷ .xs} refl =
  cong (cong (x ∷_)) (decode-encode refl)

The final result

Time to put all the pieces together! If A has UIP, then pointwise equality is a prop. Furthermore, decode and encode form a retraction, so the equality type for List A must also be a proposition. However, this is the definition of has-uip, so we are done!

has-uip→List-has-uip : has-uip A → has-uip (List A)
has-uip→List-has-uip A-set xs ys =
  retract→is-prop decode encode decode-encode (Pointwise-is-prop A-set)

Footnotes

1. In HoTT we would call this property is-set, though this is somewhat confusing, as Agda calls types Set. If this were a serious development of HoTT we would change this, but this proof is meant to be short 🙂. More generally, we should also be talking about h-levels here, but again, brevity takes precedence! ↩