{-# OPTIONS --cubical --guardedness #-}
module Padova2025.Cubical.FirstSteps where

First steps#

open import Cubical.Foundations.Prelude
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Termination.Gas using (𝟙; tt)

Proper introduction. Split off menagerie of types.

Unordered pairs#

data UnorderedPair (A : Set) : Set where
  pair : (x y : A) → UnorderedPair A
  swap : (x y : A) → pair x y ≡ pair y x

Generalities on equality#

refl' : {X : Set} {a : X} → a ≡ a
refl' {a = a} = λ i → a

symm' : {X : Set} {a b : X} → a ≡ b → b ≡ a
symm' p = λ i → p (~ i)

Exercise 1cong'

cong' : {X Y : Set} {a b : X} → (f : X → Y) → a ≡ b → f a ≡ f b
cong' f p = {!!}

Your solution

Reference solution

cong' : {X Y : Set} {a b : X} → (f : X → Y) → a ≡ b → f a ≡ f b
cong' f p = λ i → f (p i)

Exercise 2funext

funext : {A B : Set} {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g
funext = {!!}

Your solution

Reference solution

funext : {A B : Set} {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g
funext h = λ i → λ x → h x i

Verifying transitivity is more difficult. Let us just use the function from the cubical standard library:

trans' : {X : Set} {a b c : X} → a ≡ b → b ≡ c → a ≡ c
trans' p q = p ∙ q

Even though cubical Agda reimagines identity in a radical way, in the end the primitive equality type coincides with the inductively-defined type we have been using all along:

open import Padova2025.ProvingBasics.Equality.Base renaming (_≡_ to _≡ᵢ_)

Exercise 3≡ᵢ→≡

≡ᵢ→≡ : {X : Set} {a b : X} → a ≡ᵢ b → a ≡ b
≡ᵢ→≡ = {!!}

The reference solution uses: refl refl'

Your solution

Reference solution

≡ᵢ→≡ : {X : Set} {a b : X} → a ≡ᵢ b → a ≡ b
≡ᵢ→≡ refl = refl'

≡→≡ᵢ : {X : Set} {a b : X} → a ≡ b → a ≡ᵢ b
≡→≡ᵢ = J (λ b q → _ ≡ᵢ b) _≡ᵢ_.refl

Exercise: Sum of unordered pair#

open import Padova2025.ProvingBasics.Equality.NaturalNumbers

Exercise 4sum-pair

sum-pair : UnorderedPair ℕ → ℕ
sum-pair = {!!}

The reference solution uses: pair _+_ swap ≡ᵢ→≡ +-comm

Your solution

Reference solution

sum-pair : UnorderedPair ℕ → ℕ
sum-pair (pair x y)   = x + y
sum-pair (swap x y i) = ≡ᵢ→≡ (+-comm x y) i

Integers#

infixl 5 _⊝_
data ℤ : Set where
  _⊝_    : (a b : ℕ) → ℤ
  cancel : (a b : ℕ) → a ⊝ b ≡ succ a ⊝ succ b

Define the successor and predecessor functions.

Exercise 5succℤ

succℤ : ℤ → ℤ
succℤ (a ⊝ b)        = succ a ⊝ b
succℤ (cancel a b i) = {!!}

Your solution

Reference solution

succℤ : ℤ → ℤ
succℤ (a ⊝ b)        = succ a ⊝ b
succℤ (cancel a b i) = cancel (succ a) b i

Exercise 6predℤ

predℤ : ℤ → ℤ
predℤ (a ⊝ b)        = a ⊝ succ b
predℤ (cancel a b i) = {!!}

Your solution

Reference solution

predℤ : ℤ → ℤ
predℤ (a ⊝ b)        = a ⊝ succ b
predℤ (cancel a b i) = cancel a (succ b) i

Exercise: One is not zero, revisited#

Show that one is not zero.

Exercise 7lemma-nontrivial

lemma-nontrivial : one ≡ zero → ⊥
lemma-nontrivial = {!!}

The reference solution uses: ℕ succ

Your solution

Reference solution

lemma-nontrivial : one ≡ zero → ⊥
lemma-nontrivial p = transport (λ i → disambig (p i)) zero
  where
  disambig : ℕ → Set
  disambig zero     = ⊥
  disambig (succ _) = ℕ  -- or any other inhabited type

With the inductive definition of _≡_ we used before, this required an empty pattern. Now that _≡_ is no longer inductively defined, but an in-built notion, we cannot case split on equality witnesses.

Instead, proceed as follows:

Define a function disambig : ℕ → Set which maps zero to ⊥ and everything else to some inhabited type.
Assuming that there is a path zero ≡ succ zero, combine transport from the standard library and disambig:
transport : {A B : Set} → A ≡ B → A → B

Exercise: Robustness of the unordered pair abstraction#

Show that the unordered pair abstraction is not leaky, in the sense that there cannot be a function which would extract the first component of an unordered pair.

Exercise 8lemma-not-leaky

lemma-not-leaky : (f : UnorderedPair ℕ → ℕ) → ((a b : ℕ) → f (pair a b) ≡ a) → ⊥
lemma-not-leaky = {!!}

The reference solution uses: lemma-nontrivial symm' one zero cong' swap

Your solution

Reference solution

lemma-not-leaky : (f : UnorderedPair ℕ → ℕ) → ((a b : ℕ) → f (pair a b) ≡ a) → ⊥
lemma-not-leaky f p = lemma-nontrivial (symm' (p one zero) ∙ cong' f (swap one zero) ∙ p zero one)

Exercise: Reversing twice#

The solution of the following exercise is delightful. No case split is needed (nor possible):

Exercise 9symm-symm

symm-symm : {X : Set} {a b : X} → (p : a ≡ b) → symm' (symm' p) ≡ p
symm-symm = {!!}

The reference solution uses: refl'

Your solution

Reference solution

symm-symm : {X : Set} {a b : X} → (p : a ≡ b) → symm' (symm' p) ≡ p
symm-symm p = refl'

Mere propositions#

In homotopy type theory, a type is called a proposition if and only if all its inhabitants are equal. Hence all there is to know about a proposition is whether it is inhabited.

isProp' : Set → Set
isProp' X = (a b : X) → a ≡ b

Show that the types ⊥ and 𝟙 are propositions in this sense.

Exercise 10⊥-isProp

⊥-isProp : isProp' ⊥
⊥-isProp = {!!}

Your solution

Reference solution

⊥-isProp : isProp' ⊥
⊥-isProp ()

Exercise 11𝟙-isProp

𝟙-isProp : isProp' 𝟙
𝟙-isProp = {!!}

The reference solution uses: tt refl'

Your solution

Reference solution

𝟙-isProp : isProp' 𝟙
𝟙-isProp tt tt = refl'

Show that negations are propositions.

Exercise 12lemma-negations-are-props

lemma-negations-are-props : (X : Set) → isProp' (X → ⊥)
lemma-negations-are-props = {!!}

The reference solution uses: funext ⊥-isProp

Your solution

Reference solution

lemma-negations-are-props : (X : Set) → isProp' (X → ⊥)
lemma-negations-are-props X f g = funext λ x → ⊥-isProp (f x) (g x)

Zero-dimensionality of the type of natural numbers#

In homotopy type theory, a type is called hset (or just set) iff its identity types are mere propositions, i.e. iff there is at most one path between any two elements.

isHSet : Set → Set
isHSet X = (a b : X) → isProp' (a ≡ b)

To verify that ℕ is an hset, we require an explicit description of its identity types. For the following definition of Code, it will turn out that the types a ≡ b and Code a b are equivalent.

Code : ℕ → ℕ → Set
Code zero     zero     = 𝟙
Code zero     (succ y) = ⊥
Code (succ x) zero     = ⊥
Code (succ x) (succ y) = Code x y

Exercise 13fromCode

fromCode : (a b : ℕ) → Code a b → a ≡ b
fromCode = {!!}

The reference solution uses: zero refl' succ cong'

Your solution

Reference solution

fromCode : (a b : ℕ) → Code a b → a ≡ b
fromCode zero     zero     p = refl'
fromCode (succ a) (succ b) p = cong' succ (fromCode a b p)

Exercise 14Code-refl

Code-refl : (a : ℕ) → Code a a
Code-refl = {!!}

The reference solution uses: zero tt succ

Your solution

Reference solution

Code-refl : (a : ℕ) → Code a a
Code-refl zero     = tt
Code-refl (succ a) = Code-refl a

Exercise 15Code-isProp

Code-isProp : (a b : ℕ) → isProp' (Code a b)
Code-isProp = {!!}

The reference solution uses: zero 𝟙-isProp succ ⊥-isProp

Your solution

Reference solution

Code-isProp : (a b : ℕ) → isProp' (Code a b)
Code-isProp zero     zero     = 𝟙-isProp
Code-isProp zero     (succ b) = ⊥-isProp
Code-isProp (succ a) zero     = ⊥-isProp
Code-isProp (succ a) (succ b) = Code-isProp a b

Exercise 16toCode

toCode : (a b : ℕ) → a ≡ b → Code a b
toCode a b = J {!!} {!!}

The reference solution uses: Code-refl

Your solution

Reference solution

toCode : (a b : ℕ) → a ≡ b → Code a b
toCode a b = J (λ c q → Code a c) (Code-refl a)

If _≡_ was the inductively-defined equality predicate from before, we would do a case split on p to reduce to the case toCode a a refl; this case could be solved by Code-refl a.

This kind of case split is not available for _≡_, however we can emulate its effects by the standard library’s J function.

from-to₀ : (a : ℕ) → fromCode a a (toCode a a refl') ≡ refl'
from-to₀ zero       = refl'
from-to₀ (succ a) i = cong succ (from-to₀ a i)

from-to : (a b : ℕ) → (p : a ≡ b) → fromCode a b (toCode a b p) ≡ p
from-to a b p = J (λ y q → fromCode a y (toCode a y q) ≡ q) (from-to₀ a) p

Exercise 17ℕ-isHSet

ℕ-isHSet : isHSet ℕ
ℕ-isHSet = {!!}

The reference solution uses: symm' from-to cong' fromCode Code-isProp toCode

Your solution

Reference solution

ℕ-isHSet : isHSet ℕ
ℕ-isHSet a b p q =
  symm' (from-to a b p) ∙ cong' (fromCode a b) (Code-isProp a b (toCode a b p) (toCode a b q)) ∙ from-to a b q