πŸ“₯ Download raw
{-# OPTIONS --cubical #-}
module Padova2025.Cubical.FirstSteps where

First steps

open import Cubical.Core.Everything
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.Equality.Base renaming (_≑_ to _≑ᡒ_)
open import Padova2025.ProvingBasics.Equality.NaturalNumbers
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)

cong' : {X Y : Set} {a b : X} β†’ (f : X β†’ Y) β†’ a ≑ b β†’ f a ≑ f b
cong' f p = {!!}

funext : {A B : Set} {f g : A β†’ B} β†’ ((x : A) β†’ f x ≑ g x) β†’ f ≑ g
funext = {!!}

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

≑ᡒ→≑ : {X : Set} {a b : X} β†’ a ≑ᡒ b β†’ a ≑ b
≑ᡒ→≑ = {!!}

≑→≑ᡒ : {X : Set} {a b : X} β†’ a ≑ b β†’ a ≑ᡒ b
≑→≑ᡒ = J (Ξ» b q β†’ _ ≑ᡒ b) _≑ᡒ_.refl

Exercise: Sum of unordered pair

sum-pair : UnorderedPair β„• β†’ β„•
sum-pair = {!!}

Integers

infixl 5 _⊝_
data β„€ : Set where
  _⊝_    : (a b : β„•) β†’ β„€
  cancel : (a b : β„•) β†’ a ⊝ b ≑ succ a ⊝ succ b

Define the successor and predecessor functions.

succβ„€ : β„€ β†’ β„€
succβ„€ (a ⊝ b)        = succ a ⊝ b
succβ„€ (cancel a b i) = {!!}

predβ„€ : β„€ β†’ β„€
predβ„€ (a ⊝ b)        = a ⊝ succ b
predβ„€ (cancel a b i) = {!!}

Exercise: One is not zero, revisited

Show that one is not zero.

lemma-nontrivial : one ≑ zero β†’ βŠ₯
lemma-nontrivial = {!!}

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:

  1. Define a function disambig : β„• β†’ Set which maps zero to βŠ₯ and everything else to some inhabited type.

  2. 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.

lemma-not-leaky : (f : UnorderedPair β„• β†’ β„•) β†’ ((a b : β„•) β†’ f (pair a b) ≑ a) β†’ βŠ₯
lemma-not-leaky = {!!}

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.

βŠ₯-isProp : isProp' βŠ₯
βŠ₯-isProp = {!!}

πŸ™-isProp : isProp' πŸ™
πŸ™-isProp = {!!}

Show that negations are propositions.

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

fromCode : (a b : β„•) β†’ Code a b β†’ a ≑ b
fromCode = {!!}

Code-refl : (a : β„•) β†’ Code a a
Code-refl = {!!}

Code-isProp : (a b : β„•) β†’ isProp' (Code a b)
Code-isProp = {!!}

toCode : (a b : β„•) β†’ a ≑ b β†’ Code a b
toCode a b = J {!!} {!!}

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

β„•-isHSet : isHSet β„•
β„•-isHSet = {!!}