``` {-# 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) ``` ::: Todo ::: 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 ``` 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 _≑ᡒ_) ``` ``` ≑ᡒ→≑ : {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 ``` open import Padova2025.ProvingBasics.Equality.NaturalNumbers ``` ``` 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 = {!!} ``` ::: Hint ::: 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`](Cubical.Foundations.Prelude.html#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 = {!!} ``` ## Exercise: Reversing twice The solution of the following exercise is delightful. No case split is needed (nor possible): ``` symm-symm : {X : Set} {a b : X} β†’ (p : a ≑ b) β†’ symm' (symm' p) ≑ p symm-symm = {!!} ``` ## 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 = {!!} ``` ## 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 {!!} {!!} ``` ::: Hint ::: 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 = {!!} ```